spectra-tutorial/L3_patterns_solution/GridL3.spectra at main · jringert/spectra-tutorial · GitHub

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
import "DwyerPatterns.spectra"

spec GridL3

define upper:=20;

type Coord = Int(0..upper);
env Coord[2] rob;

sys {UP, DOWN, LEFT, RIGHT, STAY} move;

define p1 := rob[0]=0 & rob[1]=0;
define p2 := rob[0]=0 & rob[1]=upper;
define p3 := rob[0]=upper & rob[1]=0;

asm ini p1;
asm alw move=UP implies minusOne(rob[1]) & fix(rob[0]);
asm alw move=DOWN implies plusOne(rob[1]) & fix(rob[0]);
asm alw move=LEFT implies minusOne(rob[0]) & fix(rob[1]);
asm alw move=RIGHT implies plusOne(rob[0]) & fix(rob[1]);

predicate plusOne (Coord c):
 c + 1 = next (c) | (c = upper & next(c)=c);
predicate minusOne (Coord c):
 c -1 = next (c) | (c = 0 & next(c)=c);
predicate fix (Coord c):
 next(c)=c;


gar alwEv p2;
gar alwEv p3;

gar P_becomes_true_between_Q_and_R(p1, p2, p3);