You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 
Dave Parker 22bb6dea1c Merge prism-hoaf branch back into trunk. 11 years ago
..
APElement.java Working (but untidied) version of MDP LTL model checking. 18 years ago
APElementIterator.java Working (but untidied) version of MDP LTL model checking. 18 years ago
APSet.java Merge prism-hoaf branch back into trunk. 11 years ago
Alternating.java Next batch of LTL-related fixes from Joachim Klein (jltl2ba-fix-multiple-labels.patch, SimpleLTL-simplify-NEXT-AND-keep-order.patch, jltl2ba-fix-comments-for-release.patch, jltl2dstar-NBAAnalysis-dont-assume-NBA-is-disjoint.patch). 12 years ago
Buchi.java Next batch of LTL-related fixes from Joachim Klein (jltl2ba-fix-multiple-labels.patch, SimpleLTL-simplify-NEXT-AND-keep-order.patch, jltl2ba-fix-comments-for-release.patch, jltl2dstar-NBAAnalysis-dont-assume-NBA-is-disjoint.patch). 12 years ago
Generalized.java Next batch of LTL-related fixes from Joachim Klein (jltl2ba-fix-multiple-labels.patch, SimpleLTL-simplify-NEXT-AND-keep-order.patch, jltl2ba-fix-comments-for-release.patch, jltl2dstar-NBAAnalysis-dont-assume-NBA-is-disjoint.patch). 12 years ago
Makefile Fix makefiles with easier setup of classpath using * for jars. 14 years ago
MyBitSet.java Working (but untidied) version of MDP LTL model checking. 18 years ago
README Working (but untidied) version of MDP LTL model checking. 18 years ago
SimpleLTL.java Merge prism-hoaf branch back into trunk. 11 years ago
package-info.java Improved documentation (JavaDoc mostly). 15 years ago

README

LTL2BA - Version 1.0 - October 2001
Written by Denis Oddoux, LIAFA, France
Copyright (c) 2001 Denis Oddoux

LTL2BA - Version 1.1 - August 2007
Modified by Paul Gastin, LSV, France
Copyright (c) 2007 Paul Gastin
Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba

jltl2ba - November 2007
Ported by Carlos S. Bederian, FaMAF, Argentina
Copyright (c) 2007 Carlos S. Bederian

This package is a Java port of LTL2BA 1.1 by Carlos Bederian
for use with PRISM.

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"
in 13th International Conference on Computer Aided Verification, CAV 2001,
G. Berry, H. Comon, A. Finkel (Eds.)
Paris, France, July 1