{ "jani-version": 1, "name": "Scheduling/distributed_systems/SSLAF13_2/SSLAF13_test2.imi", "type": "sha", "features": [ "derived-operators" ], "actions": [ { "name": "pipeline_restart_1" }, { "name": "task_11_act" }, { "name": "task_11_done" }, { "name": "task_12_act" }, { "name": "task_12_done" }, { "name": "task_13_act" }, { "name": "task_13_done" }, { "name": "task_14_act" }, { "name": "task_14_done" }, { "name": "task_15_act" }, { "name": "task_15_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": "DEADLINE_MISSED_1" }, { "name": "DEADLINE_MISSED_2" }, { "name": "DEADLINE_MISSED_3" }, { "name": "DEADLINE_MISSED_4" } ], "variables": [ { "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_15", "type": "continuous", "initial_value": 0 }, { "name": "t_task_14", "type": "continuous", "initial_value": 0 }, { "name": "t_task_13", "type": "continuous", "initial_value": 0 }, { "name": "t_task_12", "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": "Token_14", "type": "real", "initial_value": 0 }, { "name": "Token_12", "type": "real", "initial_value": 0 }, { "name": "C_task_11", "type": "real" }, { "name": "C_task_15", "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 200000, "right": "t_pipeline_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 0, "right": "t_asap_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_4", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 200000, "right": "t_pipeline_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_6", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 200000, "right": "t_pipeline_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_8", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 200000, "right": "t_pipeline_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_9", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "t_asap_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_10", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 200000, "right": "t_pipeline_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_11", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 31250, "right": "t_pipeline_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 200000, "right": "t_pipeline_1" }, "destinations": [ { "location": "P1_3", "assignments": [ { "ref": "t_asap_1", "value": 0 } ] } ] }, { "location": "P1_3", "guard": { "op": "=", "left": "t_asap_1", "right": 0 }, "destinations": [ { "location": "P1_4" } ] }, { "location": "P1_4", "guard": { "op": ">", "left": 200000, "right": "t_pipeline_1" }, "destinations": [ { "location": "P1_5", "assignments": [ { "ref": "t_asap_1", "value": 0 } ] } ] }, { "location": "P1_5", "guard": { "op": "=", "left": "t_asap_1", "right": 0 }, "destinations": [ { "location": "P1_6" } ] }, { "location": "P1_6", "guard": { "op": ">", "left": 200000, "right": "t_pipeline_1" }, "destinations": [ { "location": "P1_7", "assignments": [ { "ref": "t_asap_1", "value": 0 } ] } ] }, { "location": "P1_7", "guard": { "op": "=", "left": "t_asap_1", "right": 0 }, "destinations": [ { "location": "P1_8" } ] }, { "location": "P1_8", "guard": { "op": ">", "left": 200000, "right": "t_pipeline_1" }, "destinations": [ { "location": "P1_9", "assignments": [ { "ref": "t_asap_1", "value": 0 } ] } ] }, { "location": "P1_9", "guard": { "op": "=", "left": "t_asap_1", "right": 0 }, "destinations": [ { "location": "P1_10" } ] }, { "location": "P1_10", "guard": { "op": ">", "left": 200000, "right": "t_pipeline_1" }, "destinations": [ { "location": "P1_11", "assignments": [ { "ref": "t_asap_1", "value": 0 } ] } ] }, { "location": "P1_11", "guard": { "op": "=", "left": "t_pipeline_1", "right": 31250 }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 1000000, "right": "t_pipeline_2" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 1000000, "right": "t_pipeline_2" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 1000000, "right": "t_pipeline_2" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 1000000, "right": "t_pipeline_2" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 1000000, "right": "t_pipeline_2" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 3000000, "right": "t_pipeline_2" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 1000000, "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": 1000000, "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": 1000000, "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": 1000000, "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": 1000000, "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": 3000000 }, "destinations": [ { "location": "P2_1", "assignments": [ { "ref": "t_pipeline_2", "value": 0 }, { "ref": "t_asap_2", "value": 0 } ] } ] } ] }, { "name": "proc_1", "locations": [ { "name": "DEADLINE_MISS", "time-progress": { "exp": { "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_15", "right": "t_task_15" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 22728, "right": "t_task_25" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_15", "right": "t_task_15" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_15", "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": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_100", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "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_15", "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": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_010", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_010", "guard": { "op": "≥", "left": "C_task_15", "right": "t_task_15" }, "destinations": [ { "location": "proc_1_110", "assignments": [ { "ref": "t_task_11", "value": 0 } ] } ] }, { "location": "proc_1_010", "guard": { "op": "=", "left": "C_task_15", "right": "t_task_15" }, "destinations": [ { "location": "proc_1_000" } ] }, { "location": "proc_1_010", "guard": { "op": "≥", "left": "C_task_15", "right": "t_task_15" }, "destinations": [ { "location": "proc_1_011", "assignments": [ { "ref": "t_task_25", "value": 0 } ] } ] }, { "location": "proc_1_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_001", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_001", "guard": { "op": "≥", "left": 22728, "right": "t_task_25" }, "destinations": [ { "location": "proc_1_101", "assignments": [ { "ref": "t_task_11", "value": 0 } ] } ] }, { "location": "proc_1_001", "guard": { "op": "≥", "left": 22728, "right": "t_task_25" }, "destinations": [ { "location": "proc_1_011", "assignments": [ { "ref": "t_task_15", "value": 0 } ] } ] }, { "location": "proc_1_001", "guard": { "op": "=", "left": "t_task_25", "right": 22728 }, "destinations": [ { "location": "proc_1_000" } ] }, { "location": "proc_1_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_110", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "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_15", "right": "t_task_15" }, "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": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_101", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "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_15", "value": 0 } ] } ] }, { "location": "proc_1_101", "guard": { "op": "=", "left": "t_task_25", "right": 22728 }, "destinations": [ { "location": "proc_1_100" } ] }, { "location": "proc_1_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_011", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_011", "guard": { "op": "≥", "left": "C_task_15", "right": "t_task_15" }, "destinations": [ { "location": "proc_1_111", "assignments": [ { "ref": "t_task_11", "value": 0 } ] } ] }, { "location": "proc_1_011", "guard": { "op": "=", "left": "C_task_15", "right": "t_task_15" }, "destinations": [ { "location": "proc_1_001" } ] }, { "location": "proc_1_011", "guard": { "op": "=", "left": "t_task_25", "right": 22728 }, "destinations": [ { "location": "proc_1_010" } ] }, { "location": "proc_1_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_1_111", "guard": { "op": "∧", "left": { "op": "≥", "left": 22728, "right": "t_task_25" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "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_15", "right": "t_task_15" }, "destinations": [ { "location": "proc_1_101" } ] }, { "location": "proc_1_111", "guard": { "op": "=", "left": "t_task_25", "right": 22728 }, "destinations": [ { "location": "proc_1_110" } ] } ] }, { "name": "proc_2", "locations": [ { "name": "idle", "time-progress": { "exp": { "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_12_running", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 445, "right": "t_task_12" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_14_running", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 445, "right": "t_task_14" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 889, "right": "t_task_22" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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": 889, "right": "t_task_24" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_12_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "idle", "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "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_12_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 445, "right": "t_task_12" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 445, "right": "t_task_12" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_12_running", "guard": { "op": "≥", "left": "t_task_12", "right": 0 }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": ">", "left": 0, "right": "t_task_12" }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": "≥", "left": "t_task_12", "right": 0 }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": ">", "left": 0, "right": "t_task_12" }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": "≥", "left": "t_task_12", "right": 0 }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": ">", "left": 0, "right": "t_task_12" }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": "≥", "left": "t_task_12", "right": 0 }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": ">", "left": 0, "right": "t_task_12" }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "t_task_22", "value": 0 }, { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "t_task_24", "value": 0 }, { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "t_task_22", "value": 0 }, { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_12_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_12", "right": 445 } } } }, "destinations": [ { "location": "idle", "assignments": [ { "ref": "Token_12", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 445, "right": "t_task_14" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 445, "right": "t_task_14" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_14_running", "guard": { "op": "≥", "left": "t_task_14", "right": 0 }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": ">", "left": 0, "right": "t_task_14" }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": "≥", "left": "t_task_14", "right": 0 }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": ">", "left": 0, "right": "t_task_14" }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": "≥", "left": "t_task_14", "right": 0 }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": ">", "left": 0, "right": "t_task_14" }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_22", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": "≥", "left": "t_task_14", "right": 0 }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": ">", "left": 0, "right": "t_task_14" }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_24", "value": 1 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "t_task_22", "value": 0 }, { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "t_task_24", "value": 0 }, { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "t_task_22", "value": 0 }, { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_14_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_14", "right": 445 } } } }, "destinations": [ { "location": "idle", "assignments": [ { "ref": "Token_14", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 889, "right": "t_task_22" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 889, "right": "t_task_22" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_22_running", "guard": { "op": "≥", "left": "t_task_22", "right": 0 }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": ">", "left": 0, "right": "t_task_22" }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": "≥", "left": "t_task_22", "right": 0 }, "destinations": [ { "location": "t_22_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "location": "t_22_running", "guard": { "op": ">", "left": 0, "right": "t_task_22" }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "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_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 1 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "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_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_22_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_24", "right": 0 }, "right": { "op": "=", "left": "t_task_22", "right": 889 } } } }, "destinations": [ { "location": "idle", "assignments": [ { "ref": "Token_22", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 889, "right": "t_task_24" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "≥", "left": 889, "right": "t_task_24" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "t_24_running", "guard": { "op": "≥", "left": "t_task_24", "right": 0 }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_24_running", "guard": { "op": ">", "left": 0, "right": "t_task_24" }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "Token_12", "value": 1 } ] } ] }, { "location": "t_24_running", "guard": { "op": "≥", "left": "t_task_24", "right": 0 }, "destinations": [ { "location": "t_24_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "location": "t_24_running", "guard": { "op": ">", "left": 0, "right": "t_task_24" }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "Token_14", "value": 1 } ] } ] }, { "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_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_24", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_24", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_24", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_24", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 1 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "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_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "destinations": [ { "location": "t_14_running", "assignments": [ { "ref": "t_task_14", "value": 0 }, { "ref": "Token_24", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "destinations": [ { "location": "t_12_running", "assignments": [ { "ref": "t_task_12", "value": 0 }, { "ref": "Token_24", "value": 0 } ] } ] }, { "location": "t_24_running", "guard": { "op": "∧", "left": { "op": "=", "left": "Token_12", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_14", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "Token_22", "right": 0 }, "right": { "op": "=", "left": "t_task_24", "right": 889 } } } }, "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_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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_0", "time-progress": { "exp": { "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_1", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 44248, "right": "t_task_23" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_0" ], "edges": [ { "location": "proc_3_0", "destinations": [ { "location": "proc_3_1", "assignments": [ { "ref": "t_task_23", "value": 0 } ] } ] }, { "location": "proc_3_1", "guard": { "op": "∧", "left": { "op": "≥", "left": 44248, "right": "t_task_23" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_1", "guard": { "op": "∧", "left": { "op": "≥", "left": 44248, "right": "t_task_23" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_3_1", "guard": { "op": "=", "left": "t_task_23", "right": 44248 }, "destinations": [ { "location": "proc_3_0" } ] } ] }, { "name": "proc_4", "locations": [ { "name": "DEADLINE_MISS", "time-progress": { "exp": { "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_4_00", "time-progress": { "exp": { "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_4_10", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 9091, "right": "t_task_13" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_4_01", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 90910, "right": "t_task_21" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_4_11", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 9091, "right": "t_task_13" }, "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_15" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_14" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_13" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t_task_12" }, "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_4_00" ], "edges": [ { "location": "proc_4_00", "destinations": [ { "location": "proc_4_10", "assignments": [ { "ref": "t_task_13", "value": 0 } ] } ] }, { "location": "proc_4_00", "destinations": [ { "location": "proc_4_01", "assignments": [ { "ref": "t_task_21", "value": 0 } ] } ] }, { "location": "proc_4_10", "guard": { "op": "∧", "left": { "op": "≥", "left": 90910, "right": "t_task_21" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_4_10", "guard": { "op": "∧", "left": { "op": "≥", "left": 90910, "right": "t_task_21" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_4_10", "guard": { "op": "=", "left": "t_task_13", "right": 9091 }, "destinations": [ { "location": "proc_4_00" } ] }, { "location": "proc_4_10", "guard": { "op": "≥", "left": 9091, "right": "t_task_13" }, "destinations": [ { "location": "proc_4_11", "assignments": [ { "ref": "t_task_21", "value": 0 } ] } ] }, { "location": "proc_4_01", "guard": { "op": "∧", "left": { "op": "≥", "left": 90910, "right": "t_task_21" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_4_01", "guard": { "op": "∧", "left": { "op": "≥", "left": 90910, "right": "t_task_21" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_4_01", "guard": { "op": "≥", "left": 90910, "right": "t_task_21" }, "destinations": [ { "location": "proc_4_11", "assignments": [ { "ref": "t_task_13", "value": 0 } ] } ] }, { "location": "proc_4_01", "guard": { "op": "=", "left": "t_task_21", "right": 90910 }, "destinations": [ { "location": "proc_4_00" } ] }, { "location": "proc_4_11", "guard": { "op": "∧", "left": { "op": "≥", "left": 90910, "right": "t_task_21" }, "right": { "op": "=", "left": "t_pipeline_2", "right": 1000000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_4_11", "guard": { "op": "∧", "left": { "op": "≥", "left": 90910, "right": "t_task_21" }, "right": { "op": "=", "left": "t_pipeline_1", "right": 200000 } }, "destinations": [ { "location": "DEADLINE_MISS" } ] }, { "location": "proc_4_11", "guard": { "op": "=", "left": "t_task_13", "right": 9091 }, "destinations": [ { "location": "proc_4_01" } ] }, { "location": "proc_4_11", "guard": { "op": "=", "left": "t_task_21", "right": 90910 }, "destinations": [ { "location": "proc_4_10" } ] } ] } ], "system": { "elements": [ { "automaton": "pipeline_1" }, { "automaton": "pipeline_2" }, { "automaton": "proc_1" }, { "automaton": "proc_2" }, { "automaton": "proc_3" }, { "automaton": "proc_4" } ], "syncs": [ { "synchronise": [ "pipeline_restart_1", null, null, null, null, null ], "result": "pipeline_restart_1" }, { "synchronise": [ "task_11_act", null, "task_11_act", null, null, null ], "result": "task_11_act" }, { "synchronise": [ "task_11_done", null, "task_11_done", null, null, null ], "result": "task_11_done" }, { "synchronise": [ "task_12_act", null, null, "task_12_act", null, null ], "result": "task_12_act" }, { "synchronise": [ "task_12_done", null, null, "task_12_done", null, null ], "result": "task_12_done" }, { "synchronise": [ "task_13_act", null, null, null, null, "task_13_act" ], "result": "task_13_act" }, { "synchronise": [ "task_13_done", null, null, null, null, "task_13_done" ], "result": "task_13_done" }, { "synchronise": [ "task_14_act", null, null, "task_14_act", null, null ], "result": "task_14_act" }, { "synchronise": [ "task_14_done", null, null, "task_14_done", null, null ], "result": "task_14_done" }, { "synchronise": [ "task_15_act", null, "task_15_act", null, null, null ], "result": "task_15_act" }, { "synchronise": [ "task_15_done", null, "task_15_done", null, null, null ], "result": "task_15_done" }, { "synchronise": [ null, "pipeline_restart_2", null, null, null, null ], "result": "pipeline_restart_2" }, { "synchronise": [ null, "task_21_act", null, null, null, "task_21_act" ], "result": "task_21_act" }, { "synchronise": [ null, "task_21_done", null, null, null, "task_21_done" ], "result": "task_21_done" }, { "synchronise": [ null, "task_22_act", null, "task_22_act", null, null ], "result": "task_22_act" }, { "synchronise": [ null, "task_22_done", null, "task_22_done", null, null ], "result": "task_22_done" }, { "synchronise": [ null, "task_23_act", null, null, "task_23_act", null ], "result": "task_23_act" }, { "synchronise": [ null, "task_23_done", null, null, "task_23_done", null ], "result": "task_23_done" }, { "synchronise": [ null, "task_24_act", null, "task_24_act", null, null ], "result": "task_24_act" }, { "synchronise": [ null, "task_24_done", null, "task_24_done", null, null ], "result": "task_24_done" }, { "synchronise": [ null, "task_25_act", "task_25_act", null, null, null ], "result": "task_25_act" }, { "synchronise": [ null, "task_25_done", "task_25_done", null, null, null ], "result": "task_25_done" }, { "synchronise": [ null, null, "DEADLINE_MISSED_1", null, null, null ], "result": "DEADLINE_MISSED_1" }, { "synchronise": [ null, null, null, "DEADLINE_MISSED_2", null, null ], "result": "DEADLINE_MISSED_2" }, { "synchronise": [ null, null, null, null, "DEADLINE_MISSED_3", null ], "result": "DEADLINE_MISSED_3" }, { "synchronise": [ null, null, null, null, null, "DEADLINE_MISSED_4" ], "result": "DEADLINE_MISSED_4" } ] } }