updates

Author: sjunges

.docker/install-modest.sh

@@ -1,16 +1,17 @@
 echo 'Downloading Modest (targetplatform = ${TARGETPLATFORM})';
 mkdir tmp; cd tmp;
-wget https://www.modestchecker.net/Downloads/Modest-umb-all.zip ;
-unzip Modest-umb-all.zip ;
-rm Modest-umb-all.zip ;
-ls
-if [ "${TARGETPLATFORM}" = "linux/x64" ] ; then
-  echo 'Installing Modest for linux/x64';
-  tar xvf Modest-linux-x64.tar.xz;
-else
+if [ "${TARGETPLATFORM}" = "linux/amd64" ] ; then
+  echo 'Installing Modest for linux/amd64';
+  wget wget "https://www.modestchecker.net/Downloads/Modest-Toolset-$(wget -qO- https://www.modestchecker.net/Downloads/Version.txt)-linux-x64.zip"
+elif [ "${TARGETPLATFORM}" = "linux/arm64" ] ; then
   echo 'Installing Modest for linux/arm64';
-  tar xvf Modest-linux-arm64.tar.xz ;
+  wget wget "https://www.modestchecker.net/Downloads/Modest-Toolset-$(wget -qO- https://www.modestchecker.net/Downloads/Version.txt)-linux-arm64.zip"
+else
+  echo "Unknown targetplatform ${TARGETPLATFORM}"
+  exit 1
 fi
+unzip *.zip ;
+rm *.zip ;
 mv Modest /opt/Modest
 cd .. ;
 rm -rf tmp ;

Dockerfile

@@ -42,8 +42,8 @@ ARG storm_build_type=Release
 ARG no_threads=1
 ARG storm_repo=https://github.com/tquatmann/storm.git
 ARG storm_branch=io/binaryformat
-ARG prism_repo=https://github.com/davexparker/prism.git
-ARG prism_branch=umb
+ARG prism_repo=https://github.com/prismmodelchecker/prism.git
+ARG prism_branch=master
 
 # Build Storm
 #############

umbtest/benchmarks.py

@@ -105,7 +105,7 @@ def check_prism_file(
         )
         result["checker"] = None
         result["transformer"] = None
-        if result["loader"].error_code != 0:
+        if result["loader"].exit_code != 0:
             with open(result["loader"].logfile, "r") as f:
                 print(f.read())
             if result["loader"].not_supported:
@@ -133,7 +133,7 @@ def check_prism_file(
                     Path(tmpfile_out.name),
                     log_file=Path(self._tmplogfile().name),
                 )
-                if result["transformer"].error_code != 0:
+                if result["transformer"].exit_code != 0:
                     return result
             except Exception as e:
                 raise RuntimeError(f"{self._transformer.name} raised {type(e)}:{e}!")
@@ -144,7 +144,7 @@ def check_prism_file(
             log_file=Path(self._tmplogfile().name),
             properties=properties,
         )
-        if result["checker"].error_code != 0:
+        if result["checker"].exit_code != 0:
             with open(result["checker"].logfile, "r") as f:
                 print(f.read())
             if result["checker"].anticipated_error or result["checker"].not_supported:

umbtest/tools.py

@@ -46,7 +46,7 @@ def parse_logfile_storm(log, inv):
     inv.anticipated_error = contains_any_of(log, known_error_messages)
     if inv.not_supported or inv.anticipated_error:
         return
-    if inv.error_code not in [0, 1]:
+    if inv.exit_code not in [0, 1]:
         if not inv.timeout and not inv.memout:
             print("WARN: Unexpected return code(s): {}".format(inv["return-codes"]))
 
@@ -312,13 +312,14 @@ def _call_mcsta(self, log_file, args):
         reported_result.memout = False
         reported_result.logfile = log_file
         if log_file is not None:
-            print(log_file)
             with open(log_file, "r") as log:
                 print(log.read())
                 for line in result.stdout.split("\n"):
                     print(line)
                     if "error:" in line:
                         reported_result.exit_code = 1
+                    if "UMB: error: Only deadlock-free MA, MDP, CTMC, DTMC, and LTS models are supported." in line:
+                        reported_result.not_supported = True
         return reported_result
 
     def check_umb(self, umb_file: pathlib.Path, log_file: pathlib.Path, properties=[]):