Commit before model change

tests/ra_testscenario.py

@@ -58,7 +58,7 @@ sut_m2 = RaTestScenario("store_1_true_then_remember", [
     # This is a check for Rick, ignore the traces below
     # ([act(1), act(1), act(2), act(1), act(1)], False),
     # ([act(1), act(1), act(2), act(1), act(2)], True)
-], 5, 1)
+], 4, 1)
 
 # check for unique valuedness (non-UV 4 LOC, UV 5 LOC)
 sut_m3 = RaTestScenario ("store_2_select_either_UV", [
@@ -86,7 +86,7 @@ sut_m3 = RaTestScenario ("store_2_select_either_UV", [
    ([act(1), act(2), act(2), act(1)], True),
    ([act(1), act(2), act(3), act(4), act(1)], True),
    ([act(1), act(2), act(2), act(2), act(3)], True)
-], 4, 2)
+], 5, 2)
 
 # check for non-shifting property (3 LOC NS, 4 LOC non-NS)
 # expect this system to require one additional location than if our constraints allowed value shifting between registers

tests/test_ralearner.py

@@ -6,7 +6,7 @@ from z3gi.define.ra import RegisterAutomaton
 import model.ra
 import z3
 
-num_exp = 4
+num_exp = 1
 
 class RaLearnerTest(unittest.TestCase):
 

z3gi/define/ra.py

@@ -106,7 +106,7 @@ class RegisterAutomatonBuilder(object):
 
         for (z3end_state, z3guards) in z3end_state_to_guards.items():
             # a transition which makes an assignment is never merged
-            if self.ra.fresh in z3guards and update is not self.ra.fresh:
+            if self.ra.fresh in z3guards and not translator.z3_to_bool(model.eval(update == self.ra.fresh)):
                 self._add_transition(translator, mut_ra, z3state, z3label,
                                      [self.ra.fresh], update, z3end_state, used_z3regs)
                 z3guards.remove(self.ra.fresh)
@@ -179,7 +179,7 @@ class IORegisterAutomatonBuilder(object):
         print("For {0} we have the transitions \n {1}".format(z3state, z3end_state_to_guards))
         for (z3out_state, z3guards) in z3end_state_to_guards.items():
             # a transition which makes an assignment is never merged
-            if self.ra.fresh in z3guards and update is not self.ra.fresh:
+            if self.ra.fresh in z3guards and not translator.z3_to_bool(model.eval(update == self.ra.fresh)):
                 self._add_transition(model, translator, mut_ra, z3state, z3label,
                                      [self.ra.fresh], update, z3out_state,
                                      z3output_labels, used_z3regs)

z3gi/learn/ra.py

@@ -32,9 +32,6 @@ class RALearner(Learner):
             return ra_def.export(m)
         return None
 
-    def print_tree(self):
-        self.encoder.print_tree()
-
     def _learn_model(self, min_locations=1, max_locations=20, max_registers=10):
         """generates the definition and model for an ra whose traces include the traces added so far"""
         num_values = len(self.encoder.values)

z3gi/model/ra.py

@@ -70,7 +70,7 @@ class IORATransition(RATransition):
 
     def output(self, valuation, values):
         if type(self.output_mapping) == Fresh:
-            return Action(self.output_label, max(values) + 1)
+            return Action(self.output_label, max(values) + 1 if len(values) > 0 else 0)
         else:
             return Action(self.output_label, valuation[self.output_mapping])
 
@@ -101,6 +101,7 @@ class RegisterMachine():
             raise MultipleTransitionsFired
         return fired_transitions[0]
 
+
 class RegisterAutomaton(Acceptor, RegisterMachine):
     def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
       super().__init__(locations, loc_to_trans, loc_to_acc)
@@ -165,6 +166,7 @@ class IORegisterAutomaton(Transducer, RegisterMachine):
             output_action = fired_transition.output(reg_val, values)
             # based on this output, the transition should update the set of registers
             reg_val = fired_transition.output_update(reg_val, output_action)
+            values.add(output_action.value)
 
             crt_state = fired_transition.end_state
         return (crt_state, reg_val, values)
@@ -177,9 +179,19 @@ class IORegisterAutomaton(Transducer, RegisterMachine):
             action = trace[-1]
             transitions = super().transitions(reached_state, action.label)
             fired_transition = super()._fired_transition(transitions, valuation, action)
+            values.add(action.value)
             output = fired_transition.output(valuation, values)
             return output
 
+    def compress(self):
+        mutable_ra = MutableIORegisterAutomaton()
+        [mutable_ra.add_state(state) for state in self.states()]
+        for state in self.states():
+            transitions = self.transitions()
+
+
+
+
 class MutableRegisterAutomaton(RegisterAutomaton, MutableAcceptorMixin):
     def __init__(self):
         super().__init__([], dict(), dict(), [])