Skip to content
Snippets Groups Projects
Normal view Permalink
README 2.38 KiB
Newer Older
Davide Cavezza's avatar
Initial commit
Davide Cavezza committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 
This repository contains code for computing weakness of GR(1) formulae and for refining GR(1) assumptions in controller synthesis.
The code uses Python 2.7 and the directory structure is as follows:

- Counterstrategy: Contains the definition of the class Counterstrategy: it reads a .dot file containing a counterstrategy
output by RATSY and produces an object handled by the code
- ltl3ba: Contains the LTL3BA tool for producing Buchi automata from LTL expressions (not currently used):
https://sourceforge.net/projects/ltl3ba/
- ratsy: Contains the ratsy tool for controller synthesis and realizability checking:
http://rat.fbk.eu/ratsy/
- Refinement: Contains implementation of various refinement generation and search strategies
- scripts: Several scripts to run as many tests
- spot: Contains the Spot tool for producing Buchi automata from LTL expressions:
https://spot.lrde.epita.fr/trans.html
- Weakness: Code to compute the weakness measure of an LTL formula/automaton

The collected data is in the ComputedWeakness directory.
It contains three files:
- InterpolationBased.xlsx: Contains the weakness measures of all the refinements (partial and final) obtained via the interpolation-based procedure described in
Cavezza D.G., Alrajeh D. (2017) Interpolation-Based GR(1) Assumptions Refinement. In: Legay A., Margaria T. (eds)
Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2017. Lecture Notes in Computer Science, vol 10205. Springer, Berlin, Heidelberg
The IDs in the file refer to the assumptions listed in the RAT files on https://github.com/davidecavezza/TACAS17CaseStudies

- AlurRevised.csv: Weakness measures of the refinements of the AMBA02 case study returned by a modification of Alur's approach in
R. Alur, S. Moarref and U. Topcu, Counter-strategy guided refinement of GR(1) temporal logic specifications, 2013 Formal Methods 
in Computer-Aided Design, Portland, OR, 2013, pp. 26-33.
doi: 10.1109/FMCAD.2013.6679387
where the refinement search is performed as a best-first search led by the weakness heuristic.
The columns report:
- The list of GR(1) units in the refinement
- The depth in the refinement tree (corresponds to the number of GR(1) units)
- The values of d1 and d2

- results_path_to_leaf.csv
Contains the data about AMBA08 reported in the paper. These are the weakness computation times for refinements along one path to a realizable specification computed via interpolation.