-- A "perfect" modelization of the audio control protocol var x, y, z : clock; i, c, leng, m,p,r,doublezero : discrete; alpha : parameter; automaton random synclabs : ; initially rand & i=0; loc rand : while True wait{} when True do {i'=0} goto rand; when True do {i'=1} goto rand; end ---------------------------------------------- automaton sender synclabs : up, down; initially idle & x=0 & p=0 & leng=0 & c=0 & doublezero=0 ; loc idle : while True wait{} when x>alpha do{x'=0, p'=1, leng'=1, c'=1} sync up goto oneSent; loc oneSent : while x<=4 wait{} when x>=2 & x<=2 & i=1 sync down goto waitingOne ; when x>=4 & x <= 4 & i=0 sync down do{ x'=0, p'=1-p, leng'=leng+1, c'=2*c,doublezero'=0} goto zeroSent; when p=1 do{x'=0, p'=0} goto idle; loc waitingOne : while x<=4 wait{} when x>=4 & x<=4 sync up do{x'=0, p'=1-p, leng'=leng+1, c'=2*c+1} goto oneSent; loc zeroSent : while x<=4 wait{} when x>=2 & x<=2 & i=0 sync up goto waitingZero; when x>=4 & x <= 4 & i=1 sync up do{ x'=0, p'=1-p, leng'=leng+1,c'=2*c+1} goto oneSent; when p=1 do{x'=0, p'=0} goto idle; when doublezero=1 do{x'=0, p'=0} goto idle; loc waitingZero : while x<=4 wait{} when x>=4 & x<=4 sync down do{x'=0,p'=1-p,leng'=leng+1,c'=2*c,doublezero'=1} goto zeroSent; end ----------------------------------------------------- automaton receiver synclabs : up,finalZero; initially idle2 & r=0 ; loc idle2: while True wait{} when True sync up do {y'=0,m'=1,r'=1} goto last_is_1; loc last_is_1 : while y<=9 wait{} when 3<=y & y<=5 sync up do {y'=0,m'=1-m,r'=1} goto last_is_1; when 5<=y & y<=7 sync up do {y'=0,m'=1-m,r'=0} goto last_is_0; when 7<=y sync up do {y'=0,r'=2} goto last_is_1;--next_is_o1 when y>=9 & m=1 do {y'=0} goto idle2; when y>=9 & m=0 sync finalZero do{m'=1-m,r'=0,y'=0} goto idle2; loc last_is_0 : while y<=7 wait{} when 3<=y & y<=5 sync up do {y'=0,m'=1-m,r'=0} goto last_is_0; when 5<=y sync up do {y'=0,r'=2} goto last_is_1; --next_is_o1 when y>=7 sync finalZero do {y'=0, r'=0} goto idle2; -- out end automaton checkOutput synclabs : up , finalZero; initially check & z>=0; loc check : while True wait{} when True sync up 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 var init_reg, final_reg, reached ,truc: region ; init_reg := loc[sender]=idle & x=0 & p=0 & leng=0 & c=0 & doublezero=0 & loc[receiver]=idle2 & y=0 & r=0 & m=0 & loc[checkOutput]= check & z=0 & loc[random]=rand & i=0 & alpha >1 & alpha<13; final_reg := loc[checkOutput]=cerror; reached := reach forward from init_reg endreach; print omit all locations hide non_parameters in reached & final_reg endhide;