teaching/muMLE
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Commit some outstanding changes. Add TODO for cleanup.

Browse source
This commit is contained in:
Joeri Exelmans 2025-01-27 16:03:45 +01:00
parent 200f2a3ede
commit 8fe7b0ea04
12 changed files with 114 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

4
examples/semantics/translational/rules/gen_pn/r_00_place2place_rhs.od
View file

@ -9,7 +9,7 @@
pn_place:RAM_PNPlace {
# new feature: you can control the name of the object to be created:
name = `f"pn_{get_name(matched("port_place"))}"`;
name = `f"ships_{get_name(matched("port_place"))}"`;
}
place2place:RAM_generic_link (pn_place -> port_place)
@ -19,4 +19,4 @@
pn_place_state:RAM_PNPlaceState {
RAM_numTokens = `get_slot_value(matched('port_place_state'), "numShips")`;
}
:RAM_pn_of(pn_place_state -> pn_place)
:RAM_pn_of(pn_place_state -> pn_place)

4
examples/semantics/translational/rules/gen_pn/r_10_conn2trans_lhs.od
View file

@ -1,5 +1,7 @@
# Just look for a connection:
# Just look for a connection and its state:
port_src:RAM_Source
port_snk:RAM_Sink
port_conn:RAM_connection (port_src -> port_snk)
port_conn_state:RAM_ConnectionState
port_of:RAM_of (port_conn_state -> port_conn)

20
examples/semantics/translational/rules/gen_pn/r_10_conn2trans_rhs.od
View file

@ -3,12 +3,26 @@
port_src:RAM_Source
port_snk:RAM_Sink
port_conn:RAM_connection (port_src -> port_snk)
port_conn_state:RAM_ConnectionState
port_of:RAM_of (port_conn_state -> port_conn)
# Create a Petri Net transition, and link it to our port-connection:
pn_transition:RAM_PNTransition {
name = `f"pn_{get_name(matched("port_conn"))}"`;
move_transition:RAM_PNTransition {
name = `f"move_{get_name(matched("port_conn"))}"`;
}
trans2conn:RAM_generic_link (pn_transition -> port_conn)
moved_place:RAM_PNPlace {
name = `f" moved_{get_name(matched("port_conn"))}"`;
}
moved_place_state:RAM_PNPlaceState {
RAM_numTokens = `1 if get_slot_value(matched('port_conn_state'), "moved") else 0`;
}
:RAM_pn_of (moved_place_state -> moved_place)
# when firing a 'move', put a token in the 'moved'-place
:RAM_arc (move_transition -> moved_place)
trans2conn:RAM_generic_link (move_transition -> port_conn)
moved2conn:RAM_generic_link (moved_place -> port_conn)
# Note that we are not yet creating any incoming/outgoing petri net arcs! This will be done in another rule.

4
examples/semantics/translational/runner_translate.py
View file

@ -62,9 +62,9 @@ if __name__ == "__main__":
print('loading model...')
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.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
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