Showing
1 changed file
with
102 additions
and
0 deletions
Ex3/Prism/Ex3_b.nm
0 → 100644
1 | +pta | ||
2 | + | ||
3 | +formula fk1Ca = (sPr=1) | (sPr=3); | ||
4 | +formula fk2Ca = (sCa=3); | ||
5 | +formula fk1O = (sPr=1); | ||
6 | +formula fk2O = (sO=2); | ||
7 | +formula fk3O = (sF=1); | ||
8 | +formula fk4O = (sO=4); | ||
9 | +formula fk1P = (sF=1); | ||
10 | +formula fk2P = (sP=3); | ||
11 | + | ||
12 | +module mCa | ||
13 | + xCa : clock; | ||
14 | + sCa : [0..3] init 0; | ||
15 | + | ||
16 | + invariant | ||
17 | + (sCa=0 => xCa <= 5000) & | ||
18 | + (sCa=1 => xCa <= 5000) & | ||
19 | + (sCa=2 => xCa <= 0) | ||
20 | + endinvariant | ||
21 | + | ||
22 | + [] sCa=0 & xCa >= 100 -> (sCa'=1) & (xCa'=0); | ||
23 | + [] sCa=1 & xCa >= 100 -> (sCa'=2) & (xCa'=0); | ||
24 | + [k1Ca] sCa=2 -> (sCa'=1) & (xCa'=0); | ||
25 | + [] sCa=2 & !fk1Ca -> (sCa'=3); | ||
26 | + [k2Ca] sCa=3 -> (sCa'=1) & (xCa'=0); | ||
27 | +endmodule | ||
28 | + | ||
29 | +module mO | ||
30 | + xO : clock; | ||
31 | + sO : [0..4] init 0; | ||
32 | + | ||
33 | + invariant | ||
34 | + (sO=1 => xO <= 0) & | ||
35 | + (sO=3 => xO <= 0) | ||
36 | + endinvariant | ||
37 | + | ||
38 | + [] sO=0 & xO >= 100 -> (sO'=1) & (xO'=0); | ||
39 | + [k1O] sO=1 -> (sO'=3) & (xO'=0); | ||
40 | + [] sO=1 & !fk1O -> (sO'=2); | ||
41 | + [k2O] sO=2 -> (sO'=3) & (xO'=0); | ||
42 | + [k3O] sO=3 -> (sO'=0) & (xO'=0); | ||
43 | + [] sO=3 & !fk3O -> (sO'=4); | ||
44 | + [k4O] sO=4 -> (sO'=0) & (xO'=0); | ||
45 | +endmodule | ||
46 | + | ||
47 | +module mP | ||
48 | + xP : clock; | ||
49 | + sP : [0..3] init 0; | ||
50 | + | ||
51 | + invariant | ||
52 | + (sP=0 => xP <= 5000) & | ||
53 | + (sP=1 => xP <= 5000) & | ||
54 | + (sP=2 => xP <= 0) | ||
55 | + endinvariant | ||
56 | + | ||
57 | + [] sP=0 & xP >= 100 -> (sP'=1) & (xP'=0); | ||
58 | + [] sP=1 & xP >= 100 -> (sP'=2) & (xP'=0); | ||
59 | + [k1P] sP=2 -> (sP'=1) & (xP'=0); | ||
60 | + [] sP=2 & !fk1P -> (sP'=3); | ||
61 | + [k2P] sP=3 -> (sP'=1) & (xP'=0); | ||
62 | +endmodule | ||
63 | + | ||
64 | +module mF | ||
65 | + xF : clock; | ||
66 | + sF : [0..2] init 0; | ||
67 | + | ||
68 | + invariant | ||
69 | + (sF=0 => xF<=0) & | ||
70 | + (sF=2 => xF<=5000) | ||
71 | + endinvariant | ||
72 | + | ||
73 | + [k2P] sF=0 -> (sF'=2) & (xF'=0); | ||
74 | + [k4O] sF=0 -> (sF'=2) & (xF'=0); | ||
75 | + [] sF=0 & !fk2P & !fk4O -> (sF'=1); | ||
76 | + [k1P] sF=1 -> (sF'=2) & (xF'=0); | ||
77 | + [k13O] sF=1 -> (sF'=2) & (xF'=0); | ||
78 | + [] sF=2 & xF >= 0 -> (sF'=0) & (xF'=0); | ||
79 | + | ||
80 | +endmodule | ||
81 | + | ||
82 | +module mPr | ||
83 | + xPr : clock; | ||
84 | + sPr : [0..4] init 0; | ||
85 | + | ||
86 | + invariant | ||
87 | + (sPr=0 => xPr<=0) & | ||
88 | + (sPr=2 => xPr<=0) & | ||
89 | + (sPr=4 => xPr<=5000) | ||
90 | + endinvariant | ||
91 | + | ||
92 | + [k2O] sPr=0 -> (sPr'=2) & (xPr'=0); | ||
93 | + [k2Ca] sPr=0 -> (sPr'=4) & (xPr'=0); | ||
94 | + [] sPr=0 & !fk2O & !fk2Ca -> (sPr'=1); | ||
95 | + [k1O] sPr=1 -> (sPr'=2) & (xPr'=0); | ||
96 | + [k1Ca] sPr=1 -> (sPr'=4) & (xPr'=0); | ||
97 | + [k2Ca] sPr=2 -> (sPr'=4) & (xPr'=0); | ||
98 | + [] sPr=2 & !fk2Ca -> (sPr'=3); | ||
99 | + [k1Ca] sPr=3 -> (sPr'=4) & (xPr'=0); | ||
100 | + [] sPr=4 & xPr >= 0 -> (sPr'=0) & (xPr'=0); | ||
101 | + | ||
102 | +endmodule |
-
Please register or login to post a comment