Paralleles Model Checking

dependency-reduced-pom.xml

@@ -53,15 +53,5 @@
       </plugin>
     </plugins>
   </build>
-  <repositories>
-    <repository>
-      <id>libs-milestone</id>
-      <url>http://repo.spring.io/libs-milestone/</url>
-    </repository>
-    <repository>
-      <id>libs-release</id>
-      <url>http://repo.spring.io/libs-release/</url>
-    </repository>
-  </repositories>
 </project>
 

examples/charging/charging_model.xml

@@ -17,7 +17,7 @@
     <discretePlace id="loading_delayed" marking="1"/>
     <discretePlace id="start_charging_finished" marking="0"/>
     <discretePlace id="drain_from_grid" marking="0"/>
-    <discretePlace id="P1" marking="0"/>
+    <discretePlace id="P1" marking="1"/>
     <discretePlace id="p9_on" marking="0"/>
     <continuousPlace capacity="90000" id="battery" level="0" infiniteCapacity="0"/>
   </places>

src/main/java/de/wwu/criticalsystems/libhpng/confidenceintervals/AdjustedWaldConfidenceInterval.java

@@ -44,4 +44,30 @@ public class AdjustedWaldConfidenceInterval extends ConfidenceInterval{
 	
 		}
 	
+		public Integer calculateMidpointAndHalfIntervalWidthForUntilProperty(PropertyChecker checker, Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException {
+		
+			checkPropertyResult(checker, currentRun, plot, propCheckResult);
+			
+			x = fulfilled.doubleValue();
+			n = numberOfRuns.doubleValue();
+			
+			Double mean = x / n;
+			
+			if (fulfilled == 0)
+				lowerBoundary = 0.0;
+			else
+				lowerBoundary = (x + 4.0/(2.0*n) - 2.0*Math.sqrt((mean*(1.0-mean) + 4.0/(4*n))/n))/(1.0 + 4.0/n); 
+			
+			if (fulfilled == numberOfRuns)
+				upperBoundary = 1.0;
+			else
+				upperBoundary  = (x+ 4.0/(2.0*n) + 2.0*Math.sqrt((mean*(1.0-mean) + 4.0/(4*n))/n))/(1.0 + 4.0/n); 
+			
+			currentHalfIntervalWidth = 0.5* (upperBoundary - lowerBoundary);
+			midpoint = (x + 2.0) / (n + 4.0);
+					
+			return numberOfRuns;
+		
+			}
+	
 }
\ No newline at end of file

src/main/java/de/wwu/criticalsystems/libhpng/confidenceintervals/ClopperPearsonConfidenceInterval.java

@@ -46,5 +46,30 @@ public class ClopperPearsonConfidenceInterval extends ConfidenceInterval{
 		return numberOfRuns;
 	
 		}
+
+		public Integer calculateMidpointAndHalfIntervalWidthForUntilProperty(PropertyChecker checker, Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException {
+		
+			checkPropertyResult(checker, currentRun, plot, propCheckResult);
+			
+			x = fulfilled.doubleValue();
+			n = numberOfRuns.doubleValue();
+			
+			if (fulfilled == 0)
+				beta_low = 0.0;
+			else
+				beta_low = BetaDist.inverseF(x, n - x+ 1.0, alphaHalf);
+			
+			if (fulfilled.equals(numberOfRuns))
+				beta_upp = 1.0;
+			else
+				beta_upp  = BetaDist.inverseF(x + 1, n - x, 1.0 - alphaHalf);
+			
+			
+			currentHalfIntervalWidth = 0.5* (beta_upp - beta_low);
+			midpoint = beta_low + currentHalfIntervalWidth;
+				
+			return numberOfRuns;
+		
+			}
 	
 }
\ No newline at end of file

src/main/java/de/wwu/criticalsystems/libhpng/confidenceintervals/ConfidenceInterval.java

@@ -10,6 +10,7 @@ public abstract class ConfidenceInterval {
 
 	
 	public abstract Integer calculateMidpointAndHalfIntervalWidthForProperty(PropertyChecker checker, Integer currentRun, MarkingPlot plot) throws InvalidPropertyException;
+	public abstract Integer calculateMidpointAndHalfIntervalWidthForUntilProperty(PropertyChecker checker, Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException;
 	
 	
 	public Integer getNumberOfRuns() {
@@ -43,4 +44,17 @@ public abstract class ConfidenceInterval {
 				
 		numberOfRuns++;	
 	}
+
+	protected void checkPropertyResult(PropertyChecker checker, Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException{
+			
+		if (currentRun == 1){
+			numberOfRuns = 0;
+			fulfilled = 0;
+		}
+					
+		if (propCheckResult)						
+			fulfilled++;
+				
+		numberOfRuns++;	
+	}
 }

src/main/java/de/wwu/criticalsystems/libhpng/confidenceintervals/ConfidenceIntervalCalculator.java

@@ -74,6 +74,14 @@ public class ConfidenceIntervalCalculator {
 		currentHalfIntervalWidth = interval.getCurrentHalfIntervalWidth();
 		
 	}
+
+	public void calculateConfidenceIntervalUntil(Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException{
+		
+		numberOfRuns = interval.calculateMidpointAndHalfIntervalWidthForUntilProperty(checker, currentRun, plot, propCheckResult);
+		midpoint = interval.getMidpoint();
+		currentHalfIntervalWidth = interval.getCurrentHalfIntervalWidth();
+		
+	}
 		
 	public Boolean checkBound(){
 		

src/main/java/de/wwu/criticalsystems/libhpng/confidenceintervals/ScoreConfidenceInterval.java

@@ -42,6 +42,32 @@ public class ScoreConfidenceInterval extends ConfidenceInterval{
 		return numberOfRuns;	
 	}
 
+	public Integer calculateMidpointAndHalfIntervalWidthForUntilProperty(PropertyChecker checker, Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException {
+		
+		
+		checkPropertyResult(checker, currentRun, plot, propCheckResult);
+		
+		x = fulfilled.doubleValue();
+		n = numberOfRuns.doubleValue();
+		mean = x / n;
+		
+		if (fulfilled == 0)
+			lowerBoundary = 0.0;
+		else
+			lowerBoundary = (mean + (z*z)/(2.0*n) - z*Math.sqrt((mean*(1.0-mean) + (z*z)/(4.0*n))/n))/(1.0 + (z*z)/n); 
+		
+		if (fulfilled == numberOfRuns)
+			upperBoundary = 1.0;
+		else
+			upperBoundary  = (mean + (z*z)/(2.0*n) + z*Math.sqrt((mean*(1.0-mean) + (z*z)/(4.0*n))/n))/(1.0 + (z*z)/n); 
+		
+		currentHalfIntervalWidth = 0.5* (upperBoundary - lowerBoundary);
+		midpoint =  mean*(n / (n + (z*z))) + 0.5*((z*z)/(n + (z*z)));
+			
+		return numberOfRuns;	
+
+
+	}
 
 	private Double lowerBoundary;
 	private Double upperBoundary;

src/main/java/de/wwu/criticalsystems/libhpng/confidenceintervals/StandardConfidenceInterval.java

@@ -68,6 +68,33 @@ public class StandardConfidenceInterval extends ConfidenceInterval {
 		
 		return numberOfRuns;
 	}
+
+	public Integer calculateMidpointAndHalfIntervalWidthForUntilProperty(PropertyChecker checker, Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException {
+		
+		checkPropertyResult(checker, currentRun, plot, propCheckResult);
+		
+		x = fulfilled.doubleValue();
+		n = numberOfRuns.doubleValue();
+		mean = fulfilled.doubleValue() / n;
+		
+		if (numberOfRuns == 1)
+			ssquare = 0.0;
+		else
+			ssquare = (x*(n - x))/(n*(n - 1.0));
+		
+
+		if (numberOfRuns < 2)
+			t = 0.0;
+		else {				
+			Double alphaHalf = (1.0 - confidenceLevel)/2.0;
+			t = StudentDist.inverseF(numberOfRuns - 1, 1.0 - alphaHalf);
+		}
+		
+		currentHalfIntervalWidth = t * Math.sqrt(ssquare / n);
+		midpoint = mean;
+		
+		return numberOfRuns;
+	}
 	
 
 	

src/main/java/de/wwu/criticalsystems/libhpng/confidenceintervals/WaldConfidenceInterval.java

@@ -35,5 +35,20 @@ public class WaldConfidenceInterval extends ConfidenceInterval{
 		
 		return numberOfRuns;	
 	}
+
+	public Integer calculateMidpointAndHalfIntervalWidthForUntilProperty(PropertyChecker checker, Integer currentRun, MarkingPlot plot, Boolean propCheckResult) throws InvalidPropertyException {
+		
+		checkPropertyResult(checker, currentRun, plot, propCheckResult);		
+		
+		n = numberOfRuns.doubleValue();
+		mean = fulfilled.doubleValue() / n;
+		
+		currentHalfIntervalWidth = z * Math.sqrt(mean * ( 1.0 - mean) / n);
+		midpoint = mean;
+		
+		
+		return numberOfRuns;	
+	}
+	
 	
 }
\ No newline at end of file

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/AzumaHypothesisTester.java

@@ -63,4 +63,39 @@ public class AzumaHypothesisTester extends HypothesisTester{
 		return resultAchieved;
 	}
 
+		
+	@Override
+	public Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+		
+		
+		checkPropertyForCurrentRunUntil(currentRun,plot,propChecker);
+
+		if(numberOfRuns >= minNumberOfRuns){
+			
+			
+			n = numberOfRuns.doubleValue();
+			zN = fulfilled.doubleValue() - n * boundary;
+			
+			upperBoundary = a * (Math.pow((k + n), b));
+			lowerBoundary = -upperBoundary;
+
+			
+			//accept H+1 hypothesis
+			if (zN > upperBoundary){
+				
+				resultAchieved = true;				
+				propertyFulfilled = !checkLowerThan;
+				
+			//accept H-1 hypothesis	
+			}else if (zN < lowerBoundary){
+				
+				resultAchieved = true;
+				propertyFulfilled = checkLowerThan;
+
+			}
+		}
+		
+		return resultAchieved;
+	}
+
 }

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/ChernoffCIHypothesisTester.java

@@ -31,6 +31,41 @@ public class ChernoffCIHypothesisTester extends HypothesisTester{
 		checkPropertyForCurrentRun(currentRun,plot);	
 		
 			
+		if(numberOfRuns.doubleValue() >= calcNumberOfRuns && numberOfRuns.doubleValue() < (calcNumberOfRuns + 1.0)){
+			
+			Double mean = fulfilled.doubleValue() / numberOfRuns.doubleValue();
+			
+			//reject H0 hypothesis
+			if (Math.abs(mean - boundary) > epsilon){
+				
+				//accept H+1 hypothesis
+				if (mean > boundary){
+					
+					resultAchieved = true;				
+					propertyFulfilled = !checkLowerThan;
+					
+				} else {
+					
+					resultAchieved = true;
+					propertyFulfilled = checkLowerThan;					
+				}					
+				
+			} else {
+				terminate = true;
+			}			
+			
+		}
+		
+		return resultAchieved;
+	}
+
+	@Override
+	public Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+		
+		
+		checkPropertyForCurrentRunUntil(currentRun,plot,propChecker);	
+		
+			
 		if(numberOfRuns.doubleValue() >= calcNumberOfRuns && numberOfRuns.doubleValue() < (calcNumberOfRuns + 1.0)){
 			
 			Double mean = fulfilled.doubleValue() / numberOfRuns.doubleValue();

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/ChowRobbinsHypothesisTester.java

@@ -40,6 +40,44 @@ public class ChowRobbinsHypothesisTester extends HypothesisTester {
 		checkPropertyForCurrentRun(currentRun,plot);
 		
 		
+		if(numberOfRuns >= minNumberOfRuns){
+					
+			n = numberOfRuns.doubleValue();
+			mean = fulfilled.doubleValue() / n;
+			 
+			currentWidth = 2.0 * inverseType1Error * Math.sqrt((mean * (1.0 - mean)) / (n));
+			requiredWidth = 2.0 * requiredHalfWidth;
+			
+			if (requiredWidth >= Math.abs(currentWidth) ){
+	
+				lowerBoundary = mean - requiredHalfWidth;
+				upperBoundary = mean + requiredHalfWidth;
+				
+				//accept H+1 hypothesis
+				if (lowerBoundary > boundary){
+					
+					resultAchieved = true;				
+					propertyFulfilled = !checkLowerThan;
+				
+				//accept H-1 Hypothesis	
+				}else if (upperBoundary < boundary){
+					
+					resultAchieved = true;
+					propertyFulfilled = checkLowerThan;
+				}				
+			}			
+		}
+		
+		return resultAchieved;		
+		
+	}
+
+	@Override
+	public Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+	
+		checkPropertyForCurrentRunUntil(currentRun,plot, propChecker);
+		
+		
 		if(numberOfRuns >= minNumberOfRuns){
 					
 			n = numberOfRuns.doubleValue();

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/DarlingHypothesisTester.java

@@ -63,4 +63,36 @@ public class DarlingHypothesisTester extends HypothesisTester{
 		return resultAchieved;
 	}
 
+	@Override
+	public Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+		
+		
+		checkPropertyForCurrentRunUntil(currentRun,plot,propChecker);
+
+		if(numberOfRuns >= minNumberOfRuns){
+			
+			n = numberOfRuns.doubleValue();
+			zN = fulfilled.doubleValue() - n * boundary;
+			
+			upperBoundary = Math.sqrt(a * (n + 1.0) * Math.log(n + k));
+			lowerBoundary = -upperBoundary;
+
+			
+			//accept H+1 hypothesis
+			if (zN > upperBoundary){
+				
+				resultAchieved = true;				
+				propertyFulfilled = !checkLowerThan;
+				
+			//accept H-1 hypothesis	
+			}else if (zN < lowerBoundary){
+				
+				resultAchieved = true;
+				propertyFulfilled = checkLowerThan;
+
+			}
+		}
+		
+		return resultAchieved;
+	}
 }

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/GaussCIHypothesisTester.java

@@ -62,6 +62,35 @@ public class GaussCIHypothesisTester extends HypothesisTester{
 		
 		return resultAchieved;
 	}
-	
+
+	@Override
+	public Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+		
+		checkPropertyForCurrentRunUntil(currentRun,plot,propChecker);	
+		
+			
+		if(numberOfRuns >= calcNumberOfRuns && numberOfRuns < (calcNumberOfRuns + 1)){
+			
+			Double zN = fulfilled.doubleValue() - calcNumberOfRuns.doubleValue() * boundary;
+			
+			//accept H+1 hypothesis
+			if (zN > upperBoundary){
+				
+				resultAchieved = true;				
+				propertyFulfilled = !checkLowerThan;
+				
+			//accept H-1 hypothesis	
+			}else if (zN < lowerBoundary){
+				
+				resultAchieved = true;
+				propertyFulfilled = checkLowerThan;
+				
+			}else {
+				terminate = true;
+			}
+		}
+		
+		return resultAchieved;
+	}
 
 }

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/GaussSSPHypothesisTester.java

@@ -55,6 +55,33 @@ public class GaussSSPHypothesisTester extends HypothesisTester{
 		
 		return resultAchieved;
 	}
-	
+
+	@Override
+	public Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+		
+		checkPropertyForCurrentRunUntil(currentRun,plot,propChecker);
+		
+			
+		if(numberOfRuns >= calcNumberOfRuns && numberOfRuns < (calcNumberOfRuns + 1)){
+			
+			Double zN = fulfilled.doubleValue() - calcNumberOfRuns.doubleValue() * boundary;
+			
+			//accept H+1 hypothesis
+			if (zN >= 0.0){
+				
+				resultAchieved = true;				
+				propertyFulfilled = !checkLowerThan;
+				
+			//accept H-1 hypothesis	
+			} else {
+				
+				resultAchieved = true;
+				propertyFulfilled = checkLowerThan;
+
+			}
+		}
+		
+		return resultAchieved;
+	}
 
 }

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/HypothesisTester.java

