Improved "echo" (-e) functionality for prism-auto: displays more accurately what prism-auto would do, including test (-t) and log (-l) modes [from Joachim Klein].

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

prism/etc/scripts/prism-auto

@@ -12,6 +12,7 @@
 # Run "prism-auto -h" for details of further options.
 
 import os,sys,re,subprocess,signal,tempfile,functools,filecmp,logging
+from pipes import quote
 from optparse import OptionParser
 
 #==================================================================================================
@@ -290,9 +291,20 @@ def runPrism(args, dir=""):
         if options.testAll: args.append("-testall")
         else: args.append("-test")
     prismArgs = [options.prismExec] + args
-    print ' '.join(prismArgs)
     if options.echo:
+        prismArgs = ['echo', quote(' '.join(prismArgs)), ';'] + prismArgs
+        if options.logDir:
+            logFile = os.path.relpath(os.path.join(options.logDir, createLogFileName(args, dir)))
+            logFile = quote(logFile)
+            if options.test:
+                prismArgs += ['|', 'tee', logFile]
+            else:
+                prismArgs += ['>', logFile]
+        if options.test:
+            prismArgs += ['|', 'grep "Testing result:"']
+        print ' '.join(prismArgs)
         return
+    print ' '.join(prismArgs)
     if options.logDir:
         logFile = os.path.join(options.logDir, createLogFileName(args, dir))
         f = open(logFile, 'w')

prism/src/prism/NondetModelChecker.java

@@ -567,7 +567,7 @@ public class NondetModelChecker extends NonProbModelChecker
 				throw new PrismException("Multi-objective only supports F operator for rewards");
 			}*/
 		}
-		if (exprProb != null) {// || ((ExpressionTemporal) exprReward.getExpression()).getOperator() != ExpressionTemporal.R_C) {
+		if (exprProb != null && exprProb.getExpression() instanceof ExpressionTemporal) {// || ((ExpressionTemporal) exprReward.getExpression()).getOperator() != ExpressionTemporal.R_C) {
 			exprTemp = (ExpressionTemporal) exprProb.getExpression();
 			//TODO we currently ignore the lower bound
 			if (exprTemp.getUpperBound() != null) {