Add petrinet language

.gitignore

@@ -1,5 +1,7 @@
-# Never accidently commit solutions to assignments :)
+# Never accidentally commit solutions to assignments :)
 *_solution.py
+# Never accidentally commit student submissions
+*_submission.py
 
 # ---> Python
 # Byte-compiled / optimized / DLL files

examples/cbd/fibonacci_runner.py

@@ -10,9 +10,6 @@ from concrete_syntax.plantuml.make_url import make_url as make_plantuml_url
 from concrete_syntax.graphviz.make_url import make_url as make_graphviz_url
 from concrete_syntax.graphviz import renderer as graphviz
 
-from transformation.matcher import match_od
-from transformation.rewriter import rewrite
-from transformation.cloner import clone_od
 from transformation.ramify import ramify
 from transformation.rule import RuleMatcherRewriter, ActionGenerator
 

examples/conformance/abstract_assoc.py

@@ -10,7 +10,6 @@ state = DevState()
 scd_mmm = bootstrap_scd(state)
 
 
-# Change this:
 mm_cs = """
     BaseA:Class {
         abstract = True;
@@ -49,7 +48,6 @@ print("Is our meta-model a valid class diagram?")
 conf = Conformance(state, mm, scd_mmm)
 print(render_conformance_check_result(conf.check_nominal()))
 
-# Change this:
 m_cs = """
     a0:A
     b0:B

examples/petrinet/metamodels/mm_design.od

@@ -0,0 +1,11 @@
+# Places, transitions, arcs (and only one kind of arc)
+
+Connectable:Class { abstract = True; }
+
+arc:Association (Connectable -> Connectable)
+
+Place:Class
+Transition:Class
+
+:Inheritance (Place -> Connectable)
+:Inheritance (Transition -> Connectable)

examples/petrinet/metamodels/mm_runtime.od

@@ -0,0 +1,16 @@
+# A place has a number of tokens, and that's it.
+
+PlaceState:Class
+PlaceState_numTokens:AttributeLink (PlaceState -> Integer) {
+  name = "numTokens";
+  optional = False;
+  constraint = `"numTokens cannot be negative" if get_value(get_target(this)) < 0 else None`;
+}
+
+of:Association (PlaceState -> Place) {
+  # one-to-one
+  source_lower_cardinality = 1;
+  source_upper_cardinality = 1;
+  target_lower_cardinality = 1;
+  target_upper_cardinality = 1;
+}

examples/petrinet/models/m_example_simple.od

@@ -0,0 +1,10 @@
+p0:Place
+p1:Place
+
+t0:Transition
+:arc (p0 -> t0)
+:arc (t0 -> p1)
+
+t1:Transition
+:arc (p1 -> t1)
+:arc (t1 -> p0)

examples/petrinet/models/m_example_simple_rt_initial.od

@@ -0,0 +1,11 @@
+p0s:PlaceState {
+  numTokens = 1;
+}
+
+:of (p0s -> p0)
+
+p1s:PlaceState {
+  numTokens = 0;
+}
+
+:of (p1s -> p1)

examples/petrinet/operational_semantics/r_fire_transition_lhs.od

@@ -0,0 +1 @@
+t:RAM_Transition

examples/petrinet/operational_semantics/r_fire_transition_nac.od

@@ -0,0 +1,13 @@
+# A place with no tokens:
+
+p:RAM_Place
+ps:RAM_PlaceState {
+  RAM_numTokens = `get_value(this) == 0`;
+}
+:RAM_of (ps -> p)
+
+# An incoming arc from that place to our transition:
+
+t:RAM_Transition
+
+:RAM_arc (p -> t)

examples/petrinet/operational_semantics/r_fire_transition_rhs.od

@@ -0,0 +1,19 @@
+t:RAM_Transition {
+  condition = ```
+    # remove 1 token from every place connected with incoming arc
+    for incoming in get_incoming(this, "arc"):
+      in_place = get_source(incoming)
+      in_place_state = get_source(get_incoming(in_place, "of")[0])
+      in_num_tokens = get_slot_value(in_place_state, "numTokens")
+      set_slot_value(in_place_state, "numTokens", in_num_tokens - 1)
+      print("place", get_name(in_place_state), "now has", in_num_tokens-1, "tokens")
+
+    # add 1 token to every place connected with outgoing arc
+    for outgoing in get_outgoing(this, "arc"):
+      out_place = get_target(outgoing)
+      out_place_state = get_source(get_incoming(out_place, "of")[0])
+      out_num_tokens = get_slot_value(out_place_state, "numTokens")
+      set_slot_value(out_place_state, "numTokens", out_num_tokens + 1)
+      print("place", get_name(out_place_state), "now has", out_num_tokens+1, "tokens")
+  ```;
+}

examples/petrinet/runner.py

@@ -0,0 +1,52 @@
+from state.devstate import DevState
+from api.od import ODAPI
+from bootstrap.scd import bootstrap_scd
+from util import loader
+from transformation.rule import RuleMatcherRewriter, ActionGenerator
+from transformation.ramify import ramify
+from examples.semantics.operational import simulator
+
+
+if __name__ == "__main__":
+    import os
+    THIS_DIR = os.path.dirname(__file__)
+
+    # get file contents as string
+    def read_file(filename):
+        with open(THIS_DIR+'/'+filename) as file:
+            return file.read()
+
+
+    state = DevState()
+    scd_mmm = bootstrap_scd(state)
+
+    # Read models from their files
+    mm_cs           =         read_file('metamodels/mm_design.od')
+    mm_rt_cs        = mm_cs + read_file('metamodels/mm_runtime.od')
+    m_cs            =         read_file('models/m_example_simple.od')
+    m_rt_initial_cs = m_cs +  read_file('models/m_example_simple_rt_initial.od')
+
+    # Parse them
+    mm           = loader.parse_and_check(state, mm_cs,           scd_mmm, "Petri-Net Design meta-model")
+    mm_rt        = loader.parse_and_check(state, mm_rt_cs,        scd_mmm, "Petri-Net Runtime meta-model")
+    m            = loader.parse_and_check(state, m_cs,            mm,      "Example model")
+    m_rt_initial = loader.parse_and_check(state, m_rt_initial_cs, mm_rt,   "Example model initial state")
+
+
+    mm_rt_ramified = ramify(state, mm_rt)
+
+    rules = loader.load_rules(state,
+        lambda rule_name, kind: f"{THIS_DIR}/operational_semantics/r_{rule_name}_{kind}.od",
+        mm_rt_ramified,
+        ["fire_transition"]) # only 1 rule :(
+
+    matcher_rewriter = RuleMatcherRewriter(state, mm_rt, mm_rt_ramified)
+    action_generator = ActionGenerator(matcher_rewriter, rules)
+
+    sim = simulator.Simulator(
+        action_generator=action_generator,
+        decision_maker=simulator.InteractiveDecisionMaker(auto_proceed=False),
+        # decision_maker=simulator.RandomDecisionMaker(seed=0),
+    )
+
+    sim.run(ODAPI(state, m_rt_initial, mm_rt))

examples/semantics/operational/simulator.py

@@ -17,7 +17,7 @@ class Simulator(MinimalSimulator):
     def __init__(self,
         action_generator,
         decision_maker: DecisionMaker,
-        termination_condition,
+        termination_condition=lambda od: None,
         check_conformance=True,
         verbose=True,
         renderer=lambda od: render_od(od.state, od.m, od.mm),