#no update for variables { init node idle; true [ send1||tran active; true; y=0; 1 ] [ send2||tran active; true; y=0; 1 ] } { node active; true [ end1||tran idle; true; y=0; 1 ] [ end2||tran idle; true; y=0; 1 ] [ send1||tran collision; y<26; y=0; 1 ] [ send2||tran collision; y<26; y=0; 1 ] [ busy1||tran active; y>=26; null; 1 ] [ busy2||tran active; y>=26; null; 1 ] } { node collision; y<=26 [ cd||tran idle; y<=26; y=0; 1 ] *