-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathmodel.prism
More file actions
26 lines (25 loc) · 1.27 KB
/
Copy pathmodel.prism
File metadata and controls
26 lines (25 loc) · 1.27 KB
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
ctmc
const double diskfr = 0.05;
const double dcfr = 0.0001;
const double diskrr;
const double dcrr;
module SE1A1
ss17_20: [0..4] init 4;
ss3_4: [0..2] init 2;
[fail1] (ss3_4=2 & ss17_20=4) -> 20*diskfr:(ss17_20'=3) + 4*dcfr:(ss3_4'=1);
[fail2] (ss3_4=2 & ss17_20=3) -> 19*diskfr:(ss17_20'=2) + 4*dcfr:(ss3_4'=1);
[fail3] (ss3_4=2 & ss17_20=2) -> 18*diskfr:(ss17_20'=1) + 4*dcfr:(ss3_4'=1);
[fail4] (ss3_4=2 & ss17_20=1) -> 17*diskfr:(ss17_20'=0) + 4*dcfr:(ss3_4'=1);
[fail5] (ss3_4=1 & ss17_20=4) -> 20*diskfr:(ss17_20'=3) + 3*dcfr:(ss3_4'=0);
[fail6] (ss3_4=1 & ss17_20=3) -> 19*diskfr:(ss17_20'=2) + 3*dcfr:(ss3_4'=0);
[fail7] (ss3_4=1 & ss17_20=2) -> 18*diskfr:(ss17_20'=1) + 3*dcfr:(ss3_4'=0);
[fail8] (ss3_4=1 & ss17_20=1) -> 17*diskfr:(ss17_20'=0) + 3*dcfr:(ss3_4'=0);
[fail9] (ss3_4>0 & ss17_20>0) -> 1*dcfr:(ss17_20'=0);
[repair1] (ss3_4=2 & ss17_20=1) -> 3*diskrr:(ss17_20'=2);
[repair2] (ss3_4=2 & ss17_20=2) -> 2*diskrr:(ss17_20'=3);
[repair3] (ss3_4=2 & ss17_20=3) -> 1*diskrr:(ss17_20'=4);
[repair4] (ss3_4=1 & ss17_20=1) -> 3*diskrr:(ss17_20'=2) + 1*dcrr:(ss3_4'=2);
[repair5] (ss3_4=1 & ss17_20=2) -> 2*diskrr:(ss17_20'=3) + 1*dcrr:(ss3_4'=2);
[repair6] (ss3_4=1 & ss17_20=3) -> 1*diskrr:(ss17_20'=4) + 1*dcrr:(ss3_4'=2);
[repair7] (ss3_4=1 & ss17_20=4) -> 1*dcrr:(ss3_4'=2);
endmodule