Interesting development

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())
+b.add_sut(LoginClass(), SUTType.Mealy)
 #b.add_sut(StackClass())
 
 #b.add_sut(FIFOSetClass(), SUTType.DFA)
@@ -191,16 +191,16 @@ b.add_sut(LoginClass())
 t_desc = TestDesc(max_tests=10000, prop_reset=0.2, rand_length=3)
 
 # give an smt timeout value (in ms)
-timeout = 150000
+timeout = 10000
 
 # how many times each experiment should be run
-num_exp = 5
+num_exp = 2
 
 # up to what systems of what size do we want to run experiments (set to None if size is ignored as a stop condition)
 max_size = None
 
 # do you want to augment test generation by coloring (before the rwalk, we explore all uncolored transitions in the hyp)
-use_coloring = True
+use_coloring = False
 
 # run the benchmark and collect results
 results = []

z3gi/define/__init__.py

@@ -15,7 +15,7 @@ def int_enum(name, elements):
 
 def declsort_enum(name, elements):
     d = z3.DeclareSort(name)
-    return d, [z3.Const(element) for element in elements]
+    return d, [z3.Const(element, d) for element in elements]
 
 class Automaton(metaclass=ABCMeta):
     @abstractmethod

z3gi/define/fa.py

@@ -2,7 +2,7 @@ from abc import ABCMeta, abstractmethod
 
 import z3
 import model.fa
-from define import Automaton, dt_enum
+from define import Automaton, dt_enum, declsort_enum
 from model import Transition
 
 
@@ -28,7 +28,7 @@ class DFA(FSM):
 
 
 class MealyMachine(FSM):
-    def __init__(self, input_labels, output_labels, num_states, state_enum=dt_enum, label_enum=dt_enum):
+    def __init__(self, input_labels, output_labels, num_states, state_enum=declsort_enum, label_enum=declsort_enum):
         super().__init__(num_states, state_enum=state_enum)
         self.Input, elements = label_enum('Input', input_labels)
         self.inputs = {input_labels[i]: elements[i] for i in range(len(input_labels))}
@@ -47,8 +47,12 @@ class Mapper(object):
         self.Element = z3.DeclareSort('Element')
         self.start = self.element(0)
         self.map = z3.Function('map', self.Element, fa.State)
+        self._elements = dict()
 
     def element(self, name):
+        #if name not in self._elements:
+        #    self._elements[name] = z3.Const("n"+str(name), self.Element)
+        #return self._elements[name]
         return z3.Const("n"+str(name), self.Element)
 
 

z3gi/encode/fa.py

@@ -75,7 +75,16 @@ class MealyEncoder(Encoder):
         return mm, constraints
 
     def axioms(self, mm: MealyMachine, mapper: Mapper):
-        return []
+        return [
+            z3.And([z3.And([z3.Or([mm.transition(state, input) == to_state
+                                     for to_state in mm.states]) for state in mm.states])
+                  for input in mm.inputs.values()]),
+            z3.Distinct(list(mm.inputs.values())),
+            z3.Distinct(list(mm.outputs.values())),
+            z3.Distinct(list(mm.states)),
+            z3.Distinct([mapper.element(node.id) for node in self.cache])
+        ]
+        #return []
 
     def node_constraints(self, mm, mapper):
         constraints = []

z3gi/learn/fa.py

@@ -6,13 +6,14 @@ from model import Automaton
 import define.fa
 
 class FALearner(Learner):
-    def __init__(self, encoder, solver=None, verbose=False):
+    def __init__(self, encoder, solver=None, verbose=False, stop_unknown=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)
@@ -38,6 +39,7 @@ class FALearner(Learner):
         for num_states in range(min_states, max_states + 1):
             fa, constraints = self.encoder.build(num_states)
             self.solver.reset()
+            self.solver.set(":random-seed", 0)
             self.solver.add(constraints)
             if self.timeout is not None:
                 self.solver.set("timeout", self.timeout)
@@ -50,7 +52,7 @@ class FALearner(Learner):
                 return (True, fa, model)
             else:
                 # timeout
-                if result == z3.unknown:
+                if result == z3.unknown and self.stop_unknown:
                     return (False, True, None)
                 # TODO: process the unsat core?
                 pass

z3gi/model/fa.py

@@ -96,4 +96,6 @@ class MutableMealyMachine(MealyMachine, MutableAutomatonMixin):
         super().__init__([], {})
 
     def to_immutable(self) -> MealyMachine:
-        return MealyMachine(self._states, self._state_to_trans, self.acc_trans_seq())
+        return MealyMachine(sorted(self._states),
+                            {state:list(sorted(self._state_to_trans[state], key=str)) for state in sorted(self._states)},
+                            self.acc_trans_seq())

z3gi/sut/scalable.py

@@ -33,6 +33,9 @@ class ScalableSUTClass(SUTClass, metaclass=ABCMeta):
             return sut
         else:
             return None
+    
+    def num_states(self, size:int):
+        pass
 
 
 ActionSignature = collections.namedtuple("ActionSignature", ('label', 'num_params'))

z3gi/sut/simulation.py

@@ -41,7 +41,8 @@ class MealyMachineSimulation(TransducerSimulation):
         return super().run(seq)
 
     def input_interface(self):
-        return self.model.input_labels()
+        #TODO remove non-deterministic behavior
+        return list(sorted(self.model.input_labels()))
 
 # TODO replace not suported -> print exit by throwing an adequate exception
 def get_simulation(aut: Automaton) -> Simulation: