add theory folder

benchmarks/benchmarks.sh

@@ -12,6 +12,7 @@ BASE_DIR="$(dirname "$(
   pwd -P
 )")"
 parser="${BASE_DIR}/nptav2maude/app.py"
+theory_folder="${BASE_DIR}/maude"
 
 # folder containing the folder
 model_folder="models"
@@ -54,14 +55,15 @@ function run_benchmark {
   # create folder to save the output of the model
   output_folder="logs/${model}"
   create_folder "${output_folder}"
-  cp "${model_folder}/*.maude" "${output_folder}"
+  cp ${theory_folder}/*.maude "${output_folder}"
 
-  # 1) generate the full model with parser
+  # 1) generate the maude model with the parser
   parser_files $model
 
   # 2) get the locations of the full model
-  initial_loc=".*"
-  locations=$(cat ${model_folder}/${model}.imi | grep "loc ${initial_loc}\s*:" | cut -d: -f1 | awk '{ print $NF }')
+  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"

benchmarks/models/coffee.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>) .
+red search-folding [ 1 ] in 'MODEL : init => (<replace>) .
+
+quit .
+
+eof
\ No newline at end of file