@@ -33,6 +33,8 @@ public abstract class HypothesisTester {
 	
 	
 	public abstract Boolean doTesting(Integer currentRun, MarkingPlot plot) throws InvalidPropertyException;
+
+	public abstract Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException;
 	
 		
 	public Boolean getResultAchieved() {
@@ -85,5 +87,19 @@ public abstract class HypothesisTester {
 		
 		numberOfRuns++;
 	}
+
+	protected void checkPropertyForCurrentRunUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+		
+		if (currentRun == 1){			
+			numberOfRuns = 0;
+			fulfilled = 0;
+		}
+					
+		
+		if (propChecker != invertPropertyAndThreshold) 						
+			fulfilled++;
+		
+		numberOfRuns++;
+	}
 	
 }

src/main/java/de/wwu/criticalsystems/libhpng/hypothesistesting/SequentialProbabilityRatioTester.java

@@ -59,4 +59,32 @@ public class SequentialProbabilityRatioTester extends HypothesisTester{
 		return resultAchieved;
 	}
 
+	@Override
+	public Boolean doTestingUntil(Integer currentRun, MarkingPlot plot, Boolean propChecker) throws InvalidPropertyException{
+		
+		checkPropertyForCurrentRunUntil(currentRun, plot, propChecker);		
+		
+		if (numberOfRuns >= minNumberOfRuns){
+			
+			x = fulfilled.doubleValue();
+			n = numberOfRuns.doubleValue();
+			ratio = (Math.pow(pminus1, x)*Math.pow(1.0 - pminus1, n - x)) / (Math.pow(pplus1, x)*Math.pow(1.0 - pplus1, n - x));			
+				
+			//accept H+1 (H0) hypothesis
+			if (ratio <= B){
+				resultAchieved = true;				
+				propertyFulfilled = !checkLowerThan;
+			
+				
+			//accept H-1 (H1) hypothesis
+			} else if (ratio >= A){
+				resultAchieved = true;
+				propertyFulfilled = checkLowerThan;
+			}	
+					
+		}				
+		
+		return resultAchieved;
+	}
+
 }

