fix benchmarks

benchmarks/benchmarks.sh

@@ -32,10 +32,13 @@ function run_imitator {
 function parser_files {
   local model=$1
   local mode=$2
-  [[ $mode = "folding" ]] && options=" --folding" || options=""
 
   echo "parsing" $model "with mode" "$mode" "..."
-  python3 $parser --input "${model_folder}/${model}.imi" --output "${model_folder}/${model}.${mode}.maude${options}"
+  if [[ $mode = "folding" ]]; then
+    python3 $parser --input "${model_folder}/${model}.imi" --output "${model_folder}/${model}.${mode}.maude" --folding
+  else
+    python3 $parser --input "${model_folder}/${model}.imi" --output "${model_folder}/${model}.${mode}.maude"
+  fi
 }
 
 # run Maude
@@ -71,34 +74,34 @@ function run_benchmark {
   # 2) get the locations of the full model
   locations=$(cat ${model_folder}/${model}.imi | grep "loc .*\s*:" | cut -d: -f1 | awk '{ print $NF }')
   agents=$(cat ${model_folder}/${model}.imi | grep "^\s*automaton" | awk '{ print $2; }')
-  echo "agents: " $agents
 
   # imitator files
   prop_file="${model}-EFwitness.imiprop"
   model_path="${model_folder}/${model}.imi"
 
-  a="machine"
-  for l in $locations; do
-    echo "reaching $a @ $l"
-
-    # 3) run imitator
-    new_prop_path="${output_folder}/${prop_file}.${l}"
-    if [[ ! -f "${new_prop_path}.res" ]]; then
-      sed "s/<replace>/loc[${a}] = ${l}/" "${model_folder}/${prop_file}" >"${new_prop_path}"
-      echo "Running (timeout: ${timeout}) ${model} with ${new_prop_path}"
-      run_imitator "${model_path}" "${new_prop_path}" "${timeout}"
-    fi
-
-    # 4) run maude
-    for mode in ${modes[@]}; do
-      maude_file="${model}.${mode}.maude"
-      new_file="${output_folder}/${maude_file}.${l}"
-
-      if [[ ! -f "${new_file}" ]]; then
-        sed "s/<replace>/${a} @ ${l}/" "${model_folder}/${maude_file}" >"${new_file}"
-        echo "Running Maude (timeout: ${timeout}) with ${new_file}"
-        run_maude "${new_file}" "${timeout}" >"${new_file}.res"
+  for a in $agents; do
+    for l in $locations; do
+      echo -e "\nreaching $a @ $l"
+
+      # 3) run imitator
+      new_prop_path="${output_folder}/${prop_file}.${l}"
+      if [[ ! -f "${new_prop_path}.res" ]]; then
+        sed "s/<replace>/loc[${a}] = ${l}/" "${model_folder}/${prop_file}" >"${new_prop_path}"
+        echo "Running (timeout: ${timeout}) ${model} with ${new_prop_path}"
+        run_imitator "${model_path}" "${new_prop_path}" "${timeout}"
       fi
+
+      # 4) run maude
+      for mode in ${modes[@]}; do
+        maude_file="${model}.${mode}.maude"
+        new_file="${output_folder}/${maude_file}.${l}"
+
+        if [[ ! -f "${new_file}" ]]; then
+          sed "s/<replace>/${a} @ ${l}/" "${model_folder}/${maude_file}" >"${new_file}"
+          echo "Running Maude (timeout: ${timeout}) with ${new_file}"
+          run_maude "${new_file}" "${timeout}" >"${new_file}.res"
+        fi
+      done
     done
   done
 

benchmarks/models/coffee.folding.maude

+load analysis .
+
+mod MODEL is
+    extending ANALYSIS .
+
+    ops addsugar cdone idle preparingcoffee : -> Location [ctor] .
+    ops coffee cup press sleep : -> Action [ctor] .
+    op machine : -> Agent [ctor] .
+    ops x y : -> Clock [ctor] .
+    ops p1 p2 p3 : -> Parameter [ctor] .
+
+    op Machine : -> Automaton .
+    eq Machine = < machine |
+                   (@ idle inv true : 
+                      (when true local press do { x := 0 ; y := 0 } goto addsugar)),
+                   (@ addsugar inv (y <= p2) : 
+                      (when (x >= p1) local press do { x := 0 } goto addsugar ,
+                       when (y = p2) local cup do { nothing } goto preparingcoffee)),
+                   (@ preparingcoffee inv (y <= p3) : 
+                      (when (y = p3) local coffee do { x := 0 } goto cdone)),
+                   (@ cdone inv (x <= 10) : 
+                      (when true local press do { x := 0 ; y := 0 } goto addsugar ,
+                       when (x = 10) local sleep do { nothing } goto idle)) >
+                  .
+
+    op init : -> State .
+    eq init = { Machine }
+              < tick: tickOk
+                locs: (machine @ idle)
+                clocks: (x : 0, y : 0)
+                parameters: (p1 : rr(var(p1)), p2 : rr(var(p2)), p3 : rr(var(p3)))
+                dvariables: empty
+                constraint: rr(var(p1)) >= 0 and rr(var(p2)) >= 0 and rr(var(p3)) >= 0
+                n: 1 >
+              .
+endm
+
+red search-folding [ 1 ] in 'MODEL : init => (<replace>) .
+
+quit .
+
+eof
\ No newline at end of file

benchmarks/models/coffee.no-folding.maude

+load analysis .
+
+mod MODEL is
+    extending ANALYSIS .
+
+    ops addsugar cdone idle preparingcoffee : -> Location [ctor] .
+    ops coffee cup press sleep : -> Action [ctor] .
+    op machine : -> Agent [ctor] .
+    ops x y : -> Clock [ctor] .
+    ops p1 p2 p3 : -> Parameter [ctor] .
+
+    op Machine : -> Automaton .
+    eq Machine = < machine |
+                   (@ idle inv true : 
+                      (when true local press do { x := 0 ; y := 0 } goto addsugar)),
+                   (@ addsugar inv (y <= p2) : 
+                      (when (x >= p1) local press do { x := 0 } goto addsugar ,
+                       when (y = p2) local cup do { nothing } goto preparingcoffee)),
+                   (@ preparingcoffee inv (y <= p3) : 
+                      (when (y = p3) local coffee do { x := 0 } goto cdone)),
+                   (@ cdone inv (x <= 10) : 
+                      (when true local press do { x := 0 ; y := 0 } goto addsugar ,
+                       when (x = 10) local sleep do { nothing } goto idle)) >
+                  .
+
+    op init : -> State .
+    eq init = { Machine }
+              < tick: tickOk
+                locs: (machine @ idle)
+                clocks: (x : 0, y : 0)
+                parameters: (p1 : rr(var(p1)), p2 : rr(var(p2)), p3 : rr(var(p3)))
+                dvariables: empty
+                constraint: rr(var(p1)) >= 0 and rr(var(p2)) >= 0 and rr(var(p3)) >= 0
+                n: 1 >
+              .
+endm
+
+red synthesis [ 1 ] in 'MODEL : init => (<replace>) .
+
+quit .
+
+eof
\ No newline at end of file