Commit a01c49a9 authored by Michele's avatar Michele

implemented preciseness of model, also added fake state in dot file for a better representation

parent fbff22de
......@@ -10,6 +10,10 @@ nondeterministic systems. The code is based on these scientific papers:
The goal is to constructing a model of a system for model-based testing,
simulation, or model checking.
## Included Libraries
[NumPy](https://github.com/numpy/numpy)
## Code Example
Check [the examples folder](examples/) for how to use it.
......@@ -26,7 +30,8 @@ If you are using a real system under testing (an actual running black box
software), you need to write your own adapters to connect it to the
learning tool. The adapters should inherit from `AbstractTeacher` in
[baseteacher.py](teachers/baseteacher.py) and from `AbstractOracle` in
[baseoracle.py](teachers/baseoracle.py)
[baseoracle.py](teachers/baseoracle.py).
In particular, the adapters should implement the abstract methods in
`AbstractTeacher` and `AbstractOracle`. Those method are used by the
learner to ask so called **output** and **observation** queries.
......
......@@ -21,19 +21,31 @@ def createDOTFile(lts, path, format='svg'):
states = list(range(lts.getNumStates()))
nodes = []
# Create fake initial state
nodes.append(('_nil', {'style': 'invis'}))
try:
if lts.isChaotic():
# Add chaotic states, useful for suspension automata
nodes.append((str(-1), {'label': 'χ'}))
nodes.append((str(-2), {'label': 'δ'}))
nodes.append((str(-1), {'label': u"\u03C7"}))
nodes.append((str(-2), {'label': u"\u03B4"}))
except AttributeError:
pass
for x in states:
# from numbers to strings
nodes.append(str(x))
if x == 0:
# state 0 is initial state
nodes.append((str(x), {'label': '', 'initial': 'initial'}))
else:
# from numbers to strings
nodes.append((str(x), {'label': ''}))
edges = []
# Create transition from fake initial state
edges.append((('_nil', '0'), {'label': ''}))
transitions = lts.getTransitions()
keys = transitions.keys()
for (state1, label) in keys:
......
......@@ -10,7 +10,7 @@ class LearningAlgorithm:
def __init__(self, teacher, oracle , tablePreciseness = 1000,
modelPreciseness = 0.1, closeStrategy = None,
printPath = None, maxLoops=10, logger=None):
self._logger = logger or logging.getLogger(__name__)
self._teacher = teacher
......@@ -256,9 +256,12 @@ class LearningAlgorithm:
if (self._table.preciseness() < self._tablePreciseness or
currentModelPreciseness < self._modelPreciseness):
self._logger.info("Requested table preciseness: " +
self._logger.info("Requested table preciseness: " +
str(self._tablePreciseness) + ". Actual: "+
str(self._table.preciseness()))
self._logger.info("Requested model preciseness: " +
str(self._modelPreciseness) + ". Actual: "+
str(currentModelPreciseness))
# TODO: Improve Preciseness
# For the moment, select a random way to do it:
# Add a random row or a random column, or update the table.
......@@ -281,9 +284,12 @@ class LearningAlgorithm:
pass
continue
else:
self._logger.info("Requested table preciseness: " +
self._logger.info("Requested table preciseness: " +
str(self._tablePreciseness) + ". Actual: "+
str(self._table.preciseness()))
self._logger.info("Requested model preciseness: " +
str(self._modelPreciseness) + ". Actual: "+
str(currentModelPreciseness))
self._logger.info("Stop learning")
# Exit while loop, return hMinus and hPlus
break
......
......@@ -3,6 +3,7 @@
from .baselts import AbstractIOLTS
import random
import graphviz as gv
import numpy as np
class InputOutputLTS(AbstractIOLTS):
......@@ -176,6 +177,9 @@ class SuspensionAutomaton(InputOutputLTS):
# Add transitions between the two chaotic states
self._addChaoticTransitions()
# Discounted reachability (for calculating preciseness)
self._discount = 0.5
def isChaotic(self):
return self._isChaotic
......@@ -219,4 +223,102 @@ class SuspensionAutomaton(InputOutputLTS):
return InputOutputLTS.addTransition(self, state1, label, state2)
def preciseness(self):
return 0.5
if not self.isChaotic():
return 1
# breadth first search to find n reachability of set(-1,-2)
# starting from chaotic states
queue = [self.getChaos()]
# visited states
visited = []
while queue:
# dequeue
current = queue.pop(0)
visited.append(current)
adjacents = [x for (x,label) in self._transitions.keys() \
if current in self._transitions[(x,label)]]
for adjacent in adjacents:
if not adjacent in visited + queue:
# enqueue
queue.append(adjacent)
chaos = set([self.getChaos(), self.getChaosDelta()])
# Get parents of a Chaotic states and the probability to reach
# a chaotic state from them.
probabilitiesOne = {}
distanceOne = [x for (x,label) in self._transitions.keys() \
if (self._transitions[(x,label)].intersection(chaos) != set() and
x not in chaos)]
for state in distanceOne:
# total transitions from state
totTrans = len([l for (s, l) in self._transitions.keys() \
if s == state])
# num transitions from state to chaos
numTrans = len([l for (s, l) in self._transitions.keys() \
if (self._transitions[(s,l)].intersection(chaos) != set() and
s == state)])
probabilitiesOne[state] = (numTrans,totTrans)
# visited now contains all states that can reach Chaos
# probabilitiesOne contains all state with distance one and the
# probabilities to get to Chaos from them
# for each state, get the linear equation describing the rechability
# of chaos
equations = []
values = []
for state in range(self.getNumStates()):
# if Chaos is not reacheble, then state-th variable is 0
if state not in visited:
equation = []
for stateVar in range(self.getNumStates()):
if stateVar != state:
equation.append(0)
else:
equation.append(1)
equations.append(equation)
values.append(0)
continue
# if we are in a chaotic state then variable is 1
if state in [self.getChaos(),self.getChaosDelta()]:
equation = []
for stateVar in range(self.getNumStates()):
if stateVar != state:
equation.append(0)
else:
equation.append(1)
equations.append(equation)
values.append(1)
continue
# otherwise construct linear equation
equation = []
# total transitions from state
totTrans = len([l for (s, l) in self._transitions.keys() \
if s == state])
for stateVar in range(self.getNumStates()):
# Important! stateVar cannot be in Chaos
# num transitions from state to statVar
numTrans = len([l for (s, l) in self._transitions.keys() \
if (stateVar in self._transitions[(s,l)] and
s == state)])
if stateVar != state:
equation.append(self._discount * numTrans / totTrans)
else:
# format: stateVar = a*x1 + b*x2 + ... + c * stateVar + d
equation.append((self._discount * numTrans / totTrans)-1)
equations.append(equation)
# Reachability with one step
if state in probabilitiesOne.keys():
(numTrans,totTrans) = probabilitiesOne[state]
values.append(-(numTrans / totTrans))
else:
values.append(0)
a = np.array(equations)
b = np.array(values)
x = np.linalg.solve(a, b)
# 1 - discounted reachability of chaos from first state
return 1 - x[0]
......@@ -141,3 +141,41 @@ class TestImplementations:
S1 = SuspensionAutomaton(1, inputs, outputs, quiescence, True)
gh.createDOTFile(S1, path, "pdf")
print("File " + path + ".pdf must be checked by hand.")
def model_preciseness_test(self):
inputs = set(['a'])
outputs = set(['x','y'])
quiescence = u"\u03B4"
S1=SuspensionAutomaton(5, inputs, outputs, quiescence, chaos=True)
S1.addTransition(0,'a',1)
S1.addTransition(0,quiescence,0)
S1.addTransition(1,quiescence,2)
S1.addTransition(1,'a',3)
S1.addTransition(1,'x',-1)
S1.addTransition(1,'y',-1)
S1.addTransition(2,quiescence,2)
S1.addTransition(2,'a',3)
S1.addTransition(3,'a',3)
S1.addTransition(3,'y',-1)
S1.addTransition(3,quiescence,-2)
S1.addTransition(3,'x',4)
S1.addTransition(4,'x',-1)
S1.addTransition(4,'y',-1)
S1.addTransition(4,quiescence,0)
S1.addTransition(4,'a',1)
currentdir = os.path.dirname(os.path.abspath(
inspect.getfile(inspect.currentframe())))
parentdir = os.path.dirname(currentdir)
path = os.path.join(parentdir, "tests", "test_model_preciseness_file", "g1")
gh.createDOTFile(S1, path, "pdf")
# x1 = 1/4*x2 + 1/4*x1 + 0
# x2 = 1/8*x3 + 1/8*x4 + 1/2
# 1/4*x4 - 3/4*x3 = 0
# -7/8*x4 + 1/8*x5 = -1/2
# 1/8*x2 + 1/8*x1 - x5 = -1/2
assert_almost_equal(S1.preciseness(),1-(51/251))
......@@ -188,9 +188,11 @@ class TestLearningAlgorithm:
path = os.path.join(parentdir, "tests", "test_reducibility_check")
L3 = LearningAlgorithm(T3, O3, printPath=path, maxLoops=10,
tablePreciseness = 10000, modelPreciseness = 0.1)
tablePreciseness = 10000, modelPreciseness = 0.8)
Hminus, Hplus = L3.run()
# If fail it is because our test extension methods are not implemented
# yet
assert_equal(bi.bisimilar(I3,Hplus), True)
def deterministic_learning_test(self):
......
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