// ------------------------------------------------------------ // CSMA/CD 12 // Carrier Sense, Multiple-Access with Collision Detection // // automatically generated by script genCSMA_CD.awk // M. Oliver Moeller // Wed Sep 19 11:48:20 2001 // ------------------------------------------------------------ chan begin, end, busy, cd1, cd2, cd3, cd4, cd5, cd6, cd7, cd8, cd9, cd10, cd11, cd12; process P0 { clock x; state bus_idle, bus_active, bus_collision1{ x < 26 }, bus_collision2{ x <= 0 }, bus_collision3{ x <= 0 }, bus_collision4{ x <= 0 }, bus_collision5{ x <= 0 }, bus_collision6{ x <= 0 }, bus_collision7{ x <= 0 }, bus_collision8{ x <= 0 }, bus_collision9{ x <= 0 }, bus_collision10{ x <= 0 }, bus_collision11{ x <= 0 }, bus_collision12{ x <= 0 }; init bus_idle; trans bus_idle -> bus_active { sync begin ?; assign x:= 0; }, bus_active -> bus_idle { sync end ?; assign x:= 0; }, bus_active -> bus_active { guard x >= 26; sync busy !; }, bus_active -> bus_collision1 { guard x < 26; sync begin ?; assign x:= 0; }, bus_collision1 -> bus_collision2 { guard x < 26; sync cd1 !; assign x:= 0; }, bus_collision2 -> bus_collision3 { guard x <= 0; sync cd2 !; assign x:= 0; }, bus_collision3 -> bus_collision4 { guard x <= 0; sync cd3 !; assign x:= 0; }, bus_collision4 -> bus_collision5 { guard x <= 0; sync cd4 !; assign x:= 0; }, bus_collision5 -> bus_collision6 { guard x <= 0; sync cd5 !; assign x:= 0; }, bus_collision6 -> bus_collision7 { guard x <= 0; sync cd6 !; assign x:= 0; }, bus_collision7 -> bus_collision8 { guard x <= 0; sync cd7 !; assign x:= 0; }, bus_collision8 -> bus_collision9 { guard x <= 0; sync cd8 !; assign x:= 0; }, bus_collision9 -> bus_collision10 { guard x <= 0; sync cd9 !; assign x:= 0; }, bus_collision10 -> bus_collision11 { guard x <= 0; sync cd10 !; assign x:= 0; }, bus_collision11 -> bus_collision12 { guard x <= 0; sync cd11 !; assign x:= 0; }, bus_collision12 -> bus_idle { guard x <= 0; sync cd12 !; assign x:= 0; }; } process P1 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd1 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd1 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd1 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd1 ?; assign x:= 0; }; } process P2 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd2 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd2 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd2 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd2 ?; assign x:= 0; }; } process P3 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd3 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd3 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd3 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd3 ?; assign x:= 0; }; } process P4 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd4 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd4 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd4 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd4 ?; assign x:= 0; }; } process P5 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd5 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd5 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd5 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd5 ?; assign x:= 0; }; } process P6 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd6 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd6 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd6 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd6 ?; assign x:= 0; }; } process P7 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd7 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd7 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd7 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd7 ?; assign x:= 0; }; } process P8 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd8 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd8 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd8 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd8 ?; assign x:= 0; }; } process P9 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd9 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd9 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd9 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd9 ?; assign x:= 0; }; } process P10 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd10 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd10 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd10 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd10 ?; assign x:= 0; }; } process P11 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd11 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd11 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd11 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd11 ?; assign x:= 0; }; } process P12 { clock x; state sender_wait, sender_transm{ x<= 808}, sender_retry{x < 52}; init sender_wait; trans sender_wait -> sender_transm { sync begin !; assign x:= 0; }, sender_wait -> sender_wait { sync cd12 ?; assign x:= 0; }, sender_wait -> sender_retry { sync cd12 ?; assign x:= 0; }, sender_wait -> sender_retry { sync busy ?; assign x:= 0; }, sender_transm -> sender_wait { guard x == 808; sync end !; assign x:= 0; }, sender_transm -> sender_retry { guard x < 52; sync cd12 ?; assign x:= 0; }, sender_retry -> sender_transm { guard x < 52; sync begin !; assign x:= 0; }, sender_retry -> sender_retry { guard x < 52; sync cd12 ?; assign x:= 0; }; } system P0, P1, P2, P3, P4, P5, P6, P7, P8, P9, P10, P11, P12;