| Variable | Enabling Range | State Transformation | Remarks |
|---|---|---|---|
| controllers_working25(sv25) | in {1,2} | v'=v-1 | |
| controllers_failed27(sv27) | in {0,1} | v'=v+1 | |
| system_fail33(sv33) | = 0 | non-linear function, increasing: 1, decreasing: 0, identity: 1064, v'=v+c(s) with c(s) in {0,1} |