Digital clocks engine now supports time-bounded reachability.

prism-tests/functionality/verify/ptas/reach/firewire_abst.nm

@@ -0,0 +1,83 @@
+// Abstract model of Firewire protocol (PTA model)
+// dxp/gxn 08/07/09
+
+pta
+
+// maximum and minimum delays
+// fast
+const int rc_fast_max = 850;
+const int rc_fast_min = 760;
+// slow
+const int rc_slow_max = 1670;
+const int rc_slow_min = 1590;
+// delay caused by the wire length
+const int delay;
+// probability of choosing fast and slow
+const double fast = 0.5;
+const double slow = 1-fast;
+
+module abstract_firewire
+
+	// clock 
+	x : clock;
+	// local state
+	s : [0..9];
+	// 0 - start_start
+	// 1 - fast_start
+	// 2 - start_fast
+	// 3 - start_slow
+	// 4 - slow_start
+	// 5 - fast_fast
+	// 6 - fast_slow
+	// 7 - slow_fast
+	// 8 - slow_slow
+	// 9 - done
+
+	// clock invariant
+	invariant
+		(s=0 => x<=delay) &
+		(s=1 => x<=delay) &
+		(s=2 => x<=delay) &
+		(s=3 => x<=delay) &
+		(s=4 => x<=delay) &
+		(s=5 => x<=rc_fast_max) &
+		(s=6 => x<=rc_slow_max) &
+		(s=7 => x<=rc_slow_max) &
+		(s=8 => x<=rc_slow_max)
+	endinvariant
+	
+	// start_start (initial state)
+	[] s=0 -> fast : (s'=1) + slow : (s'=4);
+	[] s=0 -> fast : (s'=2) + slow : (s'=3);
+	// fast_start
+	[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
+	// start_fast
+	[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
+	// start_slow
+	[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
+	// slow_start
+	[] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0);
+	// fast_fast
+	[] s=5 & (x>=rc_fast_min)       -> (s'=0) & (x'=0);
+	[] s=5 & (x>=rc_fast_min-delay) -> (s'=9) & (x'=0);
+	// fast_slow
+	[] s=6 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// slow_fast
+	[] s=7 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// slow_slow
+	[] s=8 & x>=rc_slow_min       -> (s'=0) & (x'=0);
+	[] s=8 & x>=rc_slow_min-delay -> (s'=9) & (x'=0);
+	// done
+	[] s=9 -> true;
+	
+endmodule
+
+// labels
+label "done" = (s=9);
+
+// reward structures
+// time
+rewards "time"
+	true : 1;
+endrewards
+

prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props

@@ -0,0 +1,11 @@
+// Minimum probability that a leader is eventually elected
+// RESULT (delay=30): 1.0
+"eventually": Pmin=? [ F "done" ];
+
+// Minimum probability that a leader has been elected by time T
+// RESULT (delay=30): 0.851563
+"deadline_min": Pmin=? [ F<=5000 "done" ];
+
+// Maximum probability that a leader has been elected by time T
+// RESULT (delay=30): 0.25
+"deadline_max": Pmax=? [ F<=750 "done" ];

prism-tests/functionality/verify/ptas/reach/firewire_abst.nm.props.args

@@ -0,0 +1,4 @@
+-const delay=30 -const L=2 -ptamethod digital
+-const delay=30 -const L=2 -ptamethod digital -ex
+-const delay=30 -const L=2 -ptamethod games
+#-const delay=30 -const L=2 -ptamethod backwards

prism-tests/functionality/verify/ptas/reach/timebounded.nm

@@ -0,0 +1,12 @@
+pta
+
+module M
+	
+	s : [0..1];
+	x : clock;
+	
+	[a] s=0 & x=2 -> 0.5:(x'=0) + 0.5:(s'=1);
+
+endmodule
+
+label "target" = s=1;

prism-tests/functionality/verify/ptas/reach/timebounded.nm.props

@@ -0,0 +1,17 @@
+const int K = 2;
+const int L;
+
+// RESULT: 7/8
+Pmax=? [ F<=6 s=1 ];
+
+// RESULT: 3/4
+Pmax=? [ F<=4 "target" ];
+
+// RESULT: 1/2
+Pmax=? [ F<=K "target" ];
+
+// RESULT: 1/2
+Pmax=? [ F<=L "target" ];
+
+// RESULT: Error:upper
+Pmax=? [ F>=2 "target" ];

prism-tests/functionality/verify/ptas/reach/timebounded.nm.props.args

@@ -0,0 +1,4 @@
+-const L=2 -ptamethod digital
+-const L=2 -ptamethod digital -ex
+-const L=2 -ptamethod games
+-const L=2 -ptamethod backwards

prism-tests/functionality/verify/ptas/reach/zeroconf.nm.props

@@ -12,3 +12,11 @@ Pmax=? [ F s=2 & ip=K ];
 // As above but testing using (undefined) constants
 // RESULT: 130321/100130321
 Pmax=? [ F s=2 & ip=L ];
+
+const int T = 150;
+
+// Maximum probability of configuring IP address incorrectly by time T
+// RESULT (T=100): 6.51605e-4
+// RESULT (T=150): 0.00107253
+// RESULT (T=200): 0.00122154
+"deadline": Pmax=? [ F<=T s=2 & ip=2 ];

prism/src/pta/DigitalClocks.java

@@ -2,7 +2,7 @@
 //	
 //	Copyright (c) 2002-
 //	Authors:
-//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
+//	* Dave Parker <d.a.parker@cs.bham.ac.uk> (University of Birmingham/Oxford)
 //	
 //------------------------------------------------------------------------------
 //	
@@ -30,6 +30,7 @@ import java.util.*;
 
 import parser.*;
 import parser.ast.*;
+import parser.ast.Module;
 import parser.type.*;
 import parser.visitor.*;
 import prism.*;
@@ -48,6 +49,8 @@ public class DigitalClocks
 	private Values constantValues;
 	// Variable list for model
 	private VarList varList;
+	// Time bound from property if present
+	private int timeBound = -1;
 
 	// Flags + settings
 	private boolean doScaling = true;
@@ -318,11 +321,78 @@ public class DigitalClocks
 			}
 		}
 
