var x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28, x29, x30 :discrete; automaton p synclabs : ; initially ss & True; loc ss : while x0 >= 0 & x1 >= 0 & x2 >= 0 & x3 >= 0 & x4 >= 0 & x5 >= 0 & x6 >= 0 & x7 >= 0 & x8 >= 0 & x9 >= 0 & x10 >= 0 & x11 >= 0 & x12 >= 0 & x13 >= 0 & x14 >= 0 & x15 >= 0 & x16 >= 0 & x17 >= 0 & x18 >= 0 & x19 >= 0 & x20 >= 0 & x21 >= 0 & x22 >= 0 & x23 >= 0 & x24 >= 0 & x25 >= 0 & x26 >= 0 & x27 >= 0 & x28 >= 0 & x29 >= 0 & x30 >= 0 & x2 +x3 + x4 + x5 + x6 + x7 + x8 + x9 + x10 = 1 & x13 + x14 + x15 + x16 + x17 + x18 + x19 + x20 = 1 wait{} when x2 >= 1 do { x2' = x2-1, x3' = x3+1, x21' = x21+1} goto ss; when x3 >= 1 & x22 >= 1 do { x3' = x3-1, x4' = x4+1, x22' = x22-1, x23' = x23+1} goto ss; when x4 >= 1 & x24 >= 1 do { x4' = x4-1, x5' = x5+1, x24' = x24-1, x25' = x25+1} goto ss; when x5 >= 1 & x27 >= 1 do { x5' = x5-1, x6' = x6+1, x27' = x27-1} goto ss; when x6 >= 1 do { x6' = x6-1, x7' = x7+1, x29' = x29+1} goto ss; when x7 >= 1 do { x7' = x7-1, x9' = x9+1} goto ss; when x9 >= 1 & x11 >= 1 do { x1' = x1+1, x2' = x2+1, x9' = x9-1, x11' = x11-1} goto ss; when x7 >= 1 & x30 >= 1 do { x6' = x6+1, x7' = x7-1, x30' = x30-1} goto ss; when x6 >= 1 do { x6' = x6-1, x8' = x8+1, x28' = x28+1} goto ss; when x8 >= 1 do { x8' = x8-1, x9' = x9+1} goto ss; when x9 >= 1 do { x0' = x0+1, x9' = x9-1, x10' = x10+1} goto ss; when x8 >= 1 & x26 >= 1 do { x0' = x0+1, x8' = x8-1, x10' = x10+1, x26' = x26-1} goto ss; when x4 >= 1 do { x0' = x0+1, x4' = x4-1, x10' = x10+1} goto ss; when x3 >= 1 do { x0' = x0+1, x3' = x3-1, x10' = x10+1} goto ss; when x10 >= 1 & x12 >= 1 do { x2' = x2+1, x10' = x10-1, x12' = x12-1} goto ss; when x10 >= 1 & x11 >= 1 do { x2' = x2+1, x10' = x10-1, x11' = x11-1} goto ss; when x10 >= 1 do { x2' = x2+1, x10' = x10-1} goto ss; when x10 >= 1 do { x0' = x0+1} goto ss; when x13 >= 1 & x21 >= 1 do { x13' = x13-1, x14' = x14+1, x21' = x21-1, x22' = x22+1} goto ss; when x14 >= 1 & x23 >= 1 do { x14' = x14-1, x15' = x15+1, x23' = x23-1, x24' = x24+1} goto ss; when x15 >= 1 & x25 >= 1 do { x15' = x15-1, x16' = x16+1, x25' = x25-1, x27' = x27+1} goto ss; when x16 >= 1 & x29 >= 1 do { x16' = x16-1, x17' = x17+1, x29' = x29-1} goto ss; when x17 >= 1 do { x17' = x17-1, x18' = x18+1} goto ss; when x18 >= 1 do { x18' = x18-1, x19' = x19+1} goto ss; when x0 >= 1 & x19 >= 1 do { x0' = x0-1, x12' = x12+1, x13' = x13+1, x19' = x19-1} goto ss; when x17 >= 1 do { x16' = x16+1, x17' = x17-1, x30' = x30+1} goto ss; when x16 >= 1 do { x16' = x16-1, x19' = x19+1} goto ss; when x16 >= 1 & x28 >= 1 do { x16' = x16-1, x19' = x19+1, x26' = x26+1, x28' = x28-1} goto ss; when x15 >= 1 do { x11' = x11+1, x15' = x15-1, x20' = x20+1} goto ss; when x19 >= 1 do { x11' = x11+1, x19' = x19-1, x20' = x20+1} goto ss; when x18 >= 1 do { x11' = x11+1, x18' = x18-1, x20' = x20+1} goto ss; when x14 >= 1 do { x11' = x11+1, x14' = x14-1, x20' = x20+1} goto ss; when x1 >= 1 & x20 >= 1 do { x1' = x1-1, x13' = x13+1, x20' = x20-1} goto ss; when x0 >= 1 & x20 >= 1 do { x0' = x0-1, x13' = x13+1, x20' = x20-1} goto ss; when x20 >= 1 do { x13' = x13+1, x20' = x20-1} goto ss; when x20 >= 1 do { x11' = x11+1} goto ss; end var Init_reg, Unsafe_reg, Reached : region; Init_reg := x0 = 0 & x1 = 0 & x2 = 1 & x3 = 0 & x4 = 0 & x5 = 0 & x6 = 0 & x7 = 0 & x8 = 0 & x9 = 0 & x10 = 0 & x11 = 0 & x12 = 0 & x13 = 1 & x14 = 0 & x15 = 0 & x16 = 0 & x17 = 0 & x18 = 0 & x19 = 0 & x20 = 0 & x21 = 0 & x22 = 0 & x23 = 0 & x24 = 0 & x25 = 0 & x26 = 0 & x27 = 0 & x28 = 0 & x29 = 0 & x30 = 0; Unsafe_reg := x12 >= 1 & x21 >= 1 & x23 >= 1 & x28 >= 1 & x30 >= 1; Reached := reach backward from Unsafe_reg endreach; if empty(Reached & Init_reg) then prints "=================================== "; prints "SAFETY HOLD!"; prints "=================================== "; else prints "SAFETY DOES NOT HOLD!"; endif;