Commit 34d793d9 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Tests are functioning

parent 79faa7ed
......@@ -2,7 +2,7 @@ from setuptools import setup, find_packages
setup(
name='z3gi',
version='0.1.1',
version='0.2.1',
description='Grammatical inference using the Z3 SMT solver',
long_description=open('README.md').read(),
url='https://gitlab.science.ru.nl/rick/z3gi/lata',
......
import collections
from z3gi.model.ra import Action
"""Test scenarios contain a list of traces together with the number of locations and registers of the SUT generating
these traces.
......
......@@ -30,7 +30,7 @@ sut_m1 = RaTestScenario("Accept everything", [
[(act(0, 'in'), act(100, 'OK'))],
[(act(0, 'in'), act(101, 'OK')), (act(0, 'in'), act(102, 'OK'))]
],
2, 1
3, 1
)
sut_m2 = RaTestScenario("OK first then always NOK", [
......@@ -45,7 +45,7 @@ sut_m2 = RaTestScenario("OK first then always NOK", [
[io(0, 'in', 100, 'OK'), io(1, 'in', 101, 'NOK'), io(1, 'in', 102, 'NOK')],
[io(0, 'in', 100, 'OK'), io(1, 'in', 101, 'NOK'), io(2, 'in', 102, 'NOK')],
],
4, 1)
5, 1)
sut_m3 = RaTestScenario("Alternating OK/NOK", [
[io(0, 'in', 100, 'OK')],
......@@ -59,7 +59,7 @@ sut_m3 = RaTestScenario("Alternating OK/NOK", [
[io(0, 'in', 100, 'OK'), io(1, 'in', 101, 'NOK'), io(1, 'in', 102, 'OK')],
[io(0, 'in', 100, 'OK'), io(1, 'in', 101, 'NOK'), io(2, 'in', 102, 'OK')],
],
4, 1)
5, 1)
# IO
sut_m4 = RaTestScenario( "Store value and produce OK output if you get that same value", [
......@@ -69,7 +69,7 @@ sut_m4 = RaTestScenario( "Store value and produce OK output if you get that same
[(act(0, 'in'), act(100, 'OK')), (act(1, 'in'), act(101, 'NOK')), (act(0, 'in'), act(102, 'OK')), (act(0, 'in'), act(103, 'OK'))],
# [(act(1, 'in'), act(100, 'NOK')), (act(0, 'in'), act(101, 'OK')), (act(0, 'in'), act(102, 'OK')), (act(0, 'in'), act(103, 'OK'))]],
],
6, 2)
5, 2)
# login model (incomplete traces)
sut_m5 = RaTestScenario("Login model", [
......
......@@ -38,7 +38,7 @@ class DFALearnerTest(unittest.TestCase):
"Register automaton output doesn't correspond to observation {0}".format(str(trace)))
def learn_model(self, test_scenario):
learner = FALearner(encoder=DFAEncoder(), verbose=True)
learner = FALearner(encoder=DFAEncoder(), verbose=False)
for trace in test_scenario.traces:
learner.add(trace)
......
......@@ -3,8 +3,6 @@ import unittest
from tests.iora_testscenario import *
from z3gi.learn.ra import RALearner
from encode.iora import IORAEncoder
from z3gi.define.ra import IORegisterAutomaton
import z3
class RaTest(unittest.TestCase):
......@@ -25,24 +23,18 @@ class RaTest(unittest.TestCase):
def check_scenario(self, test_scenario: RaTestScenario):
print("Scenario " + test_scenario.description)
(succ, iora, model) = self.learn_model(test_scenario)
print(iora)
print(model)
# self.assertTrue(succ, msg="Register Automaton could not be inferred")
# self.assertEqual(len(ra.locations), test_scenario.nr_locations,
# "Wrong number of locations.")
# self.assertEqual(len(ra.locations), test_scenario.nr_locations,
# "Wrong number of registers.")
result = self.learn_model(test_scenario)
self.assertTrue(result, msg="Register Automaton could not be inferred")
(iora, iora_def) = result
self.assertEqual(len(iora_def.locations), test_scenario.nr_locations, "Wrong number of locations.")
def learn_model(self, test_scenario: RaTestScenario):
for trace in test_scenario.traces:
self.ralearner.add(trace)
# ra_def = None
min_locations = 1
max_locations = test_scenario.nr_locations + 1
num_regs = 0
# (_, ra_def, _) = self.ralearner._learn_model(2, 2, 1)
result = self.ralearner._learn_model(min_locations, max_locations, num_regs) #
result = self.ralearner.model(min_locations, max_locations, num_regs) #
return result
......
......@@ -17,12 +17,12 @@ class MealyImporterTest(unittest.TestCase):
self.assertEqual(len(aut.transitions()), exp_num_trans, "Number of transitions not equal to expected")
def test_banking(self):
maestro_model_file = os.path.join("..","resources","models","MAESTRO.dot")
maestro_model_file = os.path.join("..","resources","models","bankcards","MAESTRO.dot")
mealy = build_automaton_from_dot("MealyMachine", maestro_model_file)
self.check_aut(mealy, exp_num_states=6)
sim = MealyMachineSimulation(mealy)
self.assertEqual(sim.run(["getValidData","selectApplication"]).trace(),
[('getValidData', '9000'), ('selectApplication', '9000')])
[('getValidData', '6A88'), ('selectApplication', '9000')])
......@@ -39,12 +39,7 @@ class MealyLearnerTest(unittest.TestCase):
.format(test.trace()))
def learn_model(self, test_scenario):
# inputs = set()
# outputs = set()
# for trace in test_scenario.traces:
# inputs.update([i for (i, _) in trace])
# outputs.update([o for (_, o) in trace])
learner = FALearner(encoder=MealyEncoder(), verbose=True)
learner = FALearner(encoder=MealyEncoder(), verbose=False)
for trace in test_scenario.traces:
learner.add(trace)
......
import unittest
from encode.ra import RAEncoder
from tests.ra_testscenario import *
from z3gi.learn.ra import RALearner
from z3gi.define.ra import RegisterAutomaton
......@@ -57,7 +58,7 @@ class RaLearnerTest(unittest.TestCase):
def learn_model(self, test_scenario : RaTestScenario) -> \
(bool, RegisterAutomaton, z3.ModelRef):
ralearner = RALearner(labels, verbose=True)
ralearner = RALearner(RAEncoder())
for trace in test_scenario.traces:
ralearner.add(trace)
......@@ -65,153 +66,4 @@ class RaLearnerTest(unittest.TestCase):
max_locations = test_scenario.nr_locations + 1
result = ralearner._learn_model(min_locations, max_locations, test_scenario.nr_registers + 1) #
return result
#
# """
# Visitor class for implementing procedures on inferred RAs.
# """
# class RaVisitor:
# def __init__(self):
# super().__init__()
# """
# Visits every location and transition in the register automaton.
# """
# def process(self, model, ra, labels, regs, locations):
# to_visit = [ra.start]
# visited = []
# while (len(to_visit) > 0):
# loc = to_visit.pop(0)
# acc = model.eval(ra.output(loc))
# self._visit_location(loc, acc)
# visited.append(loc)
# next_trans = []
# for l in labels:
# for r in regs:
# guard_enabled = model.eval(ra.guard(loc, l, r))
# if guard_enabled:
# next_loc = model.eval(ra.transition(loc, l, r))
# next_asg = model.eval(ra.update(loc, l))
# next_trans.append((loc, l, r, next_asg, next_loc))
#
# for (start_loc, label, guard, asg, end_loc) in next_trans:
# self._visit_transition(start_loc, label, guard, asg, end_loc)
# if end_loc not in visited and end_loc not in to_visit:
# to_visit.append(end_loc)
# # we sort according to the location strings so we get them in order
# to_visit.sort(key=lambda loc: str(loc))
# """
# Visits locations in the RA in lexographical order starting from the initial location.
# """
# def _visit_location(self, loc, acc):
# raise NotImplementedError()
# """
# Visits transitions in the RA.
# """
# def _visit_transition(self, start_loc, label, guard, asg, end_loc):
# raise NotImplementedError()
# class RaPrinter(RaVisitor):
# def __init__(self):
# super().__init__()
# """
# Prints location.
# """
# def _visit_location(self, loc, acc):
# print("{0}({1})".format(str(loc), "+" if acc == True else "-") )
# """
# Prints transition.
# """
# def _visit_transition(self, start_loc, label, guard, asg, end_loc):
# print("\t{0} -> {1}({2}) {3} {4}".format(str(start_loc), str(label), str(guard), str(asg), str(end_loc)))
# # TODO it should probably store locations/regs as strings
# class SimpleRa():
# def __init__(self, locations, loc_to_acc, loc_to_trans, registers):
# super().__init__()
# self.locations = locations
# self.loc_to_acc = loc_to_acc
# self.loc_to_trans = loc_to_trans
# self.register = registers
# def get_start_loc(self):
# return self.locations[0]
# def get_locations(self):
# return list(self.locations)
# def get_transitions(self, loc, label=None):
# if label is None:
# return list(self.loc_to_trans[loc])
# else:
# return list([trans for trans in self.loc_to_trans[loc] if trans[1] == label])
# def get_registers(self):
# return list(self.registers)
# def get_acc(self, loc):
# return self.loc_to_acc[loc]
# class NoTransitionTriggeredException(Exception):
# pass
# class SimpleRaSimulator():
# def __init__(self, sra):
# super().__init__()
# self.ra = sra
# """
# Runs the given sequence of values on the RA.
# """
# def accepts(self, trace):
# init = -1
# reg_val = dict()
# for reg in self.ra.get_registers():
# reg_val[reg] = init
# loc = self.ra.get_start_loc()
# for act in trace:
# next_transitions = self.ra.get_transitions(loc, act.label)
# # to define a fresh guard we need to know which register guards are present
# active_regs = [trans[2] for trans in next_transitions]
# n_loc = None
# for (_, _, guard, asg, next_loc) in next_transitions:
# if (self._is_satisfied(act, guard, active_regs, reg_val)):
# if not is_fresh(asg):
# reg_val[asg] = act.value
# n_loc = next_loc
# break
# if n_loc is None:
# print("In location {0} with trans. {1}, \n reg vals {2} and crt val {3}".format(
# str(loc), str(next_transitions), str(reg_val), str(act.value)
# ))
# raise NoTransitionTriggeredException()
# else:
# loc = n_loc
# return self.ra.get_acc(loc)
# def _is_satisfied(self, act, guard, active_regs, reg_val):
# if is_fresh(guard):
# reg_vals = list([reg_val[reg] for reg in active_regs])
# return act.value not in reg_vals
# else:
# return act.value is reg_val[guard]
# """
# Builds a SRA from the inferred uninterpreted functions for the RA.
# """
# class SimpleRaBuilder(RaVisitor):
# def __init__(self):
# super().__init__()
# self.locations = []
# self.loc_to_acc = dict()
# self.loc_to_trans = dict()
# self.registers = []
# def _visit_location(self, loc, acc):
# self.locations.append(loc)
# self.loc_to_acc[loc] = acc
# if loc not in self.loc_to_trans:
# self.loc_to_trans[loc] = []
# def _visit_transition(self, start_loc, label, guard, asg, end_loc):
# self.loc_to_trans[start_loc].append((start_loc, label, guard, asg, end_loc))
# if not is_fresh(guard) and guard not in self.registers:
# self.registers.append(guard)
# if not is_fresh(asg) and asg not in self.registers:
# self.registers.append(asg)
# """
# Builds a SRA from the RA generated functions. It uses as locations and registers the actual Z3 constants.
# """
# def build_ra(self):
# return SimpleRa(self.locations, self.loc_to_acc, self.loc_to_trans, self.registers.sort(key=lambda reg: str(reg)))
#
#
# def is_fresh(reg):
# return str(reg) == str("fresh")
\ No newline at end of file
return result
\ No newline at end of file
......@@ -7,7 +7,7 @@ from learn.fa import FALearner
from model import Automaton
from model.ra import RegisterMachine
from parse.importer import build_automaton_from_dot
from sut import SUTType, get_simulation, MealyObservation, StatsSUT, StatsTracker
from sut import get_simulation, MealyObservation, StatsSUT
from learn.algorithm import learn_mbt, Statistics
from statistics import stdev, median
import os.path
......
"""A standalone for using the z3gi package from the command line."""
"""A standalone module for using the z3gi package from the command line."""
import argparse
import learn.algorithm as alg
......@@ -9,7 +9,7 @@ import model.gen as gen
from encode.fa import MealyEncoder, DFAEncoder
from encode.iora import IORAEncoder
from encode.ra import RAQREncoder
from encode.ra import RAEncoder
from learn.fa import FALearner
from learn.ra import RALearner
from test import AcceptorTest, IORATest, MealyTest
......@@ -21,7 +21,7 @@ from test.rwalk import DFARWalkFromState
"""some configuration mappings"""
aut2learner={
model.ra.RegisterAutomaton:RALearner(RAQREncoder()),
model.ra.RegisterAutomaton:RALearner(RAEncoder()),
model.ra.IORegisterAutomaton:RALearner(IORAEncoder()),
model.fa.MealyMachine:FALearner(MealyEncoder()),
model.fa.DFA:FALearner(DFAEncoder())
......
......@@ -27,7 +27,6 @@ class RegisterAutomaton(RegisterMachine):
self.update = z3.Function('update', self.Location, self.Label, self.Register)
def export(self, model : z3.ModelRef) -> RegisterAutomaton:
print(model)
builder = RegisterAutomatonBuilder(self)
ra = builder.build_ra(model)
return ra
......
......@@ -386,6 +386,8 @@ class IORAEncoder(Encoder):
return constraints
"""A quantifier free version of the encoder. It is not functioning properly, so stay away from it"""
class IORAQREncoder(Encoder):
def __init__(self):
......
......@@ -194,7 +194,10 @@ class RAEncoder(Encoder):
constraints.append(z3.Distinct(list(values)))
return constraints
"""A quantifier-reduced version of the encoder """
"""A quantifier-reduced version of the encoder. There are some bugs in it (doesn't pass all RAtests), watch out! """
class RAQREncoder(Encoder):
def __init__(self):
self.tree = Tree(itertools.count(0))
......@@ -266,18 +269,6 @@ class RAQREncoder(Encoder):
z3.And([ra.used(ra.start, r) == False for r in ra.registers]),
]
# axioms.extend(
# [
# z3.Distinct(ra.registers),
# z3.Distinct(ra.labels.values()),
# z3.Distinct(ra.locations),
# z3.And([z3.Or([ra.transition(l, r) == lt for lt in ra.locations for r in ra.registers])
# for l in ra.locations]),
# z3.And([z3.Or([ra.update(l) == r for r in ra.registers]) for l in ra.locations]),
# z3.And([z3.Or([mapper.map(mapper.element(n.id)) == l for n in self.cache]) for l in ra.locations])
# ]
# )
return axioms
def node_constraints(self, ra, mapper):
......
......@@ -31,12 +31,8 @@ class FALearner(Learner):
return None
else:
return None
# to = fa
# return (None, to)
# to = fa
# return (None, to)
def _learn_model(self, min_states, max_states, ensure_min):
def _learn_model(self, min_states, max_states, ensure_min=True):
"""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):
......
......@@ -13,11 +13,6 @@ class RALearner(Learner):
raise Exception("RAEncoder has to be supplied")
if not solver:
solver = z3.Solver()
#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
......@@ -44,10 +39,8 @@ class RALearner(Learner):
return ra_def.export(m), ra_def
else:
return None
#to = ra_def
#return (None, to)
def _learn_model(self, min_locations, max_locations, min_registers, max_registers, ensure_min):
def _learn_model(self, min_locations, max_locations, min_registers, max_registers=3, ensure_min=True):
"""generates the definition and model for an ra whose traces include the traces added so far"""
for num_locations in range(min_locations, max_locations + 1):
# TODO: calculate max registers based on repeating values
......@@ -57,8 +50,7 @@ class RALearner(Learner):
self.solver.add(constraints)
if self.timeout is not None:
self.solver.set("timeout", self.timeout)
self.solver.set(":smt.random_seed", 0)
self.solver.set("random_seed", 0)
self.solver.set(":smt.random_seed", 0) # this is a futile attempt of making Z3 deterministic
result = self.solver.check()
if self.verbose:
print("Learning with {0} locations and {1} registers. Result: {2}"
......
from encode.iora import IORAEncoder
from learn.algorithm import learn
from learn.ra import RALearner
from test import IORATest
from test.exhaustive import ExhaustiveRAGenerator
import functools
from abc import ABCMeta
from typing import Tuple, List, Dict
from typing import Tuple, List
import collections
from encode.fa import MealyEncoder
from learn import Learner
from learn.fa import FALearner
from model import Automaton
from model.ra import RegisterMachine
from sut import SUTType
from sut import get_no_rst_simulation
from sut.scalable import ScalableSUTClass
from sut.fifoset import FIFOSetClass
from sut.stack import StackClass
from learn.algorithm import Statistics
from statistics import stdev, median
import learn.algorithm as alg
......
......@@ -4,8 +4,8 @@ from typing import Tuple, List, Dict
import collections
from encode.fa import DFAEncoder, MealyEncoder
from encode.iora import IORAEncoder, IORAQREncoder
from encode.ra import RAEncoder, RAQREncoder
from encode.iora import IORAEncoder
from encode.ra import RAEncoder
from learn import Learner
from learn.fa import FALearner
from learn.ra import RALearner
......@@ -43,7 +43,7 @@ def get_learner_setup(sut, sut_type:SUTType, size, test_desc:TestDesc):
elif sut_type is SUTType.Mealy:
return (FALearner(MealyEncoder()), MealyRWalkFromState(*args))
elif sut_type is SUTType.RA:
ra_learner = RALearner(RAQREncoder())
ra_learner = RALearner(RAEncoder())
ra_learner.set_num_reg(size)
return (ra_learner, RARWalkFromState(*args))
elif sut_type is SUTType.IORA:
......
......@@ -90,10 +90,6 @@ class AcceptorCache(Cache):
next_seqs.append(seq + [inp])
else:
obs = self.from_cache(seq)
#if obs is None:
# print(seq)
# print(self._tree)
# exit(0)
yield obs
class CacheSUT(SUT):
......@@ -115,14 +111,4 @@ class CacheSUT(SUT):
return obs
def input_interface(self):
return self._sut.input_interface()
#c = IOCache(MealyObservation)
#c.update_cache(MealyObservation([("a","oa"), ("a","ob")]))
#print(c._tree)
#c.update_cache(MealyObservation([("a","oa"), ("b","ob")]))
#print(c._tree)
#c.update_cache(MealyObservation([("b","ob"), ("b","ob")]))
#print(c._tree)
#
#print(c.from_cache(["b", "b"]))
\ No newline at end of file
return self._sut.input_interface()
\ No newline at end of file
......@@ -3,10 +3,10 @@ from typing import Set
from model import Automaton, Transition
from sut.sut_cache import Cache
from test import TestGenerator
"""Explores all transitions in a model that have not been explored (or colored) during test execution. """
class ColoringTestGenerator(TestGenerator):
class ColoringTestGenerator(TestGenerator):
def __init__(self, sut, cache:Cache):
self._sut = sut
self._cache = cache
......@@ -34,9 +34,7 @@ class ColoringTestGenerator(TestGenerator):
def _colored_transitions(self, model: Automaton) -> Set[Transition]:
trans = set()
for obs in self._cache.obs_iterator():
#print(obs)
colored_trans = model.inputs_to_trans(obs.inputs())
#print(" ".join(map(str, model.inputs_to_trans(obs.inputs()))))
trans = trans.union(set(colored_trans))
return trans
......
Markdown is supported
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