clock c;
 
clock A_c;
int A_Pf, A_Pn, A_S1, A_S2,
  A_start, A_stop;
 
clock B_c;
int B_Pf, B_Pn, B_S1, B_S2,
  B_start, B_stop;
 
chan A_frame, A_reset, A_new_Pn;
int A_msg, A_no, A_eof, A_T4;
 
chan B_frame, B_reset, B_new_Pn;
int B_msg, B_no, B_eof, B_T4;
 
chan A_check;
int A_err, A_res;
 
chan B_check;
int B_err, B_res;
 
chan A_observe;
int A_diff;
 
chan B_observe;
int B_diff;
 
chan one, zero;

 
 
 

process Sender_A {
  state  call_check, call_observe, check_eof, end_jam, ex_jam {A_c <= 781}, ex_silence1 {A_c <= 2343}, ex_silence2 {A_c <= 781}, ex_start, goto_idle, hold {A_c <= 28116}, idle {A_c <= 781}, jam {A_c <= 25000}, nPf, newPn {A_c <= 40}, other_started {A_c <= 3124}, sample {A_c <= 781}, start {A_c <= 0}, stop, transmit {A_c <= 781}, until_silence {A_c <= 781};
  commit call_check,call_observe,check_eof,ex_start,goto_idle,nPf;
  init   start;
  trans  call_check -> ex_jam {
           guard  A_stop  ==0;
           sync   A_check!;
           assign A_c := 0;
         },
          -> ex_jam {
           guard  A_stop  ==1;
           assign A_res := 0,A_c := 0;
         },
         call_observe -> call_check {
           guard  A_stop  ==0;
           sync   A_observe!;
         },
          -> call_check {
           guard  A_stop  ==1;
         },
         check_eof -> newPn {
           guard  A_eof  ==0;
           sync   one?;
           assign A_S1 := 1,A_c := 0;
         },
          -> newPn {
           guard  A_eof  ==0;
           sync   zero?;
           assign A_S1 := 0,A_c := 0;
         },
          -> stop {
           guard  A_eof ==1;
           assign A_c := 0;
         },
         ex_jam -> jam {
           guard  A_c  ==781,A_res  ==1;
           sync   A_reset!;
           assign A_Pn := 0,A_c := 0;
         },
          -> nPf {
           guard  A_c  ==781,A_res  ==0;
         },
          -> until_silence {
           guard  A_c  ==781,A_res  ==2;
           sync   A_reset!;
           assign A_Pn := 1,A_start := 0,A_c := 0;
         },
         ex_silence1 -> ex_silence2 {
           guard  A_c  ==2343;
           sync   one?;
           assign A_c := 0;
         },
          -> goto_idle {
           guard  A_c  ==2343;
           sync   zero?;
         },
         ex_silence2 -> goto_idle {
           guard  A_c  ==781;
           sync   zero?;
         },
          -> transmit {
           guard  A_c  ==781;
           sync   one?;
           assign A_c := 0;
         },
         ex_start -> ex_silence1 {
           guard  B_start  ==0;
           assign A_c := 0;
         },
          -> other_started {
           guard  B_start  ==1;
           assign A_c := 0;
         },
         goto_idle -> idle {
           assign A_c := 0;
         },
         hold -> end_jam {
           guard  A_c  ==28116;
           assign A_res := 0;
         },
         idle -> ex_start {
           guard  A_c  ==781;
         },
         jam -> end_jam {
           guard  A_c  ==25000;
           assign A_Pn := 1,A_start := 0,A_res := 0,A_c := 0;
         },
         nPf -> check_eof {
           guard  A_Pn  ==1;
           assign A_Pf := 1;
         },
          -> check_eof {
           guard  A_Pn  ==0;
           assign A_Pf := 0;
         },
         newPn -> sample {
           guard  A_c  ==40,A_err > 0;
           assign A_Pn := 1;
         },
          -> sample {
           guard  A_c  ==40,A_err  ==0;
           sync   A_new_Pn!;
         },
         other_started -> ex_silence1 {
           guard  A_c  ==3124,B_start  ==0;
           assign A_c := 0;
         },
          -> other_started {
           guard  A_c  ==3124,B_start  ==1;
           assign A_c := 0;
         },
         sample -> call_observe {
           guard  A_c  ==781;
           sync   one?;
           assign A_S2 := 1;
         },
          -> call_observe {
           guard  A_c  ==781;
           sync   zero?;
           assign A_S2 := 0;
         },
         start -> idle {
           guard  A_c  ==0;
         },
         transmit -> check_eof {
           guard  A_c  ==781;
           sync   A_frame!;
           assign A_err := 0,A_diff := 0,A_Pf := 1;
         },
         until_silence -> hold {
           guard  A_c  ==781;
           sync   one?;
           assign A_c := 0;
         },
          -> until_silence {
           guard  A_c  ==781;
           sync   zero?;
           assign A_c := 0;
         };
}