src/main/java/de/wwu/criticalsystems/libhpng/simulation/SimulationForHypothesisTesting.java

@@ -63,6 +63,8 @@ public class SimulationForHypothesisTesting {
 	Boolean invertPropertyAndThreshold;
 	Integer maxNumberOfRuns;
 	Double currentTime;
+	Double prevEventTime;
+	Boolean propResult;
 	MarkingPlot currentPlot;
 	Double maxTime;
 	Simulator simulator;
@@ -75,6 +77,8 @@ public class SimulationForHypothesisTesting {
 	Integer minRun;
 	Integer maxRun;
 	Integer totalRuns;
+	Double ti;
+	Boolean noParallelChecking = true;
 	private Integer firings = 0;
 	Integer minFirings = Integer.MAX_VALUE;
 	Integer maxFirings = Integer.MIN_VALUE;
@@ -134,6 +138,7 @@ public class SimulationForHypothesisTesting {
 		}
 
 		ArrayList<String> related = tester.getChecker().getAllRelatedPlaceAndTransitionIds();
+		PropertyChecker propChecker = tester.getChecker();
 
 		int n = 0;
 		while (n < testRuns) {
@@ -170,15 +175,39 @@ public class SimulationForHypothesisTesting {
 
 					if (printRunResults) System.out.println("Starting simulation run no." + (run + 1));
 
+					propChecker.setSimulationStatus(true);
+					noParallelChecking = true;
 					currentTime = 0.0;
+					prevEventTime = -1.0;
+					propResult = false;
 					model.resetMarking();
 					generator.sampleRandomTransitions(model, logger);
 					currentPlot = new MarkingPlot(maxTime);
 					currentPlot.initializeRelatedOnly(this.model, related);