var ddd2, zup, uuu1, ddd1, z, y, x : clock ; delta2, delta1 : parameter ; doublezero, r, p, m, leng, c, i : discrete ; automaton GWlast_is_0getup synclabs : getup, inlast_is_0, outlast_is_0; initially GWlast_is_0getup0 ; loc GWlast_is_0getup0 : while True wait{} when True sync inlast_is_0 goto GWlast_is_0getup1; when True sync getup goto GWlast_is_0getup0; loc GWlast_is_0getup1 : while True wait{} when True sync outlast_is_0 goto GWlast_is_0getup0; when asap sync getup do{uuu1' = 0 } goto GWlast_is_0getup3; when True goto GWlast_is_0getup2S72; when True goto GWlast_is_0getup2S73; loc GWlast_is_0getup2S72 : while y <= 3 + delta1 wait{} when True goto GWlast_is_0getup2S73; when True goto GWlast_is_0getup1; loc GWlast_is_0getup2S73 : while y >= 5 & y <= 5 + delta1 wait{} when True goto GWlast_is_0getup2S72; when True goto GWlast_is_0getup1; loc GWlast_is_0getup3 : while uuu1 <= 0 wait{} when True sync outlast_is_0 goto GWlast_is_0getup0; end automaton GWlast_is_1getup synclabs : getup, inlast_is_1, outlast_is_1; initially GWlast_is_1getup0 ; loc GWlast_is_1getup0 : while True wait{} when True sync inlast_is_1 goto GWlast_is_1getup1; when True sync getup goto GWlast_is_1getup0; loc GWlast_is_1getup1 : while True wait{} when True sync outlast_is_1 goto GWlast_is_1getup0; when asap sync getup do{uuu1' = 0 } goto GWlast_is_1getup3; when True goto GWlast_is_1getup2S57; when True goto GWlast_is_1getup2S59; when True goto GWlast_is_1getup2S58; loc GWlast_is_1getup2S57 : while y <= 3 + delta1 wait{} when True goto GWlast_is_1getup2S59; when True goto GWlast_is_1getup2S58; when True goto GWlast_is_1getup1; loc GWlast_is_1getup2S58 : while y >= 5 & y <= 5 + delta1 wait{} when True goto GWlast_is_1getup2S59; when True goto GWlast_is_1getup2S57; when True goto GWlast_is_1getup1; loc GWlast_is_1getup2S59 : while y >= 7 & y <= 7 + delta1 wait{} when True goto GWlast_is_1getup2S58; when True goto GWlast_is_1getup2S57; when True goto GWlast_is_1getup1; loc GWlast_is_1getup3 : while uuu1 <= 0 wait{} when True sync outlast_is_1 goto GWlast_is_1getup0; end automaton EWup synclabs : up, getup; initially EWup0 & zup = 0 ; loc EWup0 : while True wait{} when True sync up do{zup' = 0 } goto EWup1; loc EWup1 : while zup <= delta1 wait{} when True goto EWup2; when True sync up do{zup' = 0 } goto EWupERR; loc EWup2 : while True wait{} when asap sync getup goto EWup0; when True sync up do{zup' = 0 } goto EWupERR; loc EWupERR : while zup <= 0 wait{} end automaton checkOutput synclabs : getup, finalZero; initially check & z = 0 & leng = 0 & c = 0 & doublezero = 0 ; loc check : while True wait{} when True sync getup do{z' = 0 } goto treating; when True sync finalZero do{z' = 0 } goto treating; when leng > 3 goto cerror; when leng < 0 goto cerror; loc treating : while z <= 0 wait{} when r = 0 & leng = 1 & c = 1 do{z' = 0 } goto cerror; when r = 0 & leng = 1 & c = 0 do{leng' = leng - 1 , z' = 0 } goto check; when r = 0 & leng = 2 & c > 1 do{z' = 0 } goto cerror; when r = 0 & leng = 2 & c <= 1 do{leng' = leng - 1 , z' = 0 } goto check; when r = 0 & leng = 3 & c > 3 do{z' = 0 } goto cerror; when r = 0 & leng = 3 & c <= 3 do{leng' = leng - 1 , z' = 0 } goto check; when r = 1 & leng = 1 & c = 0 do{z' = 0 } goto cerror; when r = 1 & leng = 1 & c = 1 do{leng' = leng - 1 , c' = c - 1 , z' = 0 } goto check; when r = 1 & leng = 2 & c <= 1 do{z' = 0 } goto cerror; when r = 1 & leng = 2 & c > 1 do{leng' = leng - 1 , c' = c - 2 , z' = 0 } goto check; when r = 1 & leng = 3 & c <= 3 do{z' = 0 } goto cerror; when r = 1 & leng = 3 & c > 3 do{leng' = leng - 1 , c' = c - 4 , z' = 0 } goto check; when r = 2 & leng = 1 do{z' = 0 } goto cerror; when r = 2 & leng = 2 & c = 1 do{leng' = 0 , c' = 0 , z' = 0 } goto check; when r = 2 & leng = 2 & c = 0 do{z' = 0 } goto cerror; when r = 2 & leng = 2 & c > 2 do{z' = 0 } goto cerror; when r = 2 & leng = 3 & c = 3 do{leng' = 1 , c' = 1 , z' = 0 } goto check; when r = 2 & leng = 3 & c = 2 do{leng' = 1 , c' = 0 , z' = 0 } goto check; when r = 2 & leng = 3 & c > 3 do{z' = 0 } goto cerror; when r = 2 & leng = 3 & c < 2 do{z' = 0 } goto cerror; loc cerror : while True wait{} end automaton receiver synclabs : outlast_is_0, inlast_is_0, outlast_is_1, inlast_is_1, getup, finalZero; initially Inidle2 & y = 0 & m = 0 & r = 0 & ddd1 = 0 & uuu1 = 0 ; loc Postlast_is_0Nr3 : while ddd1 <= 0 wait{} when True sync outlast_is_0 do{ddd1' = 0 } goto PreInlast_is_1; loc Postlast_is_0Nr2 : while ddd1 <= 0 wait{} when True sync outlast_is_0 do{ddd1' = 0 } goto PreInlast_is_0; loc Postlast_is_0Nr1 : while ddd1 <= 0 wait{} when True sync outlast_is_0 do{ddd1' = 0 } goto Inidle2; loc Inlast_is_0 : while ddd1 <= delta1 wait{} when True goto last_is_0S74; when True goto last_is_0S75; loc PreInlast_is_0 : while ddd1 <= 0 wait{} when True sync inlast_is_0 do{ddd1' = 0 } goto Inlast_is_0; loc Postlast_is_1Nr5 : while ddd1 <= 0 wait{} when True sync outlast_is_1 do{ddd1' = 0 } goto PreInlast_is_1; loc Postlast_is_1Nr4 : while ddd1 <= 0 wait{} when True sync outlast_is_1 do{ddd1' = 0 } goto PreInlast_is_0; loc Postlast_is_1Nr3 : while ddd1 <= 0 wait{} when True sync outlast_is_1 do{ddd1' = 0 } goto PreInlast_is_1; loc Postlast_is_1Nr2 : while ddd1 <= 0 wait{} when True sync outlast_is_1 do{ddd1' = 0 } goto Inidle2; loc Postlast_is_1Nr1 : while ddd1 <= 0 wait{} when True sync outlast_is_1 do{ddd1' = 0 } goto Inidle2; loc Inlast_is_1 : while ddd1 <= delta1 wait{} when True goto last_is_1S60; when True goto last_is_1S61; loc PreInlast_is_1 : while ddd1 <= 0 wait{} when True sync inlast_is_1 do{ddd1' = 0 } goto Inlast_is_1; loc Inidle2 : while ddd1 <= delta1 wait{} when True goto idle2; loc idle2 : while True wait{} when True sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , m' = 1 , r' = 1 } goto PreInlast_is_1; loc last_is_1S60 : while ddd1 <= delta1 wait{} when True goto last_is_1S61; when y >= 9 - delta1 & m = 0 sync finalZero do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 0 , m' = 1 - m } goto Postlast_is_1Nr2; when y >= 9 - delta1 & m = 1 do{uuu1' = 0 , ddd1' = 0 , y' = 0 } goto Postlast_is_1Nr1; when y >= 7 - delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 2 } goto Postlast_is_1Nr5; when y >= 5 - delta1 & y <= 7 + delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , m' = 1 - m , r' = 0 } goto Postlast_is_1Nr4; when y >= 3 - delta1 & y <= 5 + delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , m' = 1 - m , r' = 1 } goto Postlast_is_1Nr3; loc last_is_1S61 : while y <= 9 + delta1 wait{} when True goto last_is_1S60; when y >= 9 - delta1 & m = 0 sync finalZero do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 0 , m' = 1 - m } goto Postlast_is_1Nr2; when y >= 9 - delta1 & m = 1 do{uuu1' = 0 , ddd1' = 0 , y' = 0 } goto Postlast_is_1Nr1; when y >= 7 - delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 2 } goto Postlast_is_1Nr5; when y >= 5 - delta1 & y <= 7 + delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , m' = 1 - m , r' = 0 } goto Postlast_is_1Nr4; when y >= 3 - delta1 & y <= 5 + delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , m' = 1 - m , r' = 1 } goto Postlast_is_1Nr3; loc last_is_0S74 : while ddd1 <= delta1 wait{} when True goto last_is_0S75; when y >= 7 - delta1 sync finalZero do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 0 } goto Postlast_is_0Nr1; when y >= 5 - delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 2 } goto Postlast_is_0Nr3; when y >= 3 - delta1 & y <= 5 + delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , m' = 1 - m , r' = 0 } goto Postlast_is_0Nr2; loc last_is_0S75 : while y <= 7 + delta1 wait{} when True goto last_is_0S74; when y >= 7 - delta1 sync finalZero do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 0 } goto Postlast_is_0Nr1; when y >= 5 - delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , r' = 2 } goto Postlast_is_0Nr3; when y >= 3 - delta1 & y <= 5 + delta1 sync getup do{uuu1' = 0 , ddd1' = 0 , y' = 0 , m' = 1 - m , r' = 0 } goto Postlast_is_0Nr2; end automaton sender synclabs : up, down; initially Inidle & x = 0 & p = 0 & i = 0 & leng = 0 & c = 0 & doublezero = 0 & ddd2 = 0 & uuu1 = 0 ; loc InwaitingZero : while ddd2 <= delta2 wait{} when True goto waitingZeroS96; when True goto waitingZeroS98; when True goto waitingZeroS97; loc InzeroSent : while ddd2 <= delta2 wait{} when True goto zeroSentS91; when True goto zeroSentS94; when True goto zeroSentS93; when True goto zeroSentS92; loc InwaitingOne : while ddd2 <= delta2 wait{} when True goto waitingOneS87; when True goto waitingOneS89; when True goto waitingOneS88; loc InoneSent : while ddd2 <= delta2 wait{} when True goto oneSentS82; when True goto oneSentS85; when True goto oneSentS84; when True goto oneSentS83; loc Inidle : while ddd2 <= delta2 wait{} when True goto idleS79; when True goto idleS80; loc idleS79 : while ddd2 <= delta2 wait{} when True goto idleS80; when x >= 12 - delta2 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 , c' = 1 , leng' = 1 } goto InoneSent; loc idleS80 : while x <= 12 + delta2 wait{} when True goto idleS79; when x >= 12 - delta2 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 , c' = 1 , leng' = 1 } goto InoneSent; loc oneSentS82 : while ddd2 <= delta2 wait{} when True goto oneSentS85; when True goto oneSentS84; when True goto oneSentS83; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 0 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c , i' >= 0 , i' <= 1 , doublezero' = 0 } goto InzeroSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingOne; loc oneSentS83 : while x <= 2 + delta2 wait{} when True goto oneSentS85; when True goto oneSentS84; when True goto oneSentS82; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 0 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c , i' >= 0 , i' <= 1 , doublezero' = 0 } goto InzeroSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingOne; loc oneSentS84 : while x <= 4 + delta2 & x >= 2 wait{} when True goto oneSentS85; when True goto oneSentS83; when True goto oneSentS82; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 0 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c , i' >= 0 , i' <= 1 , doublezero' = 0 } goto InzeroSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingOne; loc oneSentS85 : while x >= 4 wait{} when True goto oneSentS84; when True goto oneSentS83; when True goto oneSentS82; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 0 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c , i' >= 0 , i' <= 1 , doublezero' = 0 } goto InzeroSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 1 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingOne; loc waitingOneS87 : while ddd2 <= delta2 wait{} when True goto waitingOneS89; when True goto waitingOneS88; when x >= 2 - delta2 & x <= 2 + delta2 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c + 1 , i' >= 0 , i' <= 1 } goto InoneSent; loc waitingOneS88 : while x <= 2 + delta2 wait{} when True goto waitingOneS89; when True goto waitingOneS87; when x >= 2 - delta2 & x <= 2 + delta2 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c + 1 , i' >= 0 , i' <= 1 } goto InoneSent; loc waitingOneS89 : while x >= 2 wait{} when True goto waitingOneS88; when True goto waitingOneS87; when x >= 2 - delta2 & x <= 2 + delta2 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c + 1 , i' >= 0 , i' <= 1 } goto InoneSent; loc zeroSentS91 : while ddd2 <= delta2 wait{} when True goto zeroSentS94; when True goto zeroSentS93; when True goto zeroSentS92; when x >= 2 - delta2 & x <= 2 + delta2 & doublezero = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 1 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c + 1 , i' >= 0 , i' <= 1 } goto InoneSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 0 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingZero; loc zeroSentS92 : while x <= 2 + delta2 wait{} when True goto zeroSentS94; when True goto zeroSentS93; when True goto zeroSentS91; when x >= 2 - delta2 & x <= 2 + delta2 & doublezero = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 1 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c + 1 , i' >= 0 , i' <= 1 } goto InoneSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 0 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingZero; loc zeroSentS93 : while x >= 2 & x <= 4 + delta2 wait{} when True goto zeroSentS94; when True goto zeroSentS92; when True goto zeroSentS91; when x >= 2 - delta2 & x <= 2 + delta2 & doublezero = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 1 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c + 1 , i' >= 0 , i' <= 1 } goto InoneSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 0 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingZero; loc zeroSentS94 : while x >= 4 wait{} when True goto zeroSentS93; when True goto zeroSentS92; when True goto zeroSentS91; when x >= 2 - delta2 & x <= 2 + delta2 & doublezero = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 2 - delta2 & x <= 2 + delta2 & p = 1 do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 0 } goto Inidle; when x >= 4 - delta2 & x <= 4 + delta2 & i = 1 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c + 1 , i' >= 0 , i' <= 1 } goto InoneSent; when x >= 2 - delta2 & x <= 2 + delta2 & i = 0 sync up do{uuu1' = 0 , ddd2' = 0 , x' = 0 } goto InwaitingZero; loc waitingZeroS96 : while ddd2 <= delta2 wait{} when True goto waitingZeroS98; when True goto waitingZeroS97; when x >= 2 - delta2 & x <= 2 + delta2 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c , i' >= 0 , i' <= 1 , doublezero' = 1 } goto InzeroSent; loc waitingZeroS97 : while x <= 2 + delta2 wait{} when True goto waitingZeroS98; when True goto waitingZeroS96; when x >= 2 - delta2 & x <= 2 + delta2 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c , i' >= 0 , i' <= 1 , doublezero' = 1 } goto InzeroSent; loc waitingZeroS98 : while x >= 2 wait{} when True goto waitingZeroS97; when True goto waitingZeroS96; when x >= 2 - delta2 & x <= 2 + delta2 sync down do{uuu1' = 0 , ddd2' = 0 , x' = 0 , p' = 1 - p , leng' = leng + 1 , c' = 2 c , i' >= 0 , i' <= 1 , doublezero' = 1 } goto InzeroSent; end automaton random synclabs : ; initially ran & i = 0 ; loc ran : while True wait{} when True do{i' = 1 } goto ran; when True do{i' = 0 } goto ran; end var init_states, bad_states, reached : region; init_states := loc[GWlast_is_0getup]= GWlast_is_0getup0 & loc[GWlast_is_1getup]= GWlast_is_1getup0 & loc[EWup]= EWup0 & zup = 0 & loc[checkOutput]= check & z = 0 & leng = 0 & c = 0 & doublezero = 0 & loc[receiver]= Inidle2 & y = 0 & m = 0 & r = 0 & ddd1 = 0 & uuu1 = 0 & loc[sender]= Inidle & x = 0 & p = 0 & i = 0 & leng = 0 & c = 0 & doublezero = 0 & ddd2 = 0 & uuu1 = 0 & loc[random]= ran & i = 0 & delta2 + delta1< 1/2 & delta1 >0 & delta2 >0 ; bad_states := (loc[checkOutput]=cerror ) | (loc[EWup]=EWupERR ); reached := reach forward from init_states endreach; if empty(bad_states & reached) then prints "System safe!"; else prints "System UNsafe, printing trace to error state:" ; print trace to bad_states using reached; endif ;