Added a working console

example_iotest.py

@@ -5,8 +5,6 @@ from utils import determinize
 from z3gi.learn.ra import RALearner
 from tests.iora_testscenario import *
 from encode.iora import IORAEncoder
-from model.parsing import to_dot
-
 def determinize_act_io(tuple_seq):
     seq = list(itertools.chain.from_iterable(tuple_seq))
     det_seq = determinize(seq)

z3gi/console.py

@@ -60,6 +60,8 @@ if __name__ == '__main__':
     parser.add_argument('-sc', '--sut_class', type=str, choices=list(sut.scalable_sut_classes().keys()),
                         help='the class of the scalable SUT')
     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)')
 
     # test parameters
     parser.add_argument('-mt', '--max_tests', type=int, default=1000, help='the max number of tests executed on a '
@@ -71,7 +73,7 @@ if __name__ == '__main__':
     parser.add_argument('-y', '--yannakakis', action='store_true', help='use yannakakis instead of rwalkfromstate '
                                                                         '(only supports Mealy Machines)')
 
-
+    print(sut.scalable_sut_classes())
     args = parser.parse_args()
     formalism = args.aut
     formalisms = model.defined_formalisms()
@@ -90,7 +92,7 @@ if __name__ == '__main__':
             sut_to_learn = sut.get_simulation(aut_to_learn)
         elif args.mode == 'scalable':
             sut_class_name = args.sut_class
-            sut_size = args.sut_size
+            sut_size = args.size
             sut_to_learn = sut.get_scalable_sut(sut_class_name, aut2suttype[aut_type], sut_size)
         else:
             print("Invalid mode ", args.mode)
@@ -99,7 +101,7 @@ if __name__ == '__main__':
         num_tests = args.max_tests
         rand_test_length = args.rand_length
         reset_prob = args.reset_prob
-        test_generator = aut2rwalkcls[aut_type](rand_test_length, reset_prob)
+        test_generator = aut2rwalkcls[aut_type](sut_to_learn, rand_test_length, reset_prob)
         (automaton, statistics) = alg.learn_mbt(learner, test_generator, num_tests)
 
     print("Learned\n", automaton, "\nWith stats\n", statistics)
\ No newline at end of file

z3gi/model/__init__.py

@@ -121,7 +121,7 @@ class Automaton(metaclass=ABCMeta):
     def __str__(self):
         str_rep = ""
         for (st, acc_seq) in self._acc_trans_seq.items():
-            str_rep += "acc_seq("+ str(st) +") = " + str(list(map(str,acc_seq))) + "\n"
+            str_rep += "acc_seq("+ str(st) +") = " + " , ".join(list(map(str,acc_seq))) + "\n"
         for state in self.states():
             str_rep += str(state) + "\n"
             for tran in self.transitions(state):

z3gi/sut/__init__.py

@@ -2,8 +2,7 @@ from abc import ABCMeta, abstractmethod
 from enum import Enum
 from typing import List, Tuple
 
-from model import Automaton
-from model.fa import Symbol, MealyMachine
+from model.fa import Symbol
 from model.ra import Action
 
 __all__ = [
@@ -136,27 +135,8 @@ class SUTType(Enum):
     def is_transducer(self):
         return  not self.is_acceptor()
 
-from sut.scalable import ScalableSUTClass
-from sut.simulation import Simulation, MealyMachineSimulation
-
-def get_scalable_sut(sut_class_name, sut_type, sut_size):
-    """builds a scalable sut of the given class, type and size"""
-    sut_class = scalable_sut_classes()[sut_class_name]
-    sut = sut_class().new_sut(sut_type, sut_size)
-    return sut
-
-def scalable_sut_classes():
-    """retrieves a dictionary containing available the names of sut classes and their respective class files"""
-    sc = dict()
-    for subclass in ScalableSUTClass.__subclasses__():
-        sc[subclass.__name__.replace("SUTClass","")] = subclass
-    return sc
-
-# TODO replace not suported -> print exit by throwing an adequate exception
-def get_simulation(aut: Automaton) -> Simulation:
-    """builds a simulation for the model. The simulation acts like a deterministic sut."""
-    if aut is MealyMachine:
-        return MealyMachineSimulation(aut)
-    else:
-        print("Simulation not yet supported for ", type(aut))
-        exit(0)
\ No newline at end of file
+# some useful functions
+from sut.scalable import scalable_sut_classes, get_scalable_sut
+from sut.simulation import get_simulation
+
+

z3gi/sut/fifoset.py

-from sut import SUT, ScalableSUTClass, SUTType
-from sut.scalable import ActionSignature
+from sut import SUT, SUTType
+from sut.scalable import ActionSignature, ScalableSUTClass
 
 
 class FIFOSet():

z3gi/sut/login.py

-from sut import SUT, SUTType, ScalableSUTClass
-from sut.scalable import ActionSignature, ObjectSUT
+from sut import SUT, SUTType
+from sut.scalable import ActionSignature, ObjectSUT, ScalableSUTClass
 
 
 class Login():

z3gi/sut/scalable.py

@@ -6,7 +6,6 @@ from model.fa import Symbol
 from model.ra import Action
 from sut import SUTType, SUT, IORAObservation, RAObservation, MealyObservation, DFAObservation
 
-
 class SUTClass(metaclass=ABCMeta):
     """for a class of systems (say stacks, or logins) provides means of instantiating SUTs of different types"""
 
@@ -39,6 +38,25 @@ class ScalableSUTClass(SUTClass, metaclass=ABCMeta):
 ActionSignature = collections.namedtuple("ActionSignature", ('label', 'num_params'))
 
 
+def scalable_sut_classes():
+    """retrieves a dictionary containing available the names of sut classes and their respective class files"""
+    sc = dict()
+    from sut.login import LoginClass
+    from sut.fifoset import FIFOSetClass
+    from sut.stack import StackClass
+    scalable_classes = [LoginClass, FIFOSetClass, StackClass]
+
+    for subclass in scalable_classes:
+        sc[subclass.__name__.replace("Class","")] = subclass
+    return sc
+
+def get_scalable_sut(sut_class_name, sut_type, sut_size):
+    """builds a scalable sut of the given class, type and size"""
+    sut_class = scalable_sut_classes()[sut_class_name]
+    sut = sut_class().new_sut(sut_type, sut_size)
+    return sut
+
+
 class RASUT(metaclass=ABCMeta):
     @abstractmethod
     def input_interface(self) -> List[ActionSignature]:

z3gi/sut/simpleset.py

-from sut import SUT
-from sut.scalable import ActionSignature
+from sut import SUT, SUTType
+from sut.scalable import ActionSignature, ScalableSUTClass
 
 
 class FIFOSet():

z3gi/sut/simulation.py

 from abc import ABCMeta
 from typing import List, Type, Union
-import sys
 
 from model import Acceptor, Transducer, Automaton
 from model.fa import MealyMachine, Symbol
-from . import SUT, DFAObservation, RAObservation, IORAObservation, MealyObservation, TransducerObservation, \
+from . import SUT, MealyObservation, TransducerObservation, \
     AcceptorObservation
 
 class Simulation(SUT,metaclass=ABCMeta):
@@ -42,4 +41,13 @@ class MealyMachineSimulation(TransducerSimulation):
         return super().run(seq)
 
     def input_interface(self):
-        return self.model.input_labels()
\ No newline at end of file
+        return self.model.input_labels()
+
+# TODO replace not suported -> print exit by throwing an adequate exception
+def get_simulation(aut: Automaton) -> Simulation:
+    """builds a simulation for the model. The simulation acts like a deterministic sut."""
+    if isinstance(aut, MealyMachine):
+        return MealyMachineSimulation(aut)
+    else:
+        print("Simulation not yet supported for ", type(aut))
+        exit(0)
\ No newline at end of file

z3gi/sut/stack.py

-from sut import SUT, ScalableSUTClass, SUTType
-from sut.scalable import ActionSignature, ObjectSUT
+from sut import SUT, SUTType
+from sut.scalable import ActionSignature, ObjectSUT, ScalableSUTClass
 
 
 class Stack():