// // Specification: Autograph Window // // Specification was drawn in Autograph version 3. // // Global declaration section // clock c; // === Sender_A === clock A_c; int A_Pf, A_Pn, A_S1, A_S2, A_start, A_stop; // === Sender_B === clock B_c; int B_Pf, B_Pn, B_S1, B_S2, B_start, B_stop; // === Frame_Generator_A === chan A_frame, A_reset, A_new_Pn; int A_msg, A_no, A_eof, A_T4; // === Frame_Generator_B === chan B_frame, B_reset, B_new_Pn; int B_msg, B_no, B_eof, B_T4; // === Detector_A === chan A_check; int A_err, A_res; // === Detector_B === chan B_check; int B_err, B_res; // === Observer_A === chan A_observe; int A_diff; // === Observer_B === chan B_observe; int B_diff; // === Bus === 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; }, call_check -> 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_observe -> call_check {guard A_stop == 1; }, check_eof -> newPn {guard A_eof == 0; sync one?; assign A_S1 := 1,A_c := 0; }, check_eof -> newPn {guard A_eof == 0; sync zero?; assign A_S1 := 0,A_c := 0; }, check_eof -> 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; }, ex_jam -> nPf {guard A_c == 781,A_res == 0; }, ex_jam -> 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; }, ex_silence1 -> goto_idle {guard A_c == 2343; sync zero?; }, ex_silence2 -> goto_idle {guard A_c == 781; sync zero?; }, ex_silence2 -> transmit {guard A_c == 781; sync one?; assign A_c := 0; }, ex_start -> ex_silence1 {guard B_start == 0; assign A_c := 0; }, ex_start -> 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; }, nPf -> check_eof {guard A_Pn == 0; assign A_Pf := 0; }, newPn -> sample {guard A_c == 40,A_err > 0; assign A_Pn := 1; }, newPn -> 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 -> 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; }, sample -> 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 -> 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; }, call_check -> ex_jam {guard B_stop == 0; sync B_check!; assign B_c := 0; }, call_observe -> call_check {guard B_stop == 1; }, call_observe -> 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; }, check_eof -> newPn {guard B_eof == 0; sync one?; assign B_S1 := 1,B_c := 0; }, check_eof -> 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; }, ex_jam -> nPf {guard B_c == 781,B_res == 0; }, ex_jam -> 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; }, ex_silence1 -> goto_idle {guard B_c == 2343; sync zero?; }, ex_silence2 -> goto_idle {guard B_c == 781; sync zero?; }, ex_silence2 -> transmit {guard B_c == 781; sync one?; assign B_c := 0; }, ex_start -> ex_silence1 {guard A_start == 0; assign B_c := 0; }, ex_start -> 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; }, nPf -> check_eof {guard B_Pn == 0; assign B_Pf := 0; }, newPn -> sample {guard B_c == 40,B_err == 0; sync B_new_Pn!; }, newPn -> 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 -> 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; }, sample -> 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 -> 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; }, calc_res -> wait_call {guard A_err > 0,A_err <= 3; assign A_res := 1; }, calc_res -> wait_call {guard A_err > 3; assign A_res := 2; }, ex1_S1 -> calc_res {guard A_S1 == 1; }, ex1_S1 -> ex1_S2 {guard A_S1 == 0; }, ex1_S2 -> calc_res {guard A_S2 == 1; }, ex1_S2 -> wait_call {guard A_S2 == 0; }, ex_Pf -> ex1_S1 {guard A_Pf == 0; }, ex_Pf -> ex_S1 {guard A_Pf == 1; }, ex_Pn -> ex1_S1 {guard A_Pn == 0; }, ex_Pn -> ex_S2 {guard A_Pn == 1; }, ex_S1 -> ex_Pn {guard A_S1 == 1; }, ex_S1 -> ex_Pn {guard A_S1 == 0,A_err > 3; }, ex_S1 -> ex_Pn {guard A_S1 == 0,A_err <= 3; assign A_err := A_err + 1; }, ex_S2 -> ex1_S1 {guard A_S2 == 1; }, ex_S2 -> wait_call {guard A_S2 == 0,A_err <= 3; assign A_err := A_err + 1; }, ex_S2 -> 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; }, calc_res -> wait_call {guard B_err > 0,B_err <= 3; assign B_res := 1; }, calc_res -> wait_call {guard B_err > 3; assign B_res := 2; }, ex1_S1 -> calc_res {guard B_S1 == 1; }, ex1_S1 -> ex1_S2 {guard B_S1 == 0; }, ex1_S2 -> calc_res {guard B_S2 == 1; }, ex1_S2 -> wait_call {guard B_S2 == 0; }, ex_Pf -> ex1_S1 {guard B_Pf == 0; }, ex_Pf -> ex_S1 {guard B_Pf == 1; }, ex_Pn -> ex1_S1 {guard B_Pn == 0; }, ex_Pn -> ex_S2 {guard B_Pn == 1; }, ex_S1 -> ex_Pn {guard B_S1 == 1; }, ex_S1 -> ex_Pn {guard B_S1 == 0,B_err > 3; }, ex_S1 -> ex_Pn {guard B_S1 == 0,B_err <= 3; assign B_err := B_err + 1; }, ex_S2 -> ex1_S1 {guard B_S2 == 1; }, ex_S2 -> wait_call {guard B_S2 == 0,B_err <= 3; assign B_err := B_err + 1; }, ex_S2 -> 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 -> active {guard B_Pn == 0; sync zero!; }, active -> 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 -> compare {guard A_Pn == 1,A_S2 == 0; sync A_observe?; assign A_diff := 1; }, compare -> 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 -> compare {guard B_Pn == 1,B_S2 == 0; sync B_observe?; assign B_diff := 1; }, compare -> 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 -> msg {guard B_msg > 0; sync B_new_Pn?; assign B_Pn := 1,B_msg := B_msg - 1; }, msg -> 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; }, msg -> start {sync B_reset?; }, set_msg -> msg {guard B_no > 16,B_no <= 20; assign B_msg := 8,B_T4 := 1; }, set_msg -> msg {guard B_no < 20; assign B_msg := 6; }, set_msg -> msg {guard B_no < 20; assign B_msg := 4; }, set_msg -> 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 -> msg {guard A_msg > 0; sync A_new_Pn?; assign A_Pn := 1,A_msg := A_msg - 1; }, msg -> 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; }, msg -> start {sync A_reset?; }, set_msg -> msg {guard A_no < 20; assign A_msg := 2; }, set_msg -> 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;