From fb7208d792e279e2ade910d2da1829253f5397f9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 11 Jun 2015 14:51:59 +0000 Subject: [PATCH] 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 | 14 +++++++++++++- prism/src/prism/NondetModelChecker.java | 2 +- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/prism/etc/scripts/prism-auto b/prism/etc/scripts/prism-auto index 1a4b6ab1..a7382a1a 100755 --- a/prism/etc/scripts/prism-auto +++ b/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') diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index f0c9dbb0..5cb46635 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/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) {