// ------------------------------------------------------------ 
// Token Ring HDDI 4
// 
// automatically generated by script generate.awk 
// M. Oliver Moeller <omoeller@brics.dk> 
// Wed Sep 19 11:44:16 2001 
// ------------------------------------------------------------ 
chan tt1,tt2,tt3,tt4,
     rt1, rt2, rt3, rt4;

const   SA      20; 
const   td      0; 
const   TRTT    220;  

process RING { 
clock x; 
state 
  ring_to_1{x <= td}, ring_1,
  ring_to_2{x <= td}, ring_2,
  ring_to_3{x <= td}, ring_3,
  ring_to_4{x <= td}, ring_4;
init ring_to_1; 
trans 
ring_to_1 -> ring_1 { guard x <= td; sync tt1!; }, 
ring_1  -> ring_to_2 { sync rt1?; assign x:= 0; } ,
ring_to_2 -> ring_2 { guard x <= td; sync tt2!; }, 
ring_2  -> ring_to_3 { sync rt2?; assign x:= 0; } ,
ring_to_3 -> ring_3 { guard x <= td; sync tt3!; }, 
ring_3  -> ring_to_4 { sync rt3?; assign x:= 0; } ,
ring_to_4 -> ring_4 { guard x <= td; sync tt4!; }, 
ring_4  -> ring_to_1 { sync rt4?; assign x:= 0; } ;
}

process ST1 {
clock x, y, z;
state station_z_idle, station_z_sync{ x<=SA }, station_z_async{ z<=TRTT }, 
station_y_idle, station_y_sync{ x<=SA }, station_y_async{ y<=TRTT }; 
init station_z_idle; 
trans
station_z_idle -> station_z_sync { sync tt1 ?; assign y := 0, x:= 0; }, 
station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt1 !; }, 
station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, 
station_z_async -> station_y_idle { sync rt1 !; }, 

station_y_idle -> station_y_sync { sync tt1 ?; assign z := 0, x:= 0; }, 
station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt1 !; }, 
station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, 
station_y_async -> station_z_idle { sync rt1 !; }; 
} 

process ST2 {
clock x, y, z;
state station_z_idle, station_z_sync{ x<=SA }, station_z_async{ z<=TRTT }, 
station_y_idle, station_y_sync{ x<=SA }, station_y_async{ y<=TRTT }; 
init station_z_idle; 
trans
station_z_idle -> station_z_sync { sync tt2 ?; assign y := 0, x:= 0; }, 
station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt2 !; }, 
station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, 
station_z_async -> station_y_idle { sync rt2 !; }, 

station_y_idle -> station_y_sync { sync tt2 ?; assign z := 0, x:= 0; }, 
station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt2 !; }, 
station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, 
station_y_async -> station_z_idle { sync rt2 !; }; 
} 

process ST3 {
clock x, y, z;
state station_z_idle, station_z_sync{ x<=SA }, station_z_async{ z<=TRTT }, 
station_y_idle, station_y_sync{ x<=SA }, station_y_async{ y<=TRTT }; 
init station_z_idle; 
trans
station_z_idle -> station_z_sync { sync tt3 ?; assign y := 0, x:= 0; }, 
station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt3 !; }, 
station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, 
station_z_async -> station_y_idle { sync rt3 !; }, 

station_y_idle -> station_y_sync { sync tt3 ?; assign z := 0, x:= 0; }, 
station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt3 !; }, 
station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, 
station_y_async -> station_z_idle { sync rt3 !; }; 
} 

process ST4 {
clock x, y, z;
state station_z_idle, station_z_sync{ x<=SA }, station_z_async{ z<=TRTT }, 
station_y_idle, station_y_sync{ x<=SA }, station_y_async{ y<=TRTT }; 
init station_z_idle; 
trans
station_z_idle -> station_z_sync { sync tt4 ?; assign y := 0, x:= 0; }, 
station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt4 !; }, 
station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, 
station_z_async -> station_y_idle { sync rt4 !; }, 

station_y_idle -> station_y_sync { sync tt4 ?; assign z := 0, x:= 0; }, 
station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt4 !; }, 
station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, 
station_y_async -> station_z_idle { sync rt4 !; }; 
} 

system RING, ST1, ST2, ST3, ST4;