Commit 1b365d1e authored by Michele Volpato's avatar Michele Volpato
Browse files

Merge branch 'development' into 'master'

Development

Keep master up to date

See merge request !1
parents be37e8f3 2c5ad38c
...@@ -3,8 +3,17 @@ All notable changes to this project will be documented in this file. ...@@ -3,8 +3,17 @@ All notable changes to this project will be documented in this file.
This project adheres to [Semantic Versioning](http://semver.org/). This project adheres to [Semantic Versioning](http://semver.org/).
## [Unreleased][unreleased] ## [Unreleased][unreleased]
## [v0.2.0] - 2015-10-27
### Added ### Added
- This CHANGELOG file. - This CHANGELOG file.
- Validity of suspension automata.
- Testing algorithms
- Counterexample handling
- Algorithms for double sets in the table
### Changed
- Moved old algorithm for learning to `oraclelearning` and `oracleobservationtable`
## [v0.1.0] - 2015-09-29 ## [v0.1.0] - 2015-09-29
### Added ### Added
...@@ -16,4 +25,4 @@ This project adheres to [Semantic Versioning](http://semver.org/). ...@@ -16,4 +25,4 @@ This project adheres to [Semantic Versioning](http://semver.org/).
- Simple Examples - Simple Examples
[unreleased]: https://gitlab.science.ru.nl/mvolpato/active-learning-nondeterministic-systems/compare/v0.1.0...HEAD [unreleased]: https://gitlab.science.ru.nl/mvolpato/active-learning-nondeterministic-systems/compare/v0.1.0...HEAD
[v0.1.0]: https://gitlab.science.ru.nl/mvolpato/active-learning-nondeterministic-systems/compare/f7f05033cf5e002a45a67632e60b311892ca0850...v0.1.0 [v0.1.0]: https://gitlab.science.ru.nl/mvolpato/active-learning-nondeterministic-systems/compare/f7f05033cf5e002a45a67632e60b311892ca0850...v0.1.0
\ No newline at end of file
...@@ -4,12 +4,17 @@ The active-learning-nondeterministic-systems is an implementation of an ...@@ -4,12 +4,17 @@ The active-learning-nondeterministic-systems is an implementation of an
adaptation of adaptation of
[L*](http://www.cs.berkeley.edu/~dawnsong/teaching/s10/papers/angluin87.pdf) to [L*](http://www.cs.berkeley.edu/~dawnsong/teaching/s10/papers/angluin87.pdf) to
nondeterministic systems. The code is based on these scientific papers: nondeterministic systems. The code is based on these scientific papers:
* [Active Learning of Nondeterminisitc Systems from an ioco Perspective](http://link.springer.com/chapter/10.1007%2F978-3-662-45234-9_16) * [`[1]` Active Learning of Nondeterminisitc Systems from an ioco Perspective](http://link.springer.com/chapter/10.1007%2F978-3-662-45234-9_16)
* [Approximate Active Learning of Nondeterministic Input Output Transition Systems](http://www.italia.cs.ru.nl/html/papers/VT15.pdf) * [`[2]` Approximate Active Learning of Nondeterministic Input Output Transition Systems](http://www.italia.cs.ru.nl/html/papers/VT15.pdf)
The goal is to constructing a model of a system for model-based testing, The goal is to construct a model of a system for model-based testing,
simulation, or model checking. simulation, or model checking.
### Python version
The project is coded in Python3 and tested using Python3.4.
## Included Libraries ## Included Libraries
[NumPy](https://github.com/numpy/numpy) [NumPy](https://github.com/numpy/numpy)
...@@ -43,14 +48,15 @@ teacher = YourOwnAdapterTeacher() ...@@ -43,14 +48,15 @@ teacher = YourOwnAdapterTeacher()
oracle = YourOwnAdapterOracle() oracle = YourOwnAdapterOracle()
underModel, overModel = LearningAlgorithm(teacher, oracle, maxLoops=10, underModel, overModel = LearningAlgorithm(teacher, oracle, maxLoops=10,
tablePreciseness = 10000, modelPreciseness = 0.1) tablePreciseness = 10000, modelPreciseness = 0.1,
tester=tester)
``` ```
where `underModel` and `overModel` are the under and over approximations where `underModel` and `overModel` are the under and over approximations
of your system, respectively, `maxLoops` is the limit of learning loops of your system, respectively, `maxLoops` is the limit of learning loops
when the learned models are not changing any more, `tablePreciseness` and when the learned models are not changing any more, `tablePreciseness` and
`modelPreciseness` are the levels of preciseness you would like to reach `modelPreciseness` are the levels of preciseness you would like to reach
before stopping. before stopping. Tester is a testing algorithm.
The learning process stops when either the learned model does not change for The learning process stops when either the learned model does not change for
`maxLoops` loops, or when both the preciseness levels are met. `maxLoops` loops, or when both the preciseness levels are met.
...@@ -62,4 +68,4 @@ checking [my contact details](https://gitlab.science.ru.nl/u/mvolpato). ...@@ -62,4 +68,4 @@ checking [my contact details](https://gitlab.science.ru.nl/u/mvolpato).
## License ## License
See [LICENSE](./LICENSE) See [LICENSE](./LICENSE)
\ No newline at end of file
...@@ -9,8 +9,9 @@ from systems.implementations import InputOutputLTS ...@@ -9,8 +9,9 @@ from systems.implementations import InputOutputLTS
from teachers.ltsoracles import InputOutputPowerOracle from teachers.ltsoracles import InputOutputPowerOracle
import logging import logging
import helpers.bisimulation as bi import helpers.bisimulation as bi
from testing.randomtesting import RandomTester
logging.basicConfig(level=logging.WARNING) logging.basicConfig(level=logging.INFO)
logger = logging.getLogger(__name__) logger = logging.getLogger(__name__)
inputs = set(['a','b']) inputs = set(['a','b'])
...@@ -33,20 +34,31 @@ I1.addTransition(4,'y',2) ...@@ -33,20 +34,31 @@ I1.addTransition(4,'y',2)
I1.addTransition(4,'b',4) I1.addTransition(4,'b',4)
I1.addTransition(4,'a',0) I1.addTransition(4,'a',0)
I1.addTransition(4,'x',0)
I1.addTransition(1,'a',0)
I1.addTransition(3,'b',1)
I1.addTransition(3,'a',0)
I1.addTransition(4,'b',2)
I1.addTransition(2,'a',3)
I1.addTransition(4,'y',0)
I1.makeInputEnabled() I1.makeInputEnabled()
T1 = InputOutputTeacher(I1) T1 = InputOutputTeacher(I1)
O1 = InputOutputPowerOracle(I1) O1 = InputOutputPowerOracle(I1)
tester = RandomTester(T1, 10000, 20)
currentdir = os.path.dirname(os.path.abspath( currentdir = os.path.dirname(os.path.abspath(
inspect.getfile(inspect.currentframe()))) inspect.getfile(inspect.currentframe())))
path = os.path.join(currentdir, "dotFiles") path = os.path.join(currentdir, "dotFiles")
print("Starting learning...") print("Starting learning...")
# change printPath=None to printPath=path for dot files # change printPath=None to printPath=path for dot files
L2 = LearningAlgorithm(T1, O1, printPath=None, maxLoops=2, logger=logger) L2 = LearningAlgorithm(T1, O1, printPath=None, maxLoops=4, tablePreciseness=10000, logger=logger, tester=tester)
minus, plus = L2.run() minus, plus = L2.run()
print("Models learned. Check language equivalence...") print("Models learned. Check language equivalence...")
......
def bisimilar(system1, system2): def bisimilar(system1, system2, startState1=0, startState2=0):
# starting from initial state # starting from given states
state1 = (0,) state1 = (startState1,)
state2 = (0,) state2 = (startState2,)
past = set() past = set()
wait = set() wait = set()
trace = () trace = ()
wait.add((state1, state2, trace)) wait.add((state1, state2, trace))
while wait: while wait:
current = wait.pop() current = wait.pop()
past.add((current[0],current[1])) past.add((current[0],current[1]))
system1Labels = system1.getInputs().union(system1.getOutputs())
system1Labels.add(system1.getQuiescence())
system2Labels = system2.getInputs().union(system2.getOutputs())
system2Labels.add(system2.getQuiescence())
enabledLabels_1 = set() enabledLabels_1 = set()
for state in current[0]: for state in current[0]:
enabledLabels_1 = enabledLabels_1.union(system1.outputs(state)) enabledLabels_1 = enabledLabels_1.union(system1.outputs(state))
......
# Functions useful for handling traces
# Given a trace flatten it to only one 'label' in sequence
def flatten(trace, label):
if trace == None:
return None
if len(trace) == 0:
return trace
# If trace does not contain at least 2 quiescence symbols, return trace
if trace.count(label) < 2:
return trace
# Temporary list constructed while checking current trace
finalTrace = [trace[0]]
for action in trace[1:]:
if action != label:
finalTrace.append(action)
elif finalTrace[-1] != label:
finalTrace.append(action)
return tuple(finalTrace)
# Given a trace, returns δ(σ) as the smallest set s.t. σ ∈ δ(σ) and σ1·δ·σ2 ∈
# δ(σ) => σ1·σ2 ∈ δ(σ)
def removeLabelsInCombination(trace, label):
newTraces = set()
if label in trace:
index = trace.index(label)
withQ = trace[:(index + 1)]
withoutQ = trace[:index]
rest = trace[(index + 1):]
for subtrace in removeLabelsInCombination(rest, label):
newTraces.add(withQ + subtrace)
newTraces.add(withoutQ + subtrace)
else:
newTraces.add(trace)
return newTraces
# Given a set of traces, return a set with all prefixes of all traces
# included those traces
def getPrefixes(traces):
prefixes = set()
for trace in traces:
# If I already encountered this trace, skip it
if trace in prefixes:
continue
for pos in range(len(trace)):
prefixes.add(trace[:pos])
return traces.union(prefixes)
# simple trie structure for traces
def make_trie(traces):
trie = {}
for trace in traces:
if trace == ():
trace = (u"\u03B5",)
temp_trie = trie
for label in trace:
temp_trie = temp_trie.setdefault(label, {})
temp_trie = temp_trie.setdefault('_end_', '_end_')
return trie
# if a trace is in trie
def in_trie(trie, trace):
if trace == ():
trace = (u"\u03B5",)
temp_trie = trie
for label in trace:
if label not in temp_trie:
return False
temp_trie = temp_trie[label]
if "_end_" in temp_trie:
return True
else:
return False
# remove a trace from trie
def remove_from_trie(trie, trace, depth = 0):
if trace == ():
trace = (u"\u03B5",)
if len(trace) == depth + 1:
if '_end_' in trie[trace[depth]]:
del trie[trace[depth]]['_end_'] # baz and barz both are safe
if len(trie[trace[depth]]) > 0 and len(trie) > 1: # baz and barz both are present
return False
elif len(trie) > 1 : # only baz is present
del trie[trace[depth]]
return False
elif len(trie[trace[depth]]) > 0: # only barz is present
return False
else:
return True
else:
temp_trie = trie
# Recursively climb up to delete.
if remove_from_trie(temp_trie[trace[depth]], trace, depth + 1):
if temp_trie:
del temp_trie[trace[depth]]
return not temp_trie
else:
return False
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
# Abstract class for experts
from abc import ABCMeta, abstractmethod
class Purpose(metaclass=ABCMeta):
# Given a trace, return the set of enabled actions after that trace
@abstractmethod
def getEnabled(self, trace):
pass
...@@ -4,11 +4,16 @@ from .baselts import AbstractIOLTS ...@@ -4,11 +4,16 @@ from .baselts import AbstractIOLTS
import random import random
import graphviz as gv import graphviz as gv
import numpy as np import numpy as np
import helpers.bisimulation as bi
import logging
class InputOutputLTS(AbstractIOLTS): class InputOutputLTS(AbstractIOLTS):
def __init__(self, numstates, inputs, outputs, quiescence = 'DELTA', def __init__(self, numstates, inputs, outputs, quiescence = 'DELTA',
transitions = None): transitions = None, logger = None):
self._logger = logger or logging.getLogger(__name__)
# Every LTS has at least 1 state # Every LTS has at least 1 state
if numstates < 1: if numstates < 1:
numstates = 1 numstates = 1
...@@ -162,8 +167,10 @@ class InputOutputLTS(AbstractIOLTS): ...@@ -162,8 +167,10 @@ class InputOutputLTS(AbstractIOLTS):
# thus redefine addTransition # thus redefine addTransition
class SuspensionAutomaton(InputOutputLTS): class SuspensionAutomaton(InputOutputLTS):
def __init__(self, numStates, inputs, outputs, quiescence = 'DELTA', chaos=False): def __init__(self, numStates, inputs, outputs, quiescence = 'DELTA',
InputOutputLTS.__init__(self, numStates, inputs, outputs, quiescence) chaos=False, logger=None):
InputOutputLTS.__init__(self, numStates, inputs, outputs, quiescence,
logger=logger)
# Quiescence is explicit: add it to outputs # Quiescence is explicit: add it to outputs
self._outputs.add(quiescence) self._outputs.add(quiescence)
...@@ -322,3 +329,138 @@ class SuspensionAutomaton(InputOutputLTS): ...@@ -322,3 +329,138 @@ class SuspensionAutomaton(InputOutputLTS):
x = np.linalg.solve(a, b) x = np.linalg.solve(a, b)
# 1 - discounted reachability of chaos from first state # 1 - discounted reachability of chaos from first state
return 1 - x[0] return 1 - x[0]
# Check if the suspension automaton is valid.
# Willemse T.A.C.: Heuristics for ioco-based test-based modelling
def isValid(self):
return (self.isNonBlocking() and self.isQuiescenceReducible() and
self.isAnomalyFree() and self.isStable())
def isNonBlocking(self):
# ∀q ∈ Q, ∃λ ∈ L_U ∪ {δ} . q λ→ (for each state there is an
# output transition leaving that state, or quiescence)
for state in range(self._numstates):
found = False
for label in self._outputs: # quiescence is in self._outputs
if (state, label) in self._transitions.keys():
# found a transition
found = True
exit
if found == False:
# if we did not find an output transition return false
# otherwise go to next state
return False
# If we never returned False, then we passed all states and found
# an output transition for each of them
return True
def isQuiescenceReducible(self):
# ∀q ∈ Q, ∀σ ∈ L^∗_δ . δ·σ ∈ traces(q) => σ ∈ traces(q)
# checked by simulation algorithm
# function used for filtering states that enable some label
stateWithLabel = lambda label: lambda x: (x,label) \
in self._transitions.keys()
# past contains the pair of states already visited.
# If I visited already a pair for one loop of the following for loop,
# I do not need to check it again for other loops. Thus past is outside
# the for loop.
past = set()
# filter states
for state1 in filter(stateWithLabel(self.getQuiescence()),
range(self.getNumStates())):
# Suspension automata are "deterministic"
state2 = next(iter(self._transitions[(state1, self.getQuiescence())]))
if state1 == state2:
# same state, simulation is trivial
continue
if (state1, state2) in past:
# I already visited this pair. Go to next state enabling quiescence
continue
wait = set()
wait.add((state1, state2))
while wait:
current = wait.pop()
past.add((current[0],current[1]))
# TODO: input enabledness?
labels = self._inputs.union(self._outputs)
for label in labels:
if (state2, label) not in self._transitions.keys():
# This label is not enabled in state 2, no need to check
continue
elif (state1, label) not in self._transitions.keys():
# Found a counterexample!
return False
else:
# Both enable label, follow label and add next pair of
# states in wait queue
newState1 = next(iter(self._transitions[(state1, label)]))
newState2 = next(iter(self._transitions[(state2, label)]))
if ((newState1,newState2) not in past
and newState1 != newState2):
wait.add((newState1, newState2))
# No counterexample to quiescence reducibility has been found.
return True
def isAnomalyFree(self):
# ∀q ∈ Q, ∀λ ∈ L_U . δ·λ not ∈ traces(q)
# each state reached by quiescence does not enable any other output
# list of quiescence transitions
qTransitions = [x for x in self._transitions.keys() \
if x[1] == self._quiescence]
# list of states that I already checked
checked = []
for (start, quiescence) in qTransitions:
for state in self._transitions[(start, quiescence)]:
if state not in checked:
checked.append(state)
if len(self.outputs(state)) > 1:
# More than one output enabled, quiescence + something
return False
elif self._quiescence not in self.outputs(state):
# only one output enabled, but not quiescence
return False
return True
def isStable(self):
# TODO: this method could be improved with a custom bisimulation
# we can avoid checking the same couple of state multiple
# times.
# ∀q, q' , q'' ∈ Q . q δ→ q' δ→ q'' => traces(q' ) = traces(q'' )
# After two delta transitions, there must be a bisimulation relation
# between the last two states.
# list of quiescence transitions
qTransitions = [x for x in self._transitions.keys() \
if x[1] == self._quiescence]
# list of pair of states that I already checked
checked = []
for (start, quiescence) in qTransitions:
for state1 in self._transitions[(start, quiescence)]:
states2 = self.nextStates(quiescence, state1)
if len(states2) != 1:
# something is wrong, either non deterministic, or
# quiescence is not enabled.
self._logger.warning("Suspension automaton either " +
"nondeterministic or does not enable quiescence" +
" where it should.")
return False
for state2 in states2:
# get the only element of states2
break
if (state1, state2) not in checked and state1 != state2:
checked.append((state1, state2))
if not bi.bisimilar(self, self, state1, state2):
return False
return True
# Classes representing experts for input and output labels
from .basepurpose import Purpose
class InputPurpose(Purpose):
def __init__(self, inputs):
self._inputs = inputs.copy()
# Given a trace returns the set of inputs enabled after it.
def getEnabled(self, trace):
return self._inputs
class OutputPurpose(Purpose):
def __init__(self, outputs):
self._outputs = outputs.copy()
# Given a trace returns the set of outputs enabled after it.
def getEnabled(self, trace):
return self._outputs
...@@ -8,6 +8,11 @@ class AbstractTeacher(metaclass=ABCMeta): ...@@ -8,6 +8,11 @@ class AbstractTeacher(metaclass=ABCMeta):
def process(self, trace): def process(self, trace):
pass pass
# Provide a sequence of inputs (possibly one or even zero) end get an output
@abstractmethod
def oneOutput(self, actions):
pass
# Get the input alphabet # Get the input alphabet
@abstractmethod @abstractmethod
def getInputAlphabet(self): def getInputAlphabet(self):
......
...@@ -25,6 +25,24 @@ class InputOutputTeacher(AbstractTeacher): ...@@ -25,6 +25,24 @@ class InputOutputTeacher(AbstractTeacher):
output = random.sample(self._lts.outputs(), 1)[0] output = random.sample(self._lts.outputs(), 1)[0]
return output return output
# Provide a sequence of inputs (possibly one or even zero) end get an output
def oneOutput(self, actions):
for i in range(len(actions)):
if self._lts.move(actions[i]) == None:
return None
return self.output()
# Provide output from current state
def output(self):
# Select a randomic output for current state
output = random.sample(self._lts.outputs(), 1)[0]
self._lts.move(output)
return output
# Reset the SUT
def reset(self):
self._lts.reset()
# Get the input alphabet # Get the input alphabet
def getInputAlphabet(self): def getInputAlphabet(self):
return self._lts.getInputs() return self._lts.getInputs()
......
# Abstract class for a Teacher in a L* based learning algorithm
from abc import ABCMeta, abstractmethod
class AbstractTester(metaclass=ABCMeta):
# Run a test suite
@abstractmethod
def findCounterexample(self, model):
pass
from .basetesting import AbstractTester
import random
import logging
# Random tester.
class RandomTester(AbstractTester):
def __init__(self, teacher, limit=1000, expectedLength=20, logger=None):
# The tester will run test using the teacher
self._teacher = teacher
self._expectedLength = expectedLength
self._limit = limit
self._logger = logger or logging.getLogger(__name__)
# Search a counterexample to teacher ioco model using at most limit actions
# provide an expectedLength
def findCounterexample(self, model):
self._teacher.reset()
model.reset()
ce = ()
i = 0
# in case of multiple inputs in a row, I need to keep track of them
consecutiveInputs = ()
while i <= self._limit:
#choice to reset or not:
#(roll dice with expectedLength faces, if 0