prism-auto: --skip-duplicate-runs

When using -x to add additional options, i.e., to force a specific engine,
often runs of PRISM are effectively duplicated, e.g., if there are .args files
that select multiple engines.

Using the --skip-duplicate-runs, prism-auto tries to clean up the argument list,
remove switches that don't have an effect and to detect duplicate runs, only actually
executing the first one.

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()