From 67533cbe217ac60f3c18425df1761bac2d61a540 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 23 Dec 2024 10:52:03 +0000 Subject: [PATCH 1/9] CHANGELOG. --- CHANGELOG.txt | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/CHANGELOG.txt b/CHANGELOG.txt index 0d4573774..2732ac030 100644 --- a/CHANGELOG.txt +++ b/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 From 11a3d975d2ad0b4a641345ab1fd493ad89b066ed Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 23 Dec 2024 12:46:55 +0000 Subject: [PATCH 2/9] Comment fixes. --- prism/src/prism/Prism.java | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 7e0da32b8..e11ab0559 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2373,7 +2373,7 @@ public void exportPRISMModelWithExpandedConstants(File file) throws FileNotFound } /** - * Export various aspects, combined, the current built model. + * Export various aspects of the current built model together. * @param file File to export to * @param exportOptions The options for export */ @@ -2407,7 +2407,7 @@ public void exportBuiltModelCombined(File file, ModelExportOptions exportOptions } /** - * Export the transtion matrix for the current built model. + * Export the transition matrix for the current built model. * @param file File to export to * @param exportOptions The options for export */ @@ -4360,6 +4360,7 @@ public void exportTransRewardsToFile(boolean ordered, int exportType, File file) } /** + * @deprecated * Export the currently loaded model's states to a file * @param exportType Type of export; one of: * @param file File to export to (if null, print to the log instead) */ + @Deprecated public void exportStatesToFile(int exportType, File file) throws FileNotFoundException, PrismException { exportBuiltModelStates(file, convertExportType(exportType)); } /** + * @deprecated * Export the observations for the currently loaded model to a file * @param exportType Type of export; one of: * @param file File to export to (if null, print to the log instead) */ + @Deprecated public void exportObservationsToFile(int exportType, File file) throws FileNotFoundException, PrismException { exportBuiltModelObservations(file, convertExportType(exportType)); From b73f04873df379fde3bc50425db1e14b3f282259 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 20 Dec 2024 17:46:00 +0000 Subject: [PATCH 3/9] Simplify/update the LTL-to-HOA scripts. Now one script for each tool, configurable by changing options within. External ltl2dstar script defaults to Spot's ltl2tgba for LTL->NBA. New hoa-ltl2tgba-for-prism: direct use of Spot's ltl2tgba. Update Rabinizer to version 4. --- prism/etc/scripts/hoa/hoa-ltl2dstar-for-prism | 45 +++++++++++++++++++ .../hoa/hoa-ltl2dstar-with-ltl2ba-for-prism | 23 ---------- .../hoa/hoa-ltl2dstar-with-ltl2tgba-for-prism | 25 ----------- .../hoa/hoa-ltl2dstar-with-ltl3ba-for-prism | 36 --------------- prism/etc/scripts/hoa/hoa-ltl2tgba-for-prism | 16 +++++++ .../etc/scripts/hoa/hoa-ltl3dra-dra-for-prism | 30 ------------- ...-tdgra-for-prism => hoa-ltl3dra-for-prism} | 17 +++---- prism/etc/scripts/hoa/hoa-rabinizer-for-prism | 15 +++++++ .../scripts/hoa/hoa-rabinizer3-dgra-for-prism | 17 ------- .../scripts/hoa/hoa-rabinizer3-dra-for-prism | 17 ------- .../hoa/hoa-rabinizer3-tdgra-for-prism | 17 ------- .../scripts/hoa/hoa-rabinizer3-tdra-for-prism | 17 ------- .../hoa/hoa-rabinizer3.1-dgra-for-prism | 17 ------- .../hoa/hoa-rabinizer3.1-dra-for-prism | 17 ------- .../hoa/hoa-rabinizer3.1-tdgra-for-prism | 17 ------- .../hoa/hoa-rabinizer3.1-tdra-for-prism | 17 ------- 16 files changed, 85 insertions(+), 258 deletions(-) create mode 100755 prism/etc/scripts/hoa/hoa-ltl2dstar-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2ba-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2tgba-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl3ba-for-prism create mode 100755 prism/etc/scripts/hoa/hoa-ltl2tgba-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-ltl3dra-dra-for-prism rename prism/etc/scripts/hoa/{hoa-ltl3dra-tdgra-for-prism => hoa-ltl3dra-for-prism} (57%) create mode 100755 prism/etc/scripts/hoa/hoa-rabinizer-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3-dgra-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3-dra-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3-tdgra-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3-tdra-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism delete mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism diff --git a/prism/etc/scripts/hoa/hoa-ltl2dstar-for-prism b/prism/etc/scripts/hoa/hoa-ltl2dstar-for-prism new file mode 100755 index 000000000..a8e86c738 --- /dev/null +++ b/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" "$@" diff --git a/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2ba-for-prism b/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2ba-for-prism deleted file mode 100755 index b81389a20..000000000 --- a/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2ba-for-prism +++ /dev/null @@ -1,23 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling ltl2dstar with ltl2ba as the LTL->NBA tool -# Invoke from PRISM with -# -ltl2datool hoa-ltl2dstar-with-ltl2ba-for-prism -ltl2dasyntax lbt -# -# Expects ltl2dstar and ltl2ba executables on the PATH, otherwise -# specify their location using -# export LTL2DSTAR=path/to/ltl2dstar -# export LTL2BA=path/to/ltl2ba - - -# Take ltl2dstar executable from the LTL2DSTAR environment variable -# Otherwise, default to "ltl2dstar", which will search the PATH -LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar} - -# Take the ltl2ba executable from the LTL2BA environment variable -# Otherwise, default to "ltl2ba", which will search the PATH -LTL2BA_BIN=${LTL2BA-ltl2ba} - -# --output=automaton = we want the automaton -# --output-format=hoa = ... in HOA -$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:$LTL2BA_BIN" "$@" diff --git a/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2tgba-for-prism b/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2tgba-for-prism deleted file mode 100755 index 753ba8c0b..000000000 --- a/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl2tgba-for-prism +++ /dev/null @@ -1,25 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling ltl2dstar with Spot's ltl2tgba as the LTL->NBA tool -# Invoke from PRISM with -# -ltl2datool hoa-ltl2dstar-with-ltl2tgba-for-prism -ltl2dasyntax lbt -# -# Expects ltl2dstar and ltl2tgba executables on the PATH, otherwise -# specify their location using -# export LTL2DSTAR=path/to/ltl2dstar -# export LTL2TGBA=path/to/ltl2tgba - - -# Take ltl2dstar executable from the LTL2DSTAR environment variable -# Otherwise, default to "ltl2dstar", which will search the PATH -LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar} - -# 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 -# --ltl2nba = with ltl2tgba as LTL->NBA -# -s -B = as Spin neverclaim, NBA output -$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:${LTL2TGBA_BIN}@-s -B" "$@" diff --git a/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl3ba-for-prism b/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl3ba-for-prism deleted file mode 100755 index fcb8f12f3..000000000 --- a/prism/etc/scripts/hoa/hoa-ltl2dstar-with-ltl3ba-for-prism +++ /dev/null @@ -1,36 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling ltl2dstar with ltl3ba as the LTL->NBA tool -# Invoke from PRISM with -# -ltl2datool hoa-ltl2dstar-with-ltl3ba-for-prism -ltl2dasyntax lbt -# -# Expects ltl2dstar and ltl3ba executables on the PATH, otherwise -# specify their location using -# export LTL2DSTAR=path/to/ltl2dstar -# export LTL3BA=path/to/ltl3ba -# -# If ltl3ba is not statically compiled, you can specify the path -# to the Buddy library using -# export BUDDY_LIB=path/to/library-dir - -# Take ltl2dstar executable from the LTL2DSTAR environment variable -# Otherwise, default to "ltl2dstar", which will search the PATH -LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar} - -# Take the ltl3ba executable from the LTL3BA environment variable -# Otherwise, default to "ltl3ba", which will search the PATH -LTL3BA_BIN=${LTL3BA-ltl3ba} - -# If BUDDY_LIB environment variable is set, add to appropriate path -if [ ! -z "$BUDDY_LIB" ]; then - if [ "$(uname)" == "Darwin" ]; then - export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" - else - export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" - fi -fi - -# --output=automaton = we want the automaton -# --output-format=hoa = ... in HOA -# --ltl2nba = with ltl3ba as LTL->NBA -$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:$LTL3BA_BIN" "$@" diff --git a/prism/etc/scripts/hoa/hoa-ltl2tgba-for-prism b/prism/etc/scripts/hoa/hoa-ltl2tgba-for-prism new file mode 100755 index 000000000..ceb88f5c9 --- /dev/null +++ b/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 diff --git a/prism/etc/scripts/hoa/hoa-ltl3dra-dra-for-prism b/prism/etc/scripts/hoa/hoa-ltl3dra-dra-for-prism deleted file mode 100755 index a9335b408..000000000 --- a/prism/etc/scripts/hoa/hoa-ltl3dra-dra-for-prism +++ /dev/null @@ -1,30 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling ltl3dra (state-based DRA) -# Invoke from PRISM with -# -ltl2datool hoa-ltl3dra-dra-for-prism -ltl2dasyntax spin -# -# 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 -# 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} - -# If BUDDY_LIB environment variable is set, add to appropriate path -if [ ! -z "$BUDDY_LIB" ]; then - if [ "$(uname)" == "Darwin" ]; then - export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" - else - export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB" - fi -fi - -# -H3 = output deterministic state-based Rabin in HOA format -$LTL3DRA_BIN -H3 -F "$1" > "$2" diff --git a/prism/etc/scripts/hoa/hoa-ltl3dra-tdgra-for-prism b/prism/etc/scripts/hoa/hoa-ltl3dra-for-prism similarity index 57% rename from prism/etc/scripts/hoa/hoa-ltl3dra-tdgra-for-prism rename to prism/etc/scripts/hoa/hoa-ltl3dra-for-prism index 5b83e1ce9..ac6770489 100755 --- a/prism/etc/scripts/hoa/hoa-ltl3dra-tdgra-for-prism +++ b/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" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer-for-prism new file mode 100755 index 000000000..e769574ed --- /dev/null +++ b/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" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3-dgra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3-dgra-for-prism deleted file mode 100755 index 40db41d14..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3-dgra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3 (state-based DGRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3-dra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise -# specify its location using -# export RABINIZER3=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} - -# -hoa = output HOA -# -gen-states = output state-based generalized Rabin -java -jar $RABINIZER3_JAR -hoa -gen-states "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3-dra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3-dra-for-prism deleted file mode 100755 index b264778a1..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3-dra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3 (state-based DRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3-dra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise -# specify its location using -# export RABINIZER3=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} - -# -hoa = output HOA -# -rabin-states = output state-based DRA -java -jar $RABINIZER3_JAR -hoa -rabin-states "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3-tdgra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3-tdgra-for-prism deleted file mode 100755 index a8a467538..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3-tdgra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3 (transition-based DGRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3-tdgra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise -# specify its location using -# export RABINIZER3=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} - -# -hoa = output HOA -# -gen-edges = output transition-based generalized Rabin -java -jar $RABINIZER3_JAR -hoa -gen-edges "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3-tdra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3-tdra-for-prism deleted file mode 100755 index f7feb58c5..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3-tdra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3 (transition-based DRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3-tdra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3 in the current directory, otherwise -# specify its location using -# export RABINIZER3=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER3_JAR=${RABINIZER3-./rabinizer.jar} - -# -hoa = output HOA -# -rabin-edges = output transition-based Rabin -java -jar $RABINIZER3_JAR -hoa -rabin-edges "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism deleted file mode 100755 index ef63e622b..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3.1 (state-based DGRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3.1-dra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise -# specify its location using -# export RABINIZER31=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar} - -# -format=hoa = output HOA -# -auto=sgr = output state-based generalized Rabin -java -jar $RABINIZER31_JAR -format=hoa -auto=sgr -in=file -out=file "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism deleted file mode 100755 index 6ca16c532..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3.1 (state-based DRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3.1-dra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise -# specify its location using -# export RABINIZER31=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar} - -# -format=hoa = output HOA -# -auto=sr = output state-based Rabin -java -jar $RABINIZER31_JAR -format=hoa -auto=sr -in=file -out=file "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism deleted file mode 100755 index 540816104..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3.1 (transition-based DGRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3.1-tdgra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise -# specify its location using -# export RABINIZER31=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar} - -# -format=hoa = output HOA -# -auto=tgr = output transition-based DGRA -java -jar $RABINIZER31_JAR -format=hoa -auto=tgr -in=file -out=file "$1" && mv "$1.hoa" "$2" diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism deleted file mode 100755 index 311fc3ae4..000000000 --- a/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism +++ /dev/null @@ -1,17 +0,0 @@ -#! /bin/bash - -# Interface wrapper for calling Rabinizer3.1 (transition-based DRA) -# Invoke from PRISM with -# -ltl2datool hoa-rabinizer3.1-tdra-for-prism -ltl2dasyntax rabinizer -# -# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise -# specify its location using -# export RABINIZER31=path/to/rabinizer.jar - -# Take location of the jar file from RABINIZER3 environment variable -# Otherwise, default to current directory -RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar} - -# -format=hoa = output HOA -# -auto=tr = output transition-based Rabin -java -jar $RABINIZER31_JAR -format=hoa -auto=tr -in=file -out=file "$1" && mv "$1.hoa" "$2" From c92529e2979271e657792a9617be5251158684ae Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 6 Mar 2024 23:44:43 +0000 Subject: [PATCH 4/9] Parametric model building (not checking) added to Prism. Enabled/disabled by (probably temporary) methods setParametric(...) and setParametricOff(). Not actually called/used yet. --- prism/src/prism/Prism.java | 36 ++++++++++++++++++++++++++++++++---- 1 file changed, 32 insertions(+), 4 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index e11ab0559..ca50629da 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -236,11 +236,11 @@ public enum ModelSource { } public enum ModelBuildType { - SYMBOLIC, EXPLICIT, EXACT + SYMBOLIC, EXPLICIT, EXACT, PARAM } public enum PrismEngine { - SYMBOLIC, EXPLICIT, EXACT + SYMBOLIC, EXPLICIT, EXACT, PARAM } /** Class to store details about a loaded model */ @@ -305,6 +305,12 @@ public class ModelDetails // Info for explicit files load private ExplicitModelImporter modelImporter; + // Info about parametric mode + private boolean param = false; + private String[] paramNames; + private String[] paramLowerBounds; + private String[] paramUpperBounds; + // Has the CUDD library been initialised yet? private boolean cuddStarted = false; @@ -538,6 +544,19 @@ public void setExportAdvFilename(String s) throws PrismException // Set methods for miscellaneous options + public void setParametric(String[] paramNames, String[] paramLowerBounds, String[] paramUpperBounds) + { + param = true; + this.paramNames = paramNames; + this.paramLowerBounds = paramLowerBounds; + this.paramUpperBounds = paramUpperBounds; + } + + public void setParametricOff() + { + param = false; + } + public void setExportDigital(boolean b) throws PrismException { exportDigital = b; @@ -1869,7 +1888,9 @@ public ModulesFile getPRISMModel() */ public PrismEngine getCurrentEngine() { - if (settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED)) { + if (param) { + return PrismEngine.PARAM; + } else if (settings.getBoolean(PrismSettings.PRISM_EXACT_ENABLED)) { return PrismEngine.EXACT; } else if (getEngine() == Prism.EXPLICIT) { return PrismEngine.EXPLICIT; @@ -1905,7 +1926,10 @@ private ModelGenerator getModelGenerator(boolean buildIfMissing) throws Prism if (getPRISMModel() != null) { // Create a model generator via ModulesFileModelGenerator ModulesFileModelGenerator mfmg = null; - if (getCurrentEngine() == PrismEngine.EXACT) { + if (getCurrentEngine() == PrismEngine.PARAM) { + // Parametric model checking uses functions + mfmg = ModulesFileModelGenerator.createForRationalFunctions(getPRISMModel(), paramNames, paramLowerBounds, paramUpperBounds, this); + } else if (getCurrentEngine() == PrismEngine.EXACT) { // Exact model checking uses rationals mfmg = ModulesFileModelGenerator.createForRationalFunctions(getPRISMModel(), this); } else { @@ -2017,6 +2041,8 @@ public ModelBuildType getModelBuildTypeForEngine(PrismEngine engine) return ModelBuildType.SYMBOLIC; case EXACT: return ModelBuildType.EXACT; + case PARAM: + return ModelBuildType.PARAM; default: return null; } @@ -2152,6 +2178,7 @@ private void doBuildModel() throws PrismException break; case EXPLICIT: case EXACT: + case PARAM: explicit.Model newModelExpl; switch (getModelSource()) { case PRISM_MODEL: @@ -4153,6 +4180,7 @@ private void setBuiltModel(ModelBuildType buildType, prism.Model newModel) th break; case EXPLICIT: case EXACT: + case PARAM: if (!(newModel instanceof explicit.Model)) { throw new PrismException("Attempt to store model of incorrect type"); } From 2d689f4e244e735cf94c2f6622280087c149ef9d Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 27 Sep 2024 16:49:06 +0100 Subject: [PATCH 5/9] Integrate parametric model checking into Prism. This now goes through the usual modelCheck() call and the parametric model is built and stored in the usual way. This means that parametric models can now be built/exported. The old Prism.modelCheckParametric is recreated for compatability. --- prism/src/prism/Prism.java | 90 ++++++++++++++++-------------------- prism/src/prism/PrismCL.java | 22 ++------- 2 files changed, 45 insertions(+), 67 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index ca50629da..ac131ece6 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3141,6 +3141,15 @@ public Result modelCheck(PropertiesFile propertiesFile, Property prop) throws Pr throw new PrismNotSupportedException("Exact model checking not supported for " + getModelType() + "s"); } } + // Parametric model checking only support for some models/settings + if (getCurrentEngine() == PrismEngine.PARAM) { + if (!(getModelType() == ModelType.DTMC || getModelType() == ModelType.CTMC || getModelType() == ModelType.MDP || !getModelType().isProbabilistic())) { + throw new PrismNotSupportedException("Parametric model checking not supported for " + getModelType() + "s"); + } + if (getModelType() == ModelType.MDP && getFairness()) { + throw new PrismNotSupportedException("Parametric model checking does not support checking MDPs under fairness"); + } + } // PTA (and similar) model checking is handled separately if (getModelType().realTime()) { return modelCheckPTA(propertiesFile, prop.getExpression(), definedPFConstants); @@ -3245,6 +3254,10 @@ else if (settings.getString(PrismSettings.PRISM_HEURISTIC).equals("Speed") && ge ParamModelChecker mc = new ParamModelChecker(this, ParamMode.EXACT); mc.setModelCheckingInfo(getPRISMModel(), propertiesFile, getRewardGenerator()); res = mc.check(getBuiltModelExplicit(), prop.getExpression()); + } else if (getCurrentEngine() == PrismEngine.PARAM) { + ParamModelChecker mc = new ParamModelChecker(this, ParamMode.PARAMETRIC); + mc.setModelCheckingInfo(getPRISMModel(), propertiesFile, getRewardGenerator()); + res = mc.check(getBuiltModelExplicit(), prop.getExpression()); } // If model checking generated a strategy, store it @@ -3526,56 +3539,6 @@ public void modelCheckSimulatorExperiment(PropertiesFile propertiesFile, Undefin getSimulator().modelCheckExperiment(propertiesFile, undefinedConstants, results, expr, initialState, maxPathLength, simMethod); } - /** - * Perform parametric model checking on the currently loaded model. - * @param propertiesFile parent properties file - * @param prop property to model check - * @param paramNames parameter names - * @param paramLowerBounds lower bounds of parameters - * @param paramUpperBounds upper bounds of parameters - */ - public Result modelCheckParametric(PropertiesFile propertiesFile, Property prop, String[] paramNames, String[] paramLowerBounds, String[] paramUpperBounds) - throws PrismException - { - // Some checks - if (paramNames == null) { - throw new PrismException("Must specify some parameters when using " + "the parametric analysis"); - } - if (!(getModelType() == ModelType.DTMC || getModelType() == ModelType.CTMC || getModelType() == ModelType.MDP)) - throw new PrismNotSupportedException("Parametric model checking is only supported for DTMCs, CTMCs and MDPs"); - - if (getModelType() == ModelType.MDP && getFairness()) - throw new PrismNotSupportedException("Parametric model checking does not support checking MDPs under fairness"); - - Values definedPFConstants = propertiesFile.getConstantValues(); - Values constlist = getPRISMModel().getConstantValues(); - for (int pnr = 0; pnr < paramNames.length; pnr++) { - constlist.removeValue(paramNames[pnr]); - } - - // Print info - mainLog.printSeparator(); - mainLog.println("\nParametric model checking: " + prop); - if (getUndefinedModelValues() != null && getUndefinedModelValues().getNumValues() > 0) - mainLog.println("Model constants: " + getUndefinedModelValues()); - if (definedPFConstants != null && definedPFConstants.getNumValues() > 0) - mainLog.println("Property constants: " + definedPFConstants); - - // Remove old strategy if present - clearStrategy(); - - // Execute parameteric model checking - ConstructModel constructModel = new ConstructModel(this); - constructModel.setFixDeadlocks(getFixDeadlocks()); - ModulesFileModelGenerator modelGenFunc = ModulesFileModelGenerator.createForRationalFunctions(getPRISMModel(), paramNames, paramLowerBounds, paramUpperBounds, this); - explicit.Model modelExpl = constructModel.constructModel(modelGenFunc); - ParamModelChecker mc = new ParamModelChecker(this, ParamMode.PARAMETRIC); - mc.setModelCheckingInfo(getPRISMModel(), propertiesFile, modelGenFunc); - Result result = mc.check(modelExpl, prop.getExpression()); - - return result; - } - /** * Export the current strategy. The associated model should be attached to the strategy. * Strictly, speaking that does not need to be the currently loaded model, @@ -4526,6 +4489,33 @@ public Result modelCheckExact(PropertiesFile propertiesFile, Property prop) thro settings.set(PrismSettings.PRISM_EXACT_ENABLED, exactOld); return result; } + + /** + * Perform parametric model checking on the currently loaded model. + * @param propertiesFile parent properties file + * @param prop property to model check + * @param paramNames parameter names + * @param paramLowerBounds lower bounds of parameters + * @param paramUpperBounds upper bounds of parameters + * @deprecated Better to use {@link #modelCheck(PropertiesFile, Property)} now. + */ + @Deprecated + public Result modelCheckParametric(PropertiesFile propertiesFile, Property prop, String[] paramNames, String[] paramLowerBounds, String[] paramUpperBounds) + throws PrismException + { + boolean paramOld = param; + String[] paramNamesOld = this.paramNames; + String[] paramLowerBoundsOld = this.paramLowerBounds; + String[] paramUpperBoundsOld = this.paramUpperBounds; + setParametric(paramNames, paramLowerBounds, paramUpperBounds); + Result result = modelCheck(propertiesFile, prop); + if (paramOld) { + setParametric(paramNamesOld, paramLowerBoundsOld, paramUpperBoundsOld); + } else { + setParametricOff(); + } + return result; + } } //------------------------------------------------------------------------------ diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index c10c24857..fe89e6b38 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -300,10 +300,6 @@ public void run(String[] args) // Sort out properties to check sortProperties(); - if (param && numPropertiesToCheck == 0) { - errorAndExit("Parametric model checking requires at least one property to check"); - } - // evaluate constants exactly if we are in param or exact computation mode exactConstants = param || prism.getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); @@ -337,6 +333,9 @@ public void run(String[] args) } catch (PrismException e) { errorAndExit(e.getMessage()); } + if (param) { + prism.setParametric(paramNames, paramLowerBounds, paramUpperBounds); + } // If -exportadv was used and the explicit engine has been requested for MDPs, // or the model type is only supported by the explicit engine, stop with an error message @@ -438,21 +437,15 @@ public void run(String[] args) propertiesFile.setSomeUndefinedConstants(definedPFConstants, exactConstants); } // Normal model checking - if (!simulate && !param) { + if (!simulate) { res = prism.modelCheck(propertiesFile, propertiesToCheck.get(j)); } - // Parametric model checking - else if (param) { - res = prism.modelCheckParametric(propertiesFile, propertiesToCheck.get(j), paramNames, paramLowerBounds, paramUpperBounds); - } // Approximate (simulation-based) model checking - else if (simulate) { + else { simMethod = processSimulationOptions(propertiesToCheck.get(j).getExpression()); res = prism.modelCheckSimulator(propertiesFile, propertiesToCheck.get(j).getExpression(), definedPFConstants, null, simMaxPath, simMethod); simMethod.reset(); - } else { - throw new PrismException("Cannot use parametric model checking and simulation at the same time"); } } catch (PrismException e) { // in case of error, report it, store exception as the result and proceed @@ -628,7 +621,6 @@ protected void exportResults() private void initialise(String[] args) { try { - // prepare storage for parametric model checking // default to log going to stdout // this means all errors etc. can be safely sent to the log // even if a new log is created shortly @@ -830,10 +822,6 @@ private void doExports() exportsccs || exportbsccs || exportmecs) { - if (param) { - mainLog.printWarning("Skipping exports in parametric model checking mode, currently not supported."); - return; - } // if there are any exports to do, // force model construction to catch errors during build try { From 6984dddc5f1800722a0a535f1833c34e566215cf Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 5 Jan 2025 23:06:13 +0000 Subject: [PATCH 6/9] Connect exact model building/exporting in the GUI. --- .../userinterface/model/GUIMultiModelHandler.java | 15 ++++++++------- .../properties/GUIMultiProperties.java | 9 ++++++--- 2 files changed, 14 insertions(+), 10 deletions(-) diff --git a/prism/src/userinterface/model/GUIMultiModelHandler.java b/prism/src/userinterface/model/GUIMultiModelHandler.java index 14b584049..961a8c56f 100644 --- a/prism/src/userinterface/model/GUIMultiModelHandler.java +++ b/prism/src/userinterface/model/GUIMultiModelHandler.java @@ -649,7 +649,8 @@ private void buildAfterParse() } try { // currently, don't evaluate constants exactly - prism.setPRISMModelConstants(unC.getMFConstantValues(), false); + boolean exact = prism.getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + prism.setPRISMModelConstants(unC.getMFConstantValues(), exact); } catch (PrismException e) { theModel.error(e.getMessage()); return; @@ -737,8 +738,8 @@ private void exportAfterParse() lastMFConstants = unC.getMFConstantValues(); } try { - // currently, don't evaluate constants exactly - prism.setPRISMModelConstants(unC.getMFConstantValues(), false); + boolean exact = prism.getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + prism.setPRISMModelConstants(unC.getMFConstantValues(), exact); } catch (PrismException e) { theModel.error(e.getMessage()); return; @@ -778,8 +779,8 @@ private void computeSteadyStateAfterParse() lastMFConstants = unC.getMFConstantValues(); } try { - // for steady-state, currently don't evaluate constants exactly - prism.setPRISMModelConstants(unC.getMFConstantValues(), false); + boolean exact = prism.getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + prism.setPRISMModelConstants(unC.getMFConstantValues(), exact); } catch (PrismException e) { theModel.error(e.getMessage()); return; @@ -817,8 +818,8 @@ private void computeTransientAfterParse() lastMFConstants = unC.getMFConstantValues(); } try { - // for transient computation, currently don't evaluate constants exactly - prism.setPRISMModelConstants(unC.getMFConstantValues(), false); + boolean exact = prism.getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + prism.setPRISMModelConstants(unC.getMFConstantValues(), exact); } catch (PrismException e) { theModel.error(e.getMessage()); return; diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index bfc787247..8f0da0a81 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -1154,10 +1154,14 @@ public void exportLabelsAfterParse() // Switch off flag exportLabelsAfterReceiveParseNotification = false; try { + // are we in exact mode? + boolean exact = getPrism().getSettings().getBoolean(PrismSettings.PRISM_EXACT_ENABLED); + // Parse labels/constants parsedProperties = getPrism().parsePropertiesString(getLabelsString() + "\n" + getConstantsString()); // Query user for undefined constant values (if required) UndefinedConstants uCon = new UndefinedConstants(parsedModel, parsedProperties, true); + uCon.setExactMode(exact); if (uCon.getMFNumUndefined() + uCon.getPFNumUndefined() > 0) { // Use previous constant values as defaults in dialog Values lastModelConstants = getPrism().getUndefinedModelValues(); @@ -1167,9 +1171,8 @@ public void exportLabelsAfterParse() } // Store model/property constants pfConstants = uCon.getPFConstantValues(); - // currently, evaluate constants non-exact for model building - getPrism().setPRISMModelConstants(uCon.getMFConstantValues(), false); - parsedProperties.setSomeUndefinedConstants(pfConstants, false); + getPrism().setPRISMModelConstants(uCon.getMFConstantValues(), exact); + parsedProperties.setSomeUndefinedConstants(pfConstants, exact); // If export is being done to log, switch view to log if (exportFile == null) logToFront(); From 9fc2b1ed5391d122edaccc1e4a4ef2777b13fb0f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 6 Jan 2025 12:15:33 +0000 Subject: [PATCH 7/9] Add descriptions for some Prism enums. --- prism/src/prism/Prism.java | 51 +++++++++++++++++++++++++++++++++++--- 1 file changed, 48 insertions(+), 3 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index ac131ece6..4b5dd7c41 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -232,15 +232,60 @@ public class Prism extends PrismComponent implements PrismSettingsListener //------------------------------------------------------------------------------ public enum ModelSource { - PRISM_MODEL, MODEL_GENERATOR, EXPLICIT_FILES, BUILT_MODEL + PRISM_MODEL, MODEL_GENERATOR, EXPLICIT_FILES, BUILT_MODEL; + public String description() + { + switch (this) { + case PRISM_MODEL: + return "PRISM model"; + case MODEL_GENERATOR: + return "model generator"; + case EXPLICIT_FILES: + return "explicit files"; + case BUILT_MODEL: + return "built model"; + default: + return this.toString(); + } + } } public enum ModelBuildType { - SYMBOLIC, EXPLICIT, EXACT, PARAM + SYMBOLIC, EXPLICIT, EXACT, PARAM; + public String description() + { + switch (this) { + case SYMBOLIC: + return "symbolic"; + case EXPLICIT: + return "explicit"; + case EXACT: + return "exact"; + case PARAM: + return "parametric"; + default: + return this.toString(); + } + } } public enum PrismEngine { - SYMBOLIC, EXPLICIT, EXACT, PARAM + SYMBOLIC, EXPLICIT, EXACT, PARAM; + public String description() + { + switch (this) { + case SYMBOLIC: + return "symbolic"; + case EXPLICIT: + return "explicit"; + case EXACT: + return "exact"; + case PARAM: + return "parametric"; + default: + return this.toString(); + } + } } /** Class to store details about a loaded model */ From b55f316e59f928ad79190c3be5c75a2c65bb7ea3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 6 Jan 2025 16:12:30 +0000 Subject: [PATCH 8/9] JUnit tests change: "make unittests" runs in quiet mode. --- prism/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism/Makefile b/prism/Makefile index 3590d2523..178fa45e2 100644 --- a/prism/Makefile +++ b/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: From 15182b7456bda059f8696a4e507d99c30fa7d764 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 6 Jan 2025 16:13:35 +0000 Subject: [PATCH 9/9] prism-auto fix: pipes.quote removed from Python 3.13. Use shlex. https://peps.python.org/pep-0594/ --- prism/etc/scripts/prism-auto | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prism/etc/scripts/prism-auto b/prism/etc/scripts/prism-auto index 4425b0b7f..837257967 100755 --- a/prism/etc/scripts/prism-auto +++ b/prism/etc/scripts/prism-auto @@ -12,7 +12,7 @@ # Run "prism-auto -h" for details of further options. import os,sys,re,subprocess,signal,tempfile,functools,logging,time,platform,csv -from pipes import quote +from shlex import quote from optparse import OptionParser from threading import Timer