Showing
1 changed file
with
213 additions
and
0 deletions
Ex1/Prism/Ex1_a.nm
0 → 100644
1 | +pta | ||
2 | + | ||
3 | +formula fk1S1 = (sF1=1); | ||
4 | +formula fk2S1 = (sS1=3); | ||
5 | +formula fk1S2 = (sF2=1); | ||
6 | +formula fk2S2 = (sS2=3); | ||
7 | +formula fk3S2 = (sF1=1); | ||
8 | +formula fk4S2 = (sS2=5); | ||
9 | +formula fk1S3 = (sF2=1); | ||
10 | +formula fk2S3 = (sS3=3); | ||
11 | +formula fk3S3 = (sB=1) | (sB=5); | ||
12 | +formula fk4S3 = (sS3=5); | ||
13 | +formula fk1F2 = (sB=1) | (sB=3); | ||
14 | +formula fk2F2 = (sF2=4); | ||
15 | +formula flock1 = (sF1=4) | (sB=8) | (sR=1); | ||
16 | +formula flock2 = (sM=1); | ||
17 | +formula funlock1 = (sF1=7) | (sB=11) | (sR=4); | ||
18 | +formula funlock2 = (sM=3); | ||
19 | + | ||
20 | + | ||
21 | + | ||
22 | +module mS1 | ||
23 | + xS1 : clock; | ||
24 | + sS1 : [0..3] init 0; | ||
25 | + | ||
26 | + invariant | ||
27 | + (sS1=0 => xS1 <= 75) & | ||
28 | + (sS1=1 => xS1 <= 100) & | ||
29 | + (sS1=2 => xS1 <= 0) | ||
30 | + endinvariant | ||
31 | + | ||
32 | + [] sS1=0 & xS1 >= 50 -> (sS1'=1) & (xS1'=0); | ||
33 | + [] sS1=1 & xS1 >= 75 -> (sS1'=2) & (xS1'=0); | ||
34 | + [k1S1] sS1=2 -> (sS1'=1) & (xS1'=0); | ||
35 | + [] sS1=2 & !fk1S1 -> (sS1'=3); | ||
36 | + [k2S1] sS1=3 -> (sS1'=1) & (xS1'=0); | ||
37 | +endmodule | ||
38 | + | ||
39 | +module mS2 | ||
40 | + xS2 : clock; | ||
41 | + sS2 : [0..5] init 0; | ||
42 | + | ||
43 | + invariant | ||
44 | + (sS2=0 => xS2 <= 300) & | ||
45 | + (sS2=1 => xS2 <= 400) & | ||
46 | + (sS2=2 => xS2 <= 0) & | ||
47 | + (sS2=4 => xS2 <= 0) | ||
48 | + endinvariant | ||
49 | + | ||
50 | + [] sS2=0 & xS2 >= 200 -> (sS2'=1) & (xS2'=0); | ||
51 | + [] sS2=1 & xS2 >= 350 -> (sS2'=2) & (xS2'=0); | ||
52 | + [k1S2] sS2=2 -> (sS2'=4) & (xS2'=0); | ||
53 | + [] sS2=2 & !fk1S2 -> (sS2'=3); | ||
54 | + [k2S2] sS2=3 -> (sS2'=4) & (xS2'=0); | ||
55 | + [k3S2] sS2=4 -> (sS2'=1) & (xS2'=0); | ||
56 | + [] sS2=4 & !fk3S2 -> (sS2'=5); | ||
57 | + [k4S2] sS2=5 -> (sS2'=1) & (xS2'=0); | ||
58 | +endmodule | ||
59 | + | ||
60 | +module mS3 | ||
61 | + xS3 : clock; | ||
62 | + sS3 : [0..5] init 0; | ||
63 | + | ||
64 | + invariant | ||
65 | + (sS3=0 => xS3 <= 300) & | ||
66 | + (sS3=1 => xS3 <= 400) & | ||
67 | + (sS3=2 => xS3 <= 0) & | ||
68 | + (sS3=4 => xS3 <= 0) | ||
69 | + endinvariant | ||
70 | + | ||
71 | + [] sS3=0 & xS3 >= 200 -> (sS3'=1) & (xS3'=0); | ||
72 | + [] sS3=1 & xS3 >= 350 -> (sS3'=2) & (xS3'=0); | ||
73 | + [k1S3] sS3=2 -> (sS3'=4) & (xS3'=0); | ||
74 | + [] sS3=2 & !fk1S3 -> (sS3'=3); | ||
75 | + [k2S3] sS3=3 -> (sS3'=4) & (xS3'=0); | ||
76 | + [k3S3] sS3=4 -> (sS3'=1) & (xS3'=0); | ||
77 | + [] sS3=4 & !fk3S3 -> (sS3'=5); | ||
78 | + [k4S3] sS3=5 -> (sS3'=1) & (xS3'=0); | ||
79 | +endmodule | ||
80 | + | ||
81 | +module mF1 | ||
82 | + xF1 : clock; | ||
83 | + sF1 : [0..7] init 0; | ||
84 | + | ||
85 | + invariant | ||
86 | + (sF1=0 => xF1<=0) & | ||
87 | + (sF1=2 => xF1<=75) & | ||
88 | + (sF1=3 => xF1<=0) & | ||
89 | + (sF1=5 => xF1<=50) & | ||
90 | + (sF1=6 => xF1<=0) | ||
91 | + endinvariant | ||
92 | + | ||
93 | + [k4S2] sF1=0 -> (sF1'=2) & (xF1'=0); | ||
94 | + [k2S1] sF1=0 -> (sF1'=2) & (xF1'=0); | ||
95 | + [] sF1=0 & !fk4S2 & !fk2S1 -> (sF1'=1); | ||
96 | + [k3S2] sF1=1 -> (sF1'=2) & (xF1'=0); | ||
97 | + [k1S1] sF1=1 -> (sF1'=2) & (xF1'=0); | ||
98 | + [] sF1=2 & xF1 >= 50 -> (sF1'=3) & (xF1'=0); | ||
99 | + [] sF1=3 & !flock2 -> (sF1'=4); | ||
100 | + [lock2F1] sF1=3 -> (sF1'=5) & (xF1'=0); | ||
101 | + [lock1F1] sF1=4 -> (sF1'=5) & (xF1'=0); | ||
102 | + [] sF1=5 & xF1 >= 25 -> (sF1'=6) & (xF1'=0); | ||
103 | + [] sF1=6 & !funlock2 -> (sF1'=7); | ||
104 | + [unlock2F1] sF1=6 -> (sF1'=0) & (xF1'=0); | ||
105 | + [unlock1F1] sF1=7 -> (sF1'=0) & (xF1'=0); | ||
106 | + | ||
107 | +endmodule | ||
108 | + | ||
109 | +module mF2 | ||
110 | + xF2 : clock; | ||
111 | + sF2 : [0..4] init 0; | ||
112 | + | ||
113 | + invariant | ||
114 | + (sF2=0 => xF2<=0) & | ||
115 | + (sF2=2 => xF2<=100) & | ||
116 | + (sF2=3 => xF2<=0) | ||
117 | + endinvariant | ||
118 | + | ||
119 | + [k2S3] sF2=0 -> (sF2'=2) & (xF2'=0); | ||
120 | + [k2S2] sF2=0 -> (sF2'=2) & (xF2'=0); | ||
121 | + [] sF2=0 & !fk2S3 & !fk2S2 -> (sF2'=1); | ||
122 | + [k1S3] sF2=1 -> (sF2'=2) & (xF2'=0); | ||
123 | + [k1S2] sF2=1 -> (sF2'=2) & (xF2'=0); | ||
124 | + [] sF2=2 & xF2 >= 75 -> (sF2'=3) & (xF2'=0); | ||
125 | + [] sF2=3 & !fk1F2 -> (sF2'=4); | ||
126 | + [k1F2] sF2=3 -> (sF2'=0) & (xF2'=0); | ||
127 | + [k2F2] sF2=4 -> (sF2'=0) & (xF2'=0); | ||
128 | + | ||
129 | +endmodule | ||
130 | + | ||
131 | +module mB | ||
132 | + xB : clock; | ||
133 | + sB : [0..11] init 0; | ||
134 | + | ||
135 | + invariant | ||
136 | + (sB=0 => xB<=0) & | ||
137 | + (sB=2 => xB<=0) & | ||
138 | + (sB=4 => xB<=0) & | ||
139 | + (sB=6 => xB<=50) & | ||
140 | + (sB=7 => xB<=0) & | ||
141 | + (sB=9 => xB<=50) & | ||
142 | + (sB=10 => xB<=0) | ||
143 | + endinvariant | ||
144 | + | ||
145 | + [k4S3] sB=0 -> (sB'=2) & (xB'=0); | ||
146 | + [k2F2] sB=0 -> (sB'=4) & (xB'=0); | ||
147 | + [] sB=0 & !fk4S3 & !fk2F2 -> (sB'=1); | ||
148 | + [k3S3] sB=1 -> (sB'=2) & (xB'=0); | ||
149 | + [k1F2] sB=1 -> (sB'=4) & (xB'=0); | ||
150 | + [k2F2] sB=2 -> (sB'=6) & (xB'=0); | ||
151 | + [] sB=2 & !fk2F2 -> (sB'=3); | ||
152 | + [k1F2] sB=3 -> (sB'=6) & (xB'=0); | ||
153 | + [k4S3] sB=4 -> (sB'=6) & (xB'=0); | ||
154 | + [] sB=4 & !fk4S3 -> (sB'=5); | ||
155 | + [k3S3] sB=5 -> (sB'=6) & (xB'=0); | ||
156 | + [] sB=6 & xB >= 25 -> (sB'=7) & (xB'=0); | ||
157 | + [lock2B] sB=7 -> (sB'=9) & (xB'=0); | ||
158 | + [] sB=7 & !flock2 -> (sB'=8); | ||
159 | + [lock1B] sB=8 -> (sB'=9) & (xB'=0); | ||
160 | + [] sB=9 & xB >= 25 -> (sB'=10) & (xB'=0); | ||
161 | + [unlock2B] sB=10 -> (sB'=0) & (xB'=0); | ||
162 | + [] sB=10 & !funlock2 -> (sB'=11); | ||
163 | + [unlock1B] sB=11 -> (sB'=0) & (xB'=0); | ||
164 | + | ||
165 | +endmodule | ||
166 | + | ||
167 | +module mM | ||
168 | + xM : clock; | ||
169 | + sM : [0..3] init 1; | ||
170 | + | ||
171 | + invariant | ||
172 | + (sM=0 => xM<=0) & | ||
173 | + (sM=2 => xM<=0) | ||
174 | + endinvariant | ||
175 | + | ||
176 | + [] sM=0 & !flock1-> (sM'=1); | ||
177 | + [lock1B] sM=0 -> (sM'=2) & (xM'=0); | ||
178 | + [lock1F1] sM=0 -> (sM'=2) & (xM'=0); | ||
179 | + [lock1R] sM=0 -> (sM'=2) & (xM'=0); | ||
180 | + [lock2B] sM=1 -> (sM'=2) & (xM'=0); | ||
181 | + [lock2F1] sM=1 -> (sM'=2) & (xM'=0); | ||
182 | + [lock2R] sM=1 -> (sM'=2) & (xM'=0); | ||
183 | + [] sM=2 & !funlock1 -> (sM'=3); | ||
184 | + [unlock1B] sM=2 -> (sM'=0) & (xM'=0); | ||
185 | + [unlock1F1] sM=2 -> (sM'=0) & (xM'=0); | ||
186 | + [unlock1R] sM=2 -> (sM'=0) & (xM'=0); | ||
187 | + [unlock2B] sM=3 -> (sM'=0) & (xM'=0); | ||
188 | + [unlock2F1] sM=3 -> (sM'=0) & (xM'=0); | ||
189 | + [unlock2R] sM=3 -> (sM'=0) & (xM'=0); | ||
190 | + | ||
191 | +endmodule | ||
192 | + | ||
193 | +module mR | ||
194 | + xR : clock; | ||
195 | + sR : [0..5] init 0; | ||
196 | + | ||
197 | + invariant | ||
198 | + (sR=0 => xR<=0) & | ||
199 | + (sR=2 => xR<=50) & | ||
200 | + (sR=3 => xR<=0) & | ||
201 | + (sR=5 => xR<=100) | ||
202 | + endinvariant | ||
203 | + | ||
204 | + [lock2R] sR=0 -> (sR'=2) & (xR'=0); | ||
205 | + [] sR=0 & !flock2 -> (sR'=1); | ||
206 | + [lock1R] sR=1 -> (sR'=2) & (xR'=0); | ||
207 | + [] sR=2 & xR >= 25 -> (sR'=3) & (xR'=0); | ||
208 | + [unlock2R] sR=3 -> (sR'=5) & (xR'=0); | ||
209 | + [] sR=3 & !funlock2 -> (sR'=4); | ||
210 | + [unlock1R] sR=4 -> (sR'=5) & (xR'=0); | ||
211 | + [] sR=5 & xR >= 75 -> (sR'=0) & (xR'=0); | ||
212 | + | ||
213 | +endmodule | ||
... | \ No newline at end of file | ... | \ No newline at end of file |
-
Please register or login to post a comment