Commit e15f092b authored by Michele's avatar Michele

added learnlib model conversion and bisimulation check

parent 11ab1f18
...@@ -5,6 +5,7 @@ This project adheres to [Semantic Versioning](http://semver.org/). ...@@ -5,6 +5,7 @@ This project adheres to [Semantic Versioning](http://semver.org/).
## [Unreleased][unreleased] ## [Unreleased][unreleased]
### Added ### Added
- Case study Tic Tac Toe - Case study Tic Tac Toe
- LearnLib lib for Tic Tac Toe
### Changed ### Changed
- License - License
......
...@@ -14,7 +14,6 @@ simulation, or model checking. ...@@ -14,7 +14,6 @@ simulation, or model checking.
The project is coded in Python3 and tested using Python3.4. 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)
...@@ -31,35 +30,10 @@ This code exists as a support implementation to the papers mentioned previously. ...@@ -31,35 +30,10 @@ This code exists as a support implementation to the papers mentioned previously.
Clone the repository. Then you can modify any file in [examples](examples/), Clone the repository. Then you can modify any file in [examples](examples/),
or create your own. or create your own.
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 [Tic Tac Toe](examples/tictactoe/) uses a real *black box* system under learning.
learning tool. The adapters should inherit from `AbstractTeacher` in There is also an example for learning a model of it using another learning
[baseteacher.py](teachers/baseteacher.py) and from `AbstractOracle` in tool: [LearnLib](https://github.com/LearnLib/learnlib).
[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.
Then you can start learning your system:
```python
teacher = YourOwnAdapterTeacher()
oracle = YourOwnAdapterOracle()
underModel, overModel = LearningAlgorithm(teacher, oracle, maxLoops=10,
tablePreciseness = 10000, modelPreciseness = 0.1,
tester=tester)
```
where `underModel` and `overModel` are the under and over approximations
of your system, respectively, `maxLoops` is the limit of learning loops
when the learned models are not changing any more, `tablePreciseness` and
`modelPreciseness` are the levels of preciseness you would like to reach
before stopping. Tester is a testing algorithm.
The learning process stops when either the learned model does not change for
`maxLoops` loops, or when both the preciseness levels are met.
## Contributors ## Contributors
......
...@@ -59,8 +59,8 @@ class CompleteTicTacToeTester(AbstractTester): ...@@ -59,8 +59,8 @@ class CompleteTicTacToeTester(AbstractTester):
# return counterexample trace and output obtained by # return counterexample trace and output obtained by
# testing # testing
return ce, output return ce, output
elif 'END' in output: #elif 'END' in output:
continue # continue
else: else:
model.move(output) model.move(output)
ce = ce + (output,) ce = ce + (output,)
......
...@@ -39,6 +39,11 @@ from tictacpurpose import TicTacToeInputPurpose, TicTacToeOutputPurpose ...@@ -39,6 +39,11 @@ from tictacpurpose import TicTacToeInputPurpose, TicTacToeOutputPurpose
from learning.learning import LearningAlgorithm from learning.learning import LearningAlgorithm
from testing.randomtesting import RandomTester from testing.randomtesting import RandomTester
from completetesting import CompleteTicTacToeTester from completetesting import CompleteTicTacToeTester
from systems.implementations import SuspensionAutomaton
import helpers.bisimulation as bi
import csv
logging.basicConfig(level=logging.DEBUG) logging.basicConfig(level=logging.DEBUG)
logger = logging.getLogger(__name__) logger = logging.getLogger(__name__)
...@@ -71,7 +76,7 @@ print("Starting learning...") ...@@ -71,7 +76,7 @@ print("Starting learning...")
#print(T1.oneOutput(('1'))) #print(T1.oneOutput(('1')))
L = LearningAlgorithm(T1, O1, printPath=path, maxLoops=10, L = LearningAlgorithm(T1, O1, printPath=path, maxLoops=4,
tablePreciseness=100000, logger=logger, tester=tester, outputPurpose=outputExpert, tablePreciseness=100000, logger=logger, tester=tester, outputPurpose=outputExpert,
inputPurpose=inputExpert) inputPurpose=inputExpert)
minus, plus = L.run() minus, plus = L.run()
...@@ -80,15 +85,36 @@ print("Models learned.") ...@@ -80,15 +85,36 @@ print("Models learned.")
T1.close() T1.close()
# while True: #######################################################################
# # If there is a model learned by LearnLib, load it and run a bisimulation
# data = s.recv(1024) # check with minus
# # The file must be converted with learnlib_dot2jtorx_aut.py
# if not data or data == "EXIT": with open("/home/mic/repo/learnLTS/examples/tictactoe/learnLib/TicTacToe.aut", 'r') as csvfile:
# break first = True
# reader = csv.reader(csvfile, delimiter=';',
# msg = data.decode("utf-8") quoting=csv.QUOTE_MINIMAL)
# print(msg)
# move1 = str(input("\nNext move? ")) for row in reader:
# if first:
# s.sendall(bytes(move1, 'UTF-8')) first = False
tup = row[0][3:] # remove 'des' from the first line
tuple_row = eval(tup)
learnLibmodel = SuspensionAutomaton(tuple_row[2],
inputs.copy(),
outputs.copy(),
quiescence,
False)
else:
tuple_row = eval(row[0])
#try:
# label = eval(tuple_row[1])
#except NameError:
label = tuple_row[1]
learnLibmodel.addTransition(tuple_row[0], label,
tuple_row[2])
print("Models learned. Check language equivalence...")
print("minus bisimilar to LearnLib model: " + str(bi.bisimilar(learnLibmodel,minus,startState1=0, startState2=0, noDelta=True)))
########################################################################
#!/usr/bin/env python
"""
generates aut for jtorx from dot file learned with learnlib
'?COIN_1_1'
'!TEA_0_1'
note: dot file uses I for input instead of ? and O for output instead of !
"""
# Author: Harco Kuppens
# MOdification by Michele Volpato: removed ? and ! from inputs and outputs
import sys, re, pprint # modules from standard lib (python 2.6 and later)
def get_lts_from_dotfile(dot_file):
""" Get labeled transition system from graphviz dot file
The dot file:
- describes a digraph with labels
- encodes the start state with the color='red' attribute
note: this corresponds with the highlighted state in learnlib API
Returns: [start_state,transions]
Where :
- start_state: start state label
- transitions: list of transitions
"""
start_state='unknown'
f=file(dot_file)
lines=f.readlines()
# find start state
# line in dot: __start0 -> s0;
for line in lines:
if line.find('->') != -1:
if line.find('__start') != -1:
start_state=line[line.find('->')+2:].strip(" ;\t\n")
break
# get transitions
# line in dot: s5 -> s5 [label="ARTREG 20013226 / 531"];
transitions=[]
for line in lines:
if line.find('__start') != -1:
continue
if line.find('->') != -1:
transitions.append(line)
# throw away transitions with the keywords : quiescence or inconsistency or undefined
#transitions = [ t for t in transitions if ( 'quiescence' not in t ) and ( 'inconsistency' not in t ) and ( 'undefined' not in t )]
trans_out=[]
regexpr_transition=re.compile(r'\s*(\w*)\s*-\>\s*(\w*)\s*\[label=\"(.*)\"\]')
regexpr_tag=re.compile(r'<[^>]+>')
for transition in transitions:
match=regexpr_transition.match(transition)
if match:
match=match.groups()
label=regexpr_tag.sub('',match[2])
trans_out.append({
'source' : match[0],
'target' : match[1],
'label': label
})
states=set()
for t in trans_out:
states.add(t['source'])
states.add(t['target'])
return [start_state,states,trans_out]
def parse_labels_of_mealy_lts(transitions):
"""Parse labels of labeled transition system
"""
trans_out=[]
for t in transitions:
label=t['label']
[inputstr,outputstr]=label.split('/')
trans_out.append({
'source' : t['source'],
'target' : t['target'],
'input': inputstr,
'output': outputstr,
})
return trans_out
def split_io_transitions_in_separate_input_and_output_transition(io_transitions,nr_states):
"""Split transitions with both an input and output event into two transitions
Makes two sequential transitions with a dummy state in between:
- dummy state <midstate> is labeled :
m_<counter>
- first transition :
<source> -> <midstate> for <input>
- second transition :
<midstate> -> <target> for <output>
"""
trans_out=[]
id=nr_states
for t in io_transitions:
midstate= 'm' + str(id)
trans_out.append({
'source': t['source'],
'target': midstate,
'label' : t['input'].strip(),
})
trans_out.append({
'source': midstate,
'target': t['target'],
'label' : t['output'].strip(),
})
id=id+1
states=set()
for t in trans_out:
states.add(t['source'])
states.add(t['target'])
return [states,trans_out]
def transitions2aut(transitions,first_state,nr_of_states):
nr_of_transitions=len(transitions)
strings=[ "des(" + first_state[1:] + "," + str(nr_of_transitions) + "," + str(nr_of_states) +")"]
for t in transitions:
#aut_edge ::= "(" start_state "," label "," end_state ")"
strings.append("("+t['source'][1:] + "," + '"' + t['label'] + '"' + "," + t['target'][1:] + ")" )
return "\n".join(strings)
def dot2aut(dot_filename_in):
"""
from mealy machine in a .dot file written by DotUtil.write of learnlib
we create an .aut file containing an lts where input and output each
have its own labeled transition. An input transition has a
label starting with '?' and an output transition has a label
starting with '!'
"""
if dot_filename_in[-4:].lower() != '.dot':
print "Problem: file '"+ dot_filename_in + "' is not a dot file!!"
print "Exit!"
sys.exit(1)
[start_state,states,transitions]=get_lts_from_dotfile(dot_filename_in)
io_transitions=parse_labels_of_mealy_lts(transitions) # each transition has input and output
[states,transitions]=split_io_transitions_in_separate_input_and_output_transition(io_transitions,len(states)) # each transition only has label again
#pprint.pprint(start_state)
#pprint.pprint(states)
#pprint.pprint(transitions)
result=transitions2aut(transitions,start_state,len(states))
aut_filename=dot_filename_in[:-4] + ".aut"
f=open(aut_filename ,'w')
f.write(result)
f.close()
print "written file : " + aut_filename
if __name__ == "__main__":
dot2aut(*sys.argv[1:])
/* Copyright (c) 2015 Michele Volpato
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in
# all copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
# THE SOFTWARE.
*/
package nl.ru.cs.mvolpato.tictaclearnlib; package nl.ru.cs.mvolpato.tictaclearnlib;
import java.io.BufferedReader; import java.io.BufferedReader;
......
/* Copyright (c) 2015 Michele Volpato
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in
# all copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
# THE SOFTWARE.
*/
package nl.ru.cs.mvolpato.tictaclearnlib; package nl.ru.cs.mvolpato.tictaclearnlib;
import java.io.BufferedReader; import java.io.BufferedReader;
......
...@@ -73,6 +73,8 @@ class TicTacToeTeacher(AbstractTeacher): ...@@ -73,6 +73,8 @@ class TicTacToeTeacher(AbstractTeacher):
output = 'delta' output = 'delta'
if ready[0]: if ready[0]:
output = self._socket.recv(1024).decode("utf-8") output = self._socket.recv(1024).decode("utf-8")
if '\n' in output:
output = output[0:-1]
return output return output
# Reset the SUT # Reset the SUT
......
...@@ -18,7 +18,9 @@ ...@@ -18,7 +18,9 @@
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
# THE SOFTWARE. # THE SOFTWARE.
def bisimilar(system1, system2, startState1=0, startState2=0): def bisimilar(system1, system2, startState1=0, startState2=0, noDelta=False):
# noDelta: avoid quiescent transitions
# starting from given states # starting from given states
state1 = (startState1,) state1 = (startState1,)
state2 = (startState2,) state2 = (startState2,)
...@@ -42,6 +44,10 @@ def bisimilar(system1, system2, startState1=0, startState2=0): ...@@ -42,6 +44,10 @@ def bisimilar(system1, system2, startState1=0, startState2=0):
enabledLabels_2 = enabledLabels_2.union(system2.outputs(state)) enabledLabels_2 = enabledLabels_2.union(system2.outputs(state))
enabledLabels_2 = enabledLabels_2.union(system2.inputs(state)) enabledLabels_2 = enabledLabels_2.union(system2.inputs(state))
if noDelta:
enabledLabels_1 = enabledLabels_1 - set(system1.getQuiescence())
enabledLabels_2 = enabledLabels_2 - set(system2.getQuiescence())
if enabledLabels_1 != enabledLabels_2: if enabledLabels_1 != enabledLabels_2:
# Proved not bisimilar, return False # Proved not bisimilar, return False
return (current[0],current[1],enabledLabels_1,enabledLabels_2,current[2]) return (current[0],current[1],enabledLabels_1,enabledLabels_2,current[2])
......
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