const double T;

label "fail_sensors" = i=2&s<MIN_SENSORS;
label "fail_actuators" = o=2&a<MIN_ACTUATORS;
label "fail_io" = count=MAX_COUNT+1;
label "fail_main" = m=0;
label "down" = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0);

// Probability of any failure occurring within T hours
P=? [ true U<=T*3600 "down" ]

// Probability of each failure type occurring first (within T hours)
P=? [ !"down" U<=T*3600 "fail_sensors" ]
P=? [ !"down" U<=T*3600 "fail_actuators" ]
P=? [ !"down" U<=T*3600 "fail_io" ]
P=? [ !"down" U<=T*3600 "fail_main" ]

// Probability of each failure type occurring first (within T days)
P=? [ !"down" U<=T*3600*24 "fail_sensors" ]
P=? [ !"down" U<=T*3600*24 "fail_actuators" ]
P=? [ !"down" U<=T*3600*24 "fail_io" ]
P=? [ !"down" U<=T*3600*24 "fail_main" ]

// Probability of any failure occurring within T days
P=? [ true U<=T*3600*24 "down" ]

// Long-run probability of each failure type occurring
P=? [ !"down" U "fail_sensors" ]
P=? [ !"down" U "fail_actuators" ]
P=? [ !"down" U "fail_io" ]
P=? [ !"down" U "fail_main" ]

// Expected time spent in "up"/"danger"/"shutdown" by time T
R=? [ C<=T*3600 ]

// Expected time spent in "up"/"danger" before "shutdown"
R=? [ F "down" ]