diff --git a/CHANGELOG.md b/CHANGELOG.md index cf7d8fa43bf579ab8c2852dc0baf5cc7a9bea8ba..85f15b7d0794e6b736aab8e2cec248d4527fec71 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,7 @@ This project adheres to [Semantic Versioning](http://semver.org/). ## [Unreleased][unreleased] ### Added - Case study Tic Tac Toe +- LearnLib lib for Tic Tac Toe ### Changed - License diff --git a/README.md b/README.md index 0ecd4add515291e15ca2924bf6f298d8f0c42c5f..0e4a73c0a90e65d51edd256a8037bf23c133da1d 100644 --- a/README.md +++ b/README.md @@ -14,7 +14,6 @@ simulation, or model checking. The project is coded in Python3 and tested using Python3.4. - ## Included Libraries [NumPy](https://github.com/numpy/numpy) @@ -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/), 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 - learning tool. The adapters should inherit from `AbstractTeacher` in - [baseteacher.py](teachers/baseteacher.py) and from `AbstractOracle` in - [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. + +[Tic Tac Toe](examples/tictactoe/) uses a real *black box* system under learning. +There is also an example for learning a model of it using another learning +tool: [LearnLib](https://github.com/LearnLib/learnlib). ## Contributors diff --git a/examples/tictactoe/completetesting.py b/examples/tictactoe/completetesting.py index 7bccb598729d8ee76043bd3797c8dc119f4bd162..c7a1bbb6d27286925533bda4a1b3e7fc522123ab 100644 --- a/examples/tictactoe/completetesting.py +++ b/examples/tictactoe/completetesting.py @@ -59,8 +59,8 @@ class CompleteTicTacToeTester(AbstractTester): # return counterexample trace and output obtained by # testing return ce, output - elif 'END' in output: - continue + #elif 'END' in output: + # continue else: model.move(output) ce = ce + (output,) diff --git a/examples/tictactoe/learn.py b/examples/tictactoe/learn.py index 4410ccb7eb2a2c9d4731b104be36eb0e0717fdb1..a5f5a65729462fa373dd025ab95f638536998bec 100644 --- a/examples/tictactoe/learn.py +++ b/examples/tictactoe/learn.py @@ -39,6 +39,11 @@ from tictacpurpose import TicTacToeInputPurpose, TicTacToeOutputPurpose from learning.learning import LearningAlgorithm from testing.randomtesting import RandomTester from completetesting import CompleteTicTacToeTester +from systems.implementations import SuspensionAutomaton + +import helpers.bisimulation as bi + +import csv logging.basicConfig(level=logging.DEBUG) logger = logging.getLogger(__name__) @@ -71,7 +76,7 @@ print("Starting learning...") #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, inputPurpose=inputExpert) minus, plus = L.run() @@ -80,15 +85,36 @@ print("Models learned.") T1.close() -# while True: -# -# data = s.recv(1024) -# -# if not data or data == "EXIT": -# break -# -# msg = data.decode("utf-8") -# print(msg) -# move1 = str(input("\nNext move? ")) -# -# s.sendall(bytes(move1, 'UTF-8')) +####################################################################### +# If there is a model learned by LearnLib, load it and run a bisimulation +# check with minus +# The file must be converted with learnlib_dot2jtorx_aut.py +with open("/home/mic/repo/learnLTS/examples/tictactoe/learnLib/TicTacToe.aut", 'r') as csvfile: + first = True + reader = csv.reader(csvfile, delimiter=';', + quoting=csv.QUOTE_MINIMAL) + + for row in reader: + if first: + 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))) + +######################################################################## diff --git a/examples/tictactoe/learnLib/learnlib_dot2jtorx_aut.py b/examples/tictactoe/learnLib/learnlib_dot2jtorx_aut.py new file mode 100644 index 0000000000000000000000000000000000000000..b19216e3c30e10d480f3486c00c85a7178e7d9bd --- /dev/null +++ b/examples/tictactoe/learnLib/learnlib_dot2jtorx_aut.py @@ -0,0 +1,182 @@ +#!/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 is labeled : + m_ + - first transition : + -> for + - second transition : + -> for + """ + 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:]) diff --git a/examples/tictactoe/learnLib/version0.9.1/src/SutSocketWrapper.java b/examples/tictactoe/learnLib/version0.9.1/src/SutSocketWrapper.java index 3515b6a8c38064bbfcc7c26b2937bf8c31cc6e44..b0ce79cfec50c7b32a1f673b63c0a21c668d1c18 100644 --- a/examples/tictactoe/learnLib/version0.9.1/src/SutSocketWrapper.java +++ b/examples/tictactoe/learnLib/version0.9.1/src/SutSocketWrapper.java @@ -1,3 +1,23 @@ +/* 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; import java.io.BufferedReader; diff --git a/examples/tictactoe/learnLib/version0.9.1/src/TicTacToeLearner.java b/examples/tictactoe/learnLib/version0.9.1/src/TicTacToeLearner.java index 94c4740339bf77ff98eed23d52441a8705055b0a..4508b11a275a5e813e35c5c0c3f1e7d4bb416fdc 100644 --- a/examples/tictactoe/learnLib/version0.9.1/src/TicTacToeLearner.java +++ b/examples/tictactoe/learnLib/version0.9.1/src/TicTacToeLearner.java @@ -1,3 +1,23 @@ +/* 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; import java.io.BufferedReader; diff --git a/examples/tictactoe/tictacteacher.py b/examples/tictactoe/tictacteacher.py index 5f0653415688a0e98355f489d060dbf1cf6b50ba..4cdab864035afdfb65fe8c56b83ca9314ab5f8b5 100644 --- a/examples/tictactoe/tictacteacher.py +++ b/examples/tictactoe/tictacteacher.py @@ -73,6 +73,8 @@ class TicTacToeTeacher(AbstractTeacher): output = 'delta' if ready[0]: output = self._socket.recv(1024).decode("utf-8") + if '\n' in output: + output = output[0:-1] return output # Reset the SUT diff --git a/helpers/bisimulation.py b/helpers/bisimulation.py index 95741e83af0c9e41be0b57bb92b7ae583ab6f8e1..8106dd18e455a0654c67342ec4f239b6c7d2ad75 100644 --- a/helpers/bisimulation.py +++ b/helpers/bisimulation.py @@ -18,7 +18,9 @@ # OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN # 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 state1 = (startState1,) state2 = (startState2,) @@ -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.inputs(state)) + if noDelta: + enabledLabels_1 = enabledLabels_1 - set(system1.getQuiescence()) + enabledLabels_2 = enabledLabels_2 - set(system2.getQuiescence()) + if enabledLabels_1 != enabledLabels_2: # Proved not bisimilar, return False return (current[0],current[1],enabledLabels_1,enabledLabels_2,current[2])