alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/src/ltlvisit
History
Damien Lefortier e48338e8d8 Modify the ELTL parser to be able to support PSL operators. Add a 
new keyword in the ELTL format: finish, which applies to an
automaton operator and tells whether it just completed.

* src/eltlparse/eltlparse.yy: Clean it. Add finish.
* src/eltlparse/eltlscan.ll: Add finish.
* src/formula_tree.cc, src/formula_tree.hh: New files. Define a
small AST representing formulae where atomic props are unknown
which is used in the ELTL parser.
* src/ltlast/automatop.cc, ltlast/automatop.hh, ltlast/nfa.cc,
ltlast/nfa.hh: Adjust.
* src/ltlast/unop.cc, src/ltlast/unop.hh: Finish is an unop.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Handle finish in switches.
* src/tgbaalgos/eltl2tgba_lacim.cc: Translate finish.
* src/tgbatest/eltl2tgba.test: More tests.
2009-06-05 12:01:24 +02:00
..
.cvsignore * m4/pypath.m4: New file. 2003-04-30 12:35:22 +00:00
.gitignore Add .gitignore files 2008-03-14 16:59:32 +01:00
apcollect.cc * src/ltlast/formula.hh (hash, dump, dump_, hash_key_): New members. 2005-01-20 17:33:55 +00:00
apcollect.hh Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
basicreduce.cc Modify the ELTL parser to be able to support PSL operators. Add a 2009-06-05 12:01:24 +02:00
basicreduce.hh * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, 2004-11-17 16:23:40 +00:00
clone.cc Correct LaCIM for ELTL and make it work with LBTT. 2009-04-08 20:19:42 +02:00
clone.hh Add support for ELTL (AST & parser), and an adaptation of LaCIM 2009-03-26 12:05:08 +01:00
contain.cc Add support for ELTL (AST & parser), and an adaptation of LaCIM 2009-03-26 12:05:08 +01:00
contain.hh * src/evtgbaparse/public.hh: Work around Bison 2.3 unique guards. 2008-02-25 14:36:59 +01:00
destroy.cc Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
destroy.hh Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
dotty.cc Add support for ELTL (AST & parser), and an adaptation of LaCIM 2009-03-26 12:05:08 +01:00
dotty.hh * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, 2004-11-17 16:23:40 +00:00
dump.cc Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
dump.hh * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, 2004-11-17 16:23:40 +00:00
length.cc * src/ltlvisit/length.cc (length_visitor): Rewrite using 2005-02-23 00:35:45 +00:00
length.hh * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: New files. 2005-01-05 16:20:21 +00:00
lunabbrev.cc Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
lunabbrev.hh * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, 2004-11-17 16:23:40 +00:00
Makefile.am * src/tgbaalgos/ltl2tgba_fm.cc (language_containment_checker): Move ... 2008-02-25 14:36:58 +01:00
nenoform.cc Modify the ELTL parser to be able to support PSL operators. Add a 2009-06-05 12:01:24 +02:00
nenoform.hh Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
postfix.cc Add support for ELTL (AST & parser), and an adaptation of LaCIM 2009-03-26 12:05:08 +01:00
postfix.hh Add support for ELTL (AST & parser), and an adaptation of LaCIM 2009-03-26 12:05:08 +01:00
randomltl.cc Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
randomltl.hh * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: New files. 2005-01-05 16:20:21 +00:00
reduce.cc Modify the ELTL parser to be able to support PSL operators. Add a 2009-06-05 12:01:24 +02:00
reduce.hh Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
simpfg.cc Revert everything related to Damien's work in 2008 (he will commit a new version soon). 2009-03-25 16:44:05 +01:00
simpfg.hh * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, 2004-11-17 16:23:40 +00:00
syntimpl.cc Modify the ELTL parser to be able to support PSL operators. Add a 2009-06-05 12:01:24 +02:00
syntimpl.hh * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, 2004-11-17 16:23:40 +00:00
tostring.cc Modify the ELTL parser to be able to support PSL operators. Add a 2009-06-05 12:01:24 +02:00
tostring.hh Correct LaCIM for ELTL and make it work with LBTT. 2009-04-08 20:19:42 +02:00
tunabbrev.cc Modify the ELTL parser to be able to support PSL operators. Add a 2009-06-05 12:01:24 +02:00
tunabbrev.hh * src/ltlast/atomic_prop.hh, src/ltlast/binop.hh, 2004-11-17 16:23:40 +00:00