diff --git a/prism/etc/scripts/prism-auto b/prism/etc/scripts/prism-auto index fbbba8e2..d705c782 100755 --- a/prism/etc/scripts/prism-auto +++ b/prism/etc/scripts/prism-auto @@ -20,12 +20,45 @@ from optparse import OptionParser #================================================================================================== # statistics about test results -testStats = dict(SUCCESS = 0, FAILURE = 0, SKIPPED = 0, UNSUPPORTED = 0, WARNING = 0, DDWARNING = 0) +testStats = dict(SUCCESS = 0, FAILURE = 0, SKIPPED = 0, UNSUPPORTED = 0, WARNING = 0, DDWARNING = 0, DUPLICATE = 0) # colour coding for test results # for colour values, see https://en.wikipedia.org/wiki/ANSI_escape_code#Colors testColours = dict(SUCCESS = 32, FAILURE = 31, SKIPPED = 90, UNSUPPORTED = 34, WARNING = 33) +# mapping from PRISM switch shortcuts to the full version (for canonicalisation of arguments) +# to get a list of abbreviated settings in prism, run prism --help | grep '(or ' +switchShortcuts = { + # engines: + '-ex': '-explicit', + '-m': '-mtbdd', + '-s': '-sparse', + '-h': '-hybrid', + # iteration/solver settings: + '-pow': '-power', + '-pwr': '-power', + '-jac': '-jacobi', + '-gs' : '-gaussseidel', + '-bgs': '-bgaussseidel', + '-pgs': '-pgaussseidel', + '-bpgs': '-bpgaussseidel', + '-ii': '-intervaliter', + '-lp': '-linprog', + # epsilon related settings: + '-rel': '-relative', + '-abs': '-absolute', + '-e': '-epsilon', + # other: + '-ss': '-steadystate', + '-tr': '-transient', + '-pctl': '-pf', + '-csl': '-pf', + '-prop': '-property', + } + +# set of PRISM argument tuples that already ran +alreadyRan = set() + #================================================================================================== # Utility functions #================================================================================================== @@ -360,6 +393,87 @@ def printColoured(colour, msg): else: print(msg) +# +# Given a switch (-xyz or --xyz), expand to full-length form +# using the switchShortcuts mapping. +# Switches can also have the form -xyz:foo=..., i.e., carrying +# additional arguments; this is handled as well. +# Return expanded switch or the original parameter, if not expanded. +# +def expandShortcutSwitch(s): + xtradash = '' + if (s.startswith('--')): + xtradash = '-' + s = s[1:] + # split off extra arguments after a : + l = s.split(':',1) + # continue with the actual switch name + s = l[0] + # get entry for s; otherwise, default value is s itself + s = switchShortcuts.get(s,s) + # add back extra dash, if necessary + s = xtradash + s + # add back :arg part, if necessary + if len(l) == 2: + s += ':' + l[1] + return s + +# +# Given an argument list, expand short-form switches (-xyz or --xyz) +# to their full-length form using the switchShortcuts mapping. +# Returns processed argument list. +# +def expandShortcutsInArgs(args): + return [expandShortcutSwitch(x) for x in args] + +# +# Given an argument list, remove conflicting settings, +# e.g., if there are multiple switches for selecting +# the PRISM engine, only keep the last one, i.e., +# the switch that PRISM will actually use. +# Returns processed argument list. +# +def removeConflictingArgs(args, conflicting): + seen = False + result = [] + for x in reversed(args): + if x in conflicting: + if not seen: result.append(x) + seen = True + else: + result.append(x) + result.reverse() + return list(result) + +# +# Given an argument list, returns a (more or less) +# canonical version: +# * Performs regularisation of --switch to -switch +# * Expands short-form switches to long-form version +# (if we know about them, see switchShortcuts mapping) +# * Removes conflicting switches for +# - PRISM engine, as well as -exact and -param setting +# - model type override +# +def canonicaliseArgs(args): + # canonicalise --switch to -switch + args = [ x[1:] if x.startswith('--') else x for x in args] + # expand the short cuts via switchShortcuts mapping + args = expandShortcutsInArgs(args) + # remove conflicting engine setting + engines = frozenset(['-explicit', '-hybrid', '-sparse', '-mtbdd']) + args = removeConflictingArgs(args, engines) + # remove conflicting model type overrides + args = removeConflictingArgs(args, frozenset(['-mdp', '-dtmc', '-ctmc'])) + # handle exact / param switches + if '-exact' in args or '-param' in args: + # remove engines if we are in exact or param mode (normal engines are irrelevant) + args = [x for x in args if x not in engines ] + if '-param' in args: + # remove -exact if we are in param mode (param takes precedence) + args = [x for x in args if x != '-exact' ] + return args + #================================================================================================== # Benchmarking #================================================================================================== @@ -367,6 +481,14 @@ def printColoured(colour, msg): # Run PRISM with a given list of command-line args def runPrism(args, dir=""): + # check if we can skip + if options.skipDuplicates: + canonicalArgs = canonicaliseArgs(args) + if (tuple(canonicalArgs) in alreadyRan): + incrementTestStat('DUPLICATE') + return + alreadyRan.add(tuple(canonicalArgs)) + # keep track if we need to cleanup the log file after use cleanupLogFile = False if options.test: @@ -489,6 +611,8 @@ def printTestStatistics(): printColoured('FAILURE', ' Failure: ' + str(testStats['FAILURE'])) printColoured('UNSUPPORTED', ' Unsupported: ' + str(testStats['UNSUPPORTED'])) printColoured('SKIPPED', ' Skipped: ' + str(testStats['SKIPPED'])) + if options.skipDuplicates: + printColoured('SKIPPED', ' Skipped dup.: ' + str(testStats['DUPLICATE']) + ' (due to --skip-duplicate-runs)') def countTestResult(msg): if 'Error:' in msg or 'FAIL' in msg: @@ -812,6 +936,7 @@ parser.add_option("--echo-full", action="store_true", dest="echoFull", default=F parser.add_option("--models-filename", dest="modelsFilename", metavar="X", default="models", help="Read in list of models/parameters for a directory from file X, if present [default=models]") parser.add_option("--no-export-tests", action="store_true", dest="noExportTests", default=False, help="Don't check exported files when in test mode") parser.add_option("--skip-export-runs", action="store_true", dest="skipExportRuns", default=False, help="Skip all runs having exports") +parser.add_option("--skip-duplicate-runs", action="store_true", dest="skipDuplicates", default=False, help="Skip PRISM runs which have the same arguments as an earlier run (with some heuristics to detect equivalent arguments)") parser.add_option("--dd-warnings", action="store_true", dest="ddWarnings", default=False, help="Print the DD reference count warnings") parser.add_option("--colour", dest="colourEnabled", metavar="X", type="choice", choices=["yes","no","auto"], default="auto", help="Whether to colour test results: yes, no, auto (yes iff in terminal mode) [default=auto]") (options, args) = parser.parse_args()