{ "jani-version": 1, "name": "Scheduling/Thales/AVTS_imitator.imi", "type": "sha", "features": [ "derived-operators", "arrays", "datatypes", "functions" ], "datatypes": [ { "name": "binary_word", "members": [ { "name": "elements", "type": { "kind": "array", "base": "bool" } } ] } ], "functions": [], "actions": [ { "name": "recommence_T2_1" }, { "name": "lance_T2_1" }, { "name": "fin_T2_1" }, { "name": "recommence_T6_1" }, { "name": "lance_T6_1" }, { "name": "fin_T6_1" }, { "name": "lance_T5_1" }, { "name": "fin_T5_1" }, { "name": "fin_T6_2" }, { "name": "lance_T6_2" }, { "name": "fin_T6_3" }, { "name": "lance_T6_3" }, { "name": "lance_T7_1" }, { "name": "fin_T7_1" }, { "name": "obs1_bloc" }, { "name": "obs2_bloc" } ], "variables": [ { "name": "x2p", "type": "continuous", "initial-value": 0 }, { "name": "x2", "type": "continuous", "initial-value": 0 }, { "name": "x6p", "type": "continuous", "initial-value": 0 }, { "name": "x61", "type": "continuous", "initial-value": 0 }, { "name": "x5", "type": "continuous", "initial-value": 0 }, { "name": "x62", "type": "continuous", "initial-value": 0 }, { "name": "x63", "type": "continuous", "initial-value": 0 }, { "name": "x7", "type": "continuous", "initial-value": 0 }, { "name": "t1", "type": "continuous", "initial-value": 0 }, { "name": "t2", "type": "continuous", "initial-value": 0 }, { "name": "c2", "type": "int", "initial-value": 0 }, { "name": "c61", "type": "int", "initial-value": 0 }, { "name": "c5", "type": "int", "initial-value": 0 }, { "name": "c62", "type": "int", "initial-value": 0 }, { "name": "c63", "type": "int", "initial-value": 0 }, { "name": "c7", "type": "int", "initial-value": 0 }, { "name": "chemin_T6_1", "type": "int", "initial-value": 1 }, { "name": "chemin_T7_1", "type": "int", "initial-value": 1 }, { "name": "WT", "type": "real" } ], "properties": [], "automata": [ { "name": "periodic_event_T2_1", "locations": [ { "name": "p20", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 0, "right": "x2p" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } }, { "name": "p2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 40, "right": "x2p" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } } ], "initial-locations": [ "p20" ], "edges": [ { "location": "p20", "action": "nosync_1", "guard": { "exp": { "op": ">", "left": "x2p", "right": 0 } }, "destinations": [ { "location": "p2", "assignments": [ { "ref": "x2p", "value": 0 } ] } ] }, { "location": "p2", "action": "recommence_T2_1", "guard": { "exp": { "op": "=", "left": "x2p", "right": 40 } }, "destinations": [ { "location": "p2", "assignments": [ { "ref": "x2p", "value": 0 } ] } ] } ] }, { "name": "memoire_lancement_T2_1", "locations": [ { "name": "m20", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "m21", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "m20" ], "edges": [ { "location": "m20", "action": "recommence_T2_1", "destinations": [ { "location": "m21", "assignments": [ { "ref": "c2", "value": { "op": "+", "left": "c2", "right": 1 } } ] } ] }, { "location": "m20", "action": "fin_T2_1", "destinations": [ { "location": "m21", "assignments": [ { "ref": "c2", "value": { "op": "-", "left": "c2", "right": 1 } } ] } ] }, { "location": "m21", "action": "lance_T2_1", "guard": { "exp": { "op": "=", "left": "c2", "right": 1 } }, "destinations": [ { "location": "m20" } ] }, { "location": "m21", "action": "nosync_2", "guard": { "exp": { "op": "≠", "left": "c2", "right": 1 } }, "destinations": [ { "location": "m20" } ] } ] }, { "name": "periodic_event_T6_1", "locations": [ { "name": "p60", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 100, "right": "x6p" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } }, { "name": "p61", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 30, "right": "x6p" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } } ], "initial-locations": [ "p60" ], "edges": [ { "location": "p60", "action": "nosync_3", "guard": { "exp": { "op": "=", "left": "x6p", "right": 100 } }, "destinations": [ { "location": "p61", "assignments": [ { "ref": "x6p", "value": 0 } ] } ] }, { "location": "p61", "action": "recommence_T6_1", "destinations": [ { "location": "p60" } ] } ] }, { "name": "memoire_lancement_T6_1", "locations": [ { "name": "m610", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "m611", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "obs61", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "m610" ], "edges": [ { "location": "m610", "action": "recommence_T6_1", "destinations": [ { "location": "m611", "assignments": [ { "ref": "c61", "value": { "op": "+", "left": "c61", "right": 1 } } ] } ] }, { "location": "m610", "action": "fin_T6_1", "destinations": [ { "location": "obs61", "assignments": [ { "ref": "c61", "value": { "op": "-", "left": "c61", "right": 1 } } ] } ] }, { "location": "m611", "action": "lance_T6_1", "guard": { "exp": { "op": "=", "left": "c61", "right": 1 } }, "destinations": [ { "location": "m610" } ] }, { "location": "m611", "action": "nosync_4", "guard": { "exp": { "op": "≠", "left": "c61", "right": 1 } }, "destinations": [ { "location": "m610" } ] }, { "location": "obs61", "action": "nosync_5", "guard": { "exp": { "op": "=", "left": "chemin_T6_1", "right": 1 } }, "destinations": [ { "location": "m611", "assignments": [ { "ref": "chemin_T6_1", "value": 2 } ] } ] }, { "location": "obs61", "action": "nosync_6", "guard": { "exp": { "op": "=", "left": "chemin_T6_1", "right": 2 } }, "destinations": [ { "location": "m611", "assignments": [ { "ref": "chemin_T6_1", "value": 1 } ] } ] } ] }, { "name": "memoire_lancement_T5_1", "locations": [ { "name": "m510", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "m511", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "m510" ], "edges": [ { "location": "m510", "action": "fin_T6_1", "destinations": [ { "location": "m511", "assignments": [ { "ref": "c5", "value": { "op": "+", "left": "c5", "right": 1 } } ] } ] }, { "location": "m510", "action": "fin_T5_1", "destinations": [ { "location": "m511", "assignments": [ { "ref": "c5", "value": { "op": "-", "left": "c5", "right": 1 } } ] } ] }, { "location": "m511", "action": "lance_T5_1", "guard": { "exp": { "op": "=", "left": "c5", "right": 1 } }, "destinations": [ { "location": "m510" } ] }, { "location": "m511", "action": "nosync_7", "guard": { "exp": { "op": "≠", "left": "c5", "right": 1 } }, "destinations": [ { "location": "m510" } ] } ] }, { "name": "memoire_lancement_T6_2", "locations": [ { "name": "m620", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "m621", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "m620" ], "edges": [ { "location": "m620", "action": "fin_T5_1", "destinations": [ { "location": "m621", "assignments": [ { "ref": "c62", "value": { "op": "+", "left": "c62", "right": 1 } } ] } ] }, { "location": "m620", "action": "fin_T6_2", "destinations": [ { "location": "m621", "assignments": [ { "ref": "c62", "value": { "op": "-", "left": "c62", "right": 1 } } ] } ] }, { "location": "m621", "action": "lance_T6_2", "guard": { "exp": { "op": "=", "left": "c62", "right": 1 } }, "destinations": [ { "location": "m620" } ] }, { "location": "m621", "action": "nosync_8", "guard": { "exp": { "op": "≠", "left": "c62", "right": 1 } }, "destinations": [ { "location": "m620" } ] } ] }, { "name": "memoire_lancement_T6_3", "locations": [ { "name": "m630", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "m631", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "m630" ], "edges": [ { "location": "m630", "action": "fin_T6_2", "destinations": [ { "location": "m631", "assignments": [ { "ref": "c63", "value": { "op": "+", "left": "c63", "right": 1 } } ] } ] }, { "location": "m630", "action": "fin_T6_3", "destinations": [ { "location": "m631", "assignments": [ { "ref": "c63", "value": { "op": "-", "left": "c63", "right": 1 } } ] } ] }, { "location": "m631", "action": "lance_T6_3", "guard": { "exp": { "op": "=", "left": "c63", "right": 1 } }, "destinations": [ { "location": "m630" } ] }, { "location": "m631", "action": "nosync_9", "guard": { "exp": { "op": "≠", "left": "c63", "right": 1 } }, "destinations": [ { "location": "m630" } ] } ] }, { "name": "memoire_lancement_T7_1", "locations": [ { "name": "m70", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "m71", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "obs7", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "m70" ], "edges": [ { "location": "m70", "action": "fin_T6_2", "destinations": [ { "location": "m71", "assignments": [ { "ref": "c7", "value": { "op": "+", "left": "c7", "right": 1 } } ] } ] }, { "location": "m70", "action": "fin_T7_1", "destinations": [ { "location": "obs7", "assignments": [ { "ref": "c7", "value": { "op": "-", "left": "c7", "right": 1 } } ] } ] }, { "location": "m71", "action": "lance_T7_1", "guard": { "exp": { "op": "=", "left": "c7", "right": 1 } }, "destinations": [ { "location": "m70" } ] }, { "location": "m71", "action": "nosync_10", "guard": { "exp": { "op": "≠", "left": "c7", "right": 1 } }, "destinations": [ { "location": "m70" } ] }, { "location": "obs7", "action": "nosync_11", "guard": { "exp": { "op": "=", "left": "chemin_T7_1", "right": 1 } }, "destinations": [ { "location": "m71", "assignments": [ { "ref": "chemin_T7_1", "value": 2 } ] } ] }, { "location": "obs7", "action": "nosync_12", "guard": { "exp": { "op": "=", "left": "chemin_T7_1", "right": 2 } }, "destinations": [ { "location": "m71", "assignments": [ { "ref": "chemin_T7_1", "value": 1 } ] } ] } ] }, { "name": "tasks", "locations": [ { "name": "l0", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "l2", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 17, "right": "x2" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } }, { "name": "l2U", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "l63", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 5, "right": "x63" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } }, { "name": "l63U", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "l62", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 10, "right": "x62" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } }, { "name": "l62U", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "l61", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 4, "right": "x61" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } }, { "name": "l61U", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "l5", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 7, "right": "x5" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } }, { "name": "l5U", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "l7", "time-progress": { "exp": { "op": "∧", "left": { "op": ">", "left": 14, "right": "x7" }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } } ], "initial-locations": [ "l0" ], "edges": [ { "location": "l0", "action": "lance_T2_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "l0", "action": "lance_T6_1", "destinations": [ { "location": "l61", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l0", "action": "lance_T5_1", "destinations": [ { "location": "l5", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l0", "action": "lance_T6_2", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l0", "action": "lance_T6_3", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l0", "action": "lance_T7_1", "destinations": [ { "location": "l7", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l2", "action": "lance_T2_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "l2", "action": "fin_T2_1", "guard": { "exp": { "op": ">", "left": "x2", "right": 17 } }, "destinations": [ { "location": "l2U" } ] }, { "location": "l2", "action": "lance_T6_3", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l2", "action": "lance_T6_2", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l2", "action": "lance_T6_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l2", "action": "lance_T5_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l2", "action": "lance_T7_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l2U", "action": "nosync_13", "guard": { "exp": { "op": "≥", "left": "c63", "right": 0 } }, "destinations": [ { "location": "l63" } ] }, { "location": "l2U", "action": "nosync_14", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c63", "right": 0 }, "right": { "op": "≥", "left": "c62", "right": 0 } } }, "destinations": [ { "location": "l62" } ] }, { "location": "l2U", "action": "nosync_15", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c63", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "≥", "left": "c61", "right": 0 } } } }, "destinations": [ { "location": "l61" } ] }, { "location": "l2U", "action": "nosync_16", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c63", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "≥", "left": "c5", "right": 0 } } } } }, "destinations": [ { "location": "l5" } ] }, { "location": "l2U", "action": "nosync_17", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c63", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "≥", "left": "c7", "right": 0 } } } } } }, "destinations": [ { "location": "l7" } ] }, { "location": "l2U", "action": "nosync_18", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c63", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "=", "left": "c7", "right": 0 } } } } } }, "destinations": [ { "location": "l0" } ] }, { "location": "l2U", "action": "lance_T6_3", "destinations": [ { "location": "l2U", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l2U", "action": "lance_T6_2", "destinations": [ { "location": "l2U", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l2U", "action": "lance_T6_1", "destinations": [ { "location": "l2U", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l2U", "action": "lance_T5_1", "destinations": [ { "location": "l2U", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l2U", "action": "lance_T7_1", "destinations": [ { "location": "l2U", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l63", "action": "lance_T2_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "l63", "action": "lance_T6_3", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l63", "action": "fin_T6_3", "guard": { "exp": { "op": ">", "left": "x63", "right": 4 } }, "destinations": [ { "location": "l63U" } ] }, { "location": "l63", "action": "lance_T6_2", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l63", "action": "lance_T6_1", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l63", "action": "lance_T5_1", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l63", "action": "lance_T7_1", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l63U", "action": "nosync_19", "guard": { "exp": { "op": "≥", "left": "c62", "right": 0 } }, "destinations": [ { "location": "l62" } ] }, { "location": "l63U", "action": "nosync_20", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "≥", "left": "c61", "right": 0 } } }, "destinations": [ { "location": "l61" } ] }, { "location": "l63U", "action": "nosync_21", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "≥", "left": "c5", "right": 0 } } } }, "destinations": [ { "location": "l5" } ] }, { "location": "l63U", "action": "nosync_22", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "≥", "left": "c7", "right": 0 } } } } }, "destinations": [ { "location": "l7" } ] }, { "location": "l63U", "action": "nosync_23", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c62", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "=", "left": "c7", "right": 0 } } } } }, "destinations": [ { "location": "l0" } ] }, { "location": "l63U", "action": "lance_T6_2", "destinations": [ { "location": "l63U", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l63U", "action": "lance_T6_1", "destinations": [ { "location": "l63U", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l63U", "action": "lance_T5_1", "destinations": [ { "location": "l63U", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l63U", "action": "lance_T7_1", "destinations": [ { "location": "l63U", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l62", "action": "lance_T2_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "l62", "action": "lance_T6_3", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l62", "action": "lance_T6_2", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l62", "action": "fin_T6_2", "guard": { "exp": { "op": ">", "left": "x62", "right": 9 } }, "destinations": [ { "location": "l62U" } ] }, { "location": "l62", "action": "lance_T6_1", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l62", "action": "lance_T5_1", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l62", "action": "lance_T7_1", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l62U", "action": "nosync_24", "guard": { "exp": { "op": "≥", "left": "c61", "right": 0 } }, "destinations": [ { "location": "l61" } ] }, { "location": "l62U", "action": "nosync_25", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "≥", "left": "c5", "right": 0 } } }, "destinations": [ { "location": "l5" } ] }, { "location": "l62U", "action": "nosync_26", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "≥", "left": "c7", "right": 0 } } } }, "destinations": [ { "location": "l7" } ] }, { "location": "l62U", "action": "nosync_27", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c61", "right": 0 }, "right": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "=", "left": "c7", "right": 0 } } } }, "destinations": [ { "location": "l0" } ] }, { "location": "l62U", "action": "lance_T6_1", "destinations": [ { "location": "l62U", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l62U", "action": "lance_T5_1", "destinations": [ { "location": "l62U", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l62U", "action": "lance_T7_1", "destinations": [ { "location": "l62U", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l61", "action": "lance_T2_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "l61", "action": "lance_T6_3", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l61", "action": "lance_T6_2", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l61", "action": "lance_T6_1", "destinations": [ { "location": "l61", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l61", "action": "fin_T6_1", "guard": { "exp": { "op": ">", "left": "x61", "right": 4 } }, "destinations": [ { "location": "l61U" } ] }, { "location": "l61", "action": "lance_T5_1", "destinations": [ { "location": "l61", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l61", "action": "lance_T7_1", "destinations": [ { "location": "l61", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l61U", "action": "nosync_28", "guard": { "exp": { "op": "≥", "left": "c5", "right": 0 } }, "destinations": [ { "location": "l5" } ] }, { "location": "l61U", "action": "nosync_29", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "≥", "left": "c7", "right": 0 } } }, "destinations": [ { "location": "l7" } ] }, { "location": "l61U", "action": "nosync_30", "guard": { "exp": { "op": "∧", "left": { "op": "=", "left": "c5", "right": 0 }, "right": { "op": "=", "left": "c7", "right": 0 } } }, "destinations": [ { "location": "l0" } ] }, { "location": "l61U", "action": "lance_T5_1", "destinations": [ { "location": "l61U", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l61U", "action": "lance_T7_1", "destinations": [ { "location": "l61U", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l5", "action": "lance_T2_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "l5", "action": "lance_T6_3", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l5", "action": "lance_T6_2", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l5", "action": "lance_T6_1", "destinations": [ { "location": "l61", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l5", "action": "lance_T5_1", "destinations": [ { "location": "l5", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l5", "action": "fin_T5_1", "guard": { "exp": { "op": ">", "left": "x5", "right": 4 } }, "destinations": [ { "location": "l5U" } ] }, { "location": "l5", "action": "lance_T7_1", "destinations": [ { "location": "l5", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l5U", "action": "nosync_31", "guard": { "exp": { "op": "≥", "left": "c7", "right": 0 } }, "destinations": [ { "location": "l7" } ] }, { "location": "l5U", "action": "nosync_32", "guard": { "exp": { "op": "=", "left": "c7", "right": 0 } }, "destinations": [ { "location": "l0" } ] }, { "location": "l5U", "action": "lance_T7_1", "destinations": [ { "location": "l5U", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l7", "action": "lance_T2_1", "destinations": [ { "location": "l2", "assignments": [ { "ref": "x2", "value": 0 } ] } ] }, { "location": "l7", "action": "lance_T6_3", "destinations": [ { "location": "l63", "assignments": [ { "ref": "x63", "value": 0 } ] } ] }, { "location": "l7", "action": "lance_T6_2", "destinations": [ { "location": "l62", "assignments": [ { "ref": "x62", "value": 0 } ] } ] }, { "location": "l7", "action": "lance_T6_1", "destinations": [ { "location": "l61", "assignments": [ { "ref": "x61", "value": 0 } ] } ] }, { "location": "l7", "action": "lance_T5_1", "destinations": [ { "location": "l5", "assignments": [ { "ref": "x5", "value": 0 } ] } ] }, { "location": "l7", "action": "lance_T7_1", "destinations": [ { "location": "l7", "assignments": [ { "ref": "x7", "value": 0 } ] } ] }, { "location": "l7", "action": "fin_T7_1", "guard": { "exp": { "op": ">", "left": "x7", "right": 11 } }, "destinations": [ { "location": "l0" } ] } ] }, { "name": "Observateur1", "locations": [ { "name": "obs10", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "obs11", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "obs13", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "bloque1", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "obs10" ], "edges": [ { "location": "obs10", "action": "lance_T6_1", "guard": { "exp": { "op": "≠", "left": "chemin_T6_1", "right": 1 } }, "destinations": [ { "location": "obs10" } ] }, { "location": "obs10", "action": "lance_T6_1", "guard": { "exp": { "op": "=", "left": "chemin_T6_1", "right": 1 } }, "destinations": [ { "location": "obs11", "assignments": [ { "ref": "t1", "value": 0 } ] } ] }, { "location": "obs10", "action": "fin_T7_1", "destinations": [ { "location": "obs10" } ] }, { "location": "obs11", "action": "fin_T7_1", "guard": { "exp": { "op": "≠", "left": "chemin_T7_1", "right": 1 } }, "destinations": [ { "location": "obs11" } ] }, { "location": "obs11", "action": "fin_T7_1", "guard": { "exp": { "op": "=", "left": "chemin_T7_1", "right": 1 } }, "destinations": [ { "location": "obs13" } ] }, { "location": "obs11", "action": "lance_T6_1", "destinations": [ { "location": "obs11" } ] }, { "location": "obs13", "action": "obs1_bloc", "guard": { "exp": { "op": "≥", "left": "t1", "right": "WT" } }, "destinations": [ { "location": "bloque1" } ] }, { "location": "obs13", "action": "nosync_33", "guard": { "exp": { "op": ">", "left": "WT", "right": "t1" } }, "destinations": [ { "location": "obs10" } ] } ] }, { "name": "Observateur2", "locations": [ { "name": "obs20", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "obs21", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "obs23", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "bloque2", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "obs20" ], "edges": [ { "location": "obs20", "action": "lance_T6_1", "guard": { "exp": { "op": "≠", "left": "chemin_T6_1", "right": 2 } }, "destinations": [ { "location": "obs20" } ] }, { "location": "obs20", "action": "lance_T6_1", "guard": { "exp": { "op": "=", "left": "chemin_T6_1", "right": 2 } }, "destinations": [ { "location": "obs21", "assignments": [ { "ref": "t2", "value": 0 } ] } ] }, { "location": "obs20", "action": "fin_T7_1", "destinations": [ { "location": "obs20" } ] }, { "location": "obs21", "action": "fin_T7_1", "guard": { "exp": { "op": "≠", "left": "chemin_T7_1", "right": 2 } }, "destinations": [ { "location": "obs21" } ] }, { "location": "obs21", "action": "fin_T7_1", "guard": { "exp": { "op": "=", "left": "chemin_T7_1", "right": 2 } }, "destinations": [ { "location": "obs23" } ] }, { "location": "obs21", "action": "lance_T6_1", "destinations": [ { "location": "obs21" } ] }, { "location": "obs23", "action": "obs2_bloc", "guard": { "exp": { "op": "≥", "left": "t2", "right": "WT" } }, "destinations": [ { "location": "bloque2" } ] }, { "location": "obs23", "action": "nosync_34", "guard": { "exp": { "op": ">", "left": "WT", "right": "t2" } }, "destinations": [ { "location": "obs20" } ] } ] }, { "name": "Observateur", "locations": [ { "name": "obsI", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } }, { "name": "obsF", "time-progress": { "exp": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x2" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x6p" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x61" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x5" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x62" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x63" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "x7" }, "right": 1 }, "right": { "op": "∧", "left": { "op": "=", "left": { "op": "der", "var": "t1" }, "right": 1 }, "right": { "op": "=", "left": { "op": "der", "var": "t2" }, "right": 1 } } } } } } } } } } } } ], "initial-locations": [ "obsI" ], "edges": [ { "location": "obsI", "action": "obs1_bloc", "destinations": [ { "location": "obsF" } ] }, { "location": "obsI", "action": "obs2_bloc", "destinations": [ { "location": "obsF" } ] } ] } ], "system": { "elements": [ { "automaton": "periodic_event_T2_1" }, { "automaton": "memoire_lancement_T2_1" }, { "automaton": "periodic_event_T6_1" }, { "automaton": "memoire_lancement_T6_1" }, { "automaton": "memoire_lancement_T5_1" }, { "automaton": "memoire_lancement_T6_2" }, { "automaton": "memoire_lancement_T6_3" }, { "automaton": "memoire_lancement_T7_1" }, { "automaton": "tasks" }, { "automaton": "Observateur1" }, { "automaton": "Observateur2" }, { "automaton": "Observateur" } ], "syncs": [ { "synchronise": [ "recommence_T2_1", "recommence_T2_1", null, null, null, null, null, null, null, null, null, null ], "result": "recommence_T2_1" }, { "synchronise": [ null, "lance_T2_1", null, null, null, null, null, null, "lance_T2_1", null, null, null ], "result": "lance_T2_1" }, { "synchronise": [ null, "fin_T2_1", null, null, null, null, null, null, "fin_T2_1", null, null, null ], "result": "fin_T2_1" }, { "synchronise": [ null, null, "recommence_T6_1", "recommence_T6_1", null, null, null, null, null, null, null, null ], "result": "recommence_T6_1" }, { "synchronise": [ null, null, null, "lance_T6_1", null, null, null, null, "lance_T6_1", "lance_T6_1", "lance_T6_1", null ], "result": "lance_T6_1" }, { "synchronise": [ null, null, null, "fin_T6_1", "fin_T6_1", null, null, null, "fin_T6_1", null, null, null ], "result": "fin_T6_1" }, { "synchronise": [ null, null, null, null, "lance_T5_1", null, null, null, "lance_T5_1", null, null, null ], "result": "lance_T5_1" }, { "synchronise": [ null, null, null, null, "fin_T5_1", "fin_T5_1", null, null, "fin_T5_1", null, null, null ], "result": "fin_T5_1" }, { "synchronise": [ null, null, null, null, null, "fin_T6_2", "fin_T6_2", "fin_T6_2", "fin_T6_2", null, null, null ], "result": "fin_T6_2" }, { "synchronise": [ null, null, null, null, null, "lance_T6_2", null, null, "lance_T6_2", null, null, null ], "result": "lance_T6_2" }, { "synchronise": [ null, null, null, null, null, null, "fin_T6_3", null, "fin_T6_3", null, null, null ], "result": "fin_T6_3" }, { "synchronise": [ null, null, null, null, null, null, "lance_T6_3", null, "lance_T6_3", null, null, null ], "result": "lance_T6_3" }, { "synchronise": [ null, null, null, null, null, null, null, "lance_T7_1", "lance_T7_1", null, null, null ], "result": "lance_T7_1" }, { "synchronise": [ null, null, null, null, null, null, null, "fin_T7_1", "fin_T7_1", "fin_T7_1", "fin_T7_1", null ], "result": "fin_T7_1" }, { "synchronise": [ null, null, null, null, null, null, null, null, null, "obs1_bloc", null, "obs1_bloc" ], "result": "obs1_bloc" }, { "synchronise": [ null, null, null, null, null, null, null, null, null, null, "obs2_bloc", "obs2_bloc" ], "result": "obs2_bloc" } ] } }