// ------------------------------------------------------------ // Token Ring HDDI 2 // // automatically generated by script generate.awk // M. Oliver Moeller // Wed Sep 19 11:44:16 2001 // ------------------------------------------------------------ chan tt1,tt2, rt1, rt2; const SA 20; const td 0; const TRTT 120; process RING { clock x; state ring_to_1{x <= td}, ring_1, ring_to_2{x <= td}, ring_2; 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_1 { sync rt2?; 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 !; }; } system RING, ST1, ST2;