We can now learn mealy machines without resets

z3gi/console.py

@@ -5,6 +5,7 @@ import learn.algorithm as alg
 import parse.importer as parse
 import sut
 import model.fa
+import model.gen as gen
 
 from encode.fa import MealyEncoder, DFAEncoder
 from encode.iora import IORAEncoder
@@ -52,8 +53,9 @@ if __name__ == '__main__':
                                                  '(1) passively learn from traces file\n'
                                                  '(2) actively learn a Mealy Machine system described by a .dot file\n'
                                                  '(3) actively learn a Mealy Machine system described by a .dot file without resets\n'
-                                                 '(4) actively learn a scalable SUT (system) of a given size')
-    parser.add_argument('-m', '--mode', type=str, choices=['traces', 'dot', 'dotnorst', 'scalable'], required=True)
+                                                 '(4) actively learn a randomly generated Mealy Machine without resets\n'
+                                                 '(5) actively learn a scalable SUT (system) of a given size')
+    parser.add_argument('-m', '--mode', type=str, choices=['traces', 'dot', 'dotnorst','randnorst', 'scalable'], required=True)
     parser.add_argument('-f', '--file', type=str, help='the file location to the dot/traces file')
     parser.add_argument('-a', '--aut', type=str, choices=list(model.defined_formalisms().keys()), required=True,
                         help='the type of automaton (formalism) described in the file or '
@@ -63,9 +65,14 @@ if __name__ == '__main__':
     parser.add_argument('-s', '--size', type=int, help='the size of the scalable SUT')
     parser.add_argument('-t', '--timeout', type=int, help='the timeout used in learning '
                                                           '(i.e. the time limit given to the solver to solve the constraints)')
+    parser.add_argument('-ni', '--num-inputs', type=int, default=2, help='the input alphabet size of the random Mealy machine')
+    parser.add_argument('-no', '--num-outputs', type=int, default=2,
+                        help='the output alphabet size of the random Mealy machine')
+    parser.add_argument('-ns', '--num-states', type=int, default=10,
+                        help='the number of states of the random Mealy machine')
 
     # test parameters
-    parser.add_argument('-mi', '--max_inputs', type=int, default=10, help='the max number of inputs executed on a '
+    parser.add_argument('-mi', '--max_inputs', type=int, default=1000, help='the max number of inputs executed on a '
                                                                           'hypothesis before it is judged to be correct, '
                                                                           'only considered for learning with no resets')
     parser.add_argument('-mt', '--max_tests', type=int, default=1000, help='the max number of tests executed on a '
@@ -96,6 +103,14 @@ if __name__ == '__main__':
             sut_to_learn = sut.get_no_rst_simulation(aut_to_learn)
             max_inputs = args.max_inputs
             (automaton, statistics) = alg.learn_no_reset(sut_to_learn, learner, max_inputs)
+        elif args.mode == 'randnorst':
+            ni = args.num_inputs
+            no = args.num_inputs
+            ns = args.num_states
+            aut_to_learn = gen.random_mealy(ni, no, ns)
+            sut_to_learn = sut.get_no_rst_simulation(aut_to_learn)
+            max_inputs = args.max_inputs
+            (automaton, statistics) = alg.learn_no_reset(sut_to_learn, learner, max_inputs)
         else:
             if args.mode == 'dot':
                 dot_file = args.file

z3gi/learn/algorithm.py

@@ -8,6 +8,7 @@ from sut import StatsTracker, SUT, NoRstSUT
 from sut.scalable import ActionSignature
 from sut.simulation import get_no_rst_simulation
 from test import TestGenerator, Test
+import utils
 import time
 
 __all__ = [
@@ -79,13 +80,6 @@ def learn(learner:Learner, test_type:type, traces: List[object]) -> Tuple[Automa
                     break
         return (model, statistics)
 
-
-import random
-rand = random.Random(0)
-
-def rand_sel(l:List):
-    return l[rand.randint(0, len(l)-1)]
-
 def learn_no_reset(sut:NoRstSUT, learner:Learner, max_inputs:int) -> Tuple[Union[Automaton, None], Statistics]:
     """ takes a non-reseting SUL, a learner, a test generator, and a bound on the number of inputs and generates a model"""
     trace = []
@@ -101,14 +95,16 @@ def learn_no_reset(sut:NoRstSUT, learner:Learner, max_inputs:int) -> Tuple[Union
         sim.steps([inp for (inp,_) in trace])
         done = True
         for _ in range(0, max_inputs):
-            rand_inp = rand_sel(alpha)
+            rand_inp = utils.rand_sel(alpha)
             out_sut = sut.step(rand_inp)
             trace.append((rand_inp, out_sut))
             out_hyp = sim.step(rand_inp)
             if out_sut != out_hyp:
                 learner.add(list(trace))
                 (hyp, definition) = learner.model(old_definition=definition)
+                print("new hyp")
                 done = False
+                break
         if hyp is None:
             return None, None
     statistics.inputs = len(trace) - max_inputs

z3gi/model/__init__.py

@@ -152,7 +152,7 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
             self._state_to_trans[state] = []
         self._state_to_trans[state].append(transition)
 
-    def generate_acc_seq(self:Automaton):
+    def generate_acc_seq(self:Automaton, remove_unreachable=True):
         """generates access sequences for an automaton. It removes states that are not reachable."""
         new_acc_seq = dict()
         ptree = get_prefix_tree(self)
@@ -162,7 +162,8 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
             node = ptree.find_node(pred)
             if node is None:
                 print("Could not find state {0} in tree {1} \n for model \n {2}".format(state, ptree, self))
-                self._remove_state(state)
+                if remove_unreachable:
+                    self._remove_state(state)
                 continue
                 #print("Could not find state {0} in tree {1} \n for model \n {2}".format(state, ptree, self))
                 #raise InvalidAutomaton
@@ -216,11 +217,24 @@ class MutableAcceptorMixin(MutableAutomatonMixin, metaclass=ABCMeta):
         super().add_state(state)
         self._state_to_acc[state] = accepts
 
+def is_strongly_connected(aut : Automaton):
+    states = list(aut.states())
+    for state in states:
+        ptree = get_prefix_tree(aut, from_state=state)
+        for s in states:
+            pred = lambda x: (x.state == s)
+            node = ptree.find_node(pred)
+            if node is None:
+                return False
+    return True
+
 
-def get_prefix_tree(aut : Automaton):
+def get_prefix_tree(aut : Automaton, from_state=None):
     visited  = set()
     to_visit = set()
-    root = PrefixTree(aut.start_state())
+    if from_state is None:
+        from_state = aut.start_state()
+    root = PrefixTree(from_state)
     to_visit.add(root)
     while len(to_visit) > 0:
         crt_node = to_visit.pop()

z3gi/utils.py

 import itertools
+import random
+from typing import List
+
+rand = random.Random(0)
+
+__all__ = [
+    "rand_sel",
+    "determinize"
+    ]
+
+def rand_sel(l:List):
+    return l[rand.randint(0, len(l)-1)]
 
 
 class Tree(object):