prism-auto fix (pipes -> shlex)

CHANGELOG.txt

@@ -1,7 +1,7 @@
 This file contains details of the changes in each new version of PRISM.
 
 -----------------------------------------------------------------------------
-Changes since last release (up to 4c095aae5)
+Changes since last release (up to ed80e0ed7)
 -----------------------------------------------------------------------------
 
 * Explicit engine improvements
@@ -14,6 +14,11 @@ Changes since last release (up to 4c095aae5)
   - actions=true/false option
   - remove old options (MRMC format, unordered)
 
+* Import functionality (from explicit files)
+  - import of transition rewards
+  - import for exact mode, LTSs
+  - import progress display (symbolic engine)
+
 * Minor modelling language updates
   - new power operator a^b, equivalent to pow(a,b)
   - fix: implication (=>) is right-associative
@@ -26,8 +31,8 @@ Changes since last release (up to 4c095aae5)
   - prism.Prism: refactored storage/access for model info
   - prism.Prism: integration of exact model building/checking
   - redesign/refactoring of explicit engine reward classes
-  - refactoring of explicit engine model export code
-    (moved from model classes, centralised in io package)
+  - refactoring of explicit engine model import/export code
+    (centralised in io package, export moved from model classes)
   - parametric engine refactored to use explicit models/rewards
   - symbolic code rearranged (new symbolic package)
   - symbolic model storage refactored, simplified, documented

prism/Makefile

@@ -511,7 +511,7 @@ count_loc:
 # Run all unit tests
 unittests: make_tests
 	# Provide Regex to match our test classes. If none is given, only certain test classes are excluded by default.
-	$(JAVA) -jar lib/junit-platform-console-standalone.jar -cp classes --include-classname '^(Test.*|.+[.$$]Test.*|.+Tests?[.$$].+|.*Tests?)$$' -scan-classpath
+	$(JAVA) -jar lib/junit-platform-console-standalone.jar -cp classes --include-classname '^(Test.*|.+[.$$]Test.*|.+Tests?[.$$].+|.*Tests?)$$' -scan-classpath --details=summary
 
 # Run a single test case from the test suite (useful quick check that the build was ok)
 test:

prism/etc/scripts/hoa/hoa-ltl2dstar-for-prism

@@ -0,0 +1,45 @@
+#! /bin/bash
+
+# Interface wrapper for calling ltl2dstar
+# Invoke from PRISM with
+#  -ltl2datool hoa-ltl2dstar-for-prism -ltl2dasyntax lbt
+
+# Expects the ltl2dstar executable to be on the PATH, otherwise specify its location using
+#  export LTL2DSTAR=path/to/ltl2dstar
+
+# ---
+
+# ltl2dstar needs an LTL->NBA tool
+# We default to Spot's ltl2tgba
+# Comment/uncomment the blocks below to replace with 
+# As above, specify the paths to the executables as needed
+
+# Spot's ltl2tgba as the LTL->NBA tool
+# Take the ltl2tgba executable from the LTL2TGBA environment variable
+# Otherwise, default to "ltl2tgba", which will search the PATH
+LTL2TGBA_BIN=${LTL2TGBA-ltl2tgba}
+# ltl2tgba args: -s -B = as Spin neverclaim, NBA output
+LTL2NBA_CMD="--ltl2nba=spin:${LTL2TGBA_BIN}@-s -B"
+
+# # ltl2ba as the LTL->NBA tool
+# # Take the ltl2ba executable from the LTL2BA environment variable
+# #  export LTL2BA=path/to/ltl2ba
+# # Otherwise, default to "ltl2ba", which will search the PATH
+# LTL2BA_BIN=${LTL2BA-ltl2ba}
+# LTL2NBA_CMD="--ltl2nba=spin:$LTL2BA_BIN"
+
+# # ltl3ba as the LTL->NBA tool
+# # Take the ltl3ba executable from the LTL3BA environment variable
+# # Otherwise, default to "ltl3ba", which will search the PATH
+# LTL3BA_BIN=${LTL3BA-ltl3ba}
+# LTL2NBA_CMD="--ltl2nba=spin:$LTL3BA_BIN"
+
+# ---
+
+# Take ltl2dstar executable from the LTL2DSTAR environment variable
+# Otherwise, default to "ltl2dstar", which will search the PATH
+LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar}
+
+# --output=automaton = we want the automaton
+# --output-format=hoa = ... in HOA
+$LTL2DSTAR_BIN --output=automaton --output-format=hoa "$LTL2NBA_CMD" "$@"

prism/etc/scripts/hoa/hoa-ltl2tgba-for-prism

@@ -0,0 +1,16 @@
+#! /bin/bash
+
+# Interface wrapper for calling Spot's ltl2tgba
+# Invoke from PRISM with
+#  -ltl2datool hoa-ltl2tgba-for-prism -ltl2dasyntax lbt
+
+# Expects the ltl2tgba executable to be on the PATH, otherwise specify its location using
+#  export LTL2TGBA=path/to/ltl2tgba
+
+# Take the ltl2tgba executable from the LTL2TGBA environment variable
+# Otherwise, default to "ltl2tgba", which will search the PATH
+LTL2TGBA_BIN=${LTL2TGBA-ltl2tgba}
+
+# --output=automaton = we want the automaton
+# --output-format=hoa = ... in HOA
+$LTL2TGBA_BIN --file="$1" --lbt-input --hoaf --output="$2" --generic --deterministic

prism/etc/scripts/hoa/hoa-ltl3dra-tdgra-for-prism → prism/etc/scripts/hoa/hoa-ltl3dra-for-prism

@@ -1,18 +1,16 @@
 #! /bin/bash
 
-# Interface wrapper for calling ltl3dra (transition-based DGRA)
+# Interface wrapper for calling ltl3dra
 # Invoke from PRISM with
-#  -ltl2datool hoa-ltl3dra-tdgra-for-prism -ltl2dasyntax spin
+#  -ltl2datool hoa-ltl3dra-for-prism -ltl2dasyntax spin
 #
-# Expects the ltl3dra on the PATH, otherwise
-# specify its location using
+# Expects the ltl3dra on the PATH, otherwise specify its location using
 #  export LTL3DRA=path/to/ltl3dra
 #
-# Expects the dynamic buddy library to be in the library PATH, otherwise
-# specify its location using
+# Expects the dynamic buddy library to be in the library PATH,
+# otherwise specify its location using
 #  export BUDDY_LIB=path/to/buddy-lib-dir
 
-
 # Take ltl3dra executable from the LTL3DRA environment variable
 # Otherwise, default to "ltl3dra", which will search the PATH
 LTL3DRA_BIN=${LTL3DRA-ltl3dra}
@@ -26,5 +24,8 @@ if [ ! -z "$BUDDY_LIB" ]; then
     fi
 fi
 
+# Change the switch accordingly to get state-based Rabin
+# or transition-based generalized-Rabin automata
 # -H2 = output deterministic transition-based generalized-Rabin in HOA format
-$LTL3DRA_BIN  -H2 -F "$1" > "$2"
+# -H3 = output deterministic state-based Rabin in HOA format
+$LTL3DRA_BIN -H3 -F "$1" > "$2"

prism/etc/scripts/hoa/hoa-rabinizer-for-prism

@@ -0,0 +1,15 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer (version 4)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the ltl2dra executable to be on the PATH, otherwise specify its location using
+# specify its location using
+#  export RABINIZER_LTL2DRA=path/to/ltl2dra
+
+# Take the  executable from the RABINIZER_LTL2DRA environment variable
+# Otherwise, default to "ltl2dra", which will search the PATH
+RABINIZER_LTL2DRA_BIN=${RABINIZER_LTL2DRA-ltl2dra}
+
+$RABINIZER_LTL2DRA_BIN --filein "$1" --fileout="$2"