diff --git a/README b/README index 4f0c739..63d74db 100644 --- a/README +++ b/README @@ -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 Gastin. It is based on the translation algorithm presented at CAV '01: 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, G. Berry, H. Comon, A. Finkel (Eds.) 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 -open the archive : -> gunzip ltl2ba-1.1.tar.gz -> tar xf ltl2ba-1.1.tar -> cd ltl2ba-1.1 - -compile the program +Using autotools: +> autoconf -i -f +> ./configure > make -3. EXECUTING +Using CMake +> mkdir build && cd build +> cmake .. +> make + +3. EXECUTING AND TESTING run the program > ./ltl2ba -f "formula" @@ -97,11 +99,14 @@ run the command > ./ltl2ba 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 - 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. -- improving 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. - using getrusage to compute running times for the statistics - some other minor updates.