First iteration of corrections

z3gi/learn/algorithm.py

@@ -50,12 +50,12 @@ def learn(learner:Learner, test_type:type, traces: List[object]) -> Tuple[Automa
         statistics.set_suite_size(len(traces))
         test = cast(TestTemplate, test_type(traces.pop(0)))
         definition = None
-        learner.add(test.trace)
+        learner.add(test.tr)
         statistics.add_tests(1)
         statistics.add_inputs(test.size())
         done = False
         model = None
-        learn_traces = [test.trace]
+        learn_traces = [test.tr]
         while not done:
             start_time = int(time.time() * 1000)
             (model, definition) = learner.model(old_definition=definition)

z3gi/model/__init__.py

@@ -36,11 +36,11 @@ class MultipleTransitionsFired(Exception):
 
 
 class Automaton(metaclass=ABCMeta):
-    def __init__(self, states, state_to_trans):
+    def __init__(self, states, state_to_trans, acc_seq={}):
         super().__init__()
         self._states = states
         self._state_to_trans = state_to_trans
-        self._acc_seq = {}
+        self._acc_seq = acc_seq
 
     def start_state(self):
         return self._states[0]
@@ -55,6 +55,8 @@ class Automaton(metaclass=ABCMeta):
     def acc_seq(self, state=None):
         """returns the access sequence to a state in the form of sequences of inputs"""
         if state is not None:
+            if len(self._acc_seq) == 0:
+                raise Exception("Access sequences haven't been defined for this machine")
             return self._seq(self._acc_seq[state])
         else:
             return {state:self._seq(self._acc_seq[state]) for state in self.states()}
@@ -130,6 +132,7 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
             if node is None:
                 raise Exception("Could not find state {0} in tree {1}".format(state, ptree))
             new_acc_seq[state] = node.path()
+        assert(len(new_acc_seq) == len(self.states()))
         self._acc_seq = new_acc_seq
 
     @abstractmethod
@@ -141,24 +144,21 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
 
 
 class Transducer(Automaton, metaclass=ABCMeta):
-    def __init__(self, states, state_to_trans):
-        super().__init__(states, state_to_trans)
+    def __init__(self, states, state_to_trans, acc_seq={}):
+        super().__init__(states, state_to_trans, acc_seq)
 
     @abstractmethod
     def output(self, trace):
         pass
 
-    def output_labels(self):
-        return set([trans.output for state in self.states() for trans in self.transitions(state)])
-
 
 
 """An automaton model whose states are accepting/rejecting"""
 
 
 class Acceptor(Automaton, metaclass=ABCMeta):
-    def __init__(self, states, state_to_trans, state_to_acc):
-        super().__init__(states, state_to_trans)
+    def __init__(self, states, state_to_trans, state_to_acc, acc_seq={}):
+        super().__init__(states, state_to_trans, acc_seq)
         self._state_to_acc = state_to_acc
 
     def is_accepting(self, state):
@@ -182,9 +182,6 @@ class MutableAcceptorMixin(MutableAutomatonMixin, metaclass=ABCMeta):
         self._state_to_acc[state] = accepts
 
 
-
-
-
 def get_prefix_tree(aut : Automaton):
     visited  = set()
     to_visit = set()

z3gi/model/fa.py

@@ -43,7 +43,7 @@ class MutableDFA(DFA, MutableAcceptorMixin):
         return None
 
     def to_immutable(self) -> DFA:
-        return DFA(self._states, self._state_to_trans, self._state_to_acc)
+        return DFA(self._states, self._state_to_trans, self._state_to_acc, self.acc_seq())
 
 class MooreMachine(Transducer):
     def __init__(self, states, state_to_trans, state_to_out):
@@ -66,8 +66,8 @@ class MooreMachine(Transducer):
         return [trans.start_label for trans in transitions]#trace
 
 class MealyMachine(Transducer):
-    def __init__(self, states, state_to_trans):
-        super().__init__(states, state_to_trans)
+    def __init__(self, states, state_to_trans, acc_seq={}):
+        super().__init__(states, state_to_trans, acc_seq)
 
     def transitions(self, state: State, label: Label = None) -> List[IOTransition]:
         return super().transitions(state, label)
@@ -93,4 +93,4 @@ class MutableMealyMachine(MealyMachine, MutableAutomatonMixin):
         super().__init__([], {})
 
     def to_immutable(self) -> MealyMachine:
-        return MealyMachine(self._states, self._state_to_trans)
+        return MealyMachine(self._states, self._state_to_trans, self.acc_seq())

z3gi/model/ra.py

@@ -112,8 +112,8 @@ class RegisterMachine(Automaton):
         pass
 
 class RegisterAutomaton(Acceptor, RegisterMachine):
-    def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
-      super().__init__(locations, loc_to_trans, loc_to_acc)
+    def __init__(self, locations, loc_to_acc, loc_to_trans, registers, acc_seq={}):
+      super().__init__(locations, loc_to_trans, loc_to_acc, acc_seq)
       self._registers = registers
 
     def registers(self) -> List[Register]:
@@ -153,8 +153,8 @@ class RegisterAutomaton(Acceptor, RegisterMachine):
 
 
 class IORegisterAutomaton(Transducer, RegisterMachine):
-    def __init__(self, locations, loc_to_trans, registers):
-        super().__init__(locations, loc_to_trans)
+    def __init__(self, locations, loc_to_trans, registers, acc_seq={}):
+        super().__init__(locations, loc_to_trans, acc_seq)
         self._registers = registers
 
 
@@ -241,7 +241,8 @@ class MutableRegisterAutomaton(RegisterAutomaton, MutableAcceptorMixin):
                 self._registers.append(reg)
 
     def to_immutable(self) -> RegisterAutomaton:
-        return RegisterAutomaton(self._states, self._state_to_acc, self._state_to_trans, self._registers)
+        return RegisterAutomaton(self._states, self._state_to_acc,
+                                 self._state_to_trans, self._registers, self.acc_seq())
 
 class MutableIORegisterAutomaton(IORegisterAutomaton, MutableAutomatonMixin):
     def __init__(self):
@@ -254,7 +255,8 @@ class MutableIORegisterAutomaton(IORegisterAutomaton, MutableAutomatonMixin):
                 self._registers.append(reg)
 
     def to_immutable(self) -> IORegisterAutomaton:
-        return IORegisterAutomaton(self._states, self._state_to_trans, self._registers)
+        return IORegisterAutomaton(self._states, self._state_to_trans, self._registers,
+                                   self.acc_seq()                                   )
 
 class Guard(metaclass=ABCMeta):
     """A guard with is_satisfied implements a predicate over the current register valuation and the parameter value. """

z3gi/test/__init__.py

@@ -30,13 +30,13 @@ class Test(metaclass=ABCMeta):
 
 class TestTemplate(metaclass=ABCMeta):
     def __init__(self, trace):
-        self.trace = trace
+        self.tr = trace
 
     def check(self, model: Automaton):
-        return self._check_trace(model, self.trace)
+        return self._check_trace(model, self.tr)
 
     def trace(self):
-        return self.trace
+        return self.tr
 
     @abstractmethod
     def _check_trace(self, model, trace):
@@ -99,7 +99,7 @@ class IORATest(TestTemplate):
         return None
 
     def size(self):
-        return len(self.trace)
+        return len(self.tr)
 
 
 
@@ -125,7 +125,7 @@ class MealyTest(TestTemplate):
         return None
 
     def size(self):
-        return len(self.trace)
+        return len(self.tr)
 
 # Acceptor Test observations are tuples comprising sequences of Actions/Symbols joined by an accept/reject booleans
 class AcceptorTest(TestTemplate):
@@ -140,5 +140,5 @@ class AcceptorTest(TestTemplate):
         return None
 
     def size(self):
-        (seq, acc) = self.trace
+        (seq, acc) = self.tr
         return len(seq)
\ No newline at end of file

z3gi/test/rwalk.py

@@ -91,7 +91,7 @@ class ValueProb(collections.namedtuple("ValueProb", ("history", "register", "fre
         if pick < self.register and len(reg_vals) > 0:
             return reg_vals[rand.randint(0, len(reg_vals)-1)]
         elif pick >= self.register and pick < self.register + self.history and len(his_vals) > 0:
-            return reg_vals[rand.randint(0, len(his_vals) - 1)]
+            return his_vals[rand.randint(0, len(his_vals) - 1)]
         else:
             return fresh_value
 
@@ -113,8 +113,12 @@ class IORARWalkFromState(RWalkFromState):
                 # we have a fresh transition, which means we can either pick a fresh value or any past value
                 # as long as it is not stored in one of the guarded registers in this location
                 fresh_val = 0 if len(values) == 0 else max(values) + 1
-                active_regs = set(itertools.chain([tr.guard.registers() for tr in
-                                             model.transitions(trans.start_state) if not tr is not trans]))
+                r_list = list(itertools.chain((tr.guard.registers() for tr in
+                                            model.transitions(trans.start_state))))
+                print(r_list)
+
+                active_regs =  set() if len(model.registers()) == 0 else \
+                    set(itertools.chain([tr.guard.registers() for tr in model.transitions(trans.start_state)]))
                 active_reg_vals = [reg_val[reg] for reg in active_regs]
                 selectable_reg_vals = [val for val in reg_val.values() if val not in active_reg_vals]
                 selectable_his_vals = [val for val in values if val not in active_reg_vals