alarsyo/ltl2ba-nix
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Updated the README

Browse source
This commit is contained in:
Tom van Dijk 2020-10-25 12:19:48 +01:00
parent 26550da28e
commit ea33bb2091
1 changed files with 15 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
README
View file

@ -27,7 +27,7 @@ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
The LTL2BA software was written by Denis Oddoux and modified by Paul The LTL2BA software was written by Denis Oddoux and modified by Paul
Gastin. It is based on the translation algorithm presented at CAV '01: Gastin. It is based on the translation algorithm presented at CAV '01:
P.Gastin and D.Oddoux P.Gastin and D.Oddoux
"Fast LTL to Büchi Automata Translation" "Fast LTL to Büchi Automata Translation"
in 13th International Conference on Computer Aided Verification, CAV 2001, in 13th International Conference on Computer Aided Verification, CAV 2001,
G. Berry, H. Comon, A. Finkel (Eds.) G. Berry, H. Comon, A. Finkel (Eds.)
Paris, France, July 18-22, 2001, Paris, France, July 18-22, 2001,
@ -53,15 +53,17 @@ Here are the files that contain some code from Spin v3.4.1 :
2. COMPILING 2. COMPILING
open the archive : Using autotools:
> gunzip ltl2ba-1.1.tar.gz > autoconf -i -f
> tar xf ltl2ba-1.1.tar > ./configure
> cd ltl2ba-1.1
compile the program
> make > make
3. EXECUTING Using CMake
> mkdir build && cd build
> cmake ..
> make
3. EXECUTING AND TESTING
run the program run the program
> ./ltl2ba -f "formula" > ./ltl2ba -f "formula"
@ -97,11 +99,14 @@ run the command
> ./ltl2ba > ./ltl2ba
to see the possible options for executing the program to see the possible options for executing the program
To test, simply use a command with a formula such as:
> ./ltl2ba -f "a U b"
4. CHANGES IN VERSION 1.1 4. CHANGES IN VERSION 1.1
- fixing a bug in the way sets were used for strongly connected components. Thanks to Joachim Klein (klein@tcs.inf.tu-dresden.de) who found the bug and proposed a patch to fix it. - fixing a bug in the way sets were used for strongly connected components. Thanks to Joachim Klein (klein@tcs.inf.tu-dresden.de) who found the bug and proposed a patch to fix it.
- fixing a bug in the simplification with strongly connected components for the generalized Büchi automaton. - fixing a bug in the simplification with strongly connected components for the generalized Büchi automaton.
- improving the simplification with strongly connected components for the generalized Büchi automaton. - improving the simplification with strongly connected components for the generalized Büchi automaton.
- using getrusage to compute running times for the statistics - using getrusage to compute running times for the statistics
- some other minor updates. - some other minor updates.