{ "jani-version": 1, "name": "CSMACD/CSMACD-bc5.imi", "type": "sha", "features": [ "derived-operators" ], "actions": [ { "name": "send1" }, { "name": "send2" }, { "name": "end1" }, { "name": "end2" }, { "name": "busy1" }, { "name": "busy2" }, { "name": "cd" }, { "name": "prob1" }, { "name": "prob2" } ], "variables": [ { "name": "x1", "type": "clock", "initial_value": 0 }, { "name": "x2", "type": "clock", "initial_value": 0 }, { "name": "y", "type": "clock", "initial_value": 0 }, { "name": "lambda", "type": "real" }, { "name": "sigma", "type": "real" }, { "name": "timeslot", "type": "real" } ], "properties": [], "automata": [ { "name": "medium", "locations": [ { "name": "Init" }, { "name": "Transmit" }, { "name": "Collide", "time-progress": { "exp": { "op": ">", "left": "sigma", "right": "y" } } } ], "initial_locations": [ "Init" ], "edges": [ { "location": "Init", "destinations": [ { "location": "Transmit", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "Init", "destinations": [ { "location": "Transmit", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "Transmit", "guard": { "op": ">", "left": "sigma", "right": "y" }, "destinations": [ { "location": "Collide", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "Transmit", "guard": { "op": ">", "left": "sigma", "right": "y" }, "destinations": [ { "location": "Collide", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "Transmit", "guard": { "op": ">", "left": "y", "right": "sigma" }, "destinations": [ { "location": "Transmit" } ] }, { "location": "Transmit", "guard": { "op": ">", "left": "y", "right": "sigma" }, "destinations": [ { "location": "Transmit" } ] }, { "location": "Transmit", "destinations": [ { "location": "Init", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "Transmit", "destinations": [ { "location": "Init", "assignments": [ { "ref": "y", "value": 0 } ] } ] }, { "location": "Collide", "guard": { "op": ">", "left": "sigma", "right": "y" }, "destinations": [ { "location": "Init", "assignments": [ { "ref": "y", "value": 0 } ] } ] } ] }, { "name": "sender1", "locations": [ { "name": "Init1" }, { "name": "Transmit1", "time-progress": { "exp": { "op": ">", "left": "lambda", "right": "x1" } } }, { "name": "Collide1_1", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_1_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_1_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x1" } } }, { "name": "Wait1_1_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_1_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" } } }, { "name": "Collide1_2", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_2_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_2_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x1" } } }, { "name": "Wait1_2_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_2_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_2_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_2_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_2_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_2_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" } } }, { "name": "Collide1_3", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_3_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_3_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x1" } } }, { "name": "Wait1_3_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_8", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_9", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_10", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_11", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_12", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_13", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_14", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_3_15", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" } } }, { "name": "Collide1_4", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_4_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_4_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x1" } } }, { "name": "Wait1_4_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_8", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_9", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_10", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_11", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_12", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_13", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_14", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_15", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_16", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_17", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_18", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_19", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_20", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_21", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_22", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_23", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_24", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_25", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_26", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_27", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_28", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_29", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_30", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_4_31", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x1" } } }, { "name": "Collide1_5", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_5_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } }, { "name": "Wait1_5_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x1" } } }, { "name": "Wait1_5_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_8", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_9", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_10", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_11", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_12", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_13", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_14", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_15", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_16", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_17", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_18", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_19", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_20", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_21", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_22", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_23", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_24", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_25", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_26", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_27", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_28", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_29", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_30", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_31", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_32", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 32, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_33", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 33, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_34", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 34, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_35", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 35, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_36", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 36, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_37", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 37, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_38", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 38, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_39", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 39, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_40", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 40, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_41", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 41, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_42", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 42, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_43", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 43, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_44", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 44, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_45", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 45, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_46", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 46, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_47", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 47, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_48", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 48, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_49", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 49, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_50", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 50, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_51", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 51, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_52", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 52, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_53", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 53, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_54", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 54, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_55", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 55, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_56", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 56, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_57", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 57, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_58", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 58, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_59", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 59, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_60", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 60, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_61", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 61, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_62", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 62, "right": "timeslot" }, "right": "x1" } } }, { "name": "Wait1_5_63", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 63, "right": "timeslot" }, "right": "x1" } } }, { "name": "Done1", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x1" } } } ], "initial_locations": [ "Init1" ], "edges": [ { "location": "Init1", "destinations": [ { "location": "Transmit1" } ] }, { "location": "Transmit1", "guard": { "op": "=", "left": "lambda", "right": "x1" }, "destinations": [ { "location": "Done1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Transmit1", "destinations": [ { "location": "Collide1_1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Collide1_1", "destinations": [ { "location": "Wait1_1_3" } ] }, { "location": "Collide1_1", "destinations": [ { "location": "Wait1_1_2" } ] }, { "location": "Collide1_1", "destinations": [ { "location": "Wait1_1_1" } ] }, { "location": "Collide1_1", "destinations": [ { "location": "Wait1_1_0" } ] }, { "location": "Wait1_1_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Collide1_2", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_1_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_1_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Collide1_2", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_1_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_1_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_2", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_1_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_1_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_2", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_1_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_7" } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_6" } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_5" } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_4" } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_3" } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_2" } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_1" } ] }, { "location": "Collide1_2", "destinations": [ { "location": "Wait1_2_0" } ] }, { "location": "Wait1_2_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_3", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_2_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_15" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_14" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_13" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_12" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_11" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_10" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_9" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_8" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_7" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_6" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_5" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_4" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_3" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_2" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_1" } ] }, { "location": "Collide1_3", "destinations": [ { "location": "Wait1_3_0" } ] }, { "location": "Wait1_3_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_4", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_3_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_31" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_30" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_29" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_28" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_27" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_26" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_25" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_24" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_23" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_22" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_21" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_20" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_19" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_18" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_17" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_16" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_15" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_14" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_13" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_12" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_11" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_10" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_9" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_8" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_7" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_6" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_5" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_4" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_3" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_2" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_1" } ] }, { "location": "Collide1_4", "destinations": [ { "location": "Wait1_4_0" } ] }, { "location": "Wait1_4_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_4_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_63" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_62" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_61" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_60" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_59" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_58" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_57" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_56" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_55" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_54" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_53" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_52" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_51" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_50" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_49" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_48" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_47" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_46" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_45" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_44" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_43" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_42" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_41" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_40" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_39" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_38" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_37" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_36" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_35" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_34" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_33" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_32" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_31" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_30" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_29" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_28" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_27" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_26" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_25" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_24" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_23" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_22" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_21" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_20" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_19" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_18" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_17" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_16" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_15" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_14" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_13" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_12" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_11" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_10" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_9" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_8" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_7" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_6" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_5" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_4" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_3" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_2" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_1" } ] }, { "location": "Collide1_5", "destinations": [ { "location": "Wait1_5_0" } ] }, { "location": "Wait1_5_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_0", "guard": { "op": "=", "left": "x1", "right": 0 }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_1", "guard": { "op": "=", "left": "timeslot", "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_32", "guard": { "op": "=", "left": { "op": "*", "left": 32, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_32", "guard": { "op": "=", "left": { "op": "*", "left": 32, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_33", "guard": { "op": "=", "left": { "op": "*", "left": 33, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_33", "guard": { "op": "=", "left": { "op": "*", "left": 33, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_34", "guard": { "op": "=", "left": { "op": "*", "left": 34, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_34", "guard": { "op": "=", "left": { "op": "*", "left": 34, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_35", "guard": { "op": "=", "left": { "op": "*", "left": 35, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_35", "guard": { "op": "=", "left": { "op": "*", "left": 35, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_36", "guard": { "op": "=", "left": { "op": "*", "left": 36, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_36", "guard": { "op": "=", "left": { "op": "*", "left": 36, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_37", "guard": { "op": "=", "left": { "op": "*", "left": 37, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_37", "guard": { "op": "=", "left": { "op": "*", "left": 37, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_38", "guard": { "op": "=", "left": { "op": "*", "left": 38, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_38", "guard": { "op": "=", "left": { "op": "*", "left": 38, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_39", "guard": { "op": "=", "left": { "op": "*", "left": 39, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_39", "guard": { "op": "=", "left": { "op": "*", "left": 39, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_40", "guard": { "op": "=", "left": { "op": "*", "left": 40, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_40", "guard": { "op": "=", "left": { "op": "*", "left": 40, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_41", "guard": { "op": "=", "left": { "op": "*", "left": 41, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_41", "guard": { "op": "=", "left": { "op": "*", "left": 41, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_42", "guard": { "op": "=", "left": { "op": "*", "left": 42, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_42", "guard": { "op": "=", "left": { "op": "*", "left": 42, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_43", "guard": { "op": "=", "left": { "op": "*", "left": 43, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_43", "guard": { "op": "=", "left": { "op": "*", "left": 43, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_44", "guard": { "op": "=", "left": { "op": "*", "left": 44, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_44", "guard": { "op": "=", "left": { "op": "*", "left": 44, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_45", "guard": { "op": "=", "left": { "op": "*", "left": 45, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_45", "guard": { "op": "=", "left": { "op": "*", "left": 45, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_46", "guard": { "op": "=", "left": { "op": "*", "left": 46, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_46", "guard": { "op": "=", "left": { "op": "*", "left": 46, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_47", "guard": { "op": "=", "left": { "op": "*", "left": 47, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_47", "guard": { "op": "=", "left": { "op": "*", "left": 47, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_48", "guard": { "op": "=", "left": { "op": "*", "left": 48, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_48", "guard": { "op": "=", "left": { "op": "*", "left": 48, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_49", "guard": { "op": "=", "left": { "op": "*", "left": 49, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_49", "guard": { "op": "=", "left": { "op": "*", "left": 49, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_50", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_50", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_51", "guard": { "op": "=", "left": { "op": "*", "left": 51, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_51", "guard": { "op": "=", "left": { "op": "*", "left": 51, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_52", "guard": { "op": "=", "left": { "op": "*", "left": 52, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_52", "guard": { "op": "=", "left": { "op": "*", "left": 52, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_53", "guard": { "op": "=", "left": { "op": "*", "left": 53, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_53", "guard": { "op": "=", "left": { "op": "*", "left": 53, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_54", "guard": { "op": "=", "left": { "op": "*", "left": 54, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_54", "guard": { "op": "=", "left": { "op": "*", "left": 54, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_55", "guard": { "op": "=", "left": { "op": "*", "left": 55, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_55", "guard": { "op": "=", "left": { "op": "*", "left": 55, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_56", "guard": { "op": "=", "left": { "op": "*", "left": 56, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_56", "guard": { "op": "=", "left": { "op": "*", "left": 56, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_57", "guard": { "op": "=", "left": { "op": "*", "left": 57, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_57", "guard": { "op": "=", "left": { "op": "*", "left": 57, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_58", "guard": { "op": "=", "left": { "op": "*", "left": 58, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_58", "guard": { "op": "=", "left": { "op": "*", "left": 58, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_59", "guard": { "op": "=", "left": { "op": "*", "left": 59, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_59", "guard": { "op": "=", "left": { "op": "*", "left": 59, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_60", "guard": { "op": "=", "left": { "op": "*", "left": 60, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_60", "guard": { "op": "=", "left": { "op": "*", "left": 60, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_61", "guard": { "op": "=", "left": { "op": "*", "left": 61, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_61", "guard": { "op": "=", "left": { "op": "*", "left": 61, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_62", "guard": { "op": "=", "left": { "op": "*", "left": 62, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_62", "guard": { "op": "=", "left": { "op": "*", "left": 62, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_63", "guard": { "op": "=", "left": { "op": "*", "left": 63, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Collide1_5", "assignments": [ { "ref": "x1", "value": 0 } ] } ] }, { "location": "Wait1_5_63", "guard": { "op": "=", "left": { "op": "*", "left": 63, "right": "timeslot" }, "right": "x1" }, "destinations": [ { "location": "Transmit1", "assignments": [ { "ref": "x1", "value": 0 } ] } ] } ] }, { "name": "sender2", "locations": [ { "name": "Init2", "time-progress": { "exp": { "op": "=", "left": "x2", "right": 0 } } }, { "name": "Transmit2", "time-progress": { "exp": { "op": ">", "left": "lambda", "right": "x2" } } }, { "name": "Collide2_1", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_1_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_1_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x2" } } }, { "name": "Wait2_1_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_1_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" } } }, { "name": "Collide2_2", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_2_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_2_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x2" } } }, { "name": "Wait2_2_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_2_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_2_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_2_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_2_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_2_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" } } }, { "name": "Collide2_3", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_3_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_3_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x2" } } }, { "name": "Wait2_3_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_8", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_9", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_10", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_11", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_12", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_13", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_14", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_3_15", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" } } }, { "name": "Collide2_4", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_4_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_4_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x2" } } }, { "name": "Wait2_4_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_8", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_9", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_10", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_11", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_12", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_13", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_14", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_15", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_16", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_17", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_18", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_19", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_20", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_21", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_22", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_23", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_24", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_25", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_26", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_27", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_28", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_29", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_30", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_4_31", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x2" } } }, { "name": "Collide2_5", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_5_0", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } }, { "name": "Wait2_5_1", "time-progress": { "exp": { "op": ">", "left": "timeslot", "right": "x2" } } }, { "name": "Wait2_5_2", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_3", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_4", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_5", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_6", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_7", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_8", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_9", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_10", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_11", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_12", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_13", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_14", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_15", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_16", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_17", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_18", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_19", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_20", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_21", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_22", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_23", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_24", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_25", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_26", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_27", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_28", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_29", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_30", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_31", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_32", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 32, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_33", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 33, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_34", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 34, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_35", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 35, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_36", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 36, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_37", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 37, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_38", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 38, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_39", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 39, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_40", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 40, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_41", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 41, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_42", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 42, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_43", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 43, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_44", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 44, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_45", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 45, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_46", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 46, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_47", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 47, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_48", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 48, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_49", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 49, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_50", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 50, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_51", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 51, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_52", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 52, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_53", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 53, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_54", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 54, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_55", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 55, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_56", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 56, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_57", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 57, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_58", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 58, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_59", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 59, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_60", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 60, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_61", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 61, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_62", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 62, "right": "timeslot" }, "right": "x2" } } }, { "name": "Wait2_5_63", "time-progress": { "exp": { "op": ">", "left": { "op": "*", "left": 63, "right": "timeslot" }, "right": "x2" } } }, { "name": "Done2", "time-progress": { "exp": { "op": ">", "left": 0, "right": "x2" } } } ], "initial_locations": [ "Init2" ], "edges": [ { "location": "Init2", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Transmit2" } ] }, { "location": "Transmit2", "guard": { "op": "=", "left": "lambda", "right": "x2" }, "destinations": [ { "location": "Done2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Transmit2", "destinations": [ { "location": "Collide2_1", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Collide2_1", "destinations": [ { "location": "Wait2_1_3" } ] }, { "location": "Collide2_1", "destinations": [ { "location": "Wait2_1_2" } ] }, { "location": "Collide2_1", "destinations": [ { "location": "Wait2_1_1" } ] }, { "location": "Collide2_1", "destinations": [ { "location": "Wait2_1_0" } ] }, { "location": "Wait2_1_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Collide2_2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_1_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_1_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Collide2_2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_1_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_1_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_1_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_1_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_1_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_7" } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_6" } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_5" } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_4" } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_3" } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_2" } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_1" } ] }, { "location": "Collide2_2", "destinations": [ { "location": "Wait2_2_0" } ] }, { "location": "Wait2_2_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_3", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_2_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_15" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_14" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_13" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_12" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_11" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_10" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_9" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_8" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_7" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_6" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_5" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_4" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_3" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_2" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_1" } ] }, { "location": "Collide2_3", "destinations": [ { "location": "Wait2_3_0" } ] }, { "location": "Wait2_3_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_4", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_3_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_31" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_30" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_29" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_28" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_27" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_26" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_25" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_24" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_23" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_22" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_21" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_20" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_19" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_18" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_17" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_16" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_15" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_14" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_13" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_12" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_11" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_10" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_9" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_8" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_7" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_6" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_5" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_4" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_3" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_2" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_1" } ] }, { "location": "Collide2_4", "destinations": [ { "location": "Wait2_4_0" } ] }, { "location": "Wait2_4_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_4_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_63" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_62" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_61" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_60" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_59" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_58" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_57" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_56" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_55" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_54" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_53" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_52" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_51" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_50" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_49" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_48" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_47" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_46" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_45" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_44" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_43" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_42" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_41" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_40" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_39" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_38" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_37" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_36" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_35" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_34" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_33" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_32" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_31" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_30" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_29" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_28" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_27" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_26" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_25" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_24" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_23" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_22" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_21" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_20" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_19" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_18" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_17" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_16" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_15" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_14" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_13" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_12" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_11" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_10" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_9" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_8" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_7" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_6" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_5" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_4" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_3" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_2" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_1" } ] }, { "location": "Collide2_5", "destinations": [ { "location": "Wait2_5_0" } ] }, { "location": "Wait2_5_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_0", "guard": { "op": "=", "left": "x2", "right": 0 }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_1", "guard": { "op": "=", "left": "timeslot", "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_2", "guard": { "op": "=", "left": { "op": "*", "left": 2, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_3", "guard": { "op": "=", "left": { "op": "*", "left": 3, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_4", "guard": { "op": "=", "left": { "op": "*", "left": 4, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_5", "guard": { "op": "=", "left": { "op": "*", "left": 5, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_6", "guard": { "op": "=", "left": { "op": "*", "left": 6, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_7", "guard": { "op": "=", "left": { "op": "*", "left": 7, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_8", "guard": { "op": "=", "left": { "op": "*", "left": 8, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_9", "guard": { "op": "=", "left": { "op": "*", "left": 9, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_10", "guard": { "op": "=", "left": { "op": "*", "left": 10, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_11", "guard": { "op": "=", "left": { "op": "*", "left": 11, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_12", "guard": { "op": "=", "left": { "op": "*", "left": 12, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_13", "guard": { "op": "=", "left": { "op": "*", "left": 13, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_14", "guard": { "op": "=", "left": { "op": "*", "left": 14, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_15", "guard": { "op": "=", "left": { "op": "*", "left": 15, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_16", "guard": { "op": "=", "left": { "op": "*", "left": 16, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_17", "guard": { "op": "=", "left": { "op": "*", "left": 17, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_18", "guard": { "op": "=", "left": { "op": "*", "left": 18, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_19", "guard": { "op": "=", "left": { "op": "*", "left": 19, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_20", "guard": { "op": "=", "left": { "op": "*", "left": 20, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_21", "guard": { "op": "=", "left": { "op": "*", "left": 21, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_22", "guard": { "op": "=", "left": { "op": "*", "left": 22, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_23", "guard": { "op": "=", "left": { "op": "*", "left": 23, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_24", "guard": { "op": "=", "left": { "op": "*", "left": 24, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_25", "guard": { "op": "=", "left": { "op": "*", "left": 25, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_26", "guard": { "op": "=", "left": { "op": "*", "left": 26, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_27", "guard": { "op": "=", "left": { "op": "*", "left": 27, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_28", "guard": { "op": "=", "left": { "op": "*", "left": 28, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_29", "guard": { "op": "=", "left": { "op": "*", "left": 29, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_30", "guard": { "op": "=", "left": { "op": "*", "left": 30, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_31", "guard": { "op": "=", "left": { "op": "*", "left": 31, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_32", "guard": { "op": "=", "left": { "op": "*", "left": 32, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_32", "guard": { "op": "=", "left": { "op": "*", "left": 32, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_33", "guard": { "op": "=", "left": { "op": "*", "left": 33, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_33", "guard": { "op": "=", "left": { "op": "*", "left": 33, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_34", "guard": { "op": "=", "left": { "op": "*", "left": 34, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_34", "guard": { "op": "=", "left": { "op": "*", "left": 34, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_35", "guard": { "op": "=", "left": { "op": "*", "left": 35, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_35", "guard": { "op": "=", "left": { "op": "*", "left": 35, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_36", "guard": { "op": "=", "left": { "op": "*", "left": 36, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_36", "guard": { "op": "=", "left": { "op": "*", "left": 36, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_37", "guard": { "op": "=", "left": { "op": "*", "left": 37, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_37", "guard": { "op": "=", "left": { "op": "*", "left": 37, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_38", "guard": { "op": "=", "left": { "op": "*", "left": 38, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_38", "guard": { "op": "=", "left": { "op": "*", "left": 38, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_39", "guard": { "op": "=", "left": { "op": "*", "left": 39, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_39", "guard": { "op": "=", "left": { "op": "*", "left": 39, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_40", "guard": { "op": "=", "left": { "op": "*", "left": 40, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_40", "guard": { "op": "=", "left": { "op": "*", "left": 40, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_41", "guard": { "op": "=", "left": { "op": "*", "left": 41, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_41", "guard": { "op": "=", "left": { "op": "*", "left": 41, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_42", "guard": { "op": "=", "left": { "op": "*", "left": 42, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_42", "guard": { "op": "=", "left": { "op": "*", "left": 42, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_43", "guard": { "op": "=", "left": { "op": "*", "left": 43, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_43", "guard": { "op": "=", "left": { "op": "*", "left": 43, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_44", "guard": { "op": "=", "left": { "op": "*", "left": 44, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_44", "guard": { "op": "=", "left": { "op": "*", "left": 44, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_45", "guard": { "op": "=", "left": { "op": "*", "left": 45, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_45", "guard": { "op": "=", "left": { "op": "*", "left": 45, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_46", "guard": { "op": "=", "left": { "op": "*", "left": 46, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_46", "guard": { "op": "=", "left": { "op": "*", "left": 46, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_47", "guard": { "op": "=", "left": { "op": "*", "left": 47, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_47", "guard": { "op": "=", "left": { "op": "*", "left": 47, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_48", "guard": { "op": "=", "left": { "op": "*", "left": 48, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_48", "guard": { "op": "=", "left": { "op": "*", "left": 48, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_49", "guard": { "op": "=", "left": { "op": "*", "left": 49, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_49", "guard": { "op": "=", "left": { "op": "*", "left": 49, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_50", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_50", "guard": { "op": "=", "left": { "op": "*", "left": 50, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_51", "guard": { "op": "=", "left": { "op": "*", "left": 51, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_51", "guard": { "op": "=", "left": { "op": "*", "left": 51, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_52", "guard": { "op": "=", "left": { "op": "*", "left": 52, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_52", "guard": { "op": "=", "left": { "op": "*", "left": 52, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_53", "guard": { "op": "=", "left": { "op": "*", "left": 53, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_53", "guard": { "op": "=", "left": { "op": "*", "left": 53, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_54", "guard": { "op": "=", "left": { "op": "*", "left": 54, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_54", "guard": { "op": "=", "left": { "op": "*", "left": 54, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_55", "guard": { "op": "=", "left": { "op": "*", "left": 55, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_55", "guard": { "op": "=", "left": { "op": "*", "left": 55, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_56", "guard": { "op": "=", "left": { "op": "*", "left": 56, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_56", "guard": { "op": "=", "left": { "op": "*", "left": 56, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_57", "guard": { "op": "=", "left": { "op": "*", "left": 57, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_57", "guard": { "op": "=", "left": { "op": "*", "left": 57, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_58", "guard": { "op": "=", "left": { "op": "*", "left": 58, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_58", "guard": { "op": "=", "left": { "op": "*", "left": 58, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_59", "guard": { "op": "=", "left": { "op": "*", "left": 59, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_59", "guard": { "op": "=", "left": { "op": "*", "left": 59, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_60", "guard": { "op": "=", "left": { "op": "*", "left": 60, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_60", "guard": { "op": "=", "left": { "op": "*", "left": 60, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_61", "guard": { "op": "=", "left": { "op": "*", "left": 61, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_61", "guard": { "op": "=", "left": { "op": "*", "left": 61, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_62", "guard": { "op": "=", "left": { "op": "*", "left": 62, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_62", "guard": { "op": "=", "left": { "op": "*", "left": 62, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_63", "guard": { "op": "=", "left": { "op": "*", "left": 63, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Collide2_5", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "Wait2_5_63", "guard": { "op": "=", "left": { "op": "*", "left": 63, "right": "timeslot" }, "right": "x2" }, "destinations": [ { "location": "Transmit2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] } ] } ], "system": { "elements": [ { "automaton": "medium" }, { "automaton": "sender1" }, { "automaton": "sender2" } ], "syncs": [ { "synchronise": [ "send1", "send1", null ], "result": "send1" }, { "synchronise": [ "send2", null, "send2" ], "result": "send2" }, { "synchronise": [ "end1", "end1", null ], "result": "end1" }, { "synchronise": [ "end2", null, "end2" ], "result": "end2" }, { "synchronise": [ "busy1", "busy1", null ], "result": "busy1" }, { "synchronise": [ "busy2", null, "busy2" ], "result": "busy2" }, { "synchronise": [ "cd", "cd", "cd" ], "result": "cd" }, { "synchronise": [ null, "prob1", null ], "result": "prob1" }, { "synchronise": [ null, null, "prob2" ], "result": "prob2" } ] } }