Skip to content
Snippets Groups Projects
Commit c7da6ced authored by Jaime Arias's avatar Jaime Arias
Browse files

add folding and no-folding modes

parent 5ebb78e5
No related branches found
No related tags found
No related merge requests found
......@@ -17,6 +17,9 @@ theory_folder="${BASE_DIR}/maude"
# folder containing the folder
model_folder="models"
# modes
modes=("folding" "no-folding")
# run imitator
function run_imitator {
local model=$1
......@@ -28,8 +31,11 @@ function run_imitator {
# run parser pta2maude
function parser_files {
local model=$1
echo "parsing" $model "..."
python3 $parser --input "${model_folder}/${model}.imi" --output "${model_folder}/${model}.maude"
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}"
}
# run Maude
......@@ -58,7 +64,9 @@ function run_benchmark {
cp ${theory_folder}/*.maude "${output_folder}"
# 1) generate the maude model with the parser
parser_files $model
for mode in ${modes[@]}; do
parser_files $model "$mode"
done
# 2) get the locations of the full model
locations=$(cat ${model_folder}/${model}.imi | grep "loc .*\s*:" | cut -d: -f1 | awk '{ print $NF }')
......@@ -71,7 +79,7 @@ function run_benchmark {
a="machine"
for l in $locations; do
echo "\nreaching $a @ $l"
echo "reaching $a @ $l"
# 3) run imitator
new_prop_path="${output_folder}/${prop_file}.${l}"
......@@ -82,14 +90,16 @@ function run_benchmark {
fi
# 4) run maude
maude_file="${model}.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
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
# 5) generate file with locations where maude finishes
......
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment