Explicit engine: better error reporting of some unsupported properties + support for property references.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3205 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCModelChecker.java

@@ -50,7 +50,7 @@ public class DTMCModelChecker extends ProbModelChecker
 		if (expr.isSimplePathFormula()) {
 			return checkProbPathFormulaSimple(model, expr);
 		} else {
-			throw new PrismException("LTL-style path formulas are not yet supported");
+			throw new PrismException("Explicit engine does not yet handle LTL-style path formulas");
 		}
 	}
 
@@ -160,7 +160,7 @@ public class DTMCModelChecker extends ProbModelChecker
 				rewards = checkRewardReach(model, modelRewards, exprTemp);
 				break;
 			default:
-				throw new PrismException("Cannot model check " + exprTemp.getOperatorSymbol() + " operator in R operator");
+				throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator");
 			}
 		}
 		

prism/src/explicit/MDPModelChecker.java

@@ -51,7 +51,7 @@ public class MDPModelChecker extends ProbModelChecker
 		if (expr.isSimplePathFormula()) {
 			return checkProbPathFormulaSimple(model, expr, min);
 		} else {
-			throw new PrismException("LTL-style path formulas are not yet supported");
+			throw new PrismException("Explicit engine does not yet handle LTL-style path formulas");
 		}
 	}
 
@@ -167,7 +167,7 @@ public class MDPModelChecker extends ProbModelChecker
 				rewards = checkRewardReach(model, exprTemp, min);
 				break;
 			default:
-				throw new PrismException("Cannot model check " + exprTemp.getOperatorSymbol() + " operator in R operator");
+				throw new PrismException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " operator in the R operator");
 			}
 		}
 		

prism/src/explicit/ProbModelChecker.java

@@ -52,6 +52,10 @@ public class ProbModelChecker extends StateModelChecker
 		else if (expr instanceof ExpressionReward) {
 			res = checkExpressionReward(model, (ExpressionReward) expr);
 		}
+		// S operator
+		else if (expr instanceof ExpressionSS) {
+			throw new PrismException("Explicit engine does not yet handle the S operator");
+		}
 		// Otherwise, use the superclass
 		else {
 			res = super.checkExpression(model, expr);
@@ -76,7 +80,7 @@ public class ProbModelChecker extends StateModelChecker
 
 		// Check for unhandled cases
 		if (expr.getProb() != null)
-			throw new PrismException("Bounded P operators not yet supported");
+			throw new PrismException("Explicit engine does not yet handle bounded P operators");
 
 		// For nondeterministic models, determine whether min or max probabilities needed
 		if (modelType.nondeterministic()) {

prism/src/explicit/STPGModelChecker.java

@@ -49,7 +49,7 @@ public class STPGModelChecker extends ProbModelChecker
 		if (expr.isSimplePathFormula()) {
 			return checkProbPathFormulaSimple(model, expr, min1, min2);
 		} else {
-			throw new PrismException("LTL-style path formulas are not yet supported");
+			throw new PrismException("Explicit engine does not yet handle LTL-style path formulas");
 		}
 	}
 

prism/src/explicit/StateModelChecker.java

@@ -491,6 +491,14 @@ public class StateModelChecker
 		else if (expr instanceof ExpressionLabel) {
 			res = checkExpressionLabel(model, (ExpressionLabel) expr);
 		}
+		// Property refs
+		else if (expr instanceof ExpressionProp) {
+			res = checkExpressionProp(model, (ExpressionProp) expr);
+		}
+		// Filter
+		else if (expr instanceof ExpressionFilter) {
+			throw new PrismException("Explicit engine does not yet handle filters");
+		}
 		
 		// Anything else - just evaluate expression repeatedly
 		else if (expr.getType() instanceof TypeBool) {
@@ -600,6 +608,20 @@ public class StateModelChecker
 		}
 	}
 
+	// Check property ref
+
+	protected Object checkExpressionProp(Model model, ExpressionProp expr) throws PrismException
+	{
+		// Look up property and check recursively
+		Property prop = propertiesFile.lookUpPropertyObjectByName(expr.getName());
+		if (prop != null) {
+			mainLog.println("\nModel checking : " + prop);
+			return checkExpression(model, prop.getExpression());
+		} else {
+			throw new PrismException("Unknown property reference " + expr);
+		}
+	}
+
 	/**
 	 * Loads labels from a PRISM labels file and stores them in BitSet objects.
 	 * (Actually, it returns a map from label name Strings to BitSets.)