// ------------------------------------------------------------ 
// CSMA/CD 4
// Carrier Sense, Multiple-Access with Collision Detection 
// 
// automatically generated by script genCSMA_CD.awk 
// M. Oliver Moeller <omoeller@brics.dk> 
// Wed Sep 19 11:48:20 2001 
// ------------------------------------------------------------ 
chan begin, end, busy, cd1, cd2, cd3, cd4;
     
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 }; 
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_idle { guard x <= 0; sync cd4 !; 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; };  
}



system P0, P1, P2, P3, P4;