Fixed two run.py scripts

cmake/MCRL2Version.cmake

@@ -23,7 +23,7 @@
 #
 
 # Package maintainers may set the variable below to issue a new release.
-set(MCRL2_MAJOR_VERSION "202407.1")
+set(MCRL2_MAJOR_VERSION "202407.0")
 string(SUBSTRING ${MCRL2_MAJOR_VERSION} 0 4 MCRL2_COPYRIGHT_YEAR)
 
 option(MCRL2_PACKAGE_RELEASE "Include release version information. This discards Git commit information and only uses the MCRL2_MAJOR_VERSION CMake variable." FALSE)

examples/games/open_field_tic_tac_toe/run.py

@@ -16,12 +16,12 @@
 subprocess.run(['lpsconstelm', '-v', '-t', '-', 'temp.lps'], input=run.stdout, check=True)
 
 
-run = subprocess.run(['lps2pbes', '-fyellow_has_a_winning_strategy.mcf'], stdout=subprocess.PIPE, check=True)
+run = subprocess.run(['lps2pbes', '-fyellow_has_a_winning_strategy.mcf', 'temp.lps'], stdout=subprocess.PIPE, check=True)
 run = subprocess.run(['pbesconstelm', '-v'], input=run.stdout, stdout=subprocess.PIPE, check=True)
 run = subprocess.run(['pbesparelm', '-v'], input=run.stdout, stdout=subprocess.PIPE, check=True)
 subprocess.run(['pbesrewr', '-pquantifier-all', '-', 'temp_yellow.pbes'], input=run.stdout, check=True)
 
-run = subprocess.run(['lps2pbes', '-fred_has_a_winning_strategy.mcf'], stdout=subprocess.PIPE, check=True)
+run = subprocess.run(['lps2pbes', '-fred_has_a_winning_strategy.mcf', 'temp.lps'], stdout=subprocess.PIPE, check=True)
 run = subprocess.run(['pbesconstelm', '-v'], input=run.stdout, stdout=subprocess.PIPE, check=True)
 run = subprocess.run(['pbesparelm', '-v'], input=run.stdout, stdout=subprocess.PIPE, check=True)
 subprocess.run(['pbesrewr', '-pquantifier-all', '-', 'temp_red.pbes'], input=run.stdout, check=True)

examples/probabilistic/spinning_mule_woolhouse/run.py

@@ -3,6 +3,7 @@
 import subprocess
 import os
 
+from shutil import which
 from sys import argv
 
 # Change working dir to the script path
@@ -19,24 +20,29 @@
 else:
     print('-rjittyc is required to generate the state spaces for checking probabilistic bisimulation')
 
-print('Checking minimal_walking_distance.mcf for spinning_mule_optimised.mcrl2')
-run = subprocess.run(['lps2pres', '-fminimal_walking_distance.mcf', 'spinning_mule_optimized.lps'], stdout=subprocess.PIPE, check=True)
-run = subprocess.run(['presrewr', '-pquantifier-inside'], input=run.stdout, stdout=subprocess.PIPE, check=True)
-run = subprocess.run(['presrewr', '-pquantifier-one-point'], input=run.stdout, stdout=subprocess.PIPE, check=True)
-subprocess.run(['presrewr', '-pquantifier-all', '-', 'spinning_mule_optimized.pres'], input=run.stdout, check=True)
+lps2pres = which('lps2pres')
+pressolve = which('pressolve')
+presrewr = which('presrewr')
 
-subprocess.run(['pressolve', '-v', '-am', 'spinning_mule_optimized.pres', '-p30', '--timings'], check=True)
+if lps2pres and presrewr and pressolve:
+    print('Checking minimal_walking_distance.mcf for spinning_mule_optimised.mcrl2')
+    run = subprocess.run([lps2pres, '-fminimal_walking_distance.mcf', 'spinning_mule_optimized.lps'], stdout=subprocess.PIPE, check=True)
+    run = subprocess.run([presrewr, '-pquantifier-inside'], input=run.stdout, stdout=subprocess.PIPE, check=True)
+    run = subprocess.run([presrewr, '-pquantifier-one-point'], input=run.stdout, stdout=subprocess.PIPE, check=True)
+    subprocess.run([presrewr, '-pquantifier-all', '-', 'spinning_mule_optimized.pres'], input=run.stdout, check=True)
 
-print('Checking minimal_walking_distance.mcf for spinning_mule.mcrl2')
-run = subprocess.run(['lps2pres', '-fminimal_walking_distance.mcf', 'spinning_mule.lps'], stdout=subprocess.PIPE, check=True)
-run = subprocess.run(['presrewr', '-pquantifier-inside'], input=run.stdout, stdout=subprocess.PIPE, check=True)
-run = subprocess.run(['presrewr', '-pquantifier-one-point'], input=run.stdout, stdout=subprocess.PIPE, check=True)
-subprocess.run(['presrewr', '-pquantifier-all', '-', 'spinning_mule.pres'], input=run.stdout, check=True)
+    subprocess.run([pressolve, '-v', '-am', 'spinning_mule_optimized.pres', '-p30', '--timings'], check=True)
 
-subprocess.run(['pressolve', '-v', '-am', 'spinning_mule.pres', '-p30', '--timings'], check=True)
+    print('Checking minimal_walking_distance.mcf for spinning_mule.mcrl2')
+    run = subprocess.run([lps2pres, '-fminimal_walking_distance.mcf', 'spinning_mule.lps'], stdout=subprocess.PIPE, check=True)
+    run = subprocess.run([presrewr, '-pquantifier-inside'], input=run.stdout, stdout=subprocess.PIPE, check=True)
+    run = subprocess.run([presrewr, '-pquantifier-one-point'], input=run.stdout, stdout=subprocess.PIPE, check=True)
+    subprocess.run([presrewr, '-pquantifier-all', '-', 'spinning_mule.pres'], input=run.stdout, check=True)
 
-print('Checking minimal_walking_distance.mcf for spinning_mule_woolhouse.mcrl2')
-subprocess.run(['mcrl22lps', 'spinning_mule_woolhouse.mcrl2', '-v', 'spinning_mule_woolhouse.lps'], check=True)
-subprocess.run(['lps2pres', '-fminimal_walking_distance.mcf', 'spinning_mule_woolhouse.lps', '-v', 'spinning_mule_woolhouse.pres'], check=True)
-subprocess.run(['presrewr', '-pquantifier-one-point', 'spinning_mule_woolhouse.pres', 'spinning_mule_woolhouse1.pres'], check=True)
-subprocess.run(['pressolve', '-v', '-rjitty', '-am', 'spinning_mule_woolhouse1.pres', '-p30'], check=True)
+    subprocess.run([pressolve, '-v', '-am', 'spinning_mule.pres', '-p30', '--timings'], check=True)
+
+    print('Checking minimal_walking_distance.mcf for spinning_mule_woolhouse.mcrl2')
+    subprocess.run(['mcrl22lps', 'spinning_mule_woolhouse.mcrl2', '-v', 'spinning_mule_woolhouse.lps'], check=True)
+    subprocess.run([lps2pres, '-fminimal_walking_distance.mcf', 'spinning_mule_woolhouse.lps', '-v', 'spinning_mule_woolhouse.pres'], check=True)
+    subprocess.run([presrewr, '-pquantifier-one-point', 'spinning_mule_woolhouse.pres', 'spinning_mule_woolhouse1.pres'], check=True)
+    subprocess.run([pressolve, '-v', '-rjitty', '-am', 'spinning_mule_woolhouse1.pres', '-p30'], check=True)