fix: benchmarks script

benchmarks/benchmarks.sh

@@ -4,7 +4,7 @@
 imitator="${HOME}/Work/code/imitator/imitator/bin/imitator"
 
 # maude binary
-maude="maude.darwin64 -no-banner -batch"
+maude="maude.linux64 -no-banner -batch"
 
 # pta2maude parser
 BASE_DIR="$(dirname "$(cd -- "$(dirname "$0")" >/dev/null 2>&1; pwd -P)")"
@@ -19,30 +19,30 @@ modes=("collapsing" "no-collapsing")
 
 # run imitator
 function run_imitator {
-  model=$1
-  property=$2
-  timeout_value=$3
+  local model=$1
+  local property=$2
+  local timeout_value=$3
   timeout $timeout_value $imitator "${model}" "${property}" -output-prefix "${property}"
 }
 
 # run parser pta2maude
 function parser_files {
-  model=$1
-  mode=$2
+  local model=$1
+  local mode=$2
   echo "parsing" $name "with mode" "$mode" "..."
   python3 $parser --input "${model_folder}/${model}.imi" --output "${model_folder}/${model}.${mode}.maude" "--${mode}"
 }
 
 # run Maude
 function run_maude {
-  filename=$1
-  timeout_value=$2
+  local filename=$1
+  local timeout_value=$2
   timeout "$timeout_value" ${maude} "${filename}"
 }
 
 # create a folder
 function create_folder {
-  path=$1
+  local path=$1
 
   if [ ! -d "$path" ]; then
     mkdir -p "$path";
@@ -50,8 +50,8 @@ function create_folder {
 }
 
 function run_benchmark {
-  model=$1
-  timeout=$2
+  local model=$1
+  local timeout=$2
 
   # create folder to save the output of the model
   output_folder="logs/${model}"
@@ -87,6 +87,7 @@ function run_benchmark {
 
       # maude files
       maude_file="${model}.${mode}.maude"
+      echo $maude_file
       new_file="${output_folder}/${maude_file}.${l}"
 
       if [[ ! -f "${new_file}" ]]; then

benchmarks/models/coffee.collapsing.maude

@@ -36,7 +36,7 @@ endm
 
 load meta-pta .
 
-red reachability (<replace>, (< idle ; x:Real ; y:Real > < p1:Real ; p2:Real ; p3:Real > | ( x:Real === y:Real and x:Real >= 0/1 and y:Real >= 0/1 and p1:Real >= 0/1 and p2:Real >= 0/1 and p3:Real >= 0/1 ) )) .
+red reachability (<replace>, ( < idle ; x:Real ; y:Real > < p1:Real ; p2:Real ; p3:Real > | ( x:Real === y:Real and x:Real >= 0/1 and y:Real >= 0/1 and p1:Real >= 0/1 and p2:Real >= 0/1 and p3:Real >= 0/1 ) )) .
 
 quit .
 

benchmarks/models/coffee.no-collapsing.maude

@@ -30,8 +30,8 @@ mod MODEL is
 
 endm
 
-smt-search [1] < idle ; x ; y > < p1 ; p2 ; p3 > =>*
-               < <replace> ; x':Real ; y':Real > < p1 ; p2 ; p3 >
-               such that ( x === y and x >= 0/1 and y >= 0/1 and p1 >= 0/1 and p2 >= 0/1 and p3 >= 0/1 ) = true .
+smt-search [1] < idle ; x ; y > < p1 ; p2 ; p3 > =>* < <replace> ; x':Real ; y':Real > < p1 ; p2 ; p3 > such that ( x === y and x >= 0/1 and y >= 0/1 and p1 >= 0/1 and p2 >= 0/1 and p3 >= 0/1 ) = true .
+
+quit .
 
 eof
\ No newline at end of file