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

feature: add CLI to run benchmarks

parent 7c6e8fa0
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
benchmarks/README.md
+ 7
− 1
View file @ 4b9f7cf7
...@@ -8,10 +8,11 @@ imitator models were borrowed from the ...@@ -8,10 +8,11 @@ imitator models were borrowed from the
``` ```
. .
├── analysis.ipynb # Python notebook to generate the plots ├── analysis.ipynb # Python notebook to generate the plots (analysis.py)
├── benchmarks.sh # Bash script to run the benchmarks ├── benchmarks.sh # Bash script to run the benchmarks
├── images # Folder containing the plots of the benchmark results ├── images # Folder containing the plots of the benchmark results
├── models # Folder containing the models of the benchmark ├── models # Folder containing the models of the benchmark
├── requirements.txt # File containing the python requirements
└── results.csv # CSV file with the benchmarks results └── results.csv # CSV file with the benchmarks results
``` ```
...@@ -20,3 +21,8 @@ imitator models were borrowed from the ...@@ -20,3 +21,8 @@ imitator models were borrowed from the
The script `benchmarks.sh` allows to run the benchmarks for a specific model. The script `benchmarks.sh` allows to run the benchmarks for a specific model.
Before running it, please set the variables `imitator` and `maude` with the Before running it, please set the variables `imitator` and `maude` with the
absolute path of IMITATOR and Maude binaries, respectively. absolute path of IMITATOR and Maude binaries, respectively.
```
λ> ./benchmarks.sh
Usage: ./benchmarks.sh -m MODEL -t TIMEOUT
```
benchmarks/benchmarks.sh
+ 30
− 5
View file @ 4b9f7cf7
...@@ -109,11 +109,36 @@ function run_benchmark { ...@@ -109,11 +109,36 @@ function run_benchmark {
sed -zi 's/^\n//g' ${location_file} sed -zi 's/^\n//g' ${location_file}
} }
# Timeout in seconds (3 minutes) # Print a help message.
timeout="5m" function usage() {
echo "Usage: $0 -m MODEL -t TIMEOUT" 1>&2
}
# Exit with error.
exit_abnormal() {
usage
exit 1
}
# -----------------------------------------------------------------------------
# MAIN
# -----------------------------------------------------------------------------
TIMEOUT=""
MODEL=""
while [[ "$#" -gt 0 ]]; do
case "$1" in
-m|--model) MODEL="$2"; shift ;;
-t|--timeout) TIMEOUT="$2"; shift ;;
*) exit_abnormal ;;
esac
shift
done
# model if [ "$MODEL" = "" ] || [ "$TIMEOUT" = "" ]; then
model="coffee" exit_abnormal
fi
# run benchmark # run benchmark
run_benchmark "${model}" "${timeout}" run_benchmark "${MODEL}" "${TIMEOUT}"
\ No newline at end of file \ No newline at end of file
benchmarks/models/tgc.collapsing.maude
+ 15
− 15
View file @ 4b9f7cf7
...@@ -8,7 +8,7 @@ mod MODEL is ...@@ -8,7 +8,7 @@ mod MODEL is
vars x y z : Real . vars x y z : Real .
vars a b c d e f : Real . vars a b c d e f : Real .
ops Train0Gate0Controller0 Train1Gate0Controller1 Train1Gate1Controller2 Train1Gate2Controller2 Train2Gate2Controller2 Train3Gate2Controller2 Train0Gate2Controller3 Train0Gate3Controller0 Train1Gate3Controller1 Train2Gate3Controller1 Train3Gate3Controller1 Train3Gate0Controller1 Train3Gate1Controller2 Train0Gate1Controller3 Train2Gate0Controller1 Train2Gate1Controller2 : -> Location . ops Train0Gate0Controller0 Train1Gate0Controller1 Train1Gate1Controller2 Train1Gate2Controller2 Train2Gate2Controller2 Train3Gate2Controller2 Train0Gate2Controller3 Train0Gate3Controller0 Train1Gate3Controller1 Train2Gate3Controller1 Train2Gate0Controller1 Train2Gate1Controller2 Train3Gate1Controller2 Train0Gate1Controller3 Train3Gate0Controller1 Train3Gate3Controller1 : -> Location .
op <_;_;_;_> <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> NState . op <_;_;_;_> <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> NState .
op [_;_;_;_] <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> DState . op [_;_;_;_] <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> DState .
...@@ -36,23 +36,25 @@ mod MODEL is ...@@ -36,23 +36,25 @@ mod MODEL is
crl [Train0Gate2Controller3-Train0Gate3Controller0] : < Train0Gate2Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate3Controller0 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true . crl [Train0Gate2Controller3-Train0Gate3Controller0] : < Train0Gate2Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate3Controller0 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
crl [tick-Train0Gate2Controller3] : [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate2Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] . crl [tick-Train0Gate2Controller3] : [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate2Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train0Gate3Controller0-Train0Gate0Controller0] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
rl [Train0Gate3Controller0-Train1Gate3Controller1] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate3Controller1 ; 0/1 ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > . rl [Train0Gate3Controller0-Train1Gate3Controller1] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate3Controller1 ; 0/1 ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > .
crl [Train0Gate3Controller0-Train0Gate0Controller0] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train0Gate3Controller0] : [ Train0Gate3Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate3Controller0 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] . crl [tick-Train0Gate3Controller0] : [ Train0Gate3Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate3Controller0 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train1Gate3Controller1-Train1Gate0Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [Train1Gate3Controller1-Train2Gate3Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true . crl [Train1Gate3Controller1-Train2Gate3Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
crl [Train1Gate3Controller1-Train1Gate0Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train1Gate3Controller1] : [ Train1Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] . crl [tick-Train1Gate3Controller1] : [ Train1Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train2Gate3Controller1-Train2Gate0Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
rl [Train2Gate3Controller1-Train3Gate3Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > . rl [Train2Gate3Controller1-Train3Gate3Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
crl [Train2Gate3Controller1-Train2Gate0Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train2Gate3Controller1] : [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] . crl [tick-Train2Gate3Controller1] : [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train3Gate3Controller1-Train3Gate0Controller1] : < Train3Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true . rl [Train2Gate0Controller1-Train3Gate0Controller1] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
crl [tick-Train3Gate3Controller1] : [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] . crl [Train2Gate0Controller1-Train2Gate1Controller2] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
crl [tick-Train2Gate0Controller1] : [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train3Gate0Controller1-Train3Gate1Controller2] : < Train3Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true . rl [Train2Gate1Controller2-Train3Gate1Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
crl [tick-Train3Gate0Controller1] : [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] . crl [Train2Gate1Controller2-Train2Gate2Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train2Gate1Controller2] : [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train3Gate1Controller2-Train0Gate1Controller3] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate1Controller3 ; x ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > if (x < b) = true . crl [Train3Gate1Controller2-Train0Gate1Controller3] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate1Controller3 ; x ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > if (x < b) = true .
crl [Train3Gate1Controller2-Train3Gate2Controller2] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true . crl [Train3Gate1Controller2-Train3Gate2Controller2] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
...@@ -61,13 +63,11 @@ mod MODEL is ...@@ -61,13 +63,11 @@ mod MODEL is
crl [Train0Gate1Controller3-Train0Gate2Controller3] : < Train0Gate1Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true . crl [Train0Gate1Controller3-Train0Gate2Controller3] : < Train0Gate1Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train0Gate1Controller3] : [ Train0Gate1Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate1Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] . crl [tick-Train0Gate1Controller3] : [ Train0Gate1Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate1Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
rl [Train2Gate0Controller1-Train3Gate0Controller1] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > . crl [Train3Gate0Controller1-Train3Gate1Controller2] : < Train3Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
crl [Train2Gate0Controller1-Train2Gate1Controller2] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true . crl [tick-Train3Gate0Controller1] : [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [tick-Train2Gate0Controller1] : [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train2Gate1Controller2-Train2Gate2Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true . crl [Train3Gate3Controller1-Train3Gate0Controller1] : < Train3Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
rl [Train2Gate1Controller2-Train3Gate1Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > . crl [tick-Train3Gate3Controller1] : [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [tick-Train2Gate1Controller2] : [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
var l : Location . var l : Location .
...@@ -78,7 +78,7 @@ endm ...@@ -78,7 +78,7 @@ endm
load meta-pta . load meta-pta .
red reachability (<replace>, (< Train0Gate0Controller0 ; x:Real ; y:Real ; z:Real > < a:Real ; b:Real ; c:Real ; d:Real ; e:Real ; f:Real > | ( x:Real === y:Real and x:Real === z:Real and x:Real >= 0/1 and y:Real >= 0/1 and z:Real >= 0/1 and a:Real >= 0/1 and b:Real >= 0/1 and c:Real >= 0/1 and d:Real >= 0/1 and e:Real >= 0/1 and f:Real >= 0/1 ) )) . red reachability (<replace>, ( < Train0Gate0Controller0 ; x:Real ; y:Real ; z:Real > < a:Real ; b:Real ; c:Real ; d:Real ; e:Real ; f:Real > | ( x:Real === y:Real and x:Real === z:Real and x:Real >= 0/1 and y:Real >= 0/1 and z:Real >= 0/1 and a:Real >= 0/1 and b:Real >= 0/1 and c:Real >= 0/1 and d:Real >= 0/1 and e:Real >= 0/1 and f:Real >= 0/1 ) )) .
quit . quit .
......
benchmarks/models/tgc.imi.full
+ 3
− 3
View file @ 4b9f7cf7
...@@ -5,7 +5,7 @@ var ...@@ -5,7 +5,7 @@ var
(************************************************************) (************************************************************)
automaton tgc automaton tgc
(************************************************************) (************************************************************)
synclabs: up, inn, exit, raise, approach, down, out, lower; synclabs: inn, up, approach, down, exit, out, lower, raise;
loc Train0Gate0Controller0: invariant True loc Train0Gate0Controller0: invariant True
when True sync approach do {x:=0, z:=0} goto Train1Gate0Controller1; when True sync approach do {x:=0, z:=0} goto Train1Gate0Controller1;
...@@ -35,8 +35,8 @@ accepting loc Train0Gate3Controller0: invariant True ...@@ -35,8 +35,8 @@ accepting loc Train0Gate3Controller0: invariant True
when True sync approach do {x:=0, z:=0} goto Train1Gate3Controller1; when True sync approach do {x:=0, z:=0} goto Train1Gate3Controller1;
accepting loc Train1Gate3Controller1: invariant True accepting loc Train1Gate3Controller1: invariant True
when c<y&y<d sync up do {} goto Train1Gate0Controller1;
when x>a sync inn do {} goto Train2Gate3Controller1; when x>a sync inn do {} goto Train2Gate3Controller1;
when c<y&y<d sync up do {} goto Train1Gate0Controller1;
accepting loc Train2Gate3Controller1: invariant True accepting loc Train2Gate3Controller1: invariant True
when c<y&y<d sync up do {} goto Train2Gate0Controller1; when c<y&y<d sync up do {} goto Train2Gate0Controller1;
...@@ -49,8 +49,8 @@ loc Train3Gate0Controller1: invariant True ...@@ -49,8 +49,8 @@ loc Train3Gate0Controller1: invariant True
when e<z&z<f sync lower do {y:=0} goto Train3Gate1Controller2; when e<z&z<f sync lower do {y:=0} goto Train3Gate1Controller2;
loc Train3Gate1Controller2: invariant True loc Train3Gate1Controller2: invariant True
when x<b sync exit do {z:=0} goto Train0Gate1Controller3;
when c<y&y<d sync down do {} goto Train3Gate2Controller2; when c<y&y<d sync down do {} goto Train3Gate2Controller2;
when x<b sync exit do {z:=0} goto Train0Gate1Controller3;
loc Train0Gate1Controller3: invariant True loc Train0Gate1Controller3: invariant True
when c<y&y<d sync down do {} goto Train0Gate2Controller3; when c<y&y<d sync down do {} goto Train0Gate2Controller3;
......
benchmarks/models/tgc.no-collapsing.maude 0 → 100644
+ 79
− 0
View file @ 4b9f7cf7
load smt .
mod MODEL is
protecting REAL .
sorts State Location .
var T : Real .
vars x y z : Real .
vars a b c d e f : Real .
ops Train0Gate0Controller0 Train1Gate0Controller1 Train1Gate1Controller2 Train1Gate2Controller2 Train2Gate2Controller2 Train3Gate2Controller2 Train0Gate2Controller3 Train0Gate3Controller0 Train1Gate3Controller1 Train2Gate3Controller1 Train3Gate3Controller1 Train3Gate0Controller1 Train3Gate1Controller2 Train0Gate1Controller3 Train2Gate0Controller1 Train2Gate1Controller2 : -> Location .
op <_;_;_;_> <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> State .
op [_;_;_;_] <_;_;_;_;_;_> : Location Real Real Real Real Real Real Real Real Real -> State .
rl [Train0Gate0Controller0-Train1Gate0Controller1] : < Train0Gate0Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; 0/1 ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > .
crl [tick-Train0Gate0Controller0] : [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate0Controller0 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train1Gate0Controller1-Train2Gate0Controller1] : < Train1Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
crl [Train1Gate0Controller1-Train1Gate1Controller2] : < Train1Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
crl [tick-Train1Gate0Controller1] : [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train1Gate1Controller2-Train2Gate1Controller2] : < Train1Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
crl [Train1Gate1Controller2-Train1Gate2Controller2] : < Train1Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train1Gate1Controller2] : [ Train1Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train1Gate2Controller2-Train2Gate2Controller2] : < Train1Gate2Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
crl [tick-Train1Gate2Controller2] : [ Train1Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate2Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
rl [Train2Gate2Controller2-Train3Gate2Controller2] : < Train2Gate2Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
crl [tick-Train2Gate2Controller2] : [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate2Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train3Gate2Controller2-Train0Gate2Controller3] : < Train3Gate2Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate2Controller3 ; x ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > if (x < b) = true .
crl [tick-Train3Gate2Controller2] : [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate2Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train0Gate2Controller3-Train0Gate3Controller0] : < Train0Gate2Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate3Controller0 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
crl [tick-Train0Gate2Controller3] : [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate2Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train0Gate3Controller0-Train0Gate0Controller0] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate0Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
rl [Train0Gate3Controller0-Train1Gate3Controller1] : < Train0Gate3Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate3Controller1 ; 0/1 ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > .
crl [tick-Train0Gate3Controller0] : [ Train0Gate3Controller0 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate3Controller0 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train1Gate3Controller1-Train2Gate3Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (x > a) = true .
crl [Train1Gate3Controller1-Train1Gate0Controller1] : < Train1Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train1Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train1Gate3Controller1] : [ Train1Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train1Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train2Gate3Controller1-Train2Gate0Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
rl [Train2Gate3Controller1-Train3Gate3Controller1] : < Train2Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
crl [tick-Train2Gate3Controller1] : [ Train2Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train3Gate3Controller1-Train3Gate0Controller1] : < Train3Gate3Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train3Gate3Controller1] : [ Train3Gate3Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate3Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train3Gate0Controller1-Train3Gate1Controller2] : < Train3Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
crl [tick-Train3Gate0Controller1] : [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train3Gate1Controller2-Train3Gate2Controller2] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [Train3Gate1Controller2-Train0Gate1Controller3] : < Train3Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate1Controller3 ; x ; y ; 0/1 ] < a ; b ; c ; d ; e ; f > if (x < b) = true .
crl [tick-Train3Gate1Controller2] : [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train3Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train0Gate1Controller3-Train0Gate2Controller3] : < Train0Gate1Controller3 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train0Gate2Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
crl [tick-Train0Gate1Controller3] : [ Train0Gate1Controller3 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train0Gate1Controller3 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
rl [Train2Gate0Controller1-Train3Gate0Controller1] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
crl [Train2Gate0Controller1-Train2Gate1Controller2] : < Train2Gate0Controller1 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate1Controller2 ; x ; 0/1 ; z ] < a ; b ; c ; d ; e ; f > if (e < z and z < f) = true .
crl [tick-Train2Gate0Controller1] : [ Train2Gate0Controller1 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate0Controller1 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
crl [Train2Gate1Controller2-Train2Gate2Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train2Gate2Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > if (c < y and y < d) = true .
rl [Train2Gate1Controller2-Train3Gate1Controller2] : < Train2Gate1Controller2 ; x ; y ; z > < a ; b ; c ; d ; e ; f > => [ Train3Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > .
crl [tick-Train2Gate1Controller2] : [ Train2Gate1Controller2 ; x ; y ; z ] < a ; b ; c ; d ; e ; f > => < Train2Gate1Controller2 ; x + T ; y + T ; z + T > < a ; b ; c ; d ; e ; f > if (T >= 0/1) = true [nonexec] .
endm
smt-search [1] < Train0Gate0Controller0 ; x ; y ; z > < a ; b ; c ; d ; e ; f > =>* < <replace> ; x':Real ; y':Real ; z':Real > < a ; b ; c ; d ; e ; f > such that ( x === y and x === z and x >= 0/1 and y >= 0/1 and z >= 0/1 and a >= 0/1 and b >= 0/1 and c >= 0/1 and d >= 0/1 and e >= 0/1 and f >= 0/1 ) = true .
quit .
eof
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment