Smarter translation

example_runs.py

@@ -80,7 +80,7 @@ def scalable_learn_mbt_ra():
     print(statistics)
 
 def sim_learn_mbt_yan_mealy(dot_path):
-    learner = FAILearner(MealyTreeIEncoder())# FALearner(MealyEncoder())
+    learner = FALearner(MealyEncoder())
     learner.set_timeout(10000)
     dot_aut = build_automaton_from_dot("MealyMachine", dot_path)
     dot_sut = MealyMachineSimulation(dot_aut)

z3gi/benchmark.py

@@ -178,7 +178,7 @@ b = Benchmark()
 
 # add the sut classes we want to benchmark
 #b.add_sut(FIFOSetClass())
-b.add_sut(LoginClass(), SUTType.Mealy)
+b.add_sut(LoginClass(), SUTType.DFA)
 #b.add_sut(StackClass())
 
 #b.add_sut(FIFOSetClass(), SUTType.DFA)

z3gi/define/fa.py

@@ -13,10 +13,10 @@ class FSM(Automaton,metaclass=ABCMeta):
         self.start = self.states[0]
 
 class DFA(FSM):
-    def __init__(self, labels, num_states):
-        super().__init__(num_states)
+    def __init__(self, labels, num_states, state_enum=declsort_enum, label_enum=declsort_enum):
+        super().__init__(num_states, state_enum=state_enum)
         labels = list(labels)
-        self.Label, elements = dt_enum('Label', labels)
+        self.Label, elements = label_enum('Label', labels)
         self.labels = {labels[i]: elements[i] for i in range(len(labels))}
         self.transition = z3.Function('transition', self.State, self.Label, self.State)
         self.output = z3.Function('output', self.State, z3.BoolSort())
@@ -86,7 +86,7 @@ class DFABuilder(object):
         self.dfa = dfa
 
     def build_dfa(self, m : z3.ModelRef) -> model.fa.DFA:
-        tr = FATranslator(self.dfa)
+        tr = DFATranslator(m, self.dfa)
         mut_dfa =  model.fa.MutableDFA()
         for state in self.dfa.states:
             accepting = m.eval(self.dfa.output(state))
@@ -103,47 +103,39 @@ class DFABuilder(object):
         return mut_dfa.to_immutable()
 
 class MealyTranslator(object):
-    """Provides translation from z3 constants to RA elements. """
-    def __init__(self, model, mm: MealyMachine):
+    """Provides translation from z3 constants to Mealy elements. It evaluates everything (s.t. variables are resolved
+    to their actual values), enabling it to translate both variables and values."""
+    def __init__(self, model : z3.ModelRef, mm: MealyMachine):
         self._model = model
         self._mm = mm
-        self._z3_to_inp = dict(map(reversed, mm.inputs.items()))
-        self._z3_to_out = dict(map(reversed, mm.outputs.items()))
+        self._z3_to_inp = {model.eval(mm.inputs[inp]):inp for inp in mm.inputs.keys() }
+        self._z3_to_out = {model.eval(mm.outputs[out]):out for out in mm.outputs.keys() }
+        self._z3_states = list(map(model.eval, mm.states))
 
 
     def z3_to_state(self, z3state):
-        if z3state in self._mm.states:
-            return "q" + str(self._mm.states.index(z3state))
-        else:
-            return "q" + str(list(map(self._model.eval, self._mm.states)).index(z3state))
+        return "q" + str(self._z3_states.index(self._model.eval(z3state)))
 
     def z3_to_input(self, z3label):
-        if z3label in self._z3_to_inp:
-            return self._z3_to_inp[z3label]
-        else:
-            for inp in self._z3_to_inp:
-                if self._model.eval(inp) == self._model.eval(z3label):
-                    return self._z3_to_inp[inp]
+        return self._z3_to_inp[self._model.eval(z3label)]
 
     def z3_to_output(self, z3label):
-        if z3label in self._z3_to_out:
-            return self._z3_to_out[z3label]
-        else:
-            for out in self._z3_to_out:
-                if self._model.eval(out) == self._model.eval(z3label):
-                    return self._z3_to_out[out]
-
-class FATranslator(object):
-    """Provides translation from z3 constants to RA elements. """
-    def __init__(self, fa:FSM):
-        self.fa = fa
+        return self._z3_to_out[self._model.eval(z3label)]
+
+class DFATranslator(object):
+    """Provides translation from z3 constants to DFA elements. """
+    def __init__(self, model : z3.ModelRef, fa:DFA):
+        self._fa = fa
+        self._z3_to_label = {model.eval(fa.labels[inp]): inp for inp in fa.labels.keys()}
+        self._z3_states = list(map(model.eval, fa.states))
+        self._model = model
 
 
     def z3_to_bool(self, z3bool):
         return str(z3bool) == "True"
 
     def z3_to_state(self, z3state):
-        return "q"+str(self.fa.states.index(z3state))
+        return "q"+str(self._z3_states.index(self._model.eval(z3state)))
 
     def z3_to_label(self, z3label):
-        return str(z3label)
+        return self._z3_to_label[self._model.eval(z3label)]

z3gi/encode/fa.py

@@ -29,7 +29,14 @@ class DFAEncoder(Encoder):
         return dfa, constraints
 
     def axioms(self, dfa: DFA, mapper: Mapper):
-        return []
+        return [
+            z3.And([z3.And([z3.Or([dfa.transition(state, label) == to_state
+                                   for to_state in dfa.states]) for state in dfa.states])
+                    for label in dfa.labels.values()]),
+            z3.Distinct(list(dfa.labels.values())),
+            z3.Distinct(list(dfa.states)),
+            z3.Distinct([mapper.element(node.id) for node in self.cache])
+        ]
 
     def node_constraints(self, dfa, mapper):
         constraints = []

z3gi/learn/fa.py

@@ -6,23 +6,22 @@ from model import Automaton
 import define.fa
 
 class FALearner(Learner):
-    def __init__(self, encoder, solver=None, verbose=False, stop_unknown=False):
+    def __init__(self, encoder, solver=None, verbose=False):
         super().__init__()
         if not solver:
             solver = z3.Solver()
         self.solver = solver
         self.encoder = encoder
         self.verbose = verbose
-        self.stop_unknown = stop_unknown
 
     def add(self, trace):
         self.encoder.add(trace)
 
-    def model(self, min_states=1, max_states=20, old_definition:define.fa.FSM=None) -> Tuple[Automaton, define.fa.FSM]:
+    def model(self, min_states=1, max_states=20, old_definition:define.fa.FSM=None, ensure_min=False) -> Tuple[Automaton, define.fa.FSM]:
         if old_definition is not None:
             min_states = len(old_definition.states)
         (succ, fa, m) = self._learn_model(min_states=min_states,
-                                        max_states=max_states)
+                                        max_states=max_states, ensure_min=ensure_min)
         self.solver.reset()
         if succ:
             return fa.export(m), fa
@@ -33,7 +32,7 @@ class FALearner(Learner):
         #    to = fa
         #    return (None, to)
 
-    def _learn_model(self, min_states=1, max_states=10):
+    def _learn_model(self, min_states=1, max_states=10, ensure_min=False):
         """generates the definition and model for an fa whose traces include the traces added so far
         In case of failure, the second argument of the tuple signals occurrence of a timeout"""
         for num_states in range(min_states, max_states + 1):
@@ -51,8 +50,8 @@ class FALearner(Learner):
                 model = self.solver.model()
                 return (True, fa, model)
             else:
-                # timeout
-                if result == z3.unknown and self.stop_unknown:
+                # timeout, if minimality guarantee is required, we have to stop here
+                if result == z3.unknown and ensure_min:
                     return (False, True, None)
                 # TODO: process the unsat core?
                 pass