Commit ea6bd0c4 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

many print-outs

parent 6602b32e
......@@ -20,7 +20,7 @@ from test.rwalk import DFARWalkFromState, MealyRWalkFromState, RARWalkFromState,
class SutDesc(collections.namedtuple("SutDesc", 'sut_class type size')):
def __str__(self):
return str(self.type) + "_" + str(self.sut_class.__class__.__name__).replace("Class", "") + "(" + str(self.size) + ")"
return str(self.type).replace("SUTType.","") + "_" + str(self.sut_class.__class__.__name__).replace("Class", "") + "(" + str(self.size) + ")"
TestDesc = collections.namedtuple("TestDesc", 'max_tests rand_length prop_reset')
class CollectedStats(collections.namedtuple("CollectedStats", "states registers learn_tests "
......@@ -102,7 +102,7 @@ b.add_setup(SUTType.RA, RALearner(RAEncoder()), RARWalkFromState)
b.add_setup(SUTType.IORA, RALearner(IORAEncoder()), IORARWalkFromState)
# add the sut classes we want to benchmark
b.add_sut(LoginClass(), SUTType.RA)
b.add_sut(LoginClass(), SUTType.DFA)
# create a test description
t_desc = TestDesc(max_tests=10000, prop_reset=0.2, rand_length=5)
......
......@@ -109,6 +109,10 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
if ret is None:
return (None, statistics)
(model, definition) = ret
for learner_test in learner_tests:
print(learner_test.trace())
if learner_test.check(model) is not None:
raise Exception("Learner test doesn't pass "+str(learner_test.trace()))
print(model)
end_time = int(time.time() * 1000)
statistics.add_learning_time(end_time - start_time)
......
......@@ -28,12 +28,15 @@ class FALearner(Learner):
def model(self, min_states=1, max_states=20, old_definition:define.fa.FSM=None) -> Tuple[Automaton, define.fa.FSM]:
if old_definition is not None:
min_states = len(old_definition.states)
print("initial def ", min_states)
(succ, fa, m) = self._learn_model(min_states=min_states,
max_states=max_states)
if succ:
return fa.export(m), fa
else:
return None
return None
# to = fa
# return (None, to)
# to = fa
# return (None, to)
......@@ -41,7 +44,7 @@ class FALearner(Learner):
"""generates the definition and model for an fa whose traces include the traces added so far
In case of failure, the second argument of the tuple signals occurrence of a timeout"""
for num_states in range(min_states, max_states + 1):
print("Learning with ", min_states)
print("Learning with ", num_states, " states")
fa, constraints = self.encoder.build(num_states)
self.solver.add(constraints)
if self.timeout is not None:
......@@ -53,6 +56,7 @@ class FALearner(Learner):
print("Result {0} ".format(result))
if result == z3.sat:
model = self.solver.model()
print(model)
self.solver.reset()
return (True, fa, model)
else:
......
......@@ -130,7 +130,7 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
pred = lambda x: (x.state == state)
node = ptree.find_node(pred)
if node is None:
raise Exception("Could not find state {0} in tree {1}".format(state, ptree))
raise Exception("Could not find state {0} in tree {1} \n for model \n {2}".format(state, ptree, self))
new_acc_seq[state] = node.path()
assert(len(new_acc_seq) == len(self.states()))
self._acc_trans_seq = new_acc_seq
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment