// ------------------------------------------------------------ // Token Ring HDDI 12 // // automatically generated by script generate.awk // M. Oliver Moeller // Wed Sep 19 11:44:16 2001 // ------------------------------------------------------------ chan tt1,tt2,tt3,tt4,tt5,tt6,tt7,tt8,tt9,tt10,tt11,tt12, rt1, rt2, rt3, rt4, rt5, rt6, rt7, rt8, rt9, rt10, rt11, rt12; const SA 20; const td 0; const TRTT 620; 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, ring_to_8{x <= td}, ring_8, ring_to_9{x <= td}, ring_9, ring_to_10{x <= td}, ring_10, ring_to_11{x <= td}, ring_11, ring_to_12{x <= td}, ring_12; 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_8 { sync rt7?; assign x:= 0; } , ring_to_8 -> ring_8 { guard x <= td; sync tt8!; }, ring_8 -> ring_to_9 { sync rt8?; assign x:= 0; } , ring_to_9 -> ring_9 { guard x <= td; sync tt9!; }, ring_9 -> ring_to_10 { sync rt9?; assign x:= 0; } , ring_to_10 -> ring_10 { guard x <= td; sync tt10!; }, ring_10 -> ring_to_11 { sync rt10?; assign x:= 0; } , ring_to_11 -> ring_11 { guard x <= td; sync tt11!; }, ring_11 -> ring_to_12 { sync rt11?; assign x:= 0; } , ring_to_12 -> ring_12 { guard x <= td; sync tt12!; }, ring_12 -> ring_to_1 { sync rt12?; 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 !; }; } process ST8 { 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 tt8 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt8 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt8 !; }, station_y_idle -> station_y_sync { sync tt8 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt8 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt8 !; }; } process ST9 { 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 tt9 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt9 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt9 !; }, station_y_idle -> station_y_sync { sync tt9 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt9 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt9 !; }; } process ST10 { 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 tt10 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt10 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt10 !; }, station_y_idle -> station_y_sync { sync tt10 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt10 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt10 !; }; } process ST11 { 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 tt11 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt11 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt11 !; }, station_y_idle -> station_y_sync { sync tt11 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt11 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt11 !; }; } process ST12 { 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 tt12 ?; assign y := 0, x:= 0; }, station_z_sync -> station_y_idle { guard x >= SA, z >= TRTT ; sync rt12 !; }, station_z_sync -> station_z_async { guard x >= SA, z < TRTT ; }, station_z_async -> station_y_idle { sync rt12 !; }, station_y_idle -> station_y_sync { sync tt12 ?; assign z := 0, x:= 0; }, station_y_sync -> station_z_idle { guard x >= SA, y >= TRTT ; sync rt12 !; }, station_y_sync -> station_y_async { guard x >= SA, y < TRTT ; }, station_y_async -> station_z_idle { sync rt12 !; }; } system RING, ST1, ST2, ST3, ST4, ST5, ST6, ST7, ST8, ST9, ST10, ST11, ST12;