// ------------------------------------------------------------ // Token Ring HDDI 7 // // automatically generated by script generate.awk // M. Oliver Moeller // Wed Sep 19 11:44:16 2001 // ------------------------------------------------------------ chan tt1,tt2,tt3,tt4,tt5,tt6,tt7, rt1, rt2, rt3, rt4, rt5, rt6, rt7; const SA 20; const td 0; const TRTT 370; 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, ring_to_5{x <= td}, ring_5, ring_to_6{x <= td}, ring_6, ring_to_7{x <= td}, ring_7; 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_5 { sync rt4?; assign x:= 0; } , ring_to_5 -> ring_5 { guard x <= td; sync tt5!; }, ring_5 -> ring_to_6 { sync rt5?; assign x:= 0; } , ring_to_6 -> ring_6 { guard x <= td; sync tt6!; }, ring_6 -> ring_to_7 { sync rt6?; assign x:= 0; } , ring_to_7 -> ring_7 { guard x <= td; sync tt7!; }, ring_7 -> ring_to_1 { sync rt7?; 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 !; }; } process ST5 { 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 tt5 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt5 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt5 !; }, station_y_idle -> station_y_sync { sync tt5 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt5 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt5 !; }; } process ST6 { 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 tt6 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt6 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt6 !; }, station_y_idle -> station_y_sync { sync tt6 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt6 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt6 !; }; } process ST7 { 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 tt7 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt7 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt7 !; }, station_y_idle -> station_y_sync { sync tt7 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt7 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt7 !; }; } system RING, ST1, ST2, ST3, ST4, ST5, ST6, ST7;