Showing
1 changed file
with
202 additions
and
0 deletions
Ex2/Prism/Ex2_modif_untimed.nm
0 → 100644
1 | +pta | ||
2 | + | ||
3 | +formula fk1Ca = (sU=1); | ||
4 | +formula fk2Ca = (sCa=3); | ||
5 | +formula fk1I = (sF=1) | (sF=8); | ||
6 | +formula fk2I = (sI=3); | ||
7 | +formula fk1F = (sL=1) | (sL=3); | ||
8 | +formula fk2F = (sF=6) | (sF=11); | ||
9 | +formula fk1U = (sL=1); | ||
10 | +formula fk2U = (sU=9); | ||
11 | +formula fk1L = (sF=1) | (sF=3); | ||
12 | +formula fk2L = (sL=11); | ||
13 | +formula flock1 = (sU=4) | (sL=6) | (sG=1); | ||
14 | +formula flock2 = (sM=1); | ||
15 | +formula funlock1 = (sU=7) | (sL=9) | (sG=4); | ||
16 | +formula funlock2 = (sM=3); | ||
17 | + | ||
18 | + | ||
19 | + | ||
20 | +module mCa | ||
21 | + xCa : clock; | ||
22 | + sCa : [0..3] init 0; | ||
23 | + | ||
24 | + invariant | ||
25 | + (sCa=0 => xCa <= 0) & | ||
26 | + (sCa=1 => xCa <= 0) & | ||
27 | + (sCa=2 => xCa <= 0) | ||
28 | + endinvariant | ||
29 | + | ||
30 | + [] sCa=0 & xCa >= 0 -> (sCa'=1) & (xCa'=0); | ||
31 | + [] sCa=1 & xCa >= 0 -> (sCa'=2) & (xCa'=0); | ||
32 | + [k1Ca] sCa=2 -> (sCa'=1) & (xCa'=0); | ||
33 | + [] sCa=2 & !fk1Ca -> (sCa'=3); | ||
34 | + [k2Ca] sCa=3 -> (sCa'=1) & (xCa'=0); | ||
35 | +endmodule | ||
36 | + | ||
37 | +module mI | ||
38 | + xI : clock; | ||
39 | + sI : [0..3] init 0; | ||
40 | + | ||
41 | + invariant | ||
42 | + (sI=0 => xI <= 0) & | ||
43 | + (sI=1 => xI <= 0) & | ||
44 | + (sI=2 => xI <= 0) | ||
45 | + endinvariant | ||
46 | + | ||
47 | + [] sI=0 & xI >= 0 -> (sI'=1) & (xI'=0); | ||
48 | + [] sI=1 & xI >= 0 -> (sI'=2) & (xI'=0); | ||
49 | + [k1I] sI=2 -> (sI'=1) & (xI'=0); | ||
50 | + [] sI=2 & !fk1I -> (sI'=3); | ||
51 | + [k2I] sI=3 -> (sI'=1) & (xI'=0); | ||
52 | +endmodule | ||
53 | + | ||
54 | +module mU | ||
55 | + xU : clock; | ||
56 | + sU : [0..9] init 0; | ||
57 | + | ||
58 | + invariant | ||
59 | + (sU=0 => xU<=0) & | ||
60 | + (sU=2 => xU<=0) & | ||
61 | + (sU=3 => xU<=0) & | ||
62 | + (sU=5 => xU<=0) & | ||
63 | + (sU=6 => xU<=0) & | ||
64 | + (sU=8 => xU<=0) | ||
65 | + endinvariant | ||
66 | + | ||
67 | + [k2Ca] sU=0 -> (sU'=2) & (xU'=0); | ||
68 | + [] sU=0 & !fk2Ca -> (sU'=1); | ||
69 | + [k1Ca] sU=1 -> (sU'=2) & (xU'=0); | ||
70 | + [] sU=2 & xU >= 0 -> (sU'=3) & (xU'=0); | ||
71 | + [] sU=3 & !flock2 -> (sU'=4); | ||
72 | + [lock2U] sU=3 -> (sU'=5) & (xU'=0); | ||
73 | + [lock1U] sU=4 -> (sU'=5) & (xU'=0); | ||
74 | + [] sU=5 & xU >= 0 -> (sU'=6) & (xU'=0); | ||
75 | + [] sU=6 & !funlock2 -> (sU'=7); | ||
76 | + [unlock2U] sU=6 -> (sU'=8) & (xU'=0); | ||
77 | + [unlock1U] sU=7 -> (sU'=8) & (xU'=0); | ||
78 | + [k1U] sU=8 -> (sU'=0) & (xU'=0); | ||
79 | + [] sU=8 & !fk1U -> (sU'=9); | ||
80 | + [k2U] sU=9 -> (sU'=0) & (xU'=8); | ||
81 | + | ||
82 | + | ||
83 | +endmodule | ||
84 | + | ||
85 | +module mF | ||
86 | + xF : clock; | ||
87 | + sF : [0..11] init 7; | ||
88 | + | ||
89 | + invariant | ||
90 | + (sF=0 => xF<=0) & | ||
91 | + (sF=2 => xF<=0) & | ||
92 | + (sF=4 => xF<=0) & | ||
93 | + (sF=5 => xF<=0) & | ||
94 | + (sF=7 => xF<=0) & | ||
95 | + (sF=9 => xF<=0) & | ||
96 | + (sF=10 => xF<=0) | ||
97 | + endinvariant | ||
98 | + | ||
99 | + [k2I] sF=0 -> (sF'=2) & (xF'=0); | ||
100 | + [k2L] sF=0 -> (sF'=4) & (xF'=0); | ||
101 | + [] sF=0 & !fk2I & !fk2L -> (sF'=1); | ||
102 | + [k1I] sF=1 -> (sF'=2) & (xF'=0); | ||
103 | + [k1L] sF=1 -> (sF'=4) & (xF'=0); | ||
104 | + [k2L] sF=2 -> (sF'=4) & (xF'=0); | ||
105 | + [] sF=2 & !fk2L -> (sF'=3); | ||
106 | + [k1L] sF=3 -> (sF'=4) & (xF'=0); | ||
107 | + [] sF=4 & xF >= 0 -> (sF'=5) & (xF'=0); | ||
108 | + [] sF=5 & !fk1F -> (sF'=6); | ||
109 | + [k1F] sF=5 -> (sF'=0) & (xF'=0); | ||
110 | + [k2F] sF=6 -> (sF'=0) & (xF'=0); | ||
111 | + [k2I] sF=7 -> (sF'=9) & (xF'=0); | ||
112 | + [] sF=7 & !fk2I -> (sF'=8); | ||
113 | + [k1I] sF=8 -> (sF'=9) & (xF'=0); | ||
114 | + [] sF=9 & xF >= 0 -> (sF'=10) & (xF'=0); | ||
115 | + [] sF=10 & !fk1F -> (sF'=11); | ||
116 | + [k1F] sF=10 -> (sF'=0) & (xF'=0); | ||
117 | + [k2F] sF=11 -> (sF'=0) & (xF'=0); | ||
118 | +endmodule | ||
119 | + | ||
120 | +module mL | ||
121 | + xL : clock; | ||
122 | + sL : [0..11] init 0; | ||
123 | + | ||
124 | + invariant | ||
125 | + (sL=0 => xL<=0) & | ||
126 | + (sL=2 => xL<=0) & | ||
127 | + (sL=4 => xL<=0) & | ||
128 | + (sL=5 => xL<=0) & | ||
129 | + (sL=7 => xL<=0) & | ||
130 | + (sL=8 => xL<=0) & | ||
131 | + (sL=10 => xL<=0) | ||
132 | + endinvariant | ||
133 | + | ||
134 | + [k2U] sL=0 -> (sL'=2) & (xL'=0); | ||
135 | + [k2F] sL=0 -> (sL'=4) & (xL'=0); | ||
136 | + [] sL=0 & !fk2U & !fk2F -> (sL'=1); | ||
137 | + [k1U] sL=1 -> (sL'=2) & (xL'=0); | ||
138 | + [k1F] sL=1 -> (sL'=4) & (xL'=0); | ||
139 | + [k2F] sL=2 -> (sL'=4) & (xL'=0); | ||
140 | + [] sL=2 & !fk2F -> (sL'=3); | ||
141 | + [k1F] sL=3 -> (sL'=4) & (xL'=0); | ||
142 | + [] sL=4 & xL >= 0 -> (sL'=5) & (xL'=0); | ||
143 | + [] sL=5 & !flock2 -> (sL'=6); | ||
144 | + [lock2L] sL=5 -> (sL'=7) & (xL'=0); | ||
145 | + [lock1L] sL=6 -> (sL'=7) & (xL'=0); | ||
146 | + [] sL=7 & xL >= 0 -> (sL'=8) & (xL'=0); | ||
147 | + [] sL=8 & !funlock2 -> (sL'=9); | ||
148 | + [unlock2L] sL=8 -> (sL'=10) & (xL'=0); | ||
149 | + [unlock1L] sL=9 -> (sL'=10) & (xL'=0); | ||
150 | + [k1L] sL=10 -> (sL'=0) & (xL'=0); | ||
151 | + [] sL=10 & !fk1L -> (sL'=11); | ||
152 | + [k2L] sL=11 -> (sL'=0) & (xL'=8); | ||
153 | + | ||
154 | +endmodule | ||
155 | + | ||
156 | +module mM | ||
157 | + xM : clock; | ||
158 | + sM : [0..3] init 1; | ||
159 | + | ||
160 | + invariant | ||
161 | + (sM=0 => xM<=0) & | ||
162 | + (sM=2 => xM<=0) | ||
163 | + endinvariant | ||
164 | + | ||
165 | + [] sM=0 & !flock1-> (sM'=1); | ||
166 | + [lock1L] sM=0 -> (sM'=2) & (xM'=0); | ||
167 | + [lock1U] sM=0 -> (sM'=2) & (xM'=0); | ||
168 | + [lock1G] sM=0 -> (sM'=2) & (xM'=0); | ||
169 | + [lock2L] sM=1 -> (sM'=2) & (xM'=0); | ||
170 | + [lock2U] sM=1 -> (sM'=2) & (xM'=0); | ||
171 | + [lock2G] sM=1 -> (sM'=2) & (xM'=0); | ||
172 | + [] sM=2 & !funlock1 -> (sM'=3); | ||
173 | + [unlock1L] sM=2 -> (sM'=0) & (xM'=0); | ||
174 | + [unlock1U] sM=2 -> (sM'=0) & (xM'=0); | ||
175 | + [unlock1G] sM=2 -> (sM'=0) & (xM'=0); | ||
176 | + [unlock2L] sM=3 -> (sM'=0) & (xM'=0); | ||
177 | + [unlock2U] sM=3 -> (sM'=0) & (xM'=0); | ||
178 | + [unlock2G] sM=3 -> (sM'=0) & (xM'=0); | ||
179 | + | ||
180 | +endmodule | ||
181 | + | ||
182 | +module mG | ||
183 | + xG : clock; | ||
184 | + sG : [0..5] init 0; | ||
185 | + | ||
186 | + invariant | ||
187 | + (sG=0 => xG<=0) & | ||
188 | + (sG=2 => xG<=0) & | ||
189 | + (sG=3 => xG<=0) & | ||
190 | + (sG=5 => xG<=0) | ||
191 | + endinvariant | ||
192 | + | ||
193 | + [lock2G] sG=0 -> (sG'=2) & (xG'=0); | ||
194 | + [] sG=0 & !flock2 -> (sG'=1); | ||
195 | + [lock1G] sG=1 -> (sG'=2) & (xG'=0); | ||
196 | + [] sG=2 & xG >= 0 -> (sG'=3) & (xG'=0); | ||
197 | + [unlock2G] sG=3 -> (sG'=5) & (xG'=0); | ||
198 | + [] sG=3 & !funlock2 -> (sG'=4); | ||
199 | + [unlock1G] sG=4 -> (sG'=5) & (xG'=0); | ||
200 | + [] sG=5 & xG >= 0 -> (sG'=0) & (xG'=0); | ||
201 | + | ||
202 | +endmodule |
-
Please register or login to post a comment