-
Notifications
You must be signed in to change notification settings - Fork 0
/
ferryman.smv
43 lines (35 loc) · 1.24 KB
/
ferryman.smv
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
MODULE main
VAR
ferryman : boolean; goat : boolean;
cabbage : boolean; wolf : boolean;
carry : {g, c, w, none};
ASSIGN
init (ferryman) := FALSE; init (goat) := FALSE;
init (cabbage) := FALSE; init (wolf) := FALSE;
init (carry) := none;
next (ferryman) := !ferryman;
next (carry) := case
ferryman = goat : g;
TRUE : none;
esac union
case
ferryman = cabbage : c;
TRUE : none;
esac union
case
ferryman = wolf : w;
TRUE : none;
esac union none;
next (goat) := case
ferryman = goat & next (carry) = g : next (ferryman);
TRUE : goat;
esac;
next (cabbage) := case
ferryman = cabbage & next (carry) = c : next (ferryman);
TRUE : cabbage;
esac;
next (wolf) := case
ferryman = wolf & next (carry) = w : next (ferryman);
TRUE : wolf;
esac;
LTLSPEC !(((goat = cabbage | goat = wolf) -> goat = ferryman) U (cabbage & goat & wolf & ferryman))