process Sender_B {
  state  call_check, call_observe, check_eof, end_jam, ex_jam {B_c <= 781}, ex_silence1 {B_c <= 2343}, ex_silence2 {B_c <= 781}, ex_start, goto_idle, hold {B_c <= 28116}, idle {B_c <= 781}, jam {B_c <= 25000}, nPf, newPn {B_c <= 40}, other_started {B_c <= 3124}, sample {B_c <= 781}, start, stop, transmit {B_c <= 781}, until_silence {B_c <= 781};
  commit call_check,call_observe,check_eof,ex_start,goto_idle,nPf;
  init   start;
  trans  call_check -> ex_jam {
           guard  B_stop  ==1;
           assign B_res := 0,B_c := 0;
         },
          -> ex_jam {
           guard  B_stop  ==0;
           sync   B_check!;
           assign B_c := 0;
         },
         call_observe -> call_check {
           guard  B_stop  ==1;
         },
          -> call_check {
           guard  B_stop  ==0;
           sync   B_observe!;
         },
         check_eof -> newPn {
           guard  B_eof  ==0;
           sync   zero?;
           assign B_S1 := 0,B_c := 0;
         },
          -> newPn {
           guard  B_eof  ==0;
           sync   one?;
           assign B_S1 := 1,B_c := 0;
         },
          -> stop {
           guard  B_eof  ==1;
           assign B_c := 0;
         },
         ex_jam -> jam {
           guard  B_c  ==781,B_res  ==1;
           sync   B_reset!;
           assign B_Pn := 0,B_c := 0;
         },
          -> nPf {
           guard  B_c  ==781,B_res  ==0;
         },
          -> until_silence {
           guard  B_c  ==781,B_res  ==2;
           sync   B_reset!;
           assign B_Pn := 1,B_start := 0,B_c := 0;
         },
         ex_silence1 -> ex_silence2 {
           guard  B_c  ==2343;
           sync   one?;
           assign B_c := 0;
         },
          -> goto_idle {
           guard  B_c  ==2343;
           sync   zero?;
         },
         ex_silence2 -> goto_idle {
           guard  B_c  ==781;
           sync   zero?;
         },
          -> transmit {
           guard  B_c  ==781;
           sync   one?;
           assign B_c := 0;
         },
         ex_start -> ex_silence1 {
           guard  A_start  ==0;
           assign B_c := 0;
         },
          -> other_started {
           guard  A_start  ==1;
           assign B_c := 0;
         },
         goto_idle -> idle {
           assign B_c := 0;
         },
         hold -> end_jam {
           guard  B_c  ==28116;
           assign B_res := 0;
         },
         idle -> ex_start {
           guard  B_c  ==781;
         },
         jam -> end_jam {
           guard  B_c  ==25000;
           assign B_Pn := 1,B_start := 0,B_res := 0,B_c := 0;
         },
         nPf -> check_eof {
           guard  B_Pn  ==1;
           assign B_Pf := 1;
         },
          -> check_eof {
           guard  B_Pn  ==0;
           assign B_Pf := 0;
         },
         newPn -> sample {
           guard  B_c  ==40,B_err  ==0;
           sync   B_new_Pn!;
         },
          -> sample {
           guard  B_c  ==40,B_err > 0;
           assign B_Pn := 1;
         },
         other_started -> ex_silence1 {
           guard  B_c  ==3124,A_start  ==0;
           assign B_c := 0;
         },
          -> other_started {
           guard  B_c  ==3124,A_start  ==1;
           assign B_c := 0;
         },
         sample -> call_observe {
           guard  B_c  ==781;
           sync   zero?;
           assign B_S2 := 0;
         },
          -> call_observe {
           guard  B_c  ==781;
           sync   one?;
           assign B_S2 := 1;
         },
         start -> idle {
           assign B_c := 0;
         },
         transmit -> check_eof {
           guard  B_c  ==781;
           sync   B_frame!;
           assign B_err := 0,B_diff := 0,B_Pf := 1;
         },
         until_silence -> hold {
           guard  B_c  ==781;
           sync   one?;
           assign B_c := 0;
         },
          -> until_silence {
           guard  B_c  ==781;
           sync   zero?;
           assign B_c := 0;
         };
}

