Skip to content

Commit 6592482

Browse files
gerasimougerasimou
committed
Merge branch 'newEC'
2 parents 77ca428 + 9ec1a6e commit 6592482

26 files changed

+1971
-3
lines changed

‎libs/runtime-amd64/libdd.dylib

412 KB
Binary file not shown.

‎libs/runtime-amd64/libdv.dylib

40.8 KB
Binary file not shown.

‎libs/runtime-amd64/libjdd.dylib

48.1 KB
Binary file not shown.

‎libs/runtime-amd64/liblpsolve55.dylib

575 KB
Binary file not shown.

‎libs/runtime-amd64/libodd.dylib

34.6 KB
Binary file not shown.

‎libs/runtime-amd64/libprism.dylib

54.5 KB
Binary file not shown.

‎libs/runtime-amd64/libprismhybrid.dylib

192 KB
Binary file not shown.

‎libs/runtime-amd64/libprismmtbdd.dylib

91 KB
Binary file not shown.

‎libs/runtime-amd64/libprismsparse.dylib

261 KB
Binary file not shown.

‎models/MarcRobot/model_10.pctl

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
//objective, max
2+
P=? [ F x=9 & y=9 ]
3+
4+
//objective, min
5+
R{"cost"}=? [ C<=100 ]

‎models/MarcRobot/model_10.prism

+1,174
Large diffs are not rendered by default.

‎models/QASCAD/pal.csl

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
//Objective, max
2+
P=? [ F<=10 (PAL_I0_E1_pc = PAL_I0_E1_R1DeliveredRoomD) | (PAL_F1_E25_pc = PAL_F1_E25_R2DeliveredRoomD)]
3+
4+
//Objective, min
5+
R{"reward_door12_attempt"} =? [C <= 10]

‎models/QASCAD/pal.prism

