Ok, some added init stuff to tackle the initial non-existant model problem.

There are bugs, be warned.

scrap_alg.py

 import itertools
 
 from learn.algorithm import learn
+from learn.algorithm import learn_mbt
 from learn.ra import RALearner
+from sut.login import new_login_sut
 from test import IORATest
+from test.rwalk import IORARWalkFromState
 from tests.iora_testscenario import *
 from encode.iora import IORAEncoder
 
-learner = RALearner(IORAEncoder())
-test_type = IORATest
-exp = sut_m5
-(model, statistics) = learn(learner, test_type, exp.traces)
-print(model)
-print(statistics)
+def scrap_learn_iora():
+    learner = RALearner(IORAEncoder())
+    test_type = IORATest
+    exp = sut_m5
+    (model, statistics) = learn(learner, test_type, exp.traces)
+    print(model)
+    print(statistics)
+
+def scrap_learn_mbt_iora():
+    learner = RALearner(IORAEncoder())
+    sut = new_login_sut(1)
+    mbt = IORARWalkFromState(sut, 10)
+    (model, statistics) = learn_mbt(learner, mbt, 1000)
+    print(model)
+    print(statistics)
+
+scrap_learn_mbt_iora()
\ No newline at end of file

scrap_iotest.py

@@ -14,7 +14,7 @@ def determinize_act_io(tuple_seq):
     det_duple_seq = [(det_act_seq[i], det_act_seq[i+1]) for i in range(0, len(det_act_seq), 2)]
     return det_duple_seq
 
-def check_ra_against_obs(learner: RALearner, learned_ra:IORegisterAutomaton, m, test_scenario: RaTestScenario):
+def check_ra_against_obs(learned_ra:IORegisterAutomaton, m, test_scenario: RaTestScenario):
     """Checks if the learned RA corresponds to the scenario observations"""
     for trace in test_scenario.traces:
         trace = determinize_act_io(trace)
@@ -36,8 +36,9 @@ for i in range(1,2):
         learner.add(trace)
     (_, ra, m) = learner._learn_model(exp.nr_locations-1,exp.nr_locations+1,exp.nr_registers)
     if m is not None:
+        print(m)
         model = ra.export(m)
         print(model)
-        check_ra_against_obs(learner, model, m, exp)
+        check_ra_against_obs( model, m, exp)
     else:
         print("unsat")
\ No newline at end of file

z3gi/learn/algorithm.py

@@ -6,6 +6,11 @@ from learn import Learner
 from test import TestTemplate, TestGenerator
 import time
 
+__all__ = [
+    "learn",
+    "learn_mbt"
+    ]
+
 class Statistics():
     def __init__(self):
         self.num_tests = 0