process Detector_A {
  state  calc_res, ex1_S1, ex1_S2, ex_Pf, ex_Pn, ex_S1, ex_S2, wait_call;
  commit calc_res,ex1_S1,ex1_S2,ex_Pf,ex_Pn,ex_S1,ex_S2;
  init   wait_call;
  trans  calc_res -> wait_call {
           guard  A_err  ==0;
           assign A_res := 0;
         },
          -> wait_call {
           guard  A_err > 0,A_err <= 3;
           assign A_res := 1;
         },
          -> wait_call {
           guard  A_err > 3;
           assign A_res := 2;
         },
         ex1_S1 -> calc_res {
           guard  A_S1  ==1;
         },
          -> ex1_S2 {
           guard  A_S1  ==0;
         },
         ex1_S2 -> calc_res {
           guard  A_S2  ==1;
         },
          -> wait_call {
           guard  A_S2  ==0;
         },
         ex_Pf -> ex1_S1 {
           guard  A_Pf  ==0;
         },
          -> ex_S1 {
           guard  A_Pf  ==1;
         },
         ex_Pn -> ex1_S1 {
           guard  A_Pn  ==0;
         },
          -> ex_S2 {
           guard  A_Pn  ==1;
         },
         ex_S1 -> ex_Pn {
           guard  A_S1  ==1;
         },
          -> ex_Pn {
           guard  A_S1  ==0,A_err > 3;
         },
          -> ex_Pn {
           guard  A_S1  ==0,A_err <= 3;
           assign A_err := A_err + 1;
         },
         ex_S2 -> ex1_S1 {
           guard  A_S2  ==1;
         },
          -> wait_call {
           guard  A_S2  ==0,A_err <= 3;
           assign A_err := A_err + 1;
         },
          -> wait_call {
           guard  A_S2  ==0,A_err > 3;
         },
         wait_call -> ex_Pf {
           sync   A_check?;
           assign A_res := 0;
         };
}

process Detector_B {
  state  calc_res, ex1_S1, ex1_S2, ex_Pf, ex_Pn, ex_S1, ex_S2, wait_call;
  commit calc_res,ex1_S1,ex1_S2,ex_Pf,ex_Pn,ex_S1,ex_S2;
  init   wait_call;
  trans  calc_res -> wait_call {
           guard  B_err  ==0;
           assign B_res := 0;
         },
          -> wait_call {
           guard  B_err > 0,B_err <= 3;
           assign B_res := 1;
         },
          -> wait_call {
           guard  B_err > 3;
           assign B_res := 2;
         },
         ex1_S1 -> calc_res {
           guard  B_S1  ==1;
         },
          -> ex1_S2 {
           guard  B_S1  ==0;
         },
         ex1_S2 -> calc_res {
           guard  B_S2  ==1;
         },
          -> wait_call {
           guard  B_S2  ==0;
         },
         ex_Pf -> ex1_S1 {
           guard  B_Pf  ==0;
         },
          -> ex_S1 {
           guard  B_Pf  ==1;
         },
         ex_Pn -> ex1_S1 {
           guard  B_Pn  ==0;
         },
          -> ex_S2 {
           guard  B_Pn  ==1;
         },
         ex_S1 -> ex_Pn {
           guard  B_S1  ==1;
         },
          -> ex_Pn {
           guard  B_S1  ==0,B_err > 3;
         },
          -> ex_Pn {
           guard  B_S1  ==0,B_err <= 3;
           assign B_err := B_err + 1;
         },
         ex_S2 -> ex1_S1 {
           guard  B_S2  ==1;
         },
          -> wait_call {
           guard  B_S2  ==0,B_err <= 3;
           assign B_err := B_err + 1;
         },
          -> wait_call {
           guard  B_S2  ==0,B_err > 3;
         },
         wait_call -> ex_Pf {
           sync   B_check?;
           assign B_res := 0;
         };
}

process Bus {
  state  active, initialize;
  commit initialize;
  init   initialize;
  trans  active -> active {
           guard  A_Pn  ==1,B_Pn  ==1;
           sync   one!;
         },
          -> active {
           guard  B_Pn  ==0;
           sync   zero!;
         },
          -> active {
           guard  A_Pn  ==0;
           sync   zero!;
         },
         initialize -> active {
           assign A_Pn := 1,B_Pn := 1;
         };
}

process Observer_A {
  state  compare;
  init   compare;
  trans  compare -> compare {
           guard  A_Pf  ==A_S1,A_Pn  ==A_S2;
           sync   A_observe?;
         },
          -> compare {
           guard  A_Pn  ==1,A_S2  ==0;
           sync   A_observe?;
           assign A_diff := 1;
         },
          -> compare {
           guard  A_Pf  ==1,A_S1  ==0;
           sync   A_observe?;
           assign A_diff := 1;
         };
}

process Observer_B {
  state  compare;
  init   compare;
  trans  compare -> compare {
           guard  B_Pf  ==1,B_S1  ==0;
           sync   B_observe?;
           assign B_diff := 1;
         },
          -> compare {
           guard  B_Pn  ==1,B_S2  ==0;
           sync   B_observe?;
           assign B_diff := 1;
         },
          -> compare {
           guard  B_Pf  ==B_S1,B_Pn  ==B_S2;
           sync   B_observe?;
         };
}

process Frame_Generator_B {
  state  first, last, msg, set_msg, start;
  commit set_msg;
  init   start;
  trans  first -> msg {
           sync   B_new_Pn?;
           assign B_Pn := 0;
         },
         last -> start {
           sync   B_new_Pn?;
           assign B_Pn := 1,B_eof := 1,B_start := 0;
         },
         msg -> last {
           guard  B_T4  ==1,B_msg  ==0;
           sync   B_new_Pn?;
           assign B_Pn := 0,B_stop := 1;
         },
          -> msg {
           guard  B_msg > 0;
           sync   B_new_Pn?;
           assign B_Pn := 1,B_msg := B_msg - 1;
         },
          -> set_msg {
           guard  B_T4  ==0,B_msg  ==0;
           sync   B_new_Pn?;
           assign B_no := B_no + 1,B_Pn := 0,B_start := 1;
         },
          -> start {
           sync   B_reset?;
         },
         set_msg -> msg {
           guard  B_no > 16,B_no <= 20;
           assign B_msg := 8,B_T4 := 1;
         },
          -> msg {
           guard  B_no < 20;
           assign B_msg := 6;
         },
          -> msg {
           guard  B_no < 20;
           assign B_msg := 4;
         },
          -> msg {
           guard  B_no < 20;
           assign B_msg := 2;
         },
         start -> first {
           sync   B_frame?;
           assign B_no := 1,B_msg := 10,B_eof := 0,B_stop := 0,B_T4 := 0;
         };
}

process Frame_Generator_A {
  state  first, last, msg, set_msg, start;
  commit set_msg;
  init   start;
  trans  first -> msg {
           sync   A_new_Pn?;
           assign A_Pn := 0;
         },
         last -> start {
           sync   A_new_Pn?;
           assign A_Pn := 1,A_eof := 1,A_start := 0;
         },
         msg -> last {
           guard  A_T4  ==1,A_msg  ==0;
           sync   A_new_Pn?;
           assign A_Pn := 0,A_stop := 1;
         },
          -> msg {
           guard  A_msg > 0;
           sync   A_new_Pn?;
           assign A_Pn := 1,A_msg := A_msg - 1;
         },
          -> set_msg {
           guard  A_T4  ==0,A_msg  ==0;
           sync   A_new_Pn?;
           assign A_no := A_no + 1,A_Pn := 0,A_start := 1;
         },
          -> start {
           sync   A_reset?;
         },
         set_msg -> msg {
           guard  A_no < 20;
           assign A_msg := 2;
         },
          -> msg {
           guard  A_no > 16,A_no <= 20;
           assign A_msg := 8,A_T4 := 1;
         },
         start -> first {
           sync   A_frame?;
           assign A_no := 1,A_msg := 10,A_eof := 0,A_stop := 0,A_T4 := 0;
         };
}

 
 
 

 
system Sender_A, Sender_B, 
  Frame_Generator_A, Frame_Generator_B,
  Detector_A, Detector_B,
  Observer_A, Observer_B,
  Bus;