-		// Re-do type checking etc. on the model/properties
+		// If we are checking a time bounded property... 
+		if (timeBound != -1) {
+			
+			int scaledTimeBound = timeBound / cci.getScaleFactor();
+			
+			// First add a timer to the model
+			
+			// Create names for module/variable for timer
+			String timerModuleName = "timer";
+			while (mf.getModuleIndex(timerModuleName) != -1) {
+				timerModuleName = "_" + timerModuleName;
+			}
+			String timerVarName = "timer";
+			while (mf.isIdentUsed(timerVarName) || (pf != null && pf.isIdentUsed(timerVarName))) {
+				timerVarName = "_" + timerVarName;
+			}
+			// Store time bound as a constant
+			String timeboundName = "T";
+			while (mf.isIdentUsed(timeboundName) || (pf != null && pf.isIdentUsed(timeboundName))) {
+				timeboundName = "_" + timeboundName;
+			}
+			mf.getConstantList().addConstant(new ExpressionIdent(timeboundName), Expression.Int(scaledTimeBound), TypeInt.getInstance());
+			// Create module/variable
+			Module timerModule = new Module(timerModuleName);
+			DeclarationType timerDeclType = new DeclarationInt(Expression.Int(0),
+					Expression.Plus(new ExpressionConstant(timeboundName, TypeInt.getInstance()), Expression.Int(1)));
+			Declaration timerDecl = new Declaration(timerVarName, timerDeclType);
+			timerModule.addDeclaration(timerDecl);
+			// Construct command representing progression of time
+			Command timeCommand = new Command();
+			timeCommand.setSynch(timeAction);
+			timeCommand.setGuard(Expression.True());
+			// Construct update
+			Update up = new Update();
+			// Build expression min(timer+1,timerMax)
+			ExpressionFunc exprMin = new ExpressionFunc("min");
+			exprMin.addOperand(Expression.Plus(new ExpressionVar(timerVarName, TypeInt.getInstance()), Expression.Int(1)));
+			exprMin.addOperand(Expression.Plus(new ExpressionConstant(timeboundName, TypeInt.getInstance()), Expression.Literal(1)));
+			// Add to update
+			up.addElement(new ExpressionIdent(timerVarName), exprMin);
+			Updates ups = new Updates();
+			ups.addUpdate(Expression.Double(1.0), up);
+			timeCommand.setUpdates(ups);
+			timerModule.addCommand(timeCommand);
+			// Finally add module to model
+			mf.addModule(timerModule);
+			
+			// Then modify the property
+			
+			// Build time bound (timer <= T)
+			Expression timerRef = new ExpressionVar(timerVarName, TypeInt.getInstance()); 
+			Expression boundNew = new ExpressionBinaryOp(ExpressionBinaryOp.LE, timerRef, new ExpressionConstant(timeboundName, TypeInt.getInstance()));
+			prop.accept(new ASTTraverseModify()
+			{
+				public Object visit(ExpressionTemporal e) throws PrismLangException
+				{
+					// Push (new) time bound into target
+					e.setUpperBound(null);
+					Expression targetNew = Expression.And(e.getOperand2().deepCopy(), boundNew);
+					e.setOperand2(targetNew);
+					return e;
+				}
+			});
+		}
+							
+		// Re-do type checking, indexing, etc. on the model/properties
 		mf.tidyUp();
 		if (pf != null) {
+			pf.setModelInfo(mf);
 			pf.tidyUp();
 		}
