updated files

example_runs.py

@@ -13,6 +13,7 @@ from sut.login import new_login_sut, LoginClass
 from sut.simulation import MealyMachineSimulation
 from test import IORATest
 from test.rwalk import IORARWalkFromState, MealyRWalkFromState, DFARWalkFromState, RARWalkFromState
+from test.yanna import YannakakisTestGenerator
 from tests.iora_testscenario import *
 from encode.iora import IORAEncoder
 
@@ -65,20 +66,29 @@ def scalable_learn_mbt_ra():
     print(model)
     print(statistics)
 
-def sim_learn_mbt_ra():
+def sim_learn_mbt_mealy():
     learner = FALearner(MealyEncoder())
     learner.set_timeout(10000)
     import os.path
     maestro_aut = build_automaton_from_dot("MealyMachine", os.path.join("resources", "models", "bankcards", "MAESTRO.dot"))
-    print(maestro_aut)
-    #exit(2)
     maestro_sut = MealyMachineSimulation(maestro_aut)
     mbt = MealyRWalkFromState(maestro_sut, 3, 0.2)
     (model, statistics) = learn_mbt(learner, mbt, 10000)
     print(model)
     print(statistics)
 
+def sim_learn_mbt_yan_mealy():
+    learner = FALearner(MealyEncoder())
+    learner.set_timeout(10000)
+    import os.path
+    maestro_aut = build_automaton_from_dot("MealyMachine", os.path.join("resources", "models", "bankcards", "MAESTRO.dot"))
+    maestro_sut = MealyMachineSimulation(maestro_aut)
+    yan_cmd = os.path.join("resources", "binaries", "yannakakis.exe")
+    mbt = YannakakisTestGenerator(maestro_sut, yan_cmd)
+    (model, statistics) = learn_mbt(learner, mbt, 10000)
+    print(model)
+    print(statistics)
 
-sim_learn_mbt_ra()
+sim_learn_mbt_yan_mealy()
 #scalable_learn_mbt_mealy()
 #scalable_learn_mbt_iora()

z3gi/test/__init__.py

@@ -5,6 +5,8 @@ import itertools
 from model import Automaton, Acceptor, Transducer
 from model.fa import Symbol
 from model.ra import IORegisterAutomaton, Action
+from sut import SUT
+from sut.scalable import ActionSignature
 from utils import determinize
 
 
@@ -52,10 +54,38 @@ class TestGenerator(metaclass=ABCMeta):
         pass
 
     def gen_test_iter(self, model: Automaton) -> Iterable[Test]:
+        self.initialize(model)
         test = self.gen_test(model)
         while test is not None:
             yield test
             test = self.gen_test(model)
+        self.terminate()
+
+    def gen_blind_test(self, sut:SUT):
+        """generates a sequence covering all input elements in the sut interface"""
+        seq = []
+        for abs_inp in self.sut.input_interface():
+            cnt = 0
+            # if it's RA stuff
+            if isinstance(abs_inp, ActionSignature):
+                if abs_inp.num_params == 0:
+                    val = None
+                else:
+                    val = cnt
+                    cnt += 1
+                seq.append(Action(abs_inp.label, val))
+            elif isinstance(abs_inp, str):
+                seq.append(abs_inp)
+            else:
+                raise Exception("Unrecognized type")
+        return seq
+
+    def initialize(self, model: Automaton):
+        """feeds the tests generator the supplied automaton in an initialization step"""
+        pass
+
+    def terminate(self):
+        pass
 
 class TracesGenerator(metaclass=ABCMeta):
     def __init__(self, traces = list()):
@@ -72,13 +102,17 @@ class Tester(metaclass=ABCMeta):
 
     def find_ce(self, model:Automaton):
         """generates an observation which exposes a counterexample"""
+        self.generator.initialize(model)
+        ce = None
         while True:
             test = self.generator.gen_test(model)
             if test is None:
-                return None
+                break
             trace = test.check(model)
             if trace is not None:
-                return trace
+                ce = trace
+                break
+        self.generator.terminate()
 
 
 def determinize_act_io(tuple_seq):

z3gi/test/rwalk.py

@@ -34,7 +34,7 @@ class RWalkFromState(TestGenerator, metaclass=ABCMeta):
         if model is None:
             # if the model is None, generate a test which includes all inputs (so at least we know the next generated
             # model will be input enabled)
-            seq = self._generate_init()
+            seq = self.gen_blind_test(self.sut)
         else:
             # select a random state
             if self.rand_start_state:
@@ -64,25 +64,6 @@ class RWalkFromState(TestGenerator, metaclass=ABCMeta):
         test = self.test_gen(obs.trace())
         return test
 
-    def _generate_init(self):
-        """generates a sequence covering all input elements in the sut interface"""
-        seq = []
-        for abs_inp in self.sut.input_interface():
-            cnt = 0
-            # if it's RA stuff
-            if isinstance(abs_inp, ActionSignature):
-                if abs_inp.num_params == 0:
-                    val = None
-                else:
-                    val = cnt
-                    cnt += 1
-                seq.append(Action(abs_inp.label, val))
-            elif isinstance(abs_inp, str):
-                seq.append(abs_inp)
-            else:
-                raise Exception("Unrecognized type")
-        return seq
-
     @abstractmethod
     def _generate_seq(self, model: Automaton, trans_path:List[Transition]):
         """generates a sequence of inputs for the randomly chosen transition path"""