Skip to content
GitLab
Commit fcbf13f8 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Fix most of the bugs. Testing is an issue though due to the length of the tests.

parent 1dc65055
Hide whitespace changes
Inline Side-by-side
z3gi/define/ra.py
View file @ fcbf13f8
......@@ -103,6 +103,7 @@ class RegisterAutomatonBuilder(object):
for z3label in self.ra.labels.values():
self._add_transitions(model, translator, mut_ra, z3state, z3label)
mut_ra.generate_acc_seq()
mut_ra.set_act_arities(self.ra.param_size)
return mut_ra.to_immutable()
def _add_state(self, model, translator, mut_ra, z3state):
......@@ -178,6 +179,7 @@ class IORegisterAutomatonBuilder(object):
for z3label in z3input_labels:
self._add_transitions(model, translator, mut_ra, z3state, z3label, z3output_labels)
mut_ra.generate_acc_seq()
mut_ra.set_act_arities(self.ra.param_size)
return mut_ra.to_immutable()
def _add_state(self, translator, mut_ra, z3state):
......@@ -217,7 +219,6 @@ class IORegisterAutomatonBuilder(object):
enabled_z3guards = [guard for guard in self.ra.registers if
translator.z3_to_bool(model.eval(self.ra.used(z3out_state, guard))) or
guard is self.ra.fresh]
#print("From ", z3out_state, " enabled ", enabled_z3guards, " labels ", output_labels)
active_z3action = [(output_label, guard) for output_label in output_labels for guard in enabled_z3guards
if translator.z3_to_bool(model.eval(self.ra.transition(z3out_state, output_label, guard)
......
z3gi/model/__init__.py
View file @ fcbf13f8
import pprint
from abc import ABCMeta, abstractmethod
from typing import List
......@@ -36,11 +37,11 @@ class MultipleTransitionsFired(Exception):
class Automaton(metaclass=ABCMeta):
def __init__(self, states, state_to_trans, acc_seq={}):
def __init__(self, states, state_to_trans, acc_trans_seq={}):
super().__init__()
self._states = states
self._state_to_trans = state_to_trans
self._acc_seq = acc_seq
self._acc_trans_seq = acc_trans_seq
def start_state(self):
return self._states[0]
......@@ -48,18 +49,18 @@ class Automaton(metaclass=ABCMeta):
def acc_trans_seq(self, state=None) -> List[Transition]:
"""returns the access sequence to a state in the form of transitions"""
if state is not None:
return list(self._acc_seq[state])
return list(self._acc_trans_seq[state])
else:
return dict(self._acc_seq)
return dict(self._acc_trans_seq)
def acc_seq(self, state=None):
"""returns the access sequence to a state in the form of sequences of inputs"""
if state is not None:
if len(self._acc_seq) == 0:
if len(self._acc_trans_seq) == 0:
raise Exception("Access sequences haven't been defined for this machine")
return self._seq(self._acc_seq[state])
return self._seq(self._acc_trans_seq[state])
else:
return {state:self._seq(self._acc_seq[state]) for state in self.states()}
return {state:self._seq(self._acc_trans_seq[state]) for state in self.states()}
def states(self):
return list(self._states)
......@@ -104,7 +105,7 @@ class Automaton(metaclass=ABCMeta):
# Basic __str__ function which works for most FSMs.
def __str__(self):
str_rep = ""
str_rep += str(self._acc_seq) + "\n"
str_rep += str(self._acc_trans_seq) + "\n"
for state in self.states():
str_rep += str(state) + "\n"
for tran in self.transitions(state):
......@@ -133,7 +134,8 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
raise Exception("Could not find state {0} in tree {1}".format(state, ptree))
new_acc_seq[state] = node.path()
assert(len(new_acc_seq) == len(self.states()))
self._acc_seq = new_acc_seq
pprint.pprint(new_acc_seq)
self._acc_trans_seq = new_acc_seq
@abstractmethod
def to_immutable(self) -> Automaton:
......@@ -144,8 +146,8 @@ class MutableAutomatonMixin(metaclass=ABCMeta):
class Transducer(Automaton, metaclass=ABCMeta):
def __init__(self, states, state_to_trans, acc_seq={}):
super().__init__(states, state_to_trans, acc_seq)
def __init__(self, states, state_to_trans, acc_trans_seq={}):
super().__init__(states, state_to_trans, acc_trans_seq)
@abstractmethod
def output(self, trace):
......@@ -157,8 +159,8 @@ class Transducer(Automaton, metaclass=ABCMeta):
class Acceptor(Automaton, metaclass=ABCMeta):
def __init__(self, states, state_to_trans, state_to_acc, acc_seq={}):
super().__init__(states, state_to_trans, acc_seq)
def __init__(self, states, state_to_trans, state_to_acc, acc_trans_seq={}):
super().__init__(states, state_to_trans, acc_trans_seq)
self._state_to_acc = state_to_acc
def is_accepting(self, state):
......
z3gi/model/fa.py
View file @ fcbf13f8
......@@ -66,8 +66,8 @@ class MooreMachine(Transducer):
return [trans.start_label for trans in transitions]#trace
class MealyMachine(Transducer):
def __init__(self, states, state_to_trans, acc_seq={}):
super().__init__(states, state_to_trans, acc_seq)
def __init__(self, states, state_to_trans, acc_trans_seq={}):
super().__init__(states, state_to_trans, acc_trans_seq)
def transitions(self, state: State, label: Label = None) -> List[IOTransition]:
return super().transitions(state, label)
......
z3gi/model/ra.py
View file @ fcbf13f8
......@@ -109,12 +109,21 @@ class RegisterMachine(Automaton):
@abstractmethod
def registers(self) -> List[Register]:
"""Retrieves the registers in the automaton"""
pass
def act_arity(self, label=None):
"""Retrieves the arity of the action associated with the label, or the arity of all labels"""
if label is None:
return dict(self._act_arity)
else:
return self._act_arirty[label]
class RegisterAutomaton(Acceptor, RegisterMachine):
def __init__(self, locations, loc_to_acc, loc_to_trans, registers, acc_seq={}):
super().__init__(locations, loc_to_trans, loc_to_acc, acc_seq)
self._registers = registers
def __init__(self, locations, loc_to_acc, loc_to_trans, registers, act_arity:dict, acc_trans_seq={}):
super().__init__(locations, loc_to_trans, loc_to_acc, acc_trans_seq)
self._registers = registers
self._act_arity = act_arity
def registers(self) -> List[Register]:
return self._registers
......@@ -153,9 +162,10 @@ class RegisterAutomaton(Acceptor, RegisterMachine):
class IORegisterAutomaton(Transducer, RegisterMachine):
def __init__(self, locations, loc_to_trans, registers, acc_seq={}):
super().__init__(locations, loc_to_trans, acc_seq)
def __init__(self, locations, loc_to_trans, registers, act_arity, acc_trans_seq={}):
super().__init__(locations, loc_to_trans, acc_trans_seq)
self._registers = registers
self._act_arity = act_arity
def registers(self) -> List[Register]:
......@@ -232,7 +242,7 @@ class IORegisterAutomaton(Transducer, RegisterMachine):
class MutableRegisterAutomaton(RegisterAutomaton, MutableAcceptorMixin):
def __init__(self):
super().__init__([], dict(), dict(), [])
super().__init__([], dict(), [], [])
def add_transition(self, state:str, transition:RATransition):
super().add_transition(state, transition)
......@@ -242,11 +252,14 @@ class MutableRegisterAutomaton(RegisterAutomaton, MutableAcceptorMixin):
def to_immutable(self) -> RegisterAutomaton:
return RegisterAutomaton(self._states, self._state_to_acc,
self._state_to_trans, self._registers, self.acc_seq())
self._state_to_trans, self._registers, self._act_arity, self.acc_trans_seq())
def set_act_arities(self, act_arity:dict):
self._act_arity = act_arity
class MutableIORegisterAutomaton(IORegisterAutomaton, MutableAutomatonMixin):
def __init__(self):
super().__init__([], dict(), [])
super().__init__([], dict(), [], [])
def add_transition(self, state:str, transition:IORATransition):
super().add_transition(state, transition)
......@@ -255,8 +268,11 @@ class MutableIORegisterAutomaton(IORegisterAutomaton, MutableAutomatonMixin):
self._registers.append(reg)
def to_immutable(self) -> IORegisterAutomaton:
return IORegisterAutomaton(self._states, self._state_to_trans, self._registers,
self.acc_seq() )
return IORegisterAutomaton(self._states, self._state_to_trans, self._registers, self._act_arity,
self.acc_trans_seq())
def set_act_arities(self, act_arity:dict):
self._act_arity = act_arity
class Guard(metaclass=ABCMeta):
"""A guard with is_satisfied implements a predicate over the current register valuation and the parameter value. """
......
z3gi/sut/__init__.py
View file @ fcbf13f8
......@@ -130,10 +130,10 @@ class IORAObservation(RegisterMachineObservation):
return "Obs: " + str(self.tr)
class ObjectSUT(RASUT):
"""Wraps around an object and calls methods on it corresponding to the Actions"""
"""Wraps around an object and calls methods on it corresponding to the Actions.
IORA is the natural formalism for describing practical SUTs. Depending on the SUT characteristics,
we can describe them using less expressing formalisms."""
def __init__(self, act_sigs, obj_gen):
self.obj_gen = obj_gen
self.acts = {act_sig.label:act_sig for act_sig in act_sigs}
......@@ -188,4 +188,5 @@ class ObjectSUT(RASUT):
raise Exception("Cannot process output")
def input_interface(self) -> List[ActionSignature]:
return list(self.acts.values())
\ No newline at end of file
return list(self.acts.values())
z3gi/test/rwalk.py
View file @ fcbf13f8
......@@ -6,10 +6,11 @@ import collections
import itertools
from model import Automaton, Transition
from model.ra import IORATransition, IORegisterAutomaton, EqualityGuard, OrGuard, Action, Register
from sut import SUT, ActionSignature
from model.ra import IORATransition, IORegisterAutomaton, EqualityGuard, OrGuard, Action, Register, FreshGuard, Fresh
from sut import SUT, ActionSignature, RASUT
from test import TestGenerator, Test, AcceptorTest, MealyTest, IORATest
import random
import pprint
rand = random.Random(0)
......@@ -17,7 +18,10 @@ def rand_sel(l:List):
return l[rand.randint(0, len(l)-1)]
class RWalkFromState(TestGenerator, metaclass=ABCMeta):
def __init__(self, sut:SUT, test_gen, rand_length, rand_start_state=True):
def __init__(self, sut:SUT, test_gen, rand_length, prob_reset=0.2, rand_start_state=True):
# the probability after each input added, that we stop adding further inputs to the random sequence
# hence the rand_length is only the maximum length of the random sequence
self.prob_reset = prob_reset
self.rand_length = rand_length
self.rand_start_state = rand_start_state
self.sut = sut
......@@ -26,20 +30,32 @@ class RWalkFromState(TestGenerator, metaclass=ABCMeta):
def gen_test(self, model: Automaton) -> Test:
"""generates a test comprising an access sequence and a random sequence"""
if model is None:
# if the model is None, generate a test which includes all inputs (so at least we know the next generated
# model will be input enabled)
seq = self._generate_init()
else:
# select a random state
if self.rand_start_state:
crt_state = model.states()[rand.randint(0, len(model.states()) - 1)]
else:
crt_state = model.start_state()
# get its access sequence (in the form of a sequence of transitions)
trans_path = list(model.acc_trans_seq(crt_state))
# from this state, do a random walk and generate a random sequence of transitions
for _ in range(0, self.rand_length):
transitions = model.transitions(crt_state)
r_trans = transitions[rand.randint(0, len(transitions)-1)]
crt_state = r_trans.end_state
trans_path.append(r_trans)
# instantiate the access and random sequences by extracting the sequence of inputs to be executed on the sut
# for FSMs every sequence has a unique instantiation
# for RAs, sequences may have different instantiations depending on the values chosen
seq = self._generate_seq(model, trans_path)
# run the sequence on inputs, which results on an observation and generate a corresponding test
obs = self.sut.run(seq)
test = self.test_gen(obs.trace())
return test
......@@ -97,43 +113,52 @@ class ValueProb(collections.namedtuple("ValueProb", ("history", "register", "fre
class IORARWalkFromState(RWalkFromState):
def __init__(self, sut: SUT, rand_length, prob = ValueProb(0.4, 0.4, 0.2), rand_start_state=True):
def __init__(self, sut: RASUT, rand_length, prob = ValueProb(0.4, 0.4, 0.2), rand_start_state=True):
super().__init__(sut, IORATest, rand_length, rand_start_state)
self.prob = prob
def _generate_seq(self, model: IORegisterAutomaton, transitions:List[IORATransition]):
def _generate_seq(self, model: IORegisterAutomaton, transitions:List[IORATransition]) -> List[Action]:
"""generates a sequence of inputs for the randomly chosen transition path"""
act_arity = model.act_arity()
seq = []
values = set() # we may consider using lists to preserve order (sets cause randomness)
values = list() # we use a list to preserve order/eliminate potential non-det
reg_val = dict()
for trans in transitions:
if isinstance(trans.guard, EqualityGuard) or isinstance(trans.guard, OrGuard):
inp_val = reg_val[trans.guard.registers()[0]]
if act_arity[trans.start_label] == 1:
if isinstance(trans.guard, EqualityGuard) or isinstance(trans.guard, OrGuard):
inp_val = reg_val[trans.guard.registers()[0]]
elif isinstance(trans.guard, FreshGuard):
# we have a fresh transition, which means we can either pick a fresh value or any past value
# as long as it is not stored in one of the guarded registers in this location
fresh_val = 0 if len(values) == 0 else max(values) + 1
active_regs = list() if len(model.registers()) == 0 or len(trans.guard.registers()) == 0 else \
list(itertools.chain.from_iterable(
[tr.guard.registers() for tr in model.transitions(trans.start_state, trans.start_label)
if tr is not trans]))
active_reg_vals = [reg_val[reg] for reg in active_regs]
selectable_reg_vals = [val for val in reg_val.values() if val not in active_reg_vals]
selectable_his_vals = [val for val in values if val not in active_reg_vals
and val not in selectable_reg_vals]
inp_val = self.prob.select(selectable_reg_vals, selectable_his_vals, fresh_val)
if inp_val not in values:
values.append(inp_val)
inp = Action(trans.start_label, inp_val)
reg_val = trans.update(reg_val, inp)
else:
raise Exception("Unkown guard")
else:
# we have a fresh transition, which means we can either pick a fresh value or any past value
# as long as it is not stored in one of the guarded registers in this location
fresh_val = 0 if len(values) == 0 else max(values) + 1
r_list = list(itertools.chain((tr.guard.registers() for tr in
model.transitions(trans.start_state))))
print(r_list)
active_regs = set() if len(model.registers()) == 0 else \
set(itertools.chain([tr.guard.registers() for tr in model.transitions(trans.start_state)]))
active_reg_vals = [reg_val[reg] for reg in active_regs]
selectable_reg_vals = [val for val in reg_val.values() if val not in active_reg_vals]
selectable_his_vals = [val for val in values if val not in active_reg_vals
and val not in selectable_reg_vals]
inp_val = self.prob.select(selectable_reg_vals, selectable_his_vals, fresh_val)
values.add(inp_val)
inp_val = None
inp = Action(trans.start_label, inp_val)
reg_val = trans.update(reg_val, inp)
if isinstance(trans.output_mapping, Register):
out_val = reg_val[trans.output_mapping]
else:
out_val = 0 if len(values) == 0 else max(values) + 1
values.add(out_val)
out = Action(trans.output_label, out_val)
reg_val = trans.output_update(reg_val, out)
if act_arity[trans.output_label] == 1:
# we are only interested in the case where the output value is fresh (hence the mapping is fresh).
# In case of a "register" mapping, there can be no updates on registers (based on our encodings).
if isinstance(trans.output_mapping, Fresh):
out_val = 0 if len(values) == 0 else max(values) + 1
if out_val not in values:
values.append(out_val)
out = Action(trans.output_label, out_val)
reg_val = trans.output_update(reg_val, out)
seq.append(inp)
return seq
......@@ -141,6 +166,3 @@ class IORARWalkFromState(RWalkFromState):
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