+		prop.findAllVars(mf.getVarNames(), mf.getVarTypes());
 		// Copy across undefined constants since these get lost in the call to tidyUp()
 		mf.setSomeUndefinedConstants(modulesFile.getUndefinedConstantValues());
 		pf.setSomeUndefinedConstants(propertiesFile.getUndefinedConstantValues());
@@ -355,14 +425,22 @@ public class DigitalClocks
 			throw e;
 		}
 
-		// Bounded properties not yet handled.
+		// Bounded properties: check allowable, and store time bound if so
+		timeBound = -1;
 		try {
 			propertyToCheck.accept(new ASTTraverse()
 			{
 				public void visitPost(ExpressionTemporal e) throws PrismLangException
 				{
-					if (e.getLowerBound() != null || e.getUpperBound() != null)
-						throw new PrismLangException("The digital clocks method does not yet support bounded properties");
+					if (e.getLowerBound() != null) {
+						throw new PrismLangException("The digital clocks method does not yet support lower time bounds");
+					}
+					if (e.getUpperBound() != null) {
+						if (!ExpressionTemporal.isFinally(e)) {
+							throw new PrismLangException("The digital clocks method only ssupport time bounds on F");
+						}
+						timeBound = e.getUpperBound().evaluateInt(constantValues);
+					}
 				}
 			});
 		} catch (PrismLangException e) {
@@ -625,6 +703,21 @@ public class DigitalClocks
 			}
 		}
 		
+		// Time bounds in properties
+		public void visitPost(ExpressionTemporal e) throws PrismLangException
+		{
+			// This is easier than for clock constraints since they must be constant
+			// (so just evaluate directly)
+			// We also don't care about the max value - this is done elsewhere;
+			// we just want to make sure that the values is used to compute the GCD
+			if (e.getLowerBound() != null) {
+				allClockVals.add(e.getLowerBound().evaluateInt(constantValues));
+			}
+			if (e.getUpperBound() != null) {
+				allClockVals.add(e.getUpperBound().evaluateInt(constantValues));
+			}
+		}
+		
 		// Recurse on labels
 		public void visitPost(ExpressionLabel e) throws PrismLangException
 		{