Commit 8577efcc authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

many print-outs

parent ea6bd0c4
......@@ -12,6 +12,7 @@ from learn.ra import RALearner
from model import Automaton
from model.ra import RegisterMachine
from sut import SUTType, ScalableSUTClass
from sut.fifoset import FIFOSetClass
from sut.login import LoginClass
from test import TestGenerator
from learn.algorithm import learn_mbt, Statistics
......@@ -28,6 +29,17 @@ class CollectedStats(collections.namedtuple("CollectedStats", "states registers
pass
def get_learner_setup(sut_type:SUTType):
if sut_type is SUTType.DFA:
return (FALearner(DFAEncoder()), DFARWalkFromState)
elif sut_type is SUTType.Mealy:
return (FALearner(MealyEncoder()), MealyRWalkFromState)
elif sut_type is SUTType.RA:
return (RALearner(RAEncoder()), RARWalkFromState)
elif sut_type is SUTType.IORA:
return (RALearner(IORAEncoder()), IORARWalkFromState)
raise Exception("Invalid setup")
class Benchmark:
def __init__(self):
self.suts:List[Tuple[ScalableSUTClass, SUTType]] = []
......@@ -48,21 +60,24 @@ class Benchmark:
self.learn_setup[sut_type] = (sut_learner, sut_tester)
return self
def _run_benchmark(self, sut_class:ScalableSUTClass, sut_type:SUTType, learner:Learner,
test_gen:type, test_desc:TestDesc, tout:int) -> List[Tuple[SutDesc, CollectedStats]]:
def _run_benchmark(self, sut_class:ScalableSUTClass, sut_type:SUTType, test_desc:TestDesc, tout:int) \
-> List[Tuple[SutDesc, CollectedStats]]:
results = []
learner.set_timeout(tout)
size = 1
while True:
sut = sut_class.new_sut(sut_type, size)
learner,test_gen = get_learner_setup(sut_type)
learner.set_timeout(tout)
# ugly but there you go
tester = test_gen(sut, test_desc.rand_length, test_desc.prop_reset)
rand_length = size + test_desc.rand_length
tester = test_gen(sut, rand_length, test_desc.prop_reset)
(model, statistics) = learn_mbt(learner, tester, test_desc.max_tests)
if model is None:
break
else:
imp_stats = self._collect_stats(model, statistics)
results.append( (SutDesc(sut_class, sut_type, size), imp_stats))
sut_desc = SutDesc(sut_class, sut_type, size)
results.append( (sut_desc, imp_stats))
size += 1
return results
......@@ -79,8 +94,7 @@ class Benchmark:
def run_benchmarks(self, test_desc:TestDesc, timeout:int) -> List[Tuple[SutDesc, CollectedStats]]:
results = []
for sut_class, sut_type in self.suts:
(learner, tester) = self.learn_setup[sut_type]
res = self._run_benchmark(sut_class, sut_type, learner, tester, test_desc, timeout)
res = self._run_benchmark(sut_class, sut_type, test_desc, timeout)
results.extend(res)
return results
......@@ -96,19 +110,21 @@ def print_results(results : List[Tuple[SutDesc, CollectedStats]]):
b = Benchmark()
# adding learning setups for each type of machine
b.add_setup(SUTType.DFA, FALearner(DFAEncoder()), DFARWalkFromState)
b.add_setup(SUTType.Mealy, FALearner(MealyEncoder()), MealyRWalkFromState)
b.add_setup(SUTType.RA, RALearner(RAEncoder()), RARWalkFromState)
b.add_setup(SUTType.IORA, RALearner(IORAEncoder()), IORARWalkFromState)
# no longer used, built function which returns tuple
#b.add_setup(SUTType.DFA, FALearner(DFAEncoder()), DFARWalkFromState)
#b.add_setup(SUTType.Mealy, FALearner(MealyEncoder()), MealyRWalkFromState)
#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.DFA)
#b.add_sut(LoginClass(), SUTType.DFA)
b.add_sut(FIFOSetClass(), SUTType.Mealy)
# create a test description
t_desc = TestDesc(max_tests=10000, prop_reset=0.2, rand_length=5)
t_desc = TestDesc(max_tests=10000, prop_reset=0.1, rand_length=5)
# give an smt timeout value (in ms)
timeout = 1000
timeout = 100000
# run the benchmark and collect results
results = b.run_benchmarks(t_desc, timeout)
......
......@@ -92,7 +92,6 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
return (None, statistics)
else:
definition = None
print("next test, ", next_test.trace())
learner.add(next_test.trace())
statistics.add_learner_test(next_test)
done = False
......@@ -109,11 +108,9 @@ 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)
# for learner_test in learner_tests:
# if learner_test.check(model) is not None:
# raise Exception("Learner test doesn't pass "+str(learner_test.trace()))
end_time = int(time.time() * 1000)
statistics.add_learning_time(end_time - start_time)
done = True
......@@ -121,6 +118,7 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
for next_test in generated_tests:
ce = next_test.check(model)
if ce is not None:
print("CE: ", ce)
learner.add(ce)
learner_tests.append(next_test)
done = False
......@@ -132,6 +130,7 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
for i in range(0, max_tests):
next_test = test_generator.gen_test(model)
if next_test is None:
raise Exception("Should never be none")
break
generated_tests.append(next_test)
ce = next_test.check(model)
......
......@@ -31,6 +31,7 @@ class FALearner(Learner):
print("initial def ", min_states)
(succ, fa, m) = self._learn_model(min_states=min_states,
max_states=max_states)
self.solver.reset()
if succ:
return fa.export(m), fa
else:
......@@ -46,6 +47,7 @@ class FALearner(Learner):
for num_states in range(min_states, max_states + 1):
print("Learning with ", num_states, " states")
fa, constraints = self.encoder.build(num_states)
self.solver.reset()
self.solver.add(constraints)
if self.timeout is not None:
self.solver.set("timeout", self.timeout)
......@@ -56,11 +58,8 @@ 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:
self.solver.reset()
# timeout
if result == z3.unknown:
return (False, True, None)
......
......@@ -37,7 +37,7 @@ class MealyFIFOSet():
self.stored -= 1
return SUT.OK
def put(self, val):
def put(self):
if self.stored == self.size:
return SUT.NOK
else:
......@@ -46,7 +46,7 @@ class MealyFIFOSet():
class FIFOSetClass(ScalableSUTClass):
def __init__(self):
super({
super().__init__({
SUTType.IORA: FIFOSet,
SUTType.RA: FIFOSet,
SUTType.Mealy: MealyFIFOSet,
......
......@@ -50,7 +50,7 @@ class RWalkFromState(TestGenerator, metaclass=ABCMeta):
r_trans = transitions[rand.randint(0, len(transitions)-1)]
crt_state = r_trans.end_state
trans_path.append(r_trans)
if rand.random()> self.prob_reset:
if rand.random()< self.prob_reset:
break
# instantiate the access and random sequences by extracting the sequence of inputs to be executed on the sut
......
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