@@ -73,8 +78,8 @@ def learn(learner:Learner, test_type:type, traces: List[object]) -> Tuple[Automa
                     break
         return (model, statistics)
 
-def learn_mbt(learner:Learner, test_generator:TestGenerator) -> Tuple[Automaton, Statistics]:
-    """ takes learner and a test generator, and generates a model"""
+def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> Tuple[Automaton, Statistics]:
+    """ takes learner, a test generator, and bound on the number of tests and generates a model"""
     next_test = test_generator.gen_test(None)
     statistics = Statistics()
     if next_test is None:
@@ -93,6 +98,7 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator) -> Tuple[Automaton,
             end_time = int(time.time() * 1000)
             statistics.add_learning_time(end_time - start_time)
             done = True
+            # we first check the tests that already have been generated
             for next_test in generated_tests:
                 ce = next_test.check(model)
                 if ce is not None:
@@ -104,7 +110,12 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator) -> Tuple[Automaton,
                     break
             if not done:
                 continue
-            for next_test in test_generator.gen_test_iter(model):
+            # we then generate and check new tests, until either we find a CE,
+            # or the suite is exhausted or we have run the intended number of tests
+            for i in range(0, max_tests):
+                next_test = test_generator.gen_test(model)
+                if next_test is None:
+                    break
                 generated_tests.append(next_test)
                 ce = next_test.check(model)
                 if ce is not None:

z3gi/main.py

@@ -5,7 +5,7 @@ from sut.login import new_login_sut
 from sut.stack import new_stack_sut
 from sut.fifoset import new_fifoset_sut
 from test import IORATest
-from test.generation import ExhaustiveRAGenerator
+from test.exhaustive import ExhaustiveRAGenerator
 
 # stack_sut = new_stack_sut(2)
 # gen = ExhaustiveRAGenerator(stack_sut)

z3gi/sut/__init__.py

@@ -7,6 +7,16 @@ from model.fa import Symbol
 from model.ra import Action
 from enum import Enum
 
+class Observation():
+    @abstractmethod
+    def trace(self):
+        """returns the trace to be added to the solver"""
+        pass
+
+    @abstractmethod
+    def inputs(self):
+        """returns all the inputs from an observation"""
+        pass
 
 class SUT(metaclass=ABCMeta):
     OK = "OK"
@@ -57,17 +67,6 @@ class RASUT(metaclass=ABCMeta):
         """Runs a sequence of inputs on the SUT and returns an observation"""
         pass
 
-class Observation():
-    @abstractmethod
-    def trace(self):
-        """returns the trace to be added to the solver"""
-        pass
-
-    @abstractmethod
-    def inputs(self):
-        """returns all the inputs from an observation"""
-        pass
-
 class DFAObservation():
     def __init__(self, seq, acc):
         self.seq = seq

z3gi/test/rwalk.py

@@ -7,12 +7,15 @@ import itertools
 
 from model import Automaton, Transition
 from model.ra import IORATransition, IORegisterAutomaton, EqualityGuard, OrGuard, Action, Register
-from sut import SUT
+from sut import SUT, ActionSignature
 from test import TestGenerator, Test, AcceptorTest, MealyTest, IORATest
 import random
 
 rand = random.Random(0)
 
+def rand_sel(l:List):
+    return l[rand.randint(0, len(l)-1)]
+
 class RWalkFromState(TestGenerator, metaclass=ABCMeta):
     def __init__(self, sut:SUT, test_gen, rand_length, rand_start_state=True):
         self.rand_length = rand_length
@@ -22,22 +25,44 @@ class RWalkFromState(TestGenerator, metaclass=ABCMeta):
 
     def gen_test(self, model: Automaton) -> Test:
         """generates a test comprising an access sequence and a random sequence"""
-        if self.rand_start_state:
-            crt_state = model.states()[rand.randint(0, len(model.states()) - 1)]
+        if model is None:
+            seq = self._generate_init()
         else:
-            crt_state = model.start_state()
-
-        trans_path = list(model.acc_trans_seq(crt_state))
-        for _ in range(0, self.rand_length):
-            transitions = model.transitions(crt_state)
-            r_trans = transitions[rand.randint(0, len(transitions)-1)]
-            crt_state = r_trans.end_state
-            trans_path.append(r_trans)
-        seq = self._generate_seq(model, trans_path)
+            if self.rand_start_state:
+                crt_state = model.states()[rand.randint(0, len(model.states()) - 1)]
+            else:
+                crt_state = model.start_state()
+
+            trans_path = list(model.acc_trans_seq(crt_state))
+            for _ in range(0, self.rand_length):
+                transitions = model.transitions(crt_state)
+                r_trans = transitions[rand.randint(0, len(transitions)-1)]
+                crt_state = r_trans.end_state
+                trans_path.append(r_trans)
+            seq = self._generate_seq(model, trans_path)
         obs = self.sut.run(seq)
         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"""
@@ -60,7 +85,7 @@ class MealyRWalkFromState(RWalkFromState):
     def __init__(self, sut:SUT, rand_length, rand_start_state=True):
         super().__init__(self, sut, MealyTest, rand_length, rand_start_state)
 
-class ValueProb(collections.nametuple("ValueProb", ("history", "register", "fresh"))):
+class ValueProb(collections.namedtuple("ValueProb", ("history", "register", "fresh"))):
     def select(self, reg_vals:List[int], his_vals:List[int], fresh_value):
         pick = rand.random()
         if pick < self.register and len(reg_vals) > 0: