Enable (explicit engine) model checking of LTSs.

There is no explicit model type keyword added to the parser.
Instead, LTSs are auto-detected by the absence of probabilities.

ConstructModel is extended to build LTSs. Model checking (CTL+LTL)
can be done out of the box using the existing NonProbModelChecker class.

A few MDP regression tests are clarified to make it clear that the
models are MDPs, not LTSs.

prism-tests/functionality/testing/testing.prism

@@ -4,6 +4,6 @@ module M
 
 	x : [0..1] init 0;
 	
-	[] x=0 -> true;
+	[] x=0 -> 1.0:true;
 
 endmodule

prism-tests/functionality/verify/mdps/multi-general/test-cumulative1.nm

@@ -2,6 +2,8 @@
 // The model is in fact a MC
 // We also check -lp although it does not support the feature, but the testing ensures that an exception (and not a wrong result) is given.
 
+mdp
+
 module M
 
 x:[0..4] init 0;

prism/src/explicit/ConstructModel.java

@@ -170,6 +170,7 @@ public class ConstructModel extends PrismComponent
 		CTMCSimple ctmc = null;
 		MDPSimple mdp = null;
 		CTMDPSimple ctmdp = null;
+		LTSSimple lts = null;
 		ModelExplicit model = null;
 		Distribution distr = null;
 		// Misc
@@ -207,10 +208,12 @@ public class ConstructModel extends PrismComponent
 			case CTMDP:
 				modelSimple = ctmdp = new CTMDPSimple();
 				break;
+			case LTS:
+				modelSimple = lts = new LTSSimple();
+				break;
 			case STPG:
 			case SMG:
 			case PTA:
-			case LTS:
 				throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
 			}
 			// Attach variable info
@@ -273,10 +276,16 @@ public class ConstructModel extends PrismComponent
 						case CTMDP:
 							distr.add(dest, modelGen.getTransitionProbability(i, j));
 							break;
+						case LTS:
+							if (distinguishActions) {
+								lts.addActionLabelledTransition(src, dest, modelGen.getChoiceAction(i));
+							} else {
+								lts.addTransition(src, dest);
+							}
+							break;
 						case STPG:
 						case SMG:
 						case PTA:
-						case LTS:
 							throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
 						}
 					}
@@ -354,10 +363,12 @@ public class ConstructModel extends PrismComponent
 			case CTMDP:
 				model = sortStates ? new CTMDPSimple(ctmdp, permut) : ctmdp;
 				break;
+			case LTS:
+				model = sortStates ? new LTSSimple(lts, permut) : lts;
+				break;
 			case STPG:
 			case SMG:
 			case PTA:
-			case LTS:
 				throw new PrismNotSupportedException("Model construction not supported for " + modelType + "s");
 			}
 			model.setStatesList(statesList);

prism/src/explicit/StateModelChecker.java

@@ -196,6 +196,9 @@ public class StateModelChecker extends PrismComponent
 		case STPG:
 			mc = new STPGModelChecker(parent);
 			break;
+		case LTS:
+			mc = new NonProbModelChecker(parent);
+			break;
 		default:
 			throw new PrismException("Cannot create model checker for model type " + modelType);
 		}

prism/src/parser/ast/ModulesFile.java

@@ -37,6 +37,7 @@ import parser.State;
 import parser.Values;
 import parser.VarList;
 import parser.type.Type;
+import parser.visitor.ASTTraverse;
 import parser.visitor.ASTVisitor;
 import parser.visitor.ModulesFileSemanticCheck;
 import parser.visitor.ModulesFileSemanticCheckAfterConstants;
@@ -1287,9 +1288,11 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 	 */
 	private void finaliseModelType()
 	{
-		// Default (if unspecified) is MDP
+		// If unspecified, auto-detect model type
 		if (modelTypeInFile == null) {
-			modelType = ModelType.MDP;
+			boolean nonProb = isNonProbabilistic();
+			// MDP/LTS depending if probabilistic
+			modelType = nonProb ? ModelType.LTS : ModelType.MDP;
 		}
 		// Otherwise, it's just whatever was specified
 		else {
@@ -1297,6 +1300,34 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		}
 	}
 	
+	/**
+	 * Check whether this model is non-probabilistic,
+	 * i.e., whether none of the commands are probabilistic. 
+	 */
+	private boolean isNonProbabilistic()
+	{
+		try {
+			// Search through commands, checking for probabilities
+			accept(new ASTTraverse()
+			{
+				public Object visit(Updates e) throws PrismLangException
+				{
+					int n = e.getNumUpdates();
+					for (int i = 0; i < n; i++) {
+						if (e.getProbability(i) != null) {
+							throw new PrismLangException("Found one");
+						}
+					}
+					visitPost(e);
+					return null;
+				}
+			});
+		} catch (PrismLangException e) {
+			return false;
+		}
+		return true;
+	}
+	
 	// Methods required for ASTElement:
 
 	/**

prism/src/prism/Prism.java

@@ -285,6 +285,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 	// Has the CUDD library been initialised yet?
 	private boolean cuddStarted = false;
 
+	// Info about automatic engine switching
+	private int engineOld = -1;
+	private boolean engineSwitched = false;
+
 	//------------------------------------------------------------------------------
 	// Constructors + options methods
 	//------------------------------------------------------------------------------
@@ -1783,6 +1787,32 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		}
 		mainLog.println();
 
+		// For some models, automatically switch engine
+		switch (currentModelType) {
+		case LTS:
+			if (!getExplicit()) {
+				mainLog.println("\nSwitching to explicit engine, which supports " + currentModelType + "s...");
+				engineOld = getEngine();
+				engineSwitched = true;
+				try {
+					setEngine(Prism.EXPLICIT);
+				} catch (PrismException e) {
+					// Won't happen
+				}
+			}
+			break;
+		// For other models, switch engine back if changed earlier
+		default:
+			if (engineSwitched) {
+				try {
+					setEngine(engineOld);
+				} catch (PrismException e) {
+					// Won't happen
+				}
+				engineSwitched = false;
+			}
+		}
+
 		// If required, export parsed PRISM model
 		if (exportPrism) {
 			try {

prism/tests/lec9ctl1.prism

@@ -0,0 +1,17 @@
+// Simple LTS from Lec 9 of Computer-Aided Verification
+
+module M
+
+s:[0..3];
+
+[] s=0 -> (s'=1);
+[] s=0 -> (s'=2);
+[] s=1 -> (s'=1);
+[] s=1 -> (s'=3);
+[] s=2 -> (s'=1);
+[] s=3 -> (s'=3);
+
+endmodule
+
+label "a" = s=0 | s=1;
+label "b" = s=0 | s=3;

prism/tests/lec9ctl1.prism.props

@@ -0,0 +1,16 @@
+// Simple LTS from Lec 9 of Computer-Aided Verification
+
+// RESULT: ?
+"ex": A[ X "a" ] & E[ X !"b"];
+// RESULT: true
+filter(forall, "ex" <=> (s=2));
+
+// RESULT: ?
+"ex_lhs": A[ X "a" ]
+// RESULT: true
+filter(forall, "ex_lhs" <=> (s=2));
+
+// RESULT: ?
+"ex_rhs": E[ X !"b"];
+// RESULT: true
+filter(forall, "ex_rhs" <=> (s=0|s=1|s=2));