+156
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,156 @@
1+
// This model is automatically generated from the PRISM model
2+
3+
// All changes made will be lost after regeneration.
4+
5+
// PRISM Output
6+
7+
ctmc
8+
9+
const double p_c_a;
10+
const double p_d_12;
11+
const double p_d_1;
12+
const double p_d_2;
13+
const double p_c_c;
14+
const double p_c_b;
15+
16+
17+
const int INACTIVE = (-1);
18+
const double mean_duration = (0.001);
19+
const int PAL_I0_E1_I0 = (0);
20+
const int PAL_I0_E1_Prepare = (1);
21+
const int PAL_I0_E1_F1 = (2);
22+
const int PAL_I0_E1_R1ToCorA = (3);
23+
const int PAL_I0_E1_R1ToDoorAB = (4);
24+
const int PAL_I0_E1_D1 = (5);
25+
const int PAL_I0_E1_M1 = (6);
26+
const int PAL_I0_E1_M3 = (7);
27+
const int PAL_I0_E1_D2 = (8);
28+
const int PAL_I0_E1_R1ToCorBThrDoor1 = (9);
29+
const int PAL_I0_E1_R1ToCorBThrDoor2 = (10);
30+
const int PAL_I0_E1_D3 = (11);
31+
const int PAL_I0_E1_D4 = (12);
32+
const int PAL_I0_E1_M2 = (13);
33+
const int PAL_I0_E1_R1ToRoomD = (14);
34+
const int PAL_I0_E1_D5 = (15);
35+
const int PAL_I0_E1_R1DeliveredRoomD = (16);
36+
const int PAL_I0_E1_M4 = (17);
37+
const int PAL_I0_E1_R1Stuck = (18);
38+
const int PAL_I0_E1_J1 = (19);
39+
const int PAL_F1_E25_R2ToCorC = (0);
40+
const int PAL_F1_E25_R2ToDoorCD = (1);
41+
const int PAL_F1_E25_D6 = (2);
42+
const int PAL_F1_E25_R2DeliveredRoomD = (3);
43+
const int PAL_F1_E25_R2Stuck = (4);
44+
const int PAL_F1_E25_M5 = (5);
45+
const int PAL_F1_E25_J1 = (6);
46+
const int PAL_F1_E25_AF = (7);
47+
const double r_prep = (0.9998);
48+
const double r1 = (1.0);
49+
const double d_prep = (0.5);
50+
const double d_cor_a = (0.2);
51+
const double d_cor_c = (0.2);
52+
const double d_door_ab = (0.5);
53+
const double d_door_cd = (2.5);
54+
const double d_cor_b_d1 = (0.5);
55+
const double d_cor_b_d2 = (0.5);
56+
const double d_r1_rd = (1.0);
57+
const double d_r1_stuck = (1.0);
58+
const double d_r2_stuck = (1.0);
59+
const double d_r1_delivered = (0.5);
60+
const double d_r2_delivered = (0.5);
61+
const double t = (10.0);
62+
63+
64+
65+
formula PAL_to_be_terminated = (PAL_I0_E1_to_be_terminated)|(PAL_F1_E25_to_be_terminated);
66+
formula PAL_to_be_failed = PAL_I0_E1_to_be_failed;
67+
formula default_rate = ((1.0)/mean_duration);
68+
69+
70+
71+
72+
rewards "reward_door12_attempt"
73+
[PAL_I0_E1_R1ToCorBThrDoor1] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor1)) : r1;
74+
[PAL_I0_E1_R1ToCorBThrDoor2] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor2)) : r1;
75+
endrewards
76+
77+
78+
79+
80+
module PAL_I0_E1
81+
PAL_I0_E1_pc : [-1..19] init 0;
82+
PAL_I0_E1_to_be_terminated : bool init false;
83+
PAL_I0_E1_to_be_failed : bool init false;
84+
PAL_terminated : bool init false;
85+
86+
[PAL_I0_E1_I0] ((PAL_I0_E1_pc=PAL_I0_E1_I0))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_Prepare);
87+
88+
[PAL_I0_E1_Prepare] ((PAL_I0_E1_pc=PAL_I0_E1_Prepare))&(! (PAL_to_be_terminated)) -> (((1.0)/d_prep)*((1.0)-r_prep)):(PAL_I0_E1_pc'=INACTIVE)&(PAL_I0_E1_to_be_failed'=true)&(PAL_I0_E1_to_be_terminated'=true) + (((1.0)/d_prep)*r_prep):(PAL_I0_E1_pc'=PAL_I0_E1_F1);
89+
90+
[PAL_F1] ((PAL_I0_E1_pc=PAL_I0_E1_F1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_R1ToCorA);
91+
92+
[PAL_I0_E1_R1ToCorA] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorA))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_a):(PAL_I0_E1_pc'=PAL_I0_E1_R1ToDoorAB);
93+
94+
[PAL_I0_E1_R1ToDoorAB] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToDoorAB))&(! (PAL_to_be_terminated)) -> ((1.0)/d_door_ab):(PAL_I0_E1_pc'=PAL_I0_E1_D1);
95+
96+
[PAL_I0_E1_D1] ((PAL_I0_E1_pc=PAL_I0_E1_D1))&(! (PAL_to_be_terminated)) -> (default_rate*p_c_a):(PAL_I0_E1_pc'=PAL_I0_E1_M1) + (default_rate*((1.0)-p_c_a)):(PAL_I0_E1_pc'=PAL_I0_E1_M3);
97+
98+
[PAL_I0_E1_M1] ((PAL_I0_E1_pc=PAL_I0_E1_M1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_D2);
99+
100+
[PAL_I0_E1_M3] ((PAL_I0_E1_pc=PAL_I0_E1_M3))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_R1Stuck);
101+
102+
[PAL_I0_E1_D2] ((PAL_I0_E1_pc=PAL_I0_E1_D2))&(! (PAL_to_be_terminated)) -> (default_rate*p_d_12):(PAL_I0_E1_pc'=PAL_I0_E1_R1ToCorBThrDoor1) + (default_rate*((1.0)-p_d_12)):(PAL_I0_E1_pc'=PAL_I0_E1_R1ToCorBThrDoor2);
103+
104+
[PAL_I0_E1_R1ToCorBThrDoor1] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor1))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_b_d1):(PAL_I0_E1_pc'=PAL_I0_E1_D3);
105+
106+
[PAL_I0_E1_R1ToCorBThrDoor2] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor2))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_b_d2):(PAL_I0_E1_pc'=PAL_I0_E1_D4);
107+
108+
[PAL_I0_E1_D3] ((PAL_I0_E1_pc=PAL_I0_E1_D3))&(! (PAL_to_be_terminated)) -> (default_rate*p_d_1):(PAL_I0_E1_pc'=PAL_I0_E1_M2) + (default_rate*((1.0)-p_d_1)):(PAL_I0_E1_pc'=PAL_I0_E1_M1);
109+
110+
[PAL_I0_E1_D4] ((PAL_I0_E1_pc=PAL_I0_E1_D4))&(! (PAL_to_be_terminated)) -> (default_rate*p_d_2):(PAL_I0_E1_pc'=PAL_I0_E1_M2) + (default_rate*((1.0)-p_d_2)):(PAL_I0_E1_pc'=PAL_I0_E1_M1);
111+
112+
[PAL_I0_E1_M2] ((PAL_I0_E1_pc=PAL_I0_E1_M2))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_R1ToRoomD);
113+
114+
[PAL_I0_E1_R1ToRoomD] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToRoomD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r1_rd):(PAL_I0_E1_pc'=PAL_I0_E1_D5);
115+
116+
[PAL_I0_E1_D5] ((PAL_I0_E1_pc=PAL_I0_E1_D5))&(! (PAL_to_be_terminated)) -> (default_rate*p_c_b):(PAL_I0_E1_pc'=PAL_I0_E1_R1DeliveredRoomD) + (default_rate*((1.0)-p_c_b)):(PAL_I0_E1_pc'=PAL_I0_E1_M3);
117+
118+
[PAL_I0_E1_R1DeliveredRoomD] ((PAL_I0_E1_pc=PAL_I0_E1_R1DeliveredRoomD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r1_delivered):(PAL_I0_E1_pc'=PAL_I0_E1_M4);
119+
120+
[PAL_I0_E1_M4] ((PAL_I0_E1_pc=PAL_I0_E1_M4))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_J1);
121+
122+
[PAL_I0_E1_R1Stuck] ((PAL_I0_E1_pc=PAL_I0_E1_R1Stuck))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r1_stuck):(PAL_I0_E1_pc'=PAL_I0_E1_M4);
123+
124+
[PAL_J1] ((PAL_I0_E1_pc=PAL_I0_E1_J1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=INACTIVE);
125+
126+
[PAL_terminate] (PAL_to_be_terminated)&(! (PAL_terminated)) -> default_rate:(PAL_I0_E1_pc'=INACTIVE)&(PAL_terminated'=true);
127+
128+
[] ((PAL_I0_E1_pc=INACTIVE))&((PAL_terminated)&(! (PAL_to_be_terminated))) -> default_rate:true;
129+
130+
endmodule
131+
132+
module PAL_F1_E25
133+
PAL_F1_E25_pc : [-1..7] init INACTIVE;
134+
PAL_F1_E25_to_be_terminated : bool init false;
135+
136+
[PAL_F1] ((PAL_F1_E25_pc=INACTIVE))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_F1_E25_pc'=PAL_F1_E25_R2ToCorC);
137+
138+
[PAL_F1_E25_R2ToCorC] ((PAL_F1_E25_pc=PAL_F1_E25_R2ToCorC))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_c):(PAL_F1_E25_pc'=PAL_F1_E25_R2ToDoorCD);
139+
140+
[PAL_F1_E25_R2ToDoorCD] ((PAL_F1_E25_pc=PAL_F1_E25_R2ToDoorCD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_door_cd):(PAL_F1_E25_pc'=PAL_F1_E25_D6);
141+
142+
[PAL_F1_E25_D6] ((PAL_F1_E25_pc=PAL_F1_E25_D6))&(! (PAL_to_be_terminated)) -> (default_rate*p_c_c):(PAL_F1_E25_pc'=PAL_F1_E25_R2DeliveredRoomD) + (default_rate*((1.0)-p_c_c)):(PAL_F1_E25_pc'=PAL_F1_E25_R2Stuck);
143+
144+
[PAL_F1_E25_R2DeliveredRoomD] ((PAL_F1_E25_pc=PAL_F1_E25_R2DeliveredRoomD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r2_delivered):(PAL_F1_E25_pc'=PAL_F1_E25_M5);
145+
146+
[PAL_F1_E25_R2Stuck] ((PAL_F1_E25_pc=PAL_F1_E25_R2Stuck))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r2_stuck):(PAL_F1_E25_pc'=PAL_F1_E25_M5);
147+
148+
[PAL_F1_E25_M5] ((PAL_F1_E25_pc=PAL_F1_E25_M5))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_F1_E25_pc'=PAL_F1_E25_J1);
149+
150+
[PAL_J1] ((PAL_F1_E25_pc=PAL_F1_E25_J1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_F1_E25_pc'=PAL_F1_E25_AF)&(PAL_F1_E25_to_be_terminated'=true);
151+
152+
[PAL_terminate] PAL_to_be_terminated -> default_rate:(PAL_F1_E25_pc'=INACTIVE)&(PAL_F1_E25_to_be_terminated'=false);
153+
154+
endmodule
155+
156+

‎models/QASCAD/pal.props

+4
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
"either_success": P=? [ F (PAL_I0_E1_pc = PAL_I0_E1_R1DeliveredRoomD) | (PAL_F1_E25_pc = PAL_F1_E25_R2DeliveredRoomD)]
2+
"both_success": P=? [ F<=t (PAL_I0_E1_pc = PAL_I0_E1_R1DeliveredRoomD) & (PAL_F1_E25_pc = PAL_F1_E25_R2DeliveredRoomD)]
3+
"terminate": P=? [ F PAL_F1_E25_pc = PAL_F1_E25_AF ]
4+
"both_stuck": P=? [ F (PAL_I0_E1_pc=PAL_I0_E1_R1Stuck)&(PAL_F1_E25_pc=PAL_F1_E25_R2Stuck) ]

‎models/QASCAD/palEvoChecker.prism

+158
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,158 @@
1+
// This model is automatically generated from the PRISM model
2+
3+
// All changes made will be lost after regeneration.
4+
5+
// PRISM Output
6+
7+
ctmc
8+
9+
10+
evolve param double p_c_a [0..1];
11+
evolve param double p_d_1 [0..1];
12+
evolve param double p_d_2 [0..1];
13+
evolve param double p_c_c [0..1];
14+
evolve param double p_c_b [0..1];
15+
16+
evolve int x [0..1];
17+
18+
const double p_d_12 = 0.5;// [0..1];
19+
20+
21+
const int INACTIVE = (100);
22+
const double mean_duration = (0.001);
23+
const int PAL_I0_E1_I0 = (0);
24+
const int PAL_I0_E1_Prepare = (1);
25+
const int PAL_I0_E1_F1 = (2);
26+
const int PAL_I0_E1_R1ToCorA = (3);
27+
const int PAL_I0_E1_R1ToDoorAB = (4);
28+
const int PAL_I0_E1_D1 = (5);
29+
const int PAL_I0_E1_M1 = (6);
30+
const int PAL_I0_E1_M3 = (7);
31+
const int PAL_I0_E1_D2 = (8);
32+
const int PAL_I0_E1_R1ToCorBThrDoor1 = (9);
33+
const int PAL_I0_E1_R1ToCorBThrDoor2 = (10);
34+
const int PAL_I0_E1_D3 = (11);
35+
const int PAL_I0_E1_D4 = (12);
36+
const int PAL_I0_E1_M2 = (13);
37+
const int PAL_I0_E1_R1ToRoomD = (14);
38+
const int PAL_I0_E1_D5 = (15);
39+
const int PAL_I0_E1_R1DeliveredRoomD = (16);
40+
const int PAL_I0_E1_M4 = (17);
41+
const int PAL_I0_E1_R1Stuck = (18);
42+
const int PAL_I0_E1_J1 = (19);
43+
const int PAL_F1_E25_R2ToCorC = (0);
44+
const int PAL_F1_E25_R2ToDoorCD = (1);
45+
const int PAL_F1_E25_D6 = (2);
46+
const int PAL_F1_E25_R2DeliveredRoomD = (3);
47+
const int PAL_F1_E25_R2Stuck = (4);
48+
const int PAL_F1_E25_M5 = (5);
49+
const int PAL_F1_E25_J1 = (6);
50+
const int PAL_F1_E25_AF = (7);
51+
const double r_prep = (0.9998);
52+
const double r1 = (1.0);
53+
const double d_prep = (0.5);
54+
const double d_cor_a = (0.2);
55+
const double d_cor_c = (0.2);
56+
const double d_door_ab = (0.5);
57+
const double d_door_cd = (2.5);
58+
const double d_cor_b_d1 = (0.5);
59+
const double d_cor_b_d2 = (0.5);
60+
const double d_r1_rd = (1.0);
61+
const double d_r1_stuck = (1.0);
62+
const double d_r2_stuck = (1.0);
63+
const double d_r1_delivered = (0.5);
64+
const double d_r2_delivered = (0.5);
65+
const double t = (10.0);
66+
67+
68+
69+
formula PAL_to_be_terminated = (PAL_I0_E1_to_be_terminated)|(PAL_F1_E25_to_be_terminated);
70+
formula PAL_to_be_failed = PAL_I0_E1_to_be_failed;
71+
formula default_rate = ((1.0)/mean_duration);
72+
73+
74+
75+
76+
rewards "reward_door12_attempt"
77+
[PAL_I0_E1_R1ToCorBThrDoor1] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor1)) : r1;
78+
[PAL_I0_E1_R1ToCorBThrDoor2] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor2)) : r1;
79+
endrewards
80+
81+
82+
83+
84+
module PAL_I0_E1
85+
PAL_I0_E1_pc : [0..INACTIVE] init 0;
86+
PAL_I0_E1_to_be_terminated : bool init false;
87+
PAL_I0_E1_to_be_failed : bool init false;
88+
PAL_terminated : bool init false;
89+
90+
[PAL_I0_E1_I0] ((PAL_I0_E1_pc=PAL_I0_E1_I0))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_Prepare);
91+
92+
[PAL_I0_E1_Prepare] ((PAL_I0_E1_pc=PAL_I0_E1_Prepare))&(! (PAL_to_be_terminated)) -> (((1.0)/d_prep)*((1.0)-r_prep)):(PAL_I0_E1_pc'=INACTIVE)&(PAL_I0_E1_to_be_failed'=true)&(PAL_I0_E1_to_be_terminated'=true) + (((1.0)/d_prep)*r_prep):(PAL_I0_E1_pc'=PAL_I0_E1_F1);
93+
94+
[PAL_F1] ((PAL_I0_E1_pc=PAL_I0_E1_F1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_R1ToCorA);
95+
96+
[PAL_I0_E1_R1ToCorA] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorA))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_a):(PAL_I0_E1_pc'=PAL_I0_E1_R1ToDoorAB);
97+
98+
[PAL_I0_E1_R1ToDoorAB] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToDoorAB))&(! (PAL_to_be_terminated)) -> ((1.0)/d_door_ab):(PAL_I0_E1_pc'=PAL_I0_E1_D1);
99+
100+
[PAL_I0_E1_D1] ((PAL_I0_E1_pc=PAL_I0_E1_D1))&(! (PAL_to_be_terminated)) -> (default_rate*p_c_a):(PAL_I0_E1_pc'=PAL_I0_E1_M1) + (default_rate*((1.0)-p_c_a)):(PAL_I0_E1_pc'=PAL_I0_E1_M3);
101+
102+
[PAL_I0_E1_M1] ((PAL_I0_E1_pc=PAL_I0_E1_M1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_D2);
103+
104+
[PAL_I0_E1_M3] ((PAL_I0_E1_pc=PAL_I0_E1_M3))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_R1Stuck);
105+
106+
[PAL_I0_E1_D2] ((PAL_I0_E1_pc=PAL_I0_E1_D2))&(! (PAL_to_be_terminated)) -> (default_rate*p_d_12):(PAL_I0_E1_pc'=PAL_I0_E1_R1ToCorBThrDoor1) + (default_rate*((1.0)-p_d_12)):(PAL_I0_E1_pc'=PAL_I0_E1_R1ToCorBThrDoor2);
107+
108+
[PAL_I0_E1_R1ToCorBThrDoor1] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor1))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_b_d1):(PAL_I0_E1_pc'=PAL_I0_E1_D3);
109+
110+
[PAL_I0_E1_R1ToCorBThrDoor2] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToCorBThrDoor2))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_b_d2):(PAL_I0_E1_pc'=PAL_I0_E1_D4);
111+
112+
[PAL_I0_E1_D3] ((PAL_I0_E1_pc=PAL_I0_E1_D3))&(! (PAL_to_be_terminated)) -> (default_rate*p_d_1):(PAL_I0_E1_pc'=PAL_I0_E1_M2) + (default_rate*((1.0)-p_d_1)):(PAL_I0_E1_pc'=PAL_I0_E1_M1);
113+
114+
[PAL_I0_E1_D4] ((PAL_I0_E1_pc=PAL_I0_E1_D4))&(! (PAL_to_be_terminated)) -> (default_rate*p_d_2):(PAL_I0_E1_pc'=PAL_I0_E1_M2) + (default_rate*((1.0)-p_d_2)):(PAL_I0_E1_pc'=PAL_I0_E1_M1);
115+
116+
[PAL_I0_E1_M2] ((PAL_I0_E1_pc=PAL_I0_E1_M2))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_R1ToRoomD);
117+
118+
[PAL_I0_E1_R1ToRoomD] ((PAL_I0_E1_pc=PAL_I0_E1_R1ToRoomD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r1_rd):(PAL_I0_E1_pc'=PAL_I0_E1_D5);
119+
120+
[PAL_I0_E1_D5] ((PAL_I0_E1_pc=PAL_I0_E1_D5))&(! (PAL_to_be_terminated)) -> (default_rate*p_c_b):(PAL_I0_E1_pc'=PAL_I0_E1_R1DeliveredRoomD) + (default_rate*((1.0)-p_c_b)):(PAL_I0_E1_pc'=PAL_I0_E1_M3);
121+
122+
[PAL_I0_E1_R1DeliveredRoomD] ((PAL_I0_E1_pc=PAL_I0_E1_R1DeliveredRoomD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r1_delivered):(PAL_I0_E1_pc'=PAL_I0_E1_M4);
123+
124+
[PAL_I0_E1_M4] ((PAL_I0_E1_pc=PAL_I0_E1_M4))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=PAL_I0_E1_J1);
125+
126+
[PAL_I0_E1_R1Stuck] ((PAL_I0_E1_pc=PAL_I0_E1_R1Stuck))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r1_stuck):(PAL_I0_E1_pc'=PAL_I0_E1_M4);
127+
128+
[PAL_J1] ((PAL_I0_E1_pc=PAL_I0_E1_J1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_I0_E1_pc'=INACTIVE);
129+
130+
[PAL_terminate] (PAL_to_be_terminated)&(! (PAL_terminated)) -> default_rate:(PAL_I0_E1_pc'=INACTIVE)&(PAL_terminated'=true);
131+
132+
[] ((PAL_I0_E1_pc=INACTIVE))&((PAL_terminated)&(! (PAL_to_be_terminated))) -> default_rate:true;
133+
134+
endmodule
135+
136+
module PAL_F1_E25
137+
PAL_F1_E25_pc : [0..INACTIVE] init INACTIVE;
138+
PAL_F1_E25_to_be_terminated : bool init false;
139+
140+
[PAL_F1] ((PAL_F1_E25_pc=INACTIVE))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_F1_E25_pc'=PAL_F1_E25_R2ToCorC);
141+
142+
[PAL_F1_E25_R2ToCorC] ((PAL_F1_E25_pc=PAL_F1_E25_R2ToCorC))&(! (PAL_to_be_terminated)) -> ((1.0)/d_cor_c):(PAL_F1_E25_pc'=PAL_F1_E25_R2ToDoorCD);
143+
144+
[PAL_F1_E25_R2ToDoorCD] ((PAL_F1_E25_pc=PAL_F1_E25_R2ToDoorCD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_door_cd):(PAL_F1_E25_pc'=PAL_F1_E25_D6);
145+
146+
[PAL_F1_E25_D6] ((PAL_F1_E25_pc=PAL_F1_E25_D6))&(! (PAL_to_be_terminated)) -> (default_rate*p_c_c):(PAL_F1_E25_pc'=PAL_F1_E25_R2DeliveredRoomD) + (default_rate*((1.0)-p_c_c)):(PAL_F1_E25_pc'=PAL_F1_E25_R2Stuck);
147+
148+
[PAL_F1_E25_R2DeliveredRoomD] ((PAL_F1_E25_pc=PAL_F1_E25_R2DeliveredRoomD))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r2_delivered):(PAL_F1_E25_pc'=PAL_F1_E25_M5);
149+
150+
[PAL_F1_E25_R2Stuck] ((PAL_F1_E25_pc=PAL_F1_E25_R2Stuck))&(! (PAL_to_be_terminated)) -> ((1.0)/d_r2_stuck):(PAL_F1_E25_pc'=PAL_F1_E25_M5);
151+
152+
[PAL_F1_E25_M5] ((PAL_F1_E25_pc=PAL_F1_E25_M5))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_F1_E25_pc'=PAL_F1_E25_J1);
153+
154+
[PAL_J1] ((PAL_F1_E25_pc=PAL_F1_E25_J1))&(! (PAL_to_be_terminated)) -> default_rate:(PAL_F1_E25_pc'=PAL_F1_E25_AF)&(PAL_F1_E25_to_be_terminated'=true);
155+
156+
[PAL_terminate] PAL_to_be_terminated -> default_rate:(PAL_F1_E25_pc'=INACTIVE)&(PAL_F1_E25_to_be_terminated'=false);
157+
158+
endmodule

0 commit comments

Comments
 (0)