diff --git a/examples/semantics/operational/port/models.py b/examples/semantics/operational/port/models.py index 0ef84b1..162e753 100644 --- a/examples/semantics/operational/port/models.py +++ b/examples/semantics/operational/port/models.py @@ -298,3 +298,103 @@ port_rt_m_cs = port_m_cs + """ c10S:ConnectionState { moved = False; } :of (c10S -> c10) c11S:ConnectionState { moved = False; } :of (c11S -> c11) """ + +################################################### + +# ┌─────────────────┐ +# │ shipCapacity=3 │ +# ┌───┐ ┌───────┐ │┌──────────────┐ │ ┌───────┐ +# │gen├────►│waiting├────►│inboundPassage├───►│turning│ +# └───┘ └───────┘ │└──────────────┘ │ └───┬───┘ +# │ │ │ +# ┌──────┐ │┌───────────────┐│ │ +# │served│◄────┼outboundPassage│◄──────┘ +# └──────┘ │└───────────────┘│ +# └─────────────────┘ +smaller_model_cs = """ + gen:Generator + waiting:Place + inboundPassage:Place + turning:Place + outboundPassage:Place + served:Place + + gen2wait:connection (gen -> waiting) + wait2inbound:connection (waiting -> inboundPassage) + inbound2turning:connection (inboundPassage -> turning) + turning2outbound:connection (turning -> outboundPassage) + outbound2served:connection (outboundPassage -> served) + + # inboundPassage and outboundPassage cannot have more than 3 ships total + passageCap:CapacityConstraint { + shipCapacity = 3; + } + :capacityOf (passageCap -> inboundPassage) + :capacityOf (passageCap -> outboundPassage) +""" + +smaller_model_rt_cs = smaller_model_cs + """ + clock:Clock { + time = 0; + } + + waitingState:PlaceState { numShips = 1; } :of (waitingState -> waiting) + inboundPassageState:PlaceState { numShips = 1; } :of (inboundPassageState -> inboundPassage) + turningState:PlaceState { numShips = 1; } :of (turningState -> turning) + outboundPassageState:PlaceState { numShips = 1; } :of (outboundPassageState -> outboundPassage) + servedState:PlaceState { numShips = 0; } :of (servedState -> served) + + gen2waitState:ConnectionState { moved = False; } :of (gen2waitState -> gen2wait) + wait2inboundState:ConnectionState { moved = False; } :of (wait2inboundState -> wait2inbound) + inbound2turningState:ConnectionState { moved = False; } :of (inbound2turningState -> inbound2turning) + turning2outboundState:ConnectionState { moved = False; } :of (turning2outboundState -> turning2outbound) + outbound2servedState:ConnectionState { moved = False; } :of (outbound2servedState -> outbound2served) +""" + +################################################### + +# ┌────────────┐ +# │ workerset │ +# │ │ +# │numWorkers=1│ +# └──────┬─────┘ +# │canOperate +# │ +# ┌───▼────┐ +# ┌───┐ ┌───────┐ │┌─────┐ │ ┌──────┐ +# │gen├────►│waiting├────││berth├─┼───►│served│ +# └───┘ └───────┘ │└─────┘ │ └──────┘ +# │ship- │ +# │Capacity│ +# │ =1 │ +# └────────┘ +smaller_model2_cs = """ + gen:Generator + waiting:Place + berth:Berth + served:Place + + gen2wait:connection (gen -> waiting) + wait2berth:connection (waiting -> berth) + berth2served:connection (berth -> served) + + # berth can only hold 1 ship + passageCap:CapacityConstraint { + shipCapacity = 1; + } + :capacityOf (passageCap -> berth) +""" + +smaller_model2_rt_cs = smaller_model2_cs + """ + clock:Clock { + time = 0; + } + + waitingState:PlaceState { numShips = 1; } :of (waitingState -> waiting) + berthState:BerthState { numShips = 0; status = "empty"; } :of (berthState -> berth) + servedState:PlaceState { numShips = 0; } :of (servedState -> served) + + gen2waitState:ConnectionState { moved = False; } :of (gen2waitState -> gen2wait) + wait2berthState:ConnectionState { moved = False; } :of (wait2berthState -> wait2berth) + berth2servedState:ConnectionState { moved = False; } :of (berth2servedState -> berth2served) +""" diff --git a/examples/semantics/translational/runner_translate.py b/examples/semantics/translational/runner_translate.py index d237257..971db51 100644 --- a/examples/semantics/translational/runner_translate.py +++ b/examples/semantics/translational/runner_translate.py @@ -44,7 +44,7 @@ if __name__ == "__main__": # | | | # V V V rule_names = [ - # high to low priority: + # high to low priority (the list-order here matters, the alphabetic-order of the names does not): "00_place2place", "10_conn2trans", @@ -64,7 +64,12 @@ if __name__ == "__main__": rule_names) print('loading model...') - port_m_rt_initial = loader.parse_and_check(state, models.port_rt_m_cs, merged_mm, "Port-M-RT-initial", + port_m_rt_initial = loader.parse_and_check(state, + m_cs=models.port_rt_m_cs, # <-- your final solution should work with the full model + # m_cs=models.smaller_model_rt_cs, # <-- simpler model to try first + # m_cs=models.smaller_model2_rt_cs, # <-- simpler model to try first + mm=merged_mm, + descr="initial model", check_conformance=False, # no need to check conformance every time )