Commit 4b2a6468 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Updates

parent bdac441f
......@@ -7,6 +7,7 @@ from learn.algorithm import learn_mbt
from learn.fa import FALearner
from learn.ra import RALearner
from sut import SUTType
from sut.fifoset import FIFOSetClass
from sut.login import new_login_sut, LoginClass
from test import IORATest, MealyTest
from test.rwalk import IORARWalkFromState, MealyRWalkFromState, DFARWalkFromState, RARWalkFromState
......@@ -23,10 +24,10 @@ def scrap_learn_iora():
def scrap_learn_mbt_iora():
learner = RALearner(IORAEncoder())
learner.set_timeout(10)
learner.set_timeout(10000)
sut = new_login_sut(1)
mbt = IORARWalkFromState(sut, 5, 0.2)
(model, statistics) = learn_mbt(learner, mbt, 1000)
(model, statistics) = learn_mbt(learner, mbt, 10000)
print(model)
print(statistics)
......@@ -52,8 +53,8 @@ def scrap_learn_mbt_mealy():
def scrap_learn_mbt_ra():
learner = RALearner(RAEncoder())
learner.set_timeout(100000)
login = LoginClass()
learner.set_timeout(600000)
login = FIFOSetClass()
sut = login.new_sut(SUTType.RA, 1)
mbt = RARWalkFromState(sut, 5, 0.2)
(model, statistics) = learn_mbt(learner, mbt, 10000)
......@@ -62,4 +63,4 @@ def scrap_learn_mbt_ra():
#scrap_learn_mbt_mealy()
#scrap_learn_mbt_mealy()
scrap_learn_mbt_ra()
scrap_learn_mbt_iora()
......@@ -33,7 +33,6 @@ sut_m1 = RaTestScenario("Accept everything", [
2, 1
)
sut_m2 = RaTestScenario("OK first then always NOK", [
[io(0, 'in', 100, 'OK')],
[io(0, 'in', 100, 'OK'), io(0, 'in', 101, 'NOK')],
......
......@@ -64,11 +64,13 @@ class Benchmark:
self.learn_setup[sut_type] = (sut_learner, sut_tester)
return self
def _run_benchmark(self, sut_class:ScalableSUTClass, sut_type:SUTType, test_desc:TestDesc, tout:int) \
def _run_benchmark(self, sut_class:ScalableSUTClass, sut_type:SUTType, test_desc:TestDesc, tout:int, max_size:int) \
-> List[Tuple[SutDesc, ExperimentStats]]:
results = []
size = 1
while True:
if max_size is not None and size > max_size:
break
sut = sut_class.new_sut(sut_type, size)
learner,test_gen = get_learner_setup(sut_type)
learner.set_timeout(tout)
......@@ -96,10 +98,10 @@ class Benchmark:
return ExperimentStats(states=states, registers=registers, learn_tests=learn_tests, learn_inputs=learn_inputs,
total_tests=total_tests, learn_time=learn_time)
def run_benchmarks(self, test_desc:TestDesc, timeout:int) -> List[Tuple[SutDesc, ExperimentStats]]:
def run_benchmarks(self, test_desc:TestDesc, timeout:int, max_size:int=None) -> List[Tuple[SutDesc, ExperimentStats]]:
results = []
for sut_class, sut_type in self.suts:
res = self._run_benchmark(sut_class, sut_type, test_desc, timeout)
res = self._run_benchmark(sut_class, sut_type, test_desc, timeout, max_size)
results.extend(res)
return results
......@@ -156,27 +158,47 @@ b = Benchmark()
#b.add_setup(SUTType.IORA, RALearner(IORAEncoder()), IORARWalkFromState)
# add the sut classes we want to benchmark
#b.add_sut(FIFOSetClass())
#b.add_sut(LoginClass())
b.add_sut(FIFOSetClass())
b.add_sut(LoginClass())
b.add_sut(StackClass())
#b.add_sut(StackClass())
b.add_sut(FIFOSetClass(), SUTType.Mealy)
#b.add_sut(FIFOSetClass(), SUTType.IORA)
#b.add_sut(LoginClass(), SUTType.IORA)
#b.add_sut(StackClass(), SUTType.IORA)
# create a test description
t_desc = TestDesc(max_tests=10000, prop_reset=0.2, rand_length=4)
t_desc = TestDesc(max_tests=100000, prop_reset=0.2, rand_length=3)
# give an smt timeout value (in ms)
timeout = 10000
timeout = 600
# how many times each experiment should be run
num_exp = 4
num_exp = 1
# up to what systems of what size do we want to run experiments (set to None if size is ignored as a stop condition)
max_size = 6
# run the benchmark and collect results
results = []
for i in range(0, num_exp):
results += b.run_benchmarks(t_desc, timeout)
results += b.run_benchmarks(t_desc, timeout, max_size)
print("============================")
print_results(results)
sut_dict = dict()
for sut_desc,exp in results:
if sut_desc not in sut_dict:
sut_dict[sut_desc] = list()
sut_dict[sut_desc].append(exp)
collated_stats = [(sut_desc, collate_stats(sut_desc, experiments)) for sut_desc, experiments in sut_dict.items()]
for (sut_desc, c_stat) in collated_stats:
print(sut_desc, " ", c_stat)
# sort according to the sut_desc (the first element)
results.sort()
#results.sort()
# print results
print_results(results)
......
......@@ -120,7 +120,6 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
if ce is not None:
print("CE: ", ce)
learner.add(ce)
learner_tests.append(next_test)
done = False
break
if not done:
......@@ -140,5 +139,7 @@ def learn_mbt(learner:Learner, test_generator:TestGenerator, max_tests:int) -> T
statistics.add_learner_test(next_test)
done = False
break
#print([str(test.trace() for test in learner_tests)])
statistics.set_suite_size(len(generated_tests))
return (model, statistics)
......@@ -51,7 +51,9 @@ class FALearner(Learner):
self.solver.add(constraints)
if self.timeout is not None:
self.solver.set("timeout", self.timeout)
print(self.solver.to_smt2())
result = self.solver.check()
print(self.solver.statistics())
if self.verbose:
print("Learning with {0} states. Result: {1}"
.format(num_states, result))
......
......@@ -13,6 +13,12 @@ class RALearner(Learner):
raise Exception("RAEncoder has to be supplied")
if not solver:
solver = z3.Solver()
print(z3.describe_tactics())
#solver = z3.Z3_mk_simple_solver("smt")
# example of tactics
#solver = z3.Then('simplify',
# 'solve-eqs',
# 'qfbv', 'sat').solver()
self.encoder = encoder
self.solver = solver
self.verbose = verbose
......@@ -58,6 +64,7 @@ class RALearner(Learner):
else:
self.solver.reset()
if result == z3.unknown:
print("Timeout at {0} locations and {1} registers".format(num_locations, num_registers))
return (False, True, None)
# TODO: process the unsat core?
......
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