{ "jani-version": 1, "name": "Scheduling/distributed_systems/SSLAF13_1/SSLAF13_test1.imi", "type": "sha", "features": [ "derived-operators" ], "actions": [ { "name": "pipeline_restart_1" }, { "name": "task_11_act" }, { "name": "task_11_done" }, { "name": "pipeline_restart_2" }, { "name": "task_21_act" }, { "name": "task_21_done" }, { "name": "task_22_act" }, { "name": "task_22_done" }, { "name": "task_23_act" }, { "name": "task_23_done" }, { "name": "task_24_act" }, { "name": "task_24_done" }, { "name": "task_25_act" }, { "name": "task_25_done" }, { "name": "pipeline_restart_3" }, { "name": "task_31_act" }, { "name": "task_31_done" }, { "name": "pipeline_restart_4" }, { "name": "task_41_act" }, { "name": "task_41_done" }, { "name": "DEADLINE_MISSED_1" }, { "name": "DEADLINE_MISSED_2" }, { "name": "DEADLINE_MISSED_3" } ], "variables": [ { "name": "t_task_41", "type": "continuous", "initial_value": 0 }, { "name": "t_pipeline_4", "type": "continuous", "initial_value": 0 }, { "name": "t_asap_4", "type": "continuous", "initial_value": 0 }, { "name": "t_task_31", "type": "continuous", "initial_value": 0 }, { "name": "t_pipeline_3", "type": "continuous", "initial_value": 0 }, { "name": "t_asap_3", "type": "continuous", "initial_value": 0 }, { "name": "t_task_25", "type": "continuous", "initial_value": 0 }, { "name": "t_task_24", "type": "continuous", "initial_value": 0 }, { "name": "t_task_23", "type": "continuous", "initial_value": 0 }, { "name": "t_task_22", "type": "continuous", "initial_value": 0 }, { "name": "t_task_21", "type": "continuous", "initial_value": 0 }, { "name": "t_pipeline_2", "type": "continuous", "initial_value": 0 }, { "name": "t_asap_2", "type": "continuous", "initial_value": 0 }, { "name": "t_task_11", "type": "continuous", "initial_value": 0 }, { "name": "t_pipeline_1", "type": "continuous", "initial_value": 0 }, { "name": "t_asap_1", "type": "continuous", "initial_value": 0 }, { "name": "Token_24", "type": "real", "initial_value": 0 }, { "name": "Token_22", "type": "real", "initial_value": 0 }, { "name": "C_task_11", "type": "real" }, { "name": "C_task_21", "type": "real" } ], "properties": [], "automata": [ { "name": "pipeline_1", "locations": [ { "name": "P1_1", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_1" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P1_2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 20, "right": "t_pipeline_1" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P1_3", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 20, "right": "t_pipeline_1" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } } ], "initial_locations": [ "P1_1" ], "edges": [ { "location": "P1_1", "guard": { "op": "=", "left": "t_asap_1", "right": 0 }, "destinations": [ { "location": "P1_2" } ] }, { "location": "P1_2", "guard": { "op": ">", "left": 20, "right": "t_pipeline_1" }, "destinations": [ { "location": "P1_3", "assignments": [ { "ref": "t_asap_1", "value": 0 } ] } ] }, { "location": "P1_3", "guard": { "op": "=", "left": "t_pipeline_1", "right": 20 }, "destinations": [ { "location": "P1_1", "assignments": [ { "ref": "t_pipeline_1", "value": 0 }, { "ref": "t_asap_1", "value": 0 } ] } ] } ] }, { "name": "pipeline_2", "locations": [ { "name": "P2_1", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_3", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_4", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_6", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_8", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_9", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_10", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P2_11", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } } ], "initial_locations": [ "P2_1" ], "edges": [ { "location": "P2_1", "guard": { "op": "=", "left": "t_asap_2", "right": 0 }, "destinations": [ { "location": "P2_2" } ] }, { "location": "P2_2", "guard": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "destinations": [ { "location": "P2_3", "assignments": [ { "ref": "t_asap_2", "value": 0 } ] } ] }, { "location": "P2_3", "guard": { "op": "=", "left": "t_asap_2", "right": 0 }, "destinations": [ { "location": "P2_4" } ] }, { "location": "P2_4", "guard": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "destinations": [ { "location": "P2_5", "assignments": [ { "ref": "t_asap_2", "value": 0 } ] } ] }, { "location": "P2_5", "guard": { "op": "=", "left": "t_asap_2", "right": 0 }, "destinations": [ { "location": "P2_6" } ] }, { "location": "P2_6", "guard": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "destinations": [ { "location": "P2_7", "assignments": [ { "ref": "t_asap_2", "value": 0 } ] } ] }, { "location": "P2_7", "guard": { "op": "=", "left": "t_asap_2", "right": 0 }, "destinations": [ { "location": "P2_8" } ] }, { "location": "P2_8", "guard": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "destinations": [ { "location": "P2_9", "assignments": [ { "ref": "t_asap_2", "value": 0 } ] } ] }, { "location": "P2_9", "guard": { "op": "=", "left": "t_asap_2", "right": 0 }, "destinations": [ { "location": "P2_10" } ] }, { "location": "P2_10", "guard": { "op": ">", "left": 150, "right": "t_pipeline_2" }, "destinations": [ { "location": "P2_11", "assignments": [ { "ref": "t_asap_2", "value": 0 } ] } ] }, { "location": "P2_11", "guard": { "op": "=", "left": "t_pipeline_2", "right": 150 }, "destinations": [ { "location": "P2_1", "assignments": [ { "ref": "t_pipeline_2", "value": 0 }, { "ref": "t_asap_2", "value": 0 } ] } ] } ] }, { "name": "pipeline_3", "locations": [ { "name": "P3_1", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_3" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P3_2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 30, "right": "t_pipeline_3" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P3_3", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 30, "right": "t_pipeline_3" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } } ], "initial_locations": [ "P3_1" ], "edges": [ { "location": "P3_1", "guard": { "op": "=", "left": "t_asap_3", "right": 0 }, "destinations": [ { "location": "P3_2" } ] }, { "location": "P3_2", "guard": { "op": ">", "left": 30, "right": "t_pipeline_3" }, "destinations": [ { "location": "P3_3", "assignments": [ { "ref": "t_asap_3", "value": 0 } ] } ] }, { "location": "P3_3", "guard": { "op": "=", "left": "t_pipeline_3", "right": 30 }, "destinations": [ { "location": "P3_1", "assignments": [ { "ref": "t_pipeline_3", "value": 0 }, { "ref": "t_asap_3", "value": 0 } ] } ] } ] }, { "name": "pipeline_4", "locations": [ { "name": "P4_1", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_4" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P4_2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 200, "right": "t_pipeline_4" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "P4_3", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 200, "right": "t_pipeline_4" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } } ], "initial_locations": [ "P4_1" ], "edges": [ { "location": "P4_1", "guard": { "op": "=", "left": "t_asap_4", "right": 0 }, "destinations": [ { "location": "P4_2" } ] }, { "location": "P4_2", "guard": { "op": ">", "left": 200, "right": "t_pipeline_4" }, "destinations": [ { "location": "P4_3", "assignments": [ { "ref": "t_asap_4", "value": 0 } ] } ] }, { "location": "P4_3", "guard": { "op": "=", "left": "t_pipeline_4", "right": 200 }, "destinations": [ { "location": "P4_1", "assignments": [ { "ref": "t_pipeline_4", "value": 0 }, { "ref": "t_asap_4", "value": 0 } ] } ] } ] }, { "name": "proc_1", "locations": [ { "name": "DEADLINE_MISS", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } }, { "name": "proc_1_000", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } }, { "name": "proc_1_100", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": "C_task_11", "right": "t_task_11" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_1_010", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": "C_task_21", "right": "t_task_21" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_1_001", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 30, "right": "t_task_25" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_1_110", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": "C_task_11", "right": "t_task_11" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_1_101", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": "C_task_11", "right": "t_task_11" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_1_011", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": "C_task_21", "right": "t_task_21" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_1_111", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": "C_task_11", "right": "t_task_11" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } } ], "initial_locations": [ "proc_1_000" ], "edges": [ { "location": "proc_1_000", "destinations": [ { "location": "proc_1_100", "assignments": [ { "ref": "t_task_11", "value": 0 } ] } ] }, { "location": "proc_1_000", "destinations": [ { "location": "proc_1_010", "assignments": [ { "ref": "t_task_21", "value": 0 } ] } ] }, { "location": "proc_1_000", "destinations": [ { "location": "proc_1_001", "assignments": [ { "ref": "t_task_25", "value": 0 } ] } ] }, { "location": "proc_1_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_100", "guard": { "op": "=", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_000" } ] }, { "location": "proc_1_100", "guard": { "op": "≥", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_110", "assignments": [ { "ref": "t_task_21", "value": 0 } ] } ] }, { "location": "proc_1_100", "guard": { "op": "≥", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_101", "assignments": [ { "ref": "t_task_25", "value": 0 } ] } ] }, { "location": "proc_1_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_010", "guard": { "op": "≥", "left": "C_task_21", "right": "t_task_21" }, "destinations": [ { "location": "proc_1_110", "assignments": [ { "ref": "t_task_11", "value": 0 } ] } ] }, { "location": "proc_1_010", "guard": { "op": "=", "left": "C_task_21", "right": "t_task_21" }, "destinations": [ { "location": "proc_1_000" } ] }, { "location": "proc_1_010", "guard": { "op": "≥", "left": "C_task_21", "right": "t_task_21" }, "destinations": [ { "location": "proc_1_011", "assignments": [ { "ref": "t_task_25", "value": 0 } ] } ] }, { "location": "proc_1_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_001", "guard": { "op": "≥", "left": 30, "right": "t_task_25" }, "destinations": [ { "location": "proc_1_101", "assignments": [ { "ref": "t_task_11", "value": 0 } ] } ] }, { "location": "proc_1_001", "guard": { "op": "≥", "left": 30, "right": "t_task_25" }, "destinations": [ { "location": "proc_1_011", "assignments": [ { "ref": "t_task_21", "value": 0 } ] } ] }, { "location": "proc_1_001", "guard": { "op": "=", "left": "t_task_25", "right": 30 }, "destinations": [ { "location": "proc_1_000" } ] }, { "location": "proc_1_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_110", "guard": { "op": "=", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_010" } ] }, { "location": "proc_1_110", "guard": { "op": "=", "left": "C_task_21", "right": "t_task_21" }, "destinations": [ { "location": "proc_1_100" } ] }, { "location": "proc_1_110", "guard": { "op": "≥", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_111", "assignments": [ { "ref": "t_task_25", "value": 0 } ] } ] }, { "location": "proc_1_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_101", "guard": { "op": "=", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_001" } ] }, { "location": "proc_1_101", "guard": { "op": "≥", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_111", "assignments": [ { "ref": "t_task_21", "value": 0 } ] } ] }, { "location": "proc_1_101", "guard": { "op": "=", "left": "t_task_25", "right": 30 }, "destinations": [ { "location": "proc_1_100" } ] }, { "location": "proc_1_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_011", "guard": { "op": "≥", "left": "C_task_21", "right": "t_task_21" }, "destinations": [ { "location": "proc_1_111", "assignments": [ { "ref": "t_task_11", "value": 0 } ] } ] }, { "location": "proc_1_011", "guard": { "op": "=", "left": "C_task_21", "right": "t_task_21" }, "destinations": [ { "location": "proc_1_001" } ] }, { "location": "proc_1_011", "guard": { "op": "=", "left": "t_task_25", "right": 30 }, "destinations": [ { "location": "proc_1_010" } ] }, { "location": "proc_1_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 30, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_111", "guard": { "op": "=", "left": "C_task_11", "right": "t_task_11" }, "destinations": [ { "location": "proc_1_011" } ] }, { "location": "proc_1_111", "guard": { "op": "=", "left": "C_task_21", "right": "t_task_21" }, "destinations": [ { "location": "proc_1_101" } ] }, { "location": "proc_1_111", "guard": { "op": "=", "left": "t_task_25", "right": 30 }, "destinations": [ { "location": "proc_1_110" } ] } ] }, { "name": "proc_2", "locations": [ { "name": "idle", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } }, { "name": "DEADLINE_MISS", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } }, { "name": "t_22_running", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 25, "right": "t_task_22" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "t_24_running", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 34, "right": "t_task_24" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } } ], "initial_locations": [ "idle" ], "edges": [ { "location": "idle", "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "idle", "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 25, "right": "t_task_22" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 25, "right": "t_task_22" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 25, "right": "t_task_22" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 25, "right": "t_task_22" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_22_running", "guard": { "op": "≥", "left": "t_task_22", "right": 0 }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": ">", "left": 0, "right": "t_task_22" }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": "≥", "left": "t_task_22", "right": 0 }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": ">", "left": 0, "right": "t_task_22" }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_22", "right": 25 } }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "t_task_24", "value": 0 }, { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_22", "right": 25 } }, "destinations": [ { "location": "idle", "assignments": [ { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 34, "right": "t_task_24" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 34, "right": "t_task_24" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 34, "right": "t_task_24" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 34, "right": "t_task_24" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_24_running", "guard": { "op": "≥", "left": "t_task_24", "right": 0 }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_24_running", "guard": { "op": ">", "left": 0, "right": "t_task_24" }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_24_running", "guard": { "op": "≥", "left": "t_task_24", "right": 0 }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_24_running", "guard": { "op": ">", "left": 0, "right": "t_task_24" }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "=", "left": "t_task_24", "right": 34 } }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "t_task_22", "value": 0 }, { "ref": "Token_24", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "=", "left": "t_task_24", "right": 34 } }, "destinations": [ { "location": "idle", "assignments": [ { "ref": "Token_24", "value": 0 } ] } ] } ] }, { "name": "proc_3", "locations": [ { "name": "DEADLINE_MISS", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } }, { "name": "proc_3_000", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } }, { "name": "proc_3_100", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 15, "right": "t_task_23" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_3_010", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 5, "right": "t_task_31" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_3_001", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 80, "right": "t_task_41" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_3_110", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 5, "right": "t_task_31" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_3_101", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 15, "right": "t_task_23" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_3_011", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 5, "right": "t_task_31" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } }, { "name": "proc_3_111", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 5, "right": "t_task_31" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_41" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_4" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_31" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_3" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_25" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_24" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_23" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_22" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_21" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_asap_2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_11" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_pipeline_1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t_asap_1" }, "right": 1 } } } } } } } } } } } } } } } } } } } ], "initial_locations": [ "proc_3_000" ], "edges": [ { "location": "proc_3_000", "destinations": [ { "location": "proc_3_100", "assignments": [ { "ref": "t_task_23", "value": 0 } ] } ] }, { "location": "proc_3_000", "destinations": [ { "location": "proc_3_010", "assignments": [ { "ref": "t_task_31", "value": 0 } ] } ] }, { "location": "proc_3_000", "destinations": [ { "location": "proc_3_001", "assignments": [ { "ref": "t_task_41", "value": 0 } ] } ] }, { "location": "proc_3_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_100", "guard": { "op": "=", "left": "t_task_23", "right": 15 }, "destinations": [ { "location": "proc_3_000" } ] }, { "location": "proc_3_100", "guard": { "op": "≥", "left": 15, "right": "t_task_23" }, "destinations": [ { "location": "proc_3_110", "assignments": [ { "ref": "t_task_31", "value": 0 } ] } ] }, { "location": "proc_3_100", "guard": { "op": "≥", "left": 15, "right": "t_task_23" }, "destinations": [ { "location": "proc_3_101", "assignments": [ { "ref": "t_task_41", "value": 0 } ] } ] }, { "location": "proc_3_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_010", "guard": { "op": "≥", "left": 5, "right": "t_task_31" }, "destinations": [ { "location": "proc_3_110", "assignments": [ { "ref": "t_task_23", "value": 0 } ] } ] }, { "location": "proc_3_010", "guard": { "op": "=", "left": "t_task_31", "right": 5 }, "destinations": [ { "location": "proc_3_000" } ] }, { "location": "proc_3_010", "guard": { "op": "≥", "left": 5, "right": "t_task_31" }, "destinations": [ { "location": "proc_3_011", "assignments": [ { "ref": "t_task_41", "value": 0 } ] } ] }, { "location": "proc_3_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_001", "guard": { "op": "≥", "left": 80, "right": "t_task_41" }, "destinations": [ { "location": "proc_3_101", "assignments": [ { "ref": "t_task_23", "value": 0 } ] } ] }, { "location": "proc_3_001", "guard": { "op": "≥", "left": 80, "right": "t_task_41" }, "destinations": [ { "location": "proc_3_011", "assignments": [ { "ref": "t_task_31", "value": 0 } ] } ] }, { "location": "proc_3_001", "guard": { "op": "=", "left": "t_task_41", "right": 80 }, "destinations": [ { "location": "proc_3_000" } ] }, { "location": "proc_3_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_110", "guard": { "op": "=", "left": "t_task_23", "right": 15 }, "destinations": [ { "location": "proc_3_010" } ] }, { "location": "proc_3_110", "guard": { "op": "=", "left": "t_task_31", "right": 5 }, "destinations": [ { "location": "proc_3_100" } ] }, { "location": "proc_3_110", "guard": { "op": "≥", "left": 5, "right": "t_task_31" }, "destinations": [ { "location": "proc_3_111", "assignments": [ { "ref": "t_task_41", "value": 0 } ] } ] }, { "location": "proc_3_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_101", "guard": { "op": "=", "left": "t_task_23", "right": 15 }, "destinations": [ { "location": "proc_3_001" } ] }, { "location": "proc_3_101", "guard": { "op": "≥", "left": 15, "right": "t_task_23" }, "destinations": [ { "location": "proc_3_111", "assignments": [ { "ref": "t_task_31", "value": 0 } ] } ] }, { "location": "proc_3_101", "guard": { "op": "=", "left": "t_task_41", "right": 80 }, "destinations": [ { "location": "proc_3_100" } ] }, { "location": "proc_3_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_011", "guard": { "op": "≥", "left": 5, "right": "t_task_31" }, "destinations": [ { "location": "proc_3_111", "assignments": [ { "ref": "t_task_23", "value": 0 } ] } ] }, { "location": "proc_3_011", "guard": { "op": "=", "left": "t_task_31", "right": 5 }, "destinations": [ { "location": "proc_3_001" } ] }, { "location": "proc_3_011", "guard": { "op": "=", "left": "t_task_41", "right": 80 }, "destinations": [ { "location": "proc_3_010" } ] }, { "location": "proc_3_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_4", "right": 200 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_3", "right": 30 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 150 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 80, "right": "t_task_41" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 20 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_111", "guard": { "op": "=", "left": "t_task_23", "right": 15 }, "destinations": [ { "location": "proc_3_011" } ] }, { "location": "proc_3_111", "guard": { "op": "=", "left": "t_task_31", "right": 5 }, "destinations": [ { "location": "proc_3_101" } ] }, { "location": "proc_3_111", "guard": { "op": "=", "left": "t_task_41", "right": 80 }, "destinations": [ { "location": "proc_3_110" } ] } ] } ], "system": { "elements": [ { "automaton": "pipeline_1" }, { "automaton": "pipeline_2" }, { "automaton": "pipeline_3" }, { "automaton": "pipeline_4" }, { "automaton": "proc_1" }, { "automaton": "proc_2" }, { "automaton": "proc_3" } ], "syncs": [ { "synchronise": [ "pipeline_restart_1", null, null, null, null, null, null ], "result": "pipeline_restart_1" }, { "synchronise": [ "task_11_act", null, null, null, "task_11_act", null, null ], "result": "task_11_act" }, { "synchronise": [ "task_11_done", null, null, null, "task_11_done", null, null ], "result": "task_11_done" }, { "synchronise": [ null, "pipeline_restart_2", null, null, null, null, null ], "result": "pipeline_restart_2" }, { "synchronise": [ null, "task_21_act", null, null, "task_21_act", null, null ], "result": "task_21_act" }, { "synchronise": [ null, "task_21_done", null, null, "task_21_done", null, null ], "result": "task_21_done" }, { "synchronise": [ null, "task_22_act", null, null, null, "task_22_act", null ], "result": "task_22_act" }, { "synchronise": [ null, "task_22_done", null, null, null, "task_22_done", null ], "result": "task_22_done" }, { "synchronise": [ null, "task_23_act", null, null, null, null, "task_23_act" ], "result": "task_23_act" }, { "synchronise": [ null, "task_23_done", null, null, null, null, "task_23_done" ], "result": "task_23_done" }, { "synchronise": [ null, "task_24_act", null, null, null, "task_24_act", null ], "result": "task_24_act" }, { "synchronise": [ null, "task_24_done", null, null, null, "task_24_done", null ], "result": "task_24_done" }, { "synchronise": [ null, "task_25_act", null, null, "task_25_act", null, null ], "result": "task_25_act" }, { "synchronise": [ null, "task_25_done", null, null, "task_25_done", null, null ], "result": "task_25_done" }, { "synchronise": [ null, null, "pipeline_restart_3", null, null, null, null ], "result": "pipeline_restart_3" }, { "synchronise": [ null, null, "task_31_act", null, null, null, "task_31_act" ], "result": "task_31_act" }, { "synchronise": [ null, null, "task_31_done", null, null, null, "task_31_done" ], "result": "task_31_done" }, { "synchronise": [ null, null, null, "pipeline_restart_4", null, null, null ], "result": "pipeline_restart_4" }, { "synchronise": [ null, null, null, "task_41_act", null, null, "task_41_act" ], "result": "task_41_act" }, { "synchronise": [ null, null, null, "task_41_done", null, null, "task_41_done" ], "result": "task_41_done" }, { "synchronise": [ null, null, null, null, "DEADLINE_MISSED_1", null, null ], "result": "DEADLINE_MISSED_1" }, { "synchronise": [ null, null, null, null, null, "DEADLINE_MISSED_2", null ], "result": "DEADLINE_MISSED_2" }, { "synchronise": [ null, null, null, null, null, null, "DEADLINE_MISSED_3" ], "result": "DEADLINE_MISSED_3" } ] } }