| VAR CONDITION_AT_ENTRANCE : boolean; | |
| ASSIGN | |
| init(CONDITION_AT_ENTRANCE) := condition; | |
| next(CONDITION_AT_ENTRANCE) := case | |
| !is_fault & next(is_fault) : CONDITION_AT_ENTRANCE; | |
| is_fault & next(is_fault): CONDITION_AT_ENTRANCE; | |
| TRUE : next(condition); | |
| esac; |