{ "jani-version": 1, "name": "Scheduling/Thales_FMTV_Challenge/FMTV/FMTV2/FMTV_2.imi", "type": "sha", "features": [ "derived-operators" ], "actions": [ { "name": "T6_arr" }, { "name": "T6_start" }, { "name": "T6_dis" }, { "name": "T6_pre" }, { "name": "T6_act" }, { "name": "T7_act" }, { "name": "T5_act" }, { "name": "T6_end" }, { "name": "miss_event" }, { "name": "T5_arr" }, { "name": "T5_end" }, { "name": "T5_pre" }, { "name": "T5_dis" }, { "name": "T7_arr" }, { "name": "T7_end" }, { "name": "T7_dis" }, { "name": "T7_pre" }, { "name": "T7_finish" }, { "name": "T2_arr" }, { "name": "T2_dis" }, { "name": "T2_end" } ], "variables": [ { "name": "sched_urgent", "type": "continuous", "initial_value": 0 }, { "name": "j6", "type": "continuous", "initial_value": 0 }, { "name": "p6", "type": "continuous", "initial_value": 0 }, { "name": "c6", "type": "continuous", "initial_value": 0 }, { "name": "c5", "type": "continuous", "initial_value": 0 }, { "name": "c7", "type": "continuous", "initial_value": 0 }, { "name": "p2", "type": "continuous", "initial_value": 0 }, { "name": "c2", "type": "continuous", "initial_value": 0 }, { "name": "delay", "type": "continuous", "initial_value": 0 }, { "name": "P2_uncertain", "type": "real" }, { "name": "D", "type": "real" } ], "properties": [], "automata": [ { "name": "T6", "locations": [ { "name": "T6_idle", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 100, "right": "p6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_jitter_pre", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 20, "right": "j6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_jitter_post", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "c6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_seg1_susp", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 100, "right": "p6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_seg1_exec", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 4, "right": "c6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_hole_pre", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "c6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_hole", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "T6_hole_post", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "c6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_seg2_susp", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 100, "right": "p6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_seg2_exec", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 10, "right": "c6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_seg3_exec", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 5, "right": "c6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T6_seg3_susp", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 100, "right": "p6" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } } ], "initial_locations": [ "T6_idle" ], "edges": [ { "location": "T6_idle", "guard": { "op": "=", "left": "p6", "right": 100 }, "destinations": [ { "location": "T6_jitter_pre", "assignments": [ { "ref": "p6", "value": 0 }, { "ref": "j6", "value": 0 }, { "ref": "delay", "value": 0 } ] } ] }, { "location": "T6_jitter_pre", "guard": { "op": ">", "left": 20, "right": "j6" }, "destinations": [ { "location": "T6_jitter_post", "assignments": [ { "ref": "c6", "value": 0 } ] } ] }, { "location": "T6_jitter_post", "guard": { "op": "=", "left": "c6", "right": 0 }, "destinations": [ { "location": "T6_seg1_susp", "assignments": [ { "ref": "c6", "value": 0 } ] } ] }, { "location": "T6_seg1_susp", "destinations": [ { "location": "T6_seg1_exec" } ] }, { "location": "T6_seg1_susp", "guard": { "op": "=", "left": "p6", "right": 100 }, "destinations": [ { "location": "T6_idle", "assignments": [ { "ref": "p6", "value": 0 } ] } ] }, { "location": "T6_seg1_exec", "guard": { "op": ">", "left": "c6", "right": 4 }, "destinations": [ { "location": "T6_hole_pre", "assignments": [ { "ref": "c6", "value": 0 } ] } ] }, { "location": "T6_seg1_exec", "guard": { "op": ">", "left": "p6", "right": 100 }, "destinations": [ { "location": "T6_idle", "assignments": [ { "ref": "p6", "value": 0 } ] } ] }, { "location": "T6_seg1_exec", "destinations": [ { "location": "T6_seg1_susp" } ] }, { "location": "T6_hole_pre", "guard": { "op": "=", "left": "c6", "right": 0 }, "destinations": [ { "location": "T6_hole" } ] }, { "location": "T6_hole", "destinations": [ { "location": "T6_hole_post", "assignments": [ { "ref": "c6", "value": 0 } ] } ] }, { "location": "T6_hole_post", "guard": { "op": "=", "left": "c6", "right": 0 }, "destinations": [ { "location": "T6_seg2_susp", "assignments": [ { "ref": "c6", "value": 0 } ] } ] }, { "location": "T6_seg2_susp", "destinations": [ { "location": "T6_seg2_exec" } ] }, { "location": "T6_seg2_susp", "guard": { "op": "=", "left": "p6", "right": 100 }, "destinations": [ { "location": "T6_idle", "assignments": [ { "ref": "p6", "value": 0 } ] } ] }, { "location": "T6_seg2_exec", "guard": { "op": ">", "left": "c6", "right": 9 }, "destinations": [ { "location": "T6_seg3_exec", "assignments": [ { "ref": "c6", "value": 0 } ] } ] }, { "location": "T6_seg2_exec", "guard": { "op": ">", "left": "p6", "right": 100 }, "destinations": [ { "location": "T6_idle", "assignments": [ { "ref": "p6", "value": 0 } ] } ] }, { "location": "T6_seg2_exec", "destinations": [ { "location": "T6_seg2_susp" } ] }, { "location": "T6_seg3_exec", "guard": { "op": ">", "left": "c6", "right": 4 }, "destinations": [ { "location": "T6_idle", "assignments": [ { "ref": "c6", "value": 0 } ] } ] }, { "location": "T6_seg3_exec", "guard": { "op": ">", "left": "p6", "right": 100 }, "destinations": [ { "location": "T6_idle", "assignments": [ { "ref": "p6", "value": 0 } ] } ] }, { "location": "T6_seg3_exec", "destinations": [ { "location": "T6_seg3_susp" } ] }, { "location": "T6_seg3_susp", "destinations": [ { "location": "T6_seg3_exec" } ] }, { "location": "T6_seg3_susp", "guard": { "op": "=", "left": "p6", "right": 100 }, "destinations": [ { "location": "T6_idle", "assignments": [ { "ref": "p6", "value": 0 } ] } ] } ] }, { "name": "T5", "locations": [ { "name": "T5_idle", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "T5_starting", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "c5" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T5_susp", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "T5_exec", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 7, "right": "c5" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T5_ending", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "c5" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } } ], "initial_locations": [ "T5_idle" ], "edges": [ { "location": "T5_idle", "destinations": [ { "location": "T5_starting", "assignments": [ { "ref": "c5", "value": 0 } ] } ] }, { "location": "T5_starting", "guard": { "op": "=", "left": "c5", "right": 0 }, "destinations": [ { "location": "T5_susp" } ] }, { "location": "T5_susp", "destinations": [ { "location": "T5_exec" } ] }, { "location": "T5_exec", "guard": { "op": ">", "left": "c5", "right": 4 }, "destinations": [ { "location": "T5_ending", "assignments": [ { "ref": "c5", "value": 0 } ] } ] }, { "location": "T5_exec", "destinations": [ { "location": "T5_susp" } ] }, { "location": "T5_ending", "guard": { "op": "=", "left": "c5", "right": 0 }, "destinations": [ { "location": "T5_idle" } ] } ] }, { "name": "T7", "locations": [ { "name": "T7_idle", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "T7_starting", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "c7" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T7_susp", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "T7_exec", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 14, "right": "c7" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T7_ending", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "c7" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } } ], "initial_locations": [ "T7_idle" ], "edges": [ { "location": "T7_idle", "destinations": [ { "location": "T7_starting", "assignments": [ { "ref": "c7", "value": 0 } ] } ] }, { "location": "T7_starting", "guard": { "op": "=", "left": "c7", "right": 0 }, "destinations": [ { "location": "T7_susp", "assignments": [ { "ref": "c7", "value": 0 } ] } ] }, { "location": "T7_susp", "destinations": [ { "location": "T7_exec" } ] }, { "location": "T7_exec", "guard": { "op": "≥", "left": "c7", "right": 11 }, "destinations": [ { "location": "T7_ending", "assignments": [ { "ref": "c7", "value": 0 } ] } ] }, { "location": "T7_exec", "destinations": [ { "location": "T7_susp" } ] }, { "location": "T7_ending", "guard": { "op": "=", "left": "c7", "right": 0 }, "destinations": [ { "location": "T7_idle" } ] } ] }, { "name": "T2", "locations": [ { "name": "T2_idle", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": "P2_uncertain", "right": "p2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "T2_susp", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "T2_exec", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 17, "right": "c2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } } ], "initial_locations": [ "T2_idle" ], "edges": [ { "location": "T2_idle", "guard": { "op": "=", "left": "P2_uncertain", "right": "p2" }, "destinations": [ { "location": "T2_susp", "assignments": [ { "ref": "p2", "value": 0 }, { "ref": "c2", "value": 0 } ] } ] }, { "location": "T2_susp", "destinations": [ { "location": "T2_exec" } ] }, { "location": "T2_exec", "guard": { "op": ">", "left": "c2", "right": 17 }, "destinations": [ { "location": "T2_idle" } ] } ] }, { "name": "Observer", "locations": [ { "name": "Obs_idle", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "Obs_start", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "Obs_stop", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "Obs_miss", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } ], "initial_locations": [ "Obs_idle" ], "edges": [ { "location": "Obs_idle", "destinations": [ { "location": "Obs_start" } ] }, { "location": "Obs_idle", "destinations": [ { "location": "Obs_miss" } ] }, { "location": "Obs_start", "guard": { "op": "=", "left": "D", "right": "delay" }, "destinations": [ { "location": "Obs_stop" } ] }, { "location": "Obs_stop", "destinations": [ { "location": "Obs_stop" } ] }, { "location": "Obs_miss", "destinations": [ { "location": "Obs_miss" } ] } ] }, { "name": "sched_sched", "locations": [ { "name": "sched_loc_", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_AT2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT6", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2RT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT6RT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT6WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT5RT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT5", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2RT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT6RT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT6WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2RT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT6RT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT6WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT6", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET6", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2RT6", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2WT6", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT6WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET6WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2RT6WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2WT6WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT6WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET6WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2RT6WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2WT6WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT6WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET6WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2RT6WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_AT2WT6WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2WT6", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2WT6", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2WT6WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2WT6WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2WT6WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2WT6WT5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_RT2WT6WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } }, { "name": "sched_loc_ET2WT6WT5WT7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "sched_urgent" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } }, { "name": "sched_loc_stop", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "sched_urgent" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "j6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c6" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "p2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "c2" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "delay" }, "right": 1 } } } } } } } } } } } ], "initial_locations": [ "sched_loc_" ], "edges": [ { "location": "sched_loc_", "destinations": [ { "location": "sched_loc_AT2", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_", "destinations": [ { "location": "sched_loc_AT6", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_", "destinations": [ { "location": "sched_loc_AT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_", "destinations": [ { "location": "sched_loc_AT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_AT2", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2" } ] }, { "location": "sched_loc_AT6", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6" } ] }, { "location": "sched_loc_AT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT5" } ] }, { "location": "sched_loc_AT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT7" } ] }, { "location": "sched_loc_RT7", "destinations": [ { "location": "sched_loc_AT2RT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT7", "destinations": [ { "location": "sched_loc_AT6RT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT7", "destinations": [ { "location": "sched_loc_AT5RT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT7", "destinations": [ { "location": "sched_loc_ET7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_" } ] }, { "location": "sched_loc_AT2RT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT2WT7" } ] }, { "location": "sched_loc_AT2WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2WT7" } ] }, { "location": "sched_loc_AT6RT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT6WT7" } ] }, { "location": "sched_loc_AT6WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6WT7" } ] }, { "location": "sched_loc_AT5RT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT5WT7" } ] }, { "location": "sched_loc_AT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT5WT7" } ] }, { "location": "sched_loc_RT5", "destinations": [ { "location": "sched_loc_AT2RT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT5", "destinations": [ { "location": "sched_loc_AT6RT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT5", "destinations": [ { "location": "sched_loc_RT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT5", "destinations": [ { "location": "sched_loc_ET5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_" } ] }, { "location": "sched_loc_AT2RT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT2WT5" } ] }, { "location": "sched_loc_AT2WT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2WT5" } ] }, { "location": "sched_loc_AT6RT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT6WT5" } ] }, { "location": "sched_loc_AT6WT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6WT5" } ] }, { "location": "sched_loc_RT5WT7", "destinations": [ { "location": "sched_loc_AT2RT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT5WT7", "destinations": [ { "location": "sched_loc_AT6RT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT5WT7", "destinations": [ { "location": "sched_loc_ET5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT7" } ] }, { "location": "sched_loc_AT2RT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT2WT5WT7" } ] }, { "location": "sched_loc_AT2WT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2WT5WT7" } ] }, { "location": "sched_loc_AT6RT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT6WT5WT7" } ] }, { "location": "sched_loc_AT6WT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6WT5WT7" } ] }, { "location": "sched_loc_RT6", "destinations": [ { "location": "sched_loc_AT2RT6", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6", "destinations": [ { "location": "sched_loc_RT6WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6", "destinations": [ { "location": "sched_loc_RT6WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6", "destinations": [ { "location": "sched_loc_ET6", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET6", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_" } ] }, { "location": "sched_loc_AT2RT6", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT2WT6" } ] }, { "location": "sched_loc_AT2WT6", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2WT6" } ] }, { "location": "sched_loc_RT6WT7", "destinations": [ { "location": "sched_loc_AT2RT6WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6WT7", "destinations": [ { "location": "sched_loc_RT6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6WT7", "destinations": [ { "location": "sched_loc_ET6WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET6WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT7" } ] }, { "location": "sched_loc_AT2RT6WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT2WT6WT7" } ] }, { "location": "sched_loc_AT2WT6WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2WT6WT7" } ] }, { "location": "sched_loc_RT6WT5", "destinations": [ { "location": "sched_loc_AT2RT6WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6WT5", "destinations": [ { "location": "sched_loc_RT6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6WT5", "destinations": [ { "location": "sched_loc_ET6WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET6WT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT5" } ] }, { "location": "sched_loc_AT2RT6WT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT2WT6WT5" } ] }, { "location": "sched_loc_AT2WT6WT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2WT6WT5" } ] }, { "location": "sched_loc_RT6WT5WT7", "destinations": [ { "location": "sched_loc_AT2RT6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT6WT5WT7", "destinations": [ { "location": "sched_loc_ET6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET6WT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT5WT7" } ] }, { "location": "sched_loc_AT2RT6WT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_AT2WT6WT5WT7" } ] }, { "location": "sched_loc_AT2WT6WT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT2WT6WT5WT7" } ] }, { "location": "sched_loc_RT2", "destinations": [ { "location": "sched_loc_RT2WT6", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2", "destinations": [ { "location": "sched_loc_RT2WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2", "destinations": [ { "location": "sched_loc_RT2WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2", "destinations": [ { "location": "sched_loc_ET2", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_" } ] }, { "location": "sched_loc_RT2WT7", "destinations": [ { "location": "sched_loc_RT2WT6WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT7", "destinations": [ { "location": "sched_loc_RT2WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT7", "destinations": [ { "location": "sched_loc_ET2WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT7" } ] }, { "location": "sched_loc_RT2WT5", "destinations": [ { "location": "sched_loc_RT2WT6WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT5", "destinations": [ { "location": "sched_loc_RT2WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT5", "destinations": [ { "location": "sched_loc_ET2WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2WT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT5" } ] }, { "location": "sched_loc_RT2WT5WT7", "destinations": [ { "location": "sched_loc_RT2WT6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT5WT7", "destinations": [ { "location": "sched_loc_ET2WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2WT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT5WT7" } ] }, { "location": "sched_loc_RT2WT6", "destinations": [ { "location": "sched_loc_RT2WT6WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT6", "destinations": [ { "location": "sched_loc_RT2WT6WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT6", "destinations": [ { "location": "sched_loc_ET2WT6", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2WT6", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6" } ] }, { "location": "sched_loc_RT2WT6WT7", "destinations": [ { "location": "sched_loc_RT2WT6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT6WT7", "destinations": [ { "location": "sched_loc_ET2WT6WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2WT6WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6WT7" } ] }, { "location": "sched_loc_RT2WT6WT5", "destinations": [ { "location": "sched_loc_RT2WT6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_RT2WT6WT5", "destinations": [ { "location": "sched_loc_ET2WT6WT5", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2WT6WT5", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6WT5" } ] }, { "location": "sched_loc_RT2WT6WT5WT7", "destinations": [ { "location": "sched_loc_ET2WT6WT5WT7", "assignments": [ { "ref": "sched_urgent", "value": 0 } ] } ] }, { "location": "sched_loc_ET2WT6WT5WT7", "guard": { "op": "=", "left": "sched_urgent", "right": 0 }, "destinations": [ { "location": "sched_loc_RT6WT5WT7" } ] } ] } ], "system": { "elements": [ { "automaton": "T6" }, { "automaton": "T5" }, { "automaton": "T7" }, { "automaton": "T2" }, { "automaton": "Observer" }, { "automaton": "sched_sched" } ], "syncs": [ { "synchronise": [ "T6_arr", null, null, null, null, "T6_arr" ], "result": "T6_arr" }, { "synchronise": [ "T6_start", null, null, null, "T6_start", null ], "result": "T6_start" }, { "synchronise": [ "T6_dis", null, null, null, null, "T6_dis" ], "result": "T6_dis" }, { "synchronise": [ "T6_pre", null, null, null, null, "T6_pre" ], "result": "T6_pre" }, { "synchronise": [ "T6_act", "T6_act", null, null, null, null ], "result": "T6_act" }, { "synchronise": [ "T7_act", null, "T7_act", null, null, null ], "result": "T7_act" }, { "synchronise": [ "T5_act", "T5_act", null, null, null, null ], "result": "T5_act" }, { "synchronise": [ "T6_end", null, null, null, null, "T6_end" ], "result": "T6_end" }, { "synchronise": [ "miss_event", null, null, null, "miss_event", null ], "result": "miss_event" }, { "synchronise": [ null, "T5_arr", null, null, null, "T5_arr" ], "result": "T5_arr" }, { "synchronise": [ null, "T5_end", null, null, null, "T5_end" ], "result": "T5_end" }, { "synchronise": [ null, "T5_pre", null, null, null, "T5_pre" ], "result": "T5_pre" }, { "synchronise": [ null, "T5_dis", null, null, null, "T5_dis" ], "result": "T5_dis" }, { "synchronise": [ null, null, "T7_arr", null, null, "T7_arr" ], "result": "T7_arr" }, { "synchronise": [ null, null, "T7_end", null, null, "T7_end" ], "result": "T7_end" }, { "synchronise": [ null, null, "T7_dis", null, null, "T7_dis" ], "result": "T7_dis" }, { "synchronise": [ null, null, "T7_pre", null, null, "T7_pre" ], "result": "T7_pre" }, { "synchronise": [ null, null, "T7_finish", null, "T7_finish", null ], "result": "T7_finish" }, { "synchronise": [ null, null, null, "T2_arr", null, "T2_arr" ], "result": "T2_arr" }, { "synchronise": [ null, null, null, "T2_dis", null, "T2_dis" ], "result": "T2_dis" }, { "synchronise": [ null, null, null, "T2_end", null, "T2_end" ], "result": "T2_end" } ] } }