forked from cubicle-model-checker/cubicle
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathgerman_subtype.cub
103 lines (82 loc) · 3.1 KB
/
german_subtype.cub
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
type state = Invalid | Shared | Exclusive
(*type msg = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte*)
type msg1 = Empty1 | Reqs | Reqe
type msg2 = Empty2 | Inv | Gnts | Gnte
type msg3 = Empty3 | Invack
var Exgntd : bool
var Curcmd : msg1
var Curptr : proc
array Chan1[proc] : msg1
array Chan2[proc] : msg2
array Chan3[proc] : msg3
array Cache[proc] : state
array Invset[proc] : bool
array Shrset[proc] : bool
init (z) {
Chan1[z] = Empty1 &&
Chan2[z] = Empty2 &&
Chan3[z] = Empty3 &&
Cache[z] = Invalid &&
Invset[z] = False &&
Shrset[z] = False &&
Curcmd = Empty1 &&
Exgntd = False }
unsafe (z1 z2) { Cache[z1] = Exclusive && Cache[z2] = Shared }
(*unsafe (z1 z2) { Cache[z1] = Exclusive && Cache[z2] = Exclusive }*)
transition send_req_shared(n)
require { Cache[n] = Invalid && Chan1[n] = Empty1 }
Chan1[j] := {| j = n : Reqs | _ : Chan1[j] }
transition send_req_exclusive_1(n)
require { Cache[n] = Invalid && Chan1[n] = Empty1 }
Chan1[j] := {| j = n : Reqe | _ : Chan1[j] }
transition send_req_exclusive(n)
require { Cache[n] = Shared && Chan1[n] = Empty1 }
Chan1[j] := {| j = n : Reqe | _ : Chan1[j] }
transition recv_req_shared(n)
require { Curcmd = Empty1 && Chan1[n] = Reqs }
assign { Curcmd := Reqs; Curptr := n; Invset := Shrset }
Chan1[j] := {| j = n: Empty1 | _ : Chan1[j] }
transition recv_req_exclusive(n)
require { Curcmd = Empty1 && Chan1[n] = Reqe }
assign { Curcmd := Reqe; Curptr := n; Invset := Shrset }
Chan1[j] := {| j = n : Empty1 | _ : Chan1[j] }
transition send_inv_1(n)
require { Chan2[n] = Empty2 && Invset[n] = True && Curcmd = Reqe }
Chan2[j] := {| j = n : Inv | _ : Chan2[j] }
Invset[j] := {| j = n : False | _ : Invset[j] }
transition send_inv_2(n)
require { Chan2[n] = Empty2 && Invset[n] = True &&
Curcmd = Reqs && Exgntd = True}
Chan2[j] := {| j = n : Inv | _ : Chan2[j] }
Invset[j] := {| j = n : False | _ : Invset[j] }
transition send_invack(n)
require { Chan2[n] = Inv && Chan3[n] = Empty3 }
Chan2[j] := {| j = n : Empty2 | _ : Chan2[j] }
Chan3[j] := {| j = n : Invack | _ : Chan3[j] }
Cache[j] := {| j = n : Invalid | _ : Cache[j] }
transition recv_invack(n)
require { Chan3[n] = Invack && Curcmd <> Empty1 }
assign { Exgntd := False }
Chan3[j] := {| j = n : Empty3 | _ : Chan3[j] }
Shrset[j] := {| j = n : False | _ : Shrset[j] }
transition send_gnt_shared(n)
require { Curptr = n && Curcmd = Reqs &&
Exgntd = False && Chan2[n] = Empty2 }
assign { Curcmd := Empty1 }
Chan2[j] := {| j = n : Gnts | _ : Chan2[j] }
Shrset[j] := {| j = n : True | _ : Shrset[j] }
transition send_gnt_exclusive(n)
require { Curptr = n && Curcmd = Reqe &&
Chan2[n] = Empty2 && Shrset[n] = False }
uguard (j) { Shrset[j] = False }
assign { Curcmd := Empty1; Exgntd := True }
Chan2[j] := {| j = n : Gnte | _ : Chan2[j] }
Shrset[j] := {| j = n : True | _ : Shrset[j] }
transition recv_gnt_shared(n)
require {Chan2[n] = Gnts}
Cache[j] := {| j = n : Shared | _ : Cache[j] }
Chan2[j] := {| j = n : Empty2 | _ : Chan2[j] }
transition recv_gnt_exclusive(n)
require { Chan2[n] = Gnte }
Cache[j] := {| j = n : Exclusive | _ : Cache[j] }
Chan2[j] := {| j = n : Empty2 | _ : Chan2[j] }