--little example of the second page of the paper [DEP99] var Think, Wait, Use : discrete; automaton P synclabs : ; initially LOC & True; loc LOC : while Think >= 0 & Wait >= 0 & Use >= 0 wait {} when Think >= 1 do { Use' = Use + 1, Wait' = Wait + Think - 1, Think' = 0} goto LOC; when Use >= 1 do { Use' = Use - 1, Think' = Think + Wait + 1, Wait' = 0} goto LOC; end var init_reg, final_reg, reached : region; init_reg := Think >= 1 & Wait = 0 & Use = 0; final_reg := Use >= 2; reached := reach backward from final_reg endreach; if empty(reached & init_reg) then prints "SAFETY HOLDS!"; else prints "SAFETY DOES NOT HOLD!"; endif;