CBD model is computing Fibonacci numbers! :)

examples/cbd/models.py

@@ -51,7 +51,7 @@ def get_fibonacci(state, scd_mmm):
 
     return (mm, mm_rt, m, m_rt_initial)
 
-RULE_NAMES = ["delay"]
+RULE_NAMES = ["delay_out", "function_out", "delay_in", "advance_time"]
 KINDS = ["nac", "lhs", "rhs"]
 
 def get_rules(state, rt_mm):

examples/cbd/models/m_fibonacci.od

@@ -1,7 +1,7 @@
 # Adder, two inputs, one output
 adder:Function {
   func = ```
-    n2_out = n0_in + n1_in
+    read('n0_in') + read('n1_in')
   ```;
 }
 n0_in:InPort

examples/cbd/models/m_fibonacci_initial.od

@@ -1,9 +1,13 @@
 # Initial state for both delay blocks:
 d0s:State {
-  state = 0;
+  x = 0;
 }
 d1s:State {
-  state = 1;
+  x = 1;
 }
 :delay2State (d0 -> d0s)
 :delay2State (d1 -> d1s)
+
+clock:Clock {
+  time = 0;
+}

examples/cbd/models/mm_design.od

@@ -2,12 +2,8 @@ Block:Class {
   abstract = True;
 }
 
-InPort:Class {
-  # abstract = True;
-}
-OutPort:Class {
-  # abstract = True;
-}
+InPort:Class
+OutPort:Class
 
 hasInPort:Association (Block -> InPort) {
   # Every Port contained by exactly one Block:
@@ -21,27 +17,12 @@ hasOutPort:Association (Block -> OutPort) {
 }
 
 link:Association (OutPort -> InPort) {
-  #abstract = True;
-
   # Every InPort connected to exactly one OutPort
   source_lower_cardinality = 1;
   source_upper_cardinality = 1;
 }
 
 
-# In- and Out-Ports are labeled:
-
-# hasInPort_label:AttributeLink (hasInPort -> String) {
-#   name = "label";
-#   optional = False;
-# }
-# hasOutPort_label:AttributeLink (hasOutPort -> String) {
-#   name = "label";
-#   optional = False;
-# }
-
-
-
 # Function Block: pure function that computes outputs based on inputs
 
 Function:Class
@@ -69,61 +50,9 @@ Delay:Class {
     num_outports = len(get_outgoing(this, "hasOutPort"))
     if num_inports != 1:
       errors.append(f"Delay block must have one inport, instead got {num_inports}")
-      in_type = None
-    else:
-      in_type = get_type_name(get_target(get_outgoing(this, "hasInPort")[0]))
     if num_outports != 1:
       errors.append(f"Delay block must have one inport, instead got {num_outports}")
-      out_type = None
-    else:
-      out_type = get_type_name(get_target(get_outgoing(this, "hasOutPort")[0]))
-    # if in_type != None and out_type != None and in_type[0:3] != out_type[0:3]:
-    #   errors.append(f"Inport type ({in_type}) differs from outport type ({out_type})")
     errors
   ```;
 }
 :Inheritance (Delay -> Block)
-
-
-
-
-# Object Diagrams are statically typed, so we must create in/out-ports, and MemorySlots for all primitive types:
-
-
-# # Port types
-
-# BoolInPort:Class
-# IntInPort:Class
-# StrInPort:Class
-
-# BoolOutPort:Class
-# IntOutPort:Class
-# StrOutPort:Class
-
-# :Inheritance (BoolInPort -> InPort)
-# :Inheritance (IntInPort -> InPort)
-# :Inheritance (StrInPort -> InPort)
-
-# :Inheritance (BoolOutPort -> OutPort)
-# :Inheritance (IntOutPort -> OutPort)
-# :Inheritance (StrOutPort -> OutPort)
-
-# # Link types
-
-# boolLink:Association (BoolOutPort -> BoolInPort)
-# intLink:Association (IntOutPort -> IntInPort)
-# strLink:Association (StrOutPort -> StrInPort)
-
-# :Inheritance (boolLink -> link)
-# :Inheritance (intLink -> link)
-# :Inheritance (strLink -> link)
-
-# # Delay block types
-
-# BoolDelay:Class
-# IntDelay:Class
-# StrDelay:Class
-
-# :Inheritance (BoolDelay -> Delay)
-# :Inheritance (IntDelay -> Delay)
-# :Inheritance (StrDelay -> Delay)

examples/cbd/models/mm_runtime.od

@@ -1,85 +1,47 @@
 # Link state ("signal")
 
-Signal:Class {
-  # abstract = True;
-}
+Signal:Class
 
-Signal_signal:AttributeLink (Signal -> Integer) {
-  name = "signal";
+Signal_x:AttributeLink (Signal -> Integer) {
+  name = "x";
   optional = False;
 }
 
-hasSignal:Association (link -> Signal) {
+hasSignal:Association (OutPort -> Signal) {
   # every Signal has 1 link
   source_lower_cardinality = 1;
   source_upper_cardinality = 1;
+
    # every link has 0..1 Signals: 
   target_upper_cardinality = 1;
 }
 
-# BoolSignal:Class
-# IntSignal:Class
-# StrSignal:Class
-
-# :Inheritance (BoolSignal -> Signal)
-# :Inheritance (IntSignal -> Signal)
-# :Inheritance (StrSignal -> Signal)
-
-# BoolSignal_signal:AttributeLink (BoolSignal -> Boolean) {
-#   name = "signal";
-#   optional = False;
-# }
-# IntSignal_signal:AttributeLink (IntSignal -> Integer) {
-#   name = "signal";
-#   optional = False;
-# }
-# StrSignal_signal:AttributeLink (StrSignal -> String) {
-#   name = "signal";
-#   optional = False;
-# }
-
-
 
 # Delay block state
 # mandatory - otherwise we cannot determine the output signal of a delay block
 
-State:Class {
-  # abstract = True;
-}
+State:Class
 
-State_state:AttributeLink (State -> Integer) {
-  name = "state";
+State_x:AttributeLink (State -> Integer) {
+  name = "x";
   optional = False;
 }
 
 
 delay2State:Association (Delay -> State) {
+  # one-to-one
   source_lower_cardinality = 1;
   source_upper_cardinality = 1;
   target_lower_cardinality = 1;
   target_upper_cardinality = 1;
 }
 
-# BoolState:Class
-# IntState:Class
-# StrState:Class
+Clock:Class {
+  lower_cardinality = 1;
+  upper_cardinality = 1;
+}
 
-# :Inheritance (BoolState -> State)
-# :Inheritance (IntState -> State)
-# :Inheritance (StrState -> State)
-
-
-# BoolState_state:AttributeLink (BoolState -> Boolean) {
-#   name = "state";
-#   optional = False;
-# }
-
-# IntState_state:AttributeLink (IntState -> Integer) {
-#   name = "state";
-#   optional = False;
-# }
-
-# StrState_state:AttributeLink (StrState -> String) {
-#   name = "state";
-#   optional = False;
-# }
+Clock_time:AttributeLink (Clock -> Integer) {
+  name = "time";
+  optional = False;
+}

examples/cbd/models/r_advance_time_lhs.od

@@ -0,0 +1,3 @@
+clock:RAM_Clock {
+  RAM_time = `True`;
+}

examples/cbd/models/r_advance_time_nac.od

@@ -0,0 +1,36 @@
+
+# If there is a Delay-block whose input signal differs from its state, we cannot yet advance time:
+
+delay:RAM_Delay
+
+delay_in:RAM_InPort
+
+delay_has_input:RAM_hasInPort (delay -> delay_in)
+
+some_outport:RAM_OutPort
+
+delay_in_conn:RAM_link (some_outport -> delay_in)
+
+in_signal:RAM_Signal
+
+port_has_signal:RAM_hasSignal (some_outport -> in_signal)
+
+state:RAM_State {
+  RAM_x = `get_slot_value(matched('in_signal'), 'x') != get_value(this)`;
+}
+
+delay_to_state:RAM_delay2State (delay -> state)
+
+
+# Also, we cannot advance time until all outports have signals:
+
+:GlobalCondition {
+  condition = ```
+    missing_signals = False
+    for _, outport in get_all_instances("OutPort"):
+      if len(get_outgoing(outport, 'hasSignal')) == 0:
+        missing_signals = True
+        break
+    missing_signals
+  ```;
+}

examples/cbd/models/r_advance_time_rhs.od

@@ -0,0 +1,10 @@
+clock:RAM_Clock {
+  RAM_time = `get_value(this) + 1`;
+}
+
+:GlobalCondition {
+  condition = ```
+    for _, signal in get_all_instances("Signal"):
+      delete(signal)
+  ```;
+}

examples/cbd/models/r_delay_in_lhs.od

@@ -0,0 +1,27 @@
+# We look for a Delay-block, its inport connected to an outport that has a signal
+
+delay:RAM_Delay
+
+delay_in:RAM_InPort
+
+delay_has_input:RAM_hasInPort (delay -> delay_in)
+
+some_outport:RAM_OutPort
+
+delay_in_conn:RAM_link (some_outport -> delay_in)
+
+in_signal:RAM_Signal
+
+port_has_signal:RAM_hasSignal (some_outport -> in_signal)
+
+
+
+# State of Delay block... (will be updated in RHS)
+
+state:RAM_State {
+  # Attention: you MUST match the existing attribute, in order to force an UDPATE of the attribute, rather than CREATION
+  
+  RAM_x = `True`;
+}
+
+delay_to_state:RAM_delay2State (delay -> state)

examples/cbd/models/r_delay_in_nac.od

@@ -0,0 +1,6 @@
+state:RAM_State # <- must repeat elements from LHS that we refer to
+
+in_signal:RAM_Signal {
+  # If the signal is already equal to the state, the NAC holds:
+  RAM_x = `get_value(this) == get_slot_value(matched('state'), 'x')`;
+}

examples/cbd/models/r_delay_in_rhs.od

@@ -0,0 +1,26 @@
+# Everything from our LHS (don't delete anything)
+
+delay:RAM_Delay
+
+delay_in:RAM_InPort
+
+delay_has_input:RAM_hasOutPort (delay -> delay_in)
+
+some_outport:RAM_OutPort
+
+delay_in_conn:RAM_link (some_outport -> delay_in)
+
+in_signal:RAM_Signal
+
+port_has_signal:RAM_hasSignal (some_outport -> in_signal)
+
+state:RAM_State {
+  # Update:
+  RAM_x = ```
+    new_state = get_slot_value(matched('in_signal'), 'x')
+    print(f"Updating delay {get_name(matched('delay'))} state: {new_state}")
+    new_state
+  ```;
+}
+
+delay_to_state:RAM_delay2State (delay -> state)

examples/cbd/models/r_delay_lhs.od

@@ -1,16 +0,0 @@
-# We look for a Delay-block, its outgoing connection, and its State
-
-delay:RAM_Delay
-
-delay_out:RAM_OutPort # abstract
-
-delay_has_output:RAM_hasOutPort (delay -> delay_out)
-
-some_inport:RAM_InPort # abstract
-
-delay_out_conn:RAM_link (delay_out -> some_inport)
-
-
-state:RAM_State
-
-delay_to_state:RAM_delay2State (delay -> state)

examples/cbd/models/r_delay_nac.od

@@ -1,14 +0,0 @@
-# From our LHS:
-
-delay_out:RAM_OutPort # abstract
-
-some_inport:RAM_InPort # abstract
-
-delay_out_conn:RAM_link (delay_out -> some_inport) # abstract
-
-
-# The delay block's outgoing connection already has a signal:
-
-some_signal:RAM_Signal
-
-:RAM_hasSignal (delay_out_conn -> some_signal)

examples/cbd/models/r_delay_out_lhs.od

@@ -0,0 +1,14 @@
+# We look for a Delay-block, its outport, and its State
+
+delay:RAM_Delay
+
+delay_out:RAM_OutPort
+
+delay_has_output:RAM_hasOutPort (delay -> delay_out)
+
+
+state:RAM_State
+
+delay_to_state:RAM_delay2State (delay -> state)
+
+clock:RAM_Clock

examples/cbd/models/r_delay_out_nac.od

@@ -0,0 +1,10 @@
+# From our LHS:
+
+delay_out:RAM_OutPort
+
+
+# We don't want to see the delay block's outport already having a signal:
+
+some_signal:RAM_Signal
+
+:RAM_hasSignal (delay_out -> some_signal)

examples/cbd/models/r_delay_out_rhs.od

@@ -0,0 +1,20 @@
+# Our entire LHS (don't delete anything):
+
+delay:RAM_Delay
+
+delay_out:RAM_OutPort
+
+delay_has_output:RAM_hasOutPort (delay -> delay_out)
+
+state:RAM_State
+
+delay_to_state:RAM_delay2State (delay -> state)
+
+clock:RAM_Clock
+
+# To create:
+
+new_signal:RAM_Signal {
+  RAM_x = `get_slot_value(matched('state'), 'x')`;
+}
+:RAM_hasSignal (delay_out -> new_signal)

examples/cbd/models/r_delay_rhs.od

@@ -1,23 +0,0 @@
-# Our entire LHS (don't delete anything):
-
-delay:RAM_Delay
-
-delay_out:RAM_OutPort # abstract
-
-delay_has_output:RAM_hasOutPort (delay -> delay_out)
-
-some_inport:RAM_InPort # abstract
-
-delay_out_conn:RAM_link (delay_out -> some_inport) # abstract
-
-state:RAM_State
-
-delay_to_state:RAM_delay2State (delay -> state)
-
-
-# To create:
-
-new_signal:RAM_Signal {
-  RAM_signal = `get_slot_value(match('state'), 'state')`;
-}
-:RAM_hasSignal (delay_out_conn -> new_signal)

examples/cbd/models/r_function_out_lhs.od

@@ -0,0 +1,22 @@
+# Match function and its out-connection
+
+f:RAM_Function {
+  # Only match if the signal of all inputs has been computed:
+  condition = ```
+    ok = True
+    for o in get_outgoing(this, "hasInPort"):
+      inport = get_target(o)
+      in_conn = get_incoming(inport, "link")[0]
+      some_outport = get_source(in_conn)
+      if len(get_outgoing(some_outport, "hasSignal")) == 0:
+        ok = False
+        break
+    ok
+  ```;
+}
+
+f_outport:RAM_OutPort
+
+f_has_outport:RAM_hasOutPort (f -> f_outport)
+
+clock:RAM_Clock

examples/cbd/models/r_function_out_nac.od

@@ -0,0 +1,14 @@
+# From our LHS:
+
+f:RAM_Function
+
+f_outport:RAM_OutPort
+
+f_has_outport:RAM_hasOutPort (f -> f_outport)
+
+
+# We don't want to see the function's out-connection already having a signal:
+
+some_signal:RAM_Signal
+
+:RAM_hasSignal (f_outport -> some_signal)

examples/cbd/models/r_function_out_rhs.od

@@ -0,0 +1,26 @@
+# Our entire LHS (don't delete anything):
+
+f:RAM_Function
+
+f_outport:RAM_OutPort
+
+f_has_outport:RAM_hasOutPort (f -> f_outport)
+
+clock:RAM_Clock
+
+# To create:
+
+f_out_signal:RAM_Signal {
+  RAM_x = ```
+    def read(inport_name):
+      inport = get(inport_name)
+      outport = get_source(get_incoming(inport, "link")[0])
+      signal = get_target(get_outgoing(outport, "hasSignal")[0])
+      return get_slot_value(signal, "x")
+
+    code = get_slot_value(matched('f'), 'func')
+
+    eval(code, {}, { 'read': read })
+  ```;
+}
+:RAM_hasSignal (f_outport -> f_out_signal)

examples/cbd/runner.py

@@ -1,6 +1,8 @@
 from state.devstate import DevState
 from bootstrap.scd import bootstrap_scd
 
+from framework.conformance import Conformance, render_conformance_check_result
+
 from concrete_syntax.common import indent
 from concrete_syntax.textual_od import renderer as od_renderer
 from concrete_syntax.plantuml import renderer as plantuml
@@ -17,12 +19,10 @@ import models
 state = DevState()
 scd_mmm = bootstrap_scd(state)
 
+print("Parsing models...")
 mm, mm_rt, m, m_rt_initial = models.get_fibonacci(state, scd_mmm)
-
 mm_rt_ram, rules = models.get_rules(state, mm_rt)
 
-
-
 # print("RT-MM")
 # print(make_plantuml_url(plantuml.render_class_diagram(state, mm_rt)))
 
@@ -42,28 +42,40 @@ def get_matches():
             pattern_m=lhs,
             pattern_mm=mm_rt_ram)
 
-        for i, lhs_match in enumerate(lhs_matcher):
+        try:
+            for i, lhs_match in enumerate(lhs_matcher):
+                nac_matcher = match_od(state,
+                    host_m=m_rt,
+                    host_mm=mm_rt,
+                    pattern_m=rule["nac"],
+                    pattern_mm=mm_rt_ram,
+                    pivot=lhs_match)
 
-            nac_matcher = match_od(state,
-                host_m=m_rt,
-                host_mm=mm_rt,
-                pattern_m=rule["nac"],
-                pattern_mm=mm_rt_ram,
-                pivot=lhs_match)
+                try:
+                    for j, nac_match in enumerate(nac_matcher):
+                        break # there may be more NAC-matches, but we already now enough
+                    else:
+                        # We got a match!
+                        yield (rule_name, lhs, rule["rhs"], lhs_match)
+                except Exception as e:
+                    # Make exceptions raised in eval'ed code easier to trace:
+                    e.add_note(f"while matching NAC of '{rule_name}'")
+                    raise
 
-            for j, nac_match in enumerate(nac_matcher):
-                break # there may be more NAC-matches, but we already now enough
-            else:
-                # We got a match!
-                yield (rule_name, lhs, rule["rhs"], lhs_match)
+        except Exception as e:
+            # Make exceptions raised in eval'ed code easier to trace:
+            e.add_note(f"while matching LHS of '{rule_name}'")
+            raise
 
 while True:
     # print(make_graphviz_url(graphviz.render_object_diagram(state, m_rt, mm_rt)))
     cs = od_renderer.render_od(state, m_rt, mm_rt, hide_names=False)
     print(indent(cs, 6))
-
+    conf = Conformance(state, m_rt, mm_rt)
+    print(render_conformance_check_result(conf.check_nominal()))
 
     matches = list(get_matches())
+
     print(f"There are {len(matches)} matches.")
     if len(matches) == 0:
         break
@@ -75,21 +87,23 @@ while True:
                 # txt += graphviz.render_trace_match(state, lhs_match, lhs, m_rt, color="orange")
                 # match_urls.append(make_graphviz_url(txt))
 
-    print('picking', lhs_match)
-
-    print('rewriting')
+    print(f"executing rule '{rule_name}' ", lhs_match)
 
     # copy or will be overwritten in-place
     m_rt = clone_od(state, m_rt, mm_rt)
     rhs_match = dict(lhs_match)
-
-    rewrite(state,
-        lhs_m=lhs,
-        rhs_m=rhs,
-        pattern_mm=mm_rt_ram,
-        name_mapping=rhs_match,
-        host_m=m_rt,
-        mm=mm_rt)
+    try:
+        rewrite(state,
+            lhs_m=lhs,
+            rhs_m=rhs,
+            pattern_mm=mm_rt_ram,
+            name_mapping=rhs_match,
+            host_m=m_rt,
+            host_mm=mm_rt)
+    except Exception as e:
+        # Make exceptions raised in eval'ed code easier to trace:
+        e.add_note(f"while executing RHS of '{rule_name}'")
+        raise
 
     # import subprocess
     # subprocess.run(["firefox", "--new-window", *match_urls])