Commit graph

24 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
847270b480 ltlcross: replace %H,%T,%N by %O
Also get rid of the lbt_parser, and fix the LBT support of the HOA
parser.

* doc/org/ltlcross.org, doc/org/ltldo.org: Update.
* src/bin/common_trans.cc, src/bin/common_trans.hh: Add support for
%O, and keep %T,%N,%H as hidden aliases without disabling them.
* src/bin/ltlcross.cc, src/bin/ltldo.cc, src/tgbatest/ltl2tgba.cc:
Call hoa_parse instead of lbt_parse.
* src/hoaparse/hoaparse.yy: Improve error reporting from LBT.
* src/hoaparse/hoascan.ll: Fix typos preventing parsing of
LBT files with more than 10 states.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: Delete the lbt
parser.
* src/tgbatest/lbttparse.test: Adjust the expected error message.
* NEWS: Update.
2015-02-01 02:09:48 +01:00
Alexandre Duret-Lutz
4673427252 remove obsolete comments
* src/tgbaalgos/lbtt.hh, src/tgbaalgos/neverclaim.hh: Remove obsolete
comments.  Reported by Claire Parquier.
2015-01-08 17:01:40 +01:00
Alexandre Duret-Lutz
e4158c21ee tgbaparse, lbttparse: do not pass an environment for acceptance sets
* src/priv/accmap.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/ltl2tgba.cc, src/tgbatest/tgbaread.cc: Do not pass any
environment parameter to parse acceptance sets.  This is not used
anymore since we moved to int-labeled acceptance sets.
2014-12-10 20:49:17 +01:00
Alexandre Duret-Lutz
bf6c906772 Fix some bdd_dict_ptr not being passed by const reference.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/formula2bdd.cc,
src/tgba/formula2bdd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh,
src/tgba/tgbagraph.hh, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/translate.cc,
src/tgbaalgos/translate.hh, src/tgbaalgos/word.cc,
src/tgbaalgos/word.hh: Pass shared_ptr to functions by const ref.
2014-08-15 11:07:05 +02:00
Alexandre Duret-Lutz
51151ab271 Handle all automata through shared_ptr. (monstro patch)
A type such as 'const tgba_digraph*' and 'tgba_digraph*' are replaced
by 'const_tgba_digraph_ptr' and 'tgba_digraph_ptr'.  Additionally 'new
tgba_digraph(...)' is replaced by 'make_tgba_digraph(...)'.

This convention is followed by all automata types. Those smart
pointers should normally be passed by const reference as input of
function to avoid the atomic increments/decrements, but I probably
missed a few, as this huge patch took me nearly 12h.

* src/kripke/fwd.hh, src/tgba/fwd.hh: New files.
* src/kripke/Makefile.am, src/tgba/Makefile.am: Adjust.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
src/bin/common_output.hh, src/bin/dstar2tgba.cc,
src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
src/bin/ltlfilt.cc, src/dstarparse/dra2ba.cc,
src/dstarparse/dstar2tgba.cc, src/dstarparse/dstarparse.yy,
src/dstarparse/nra2nba.cc, src/dstarparse/nsa2tgba.cc,
src/dstarparse/public.hh, src/graphtest/tgbagraph.cc,
src/kripke/fairkripke.hh, src/kripke/kripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/neverparse/neverclaimparse.yy,
src/neverparse/public.hh, src/priv/accmap.hh,
src/priv/countstates.cc, src/priv/countstates.hh, src/saba/saba.hh,
src/saba/sabacomplementtgba.cc, src/saba/sabacomplementtgba.hh,
src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
src/sabatest/sabacomplementtgba.cc, src/ta/ta.hh,
src/ta/taexplicit.cc, src/ta/taexplicit.hh, src/ta/taproduct.cc,
src/ta/taproduct.hh, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc,
src/ta/tgtaproduct.hh, src/taalgos/dotty.cc, src/taalgos/dotty.hh,
src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
src/taalgos/minimize.cc, src/taalgos/minimize.hh,
src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
src/taalgos/tgba2ta.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
src/tgba/formula2bdd.hh, src/tgba/futurecondcol.cc,
src/tgba/futurecondcol.hh, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgba/tgbagraph.hh,
src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbamask.cc, src/tgba/tgbamask.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc,
src/tgba/tgbaproxy.hh, src/tgba/tgbasafracomplement.cc,
src/tgba/tgbasafracomplement.hh, src/tgba/tgbascc.cc,
src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh,
src/tgba/wdbacomp.cc, src/tgba/wdbacomp.hh,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
src/tgbaalgos/complete.cc, src/tgbaalgos/complete.hh,
src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh,
src/tgbaalgos/cycles.hh, src/tgbaalgos/degen.cc,
src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dotty.hh, src/tgbaalgos/dottydec.cc,
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dtbasat.cc,
src/tgbaalgos/dtbasat.hh, src/tgbaalgos/dtgbacomp.cc,
src/tgbaalgos/dtgbacomp.hh, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/dtgbasat.hh, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness.cc,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/gtec.cc,
src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/status.cc,
src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.cc,
src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.cc,
src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
src/tgbaalgos/minimize.cc, src/tgbaalgos/minimize.hh,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/postproc.cc,
src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.cc,
src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.cc,
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.cc,
src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.cc,
src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.cc,
src/tgbaalgos/rundotdec.hh, src/tgbaalgos/safety.cc,
src/tgbaalgos/safety.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh,
src/tgbaalgos/sccfilter.cc, src/tgbaalgos/sccfilter.hh,
src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh,
src/tgbaalgos/stats.cc, src/tgbaalgos/stats.hh,
src/tgbaalgos/stripacc.cc, src/tgbaalgos/stripacc.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/maskacc.cc, src/tgbatest/powerset.cc,
src/tgbatest/randtgba.cc, src/tgbatest/taatgba.cc,
src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc,
wrap/python/ajax/spot.in, wrap/python/spot.i,
wrap/python/tests/interdep.py: Use shared pointers for automata.
2014-08-15 11:07:05 +02:00
Alexandre Duret-Lutz
dc5ad78b3e Make bdd_dict a shared pointer.
* src/tgba/bdddict.hh (bdd_dict_ptr): New type.
(make_bdd_dict): New function.
* iface/dve2/dve2.cc, iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
src/dstarparse/dstarparse.yy, src/dstarparse/public.hh,
src/graphtest/tgbagraph.cc, src/kripke/kripkeexplicit.cc,
src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.cc,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
src/kripketest/parse_print_test.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/contain.cc, src/ltlvisit/contain.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/neverparse/neverclaimparse.yy, src/neverparse/public.hh,
src/priv/accmap.hh, src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/sabatest/sabacomplementtgba.cc,
src/ta/ta.hh, src/ta/taexplicit.cc, src/ta/taexplicit.hh,
src/ta/taproduct.cc, src/ta/taproduct.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/taalgos/dotty.cc, src/tgba/bddprint.cc,
src/tgba/bddprint.hh, src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.hh,
src/tgba/tgbagraph.hh, src/tgba/tgbakvcomplement.cc,
src/tgba/tgbakvcomplement.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbaproxy.cc, src/tgba/tgbaproxy.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh,
src/tgba/wdbacomp.cc, src/tgbaalgos/compsusp.cc,
src/tgbaalgos/compsusp.hh, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh,
src/tgbaalgos/word.cc, src/tgbaalgos/word.hh, src/tgbaparse/public.hh,
src/tgbaparse/tgbaparse.yy, src/tgbatest/complementation.cc,
src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/maskacc.cc,
src/tgbatest/powerset.cc, src/tgbatest/randtgba.cc,
src/tgbatest/taatgba.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc, wrap/python/ajax/spot.in,
wrap/python/tests/alarm.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/parsetgba.py: Update to use bdd_dict_ptr and
make_bdd_dict().
2014-08-13 20:23:09 +02:00
Alexandre Duret-Lutz
120ce7d8e6 lbtt: build an explicit automaton on input.
* src/priv/accmap.hh (acc_mapper): Rename into...
(acc_mapper_string): ... this, and add
(acc_mapper_int): ... this variant.
* src/tgbaparse/tgbaparse.yy: Adjust to renaming.
* src/tgbaalgos/lbtt.cc: Use acc_mapper_int and build an explicit
automaton.
* src/tgbaalgos/lbtt.hh: Adjust return type.
* src/tgbatest/ltl2tgba.cc: Adjust to new return type.
2014-07-03 10:06:53 +02:00
Alexandre Duret-Lutz
a0f5d53ea4 Use -fvisibility=hidden in src/tgbaalgos/.
* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/Makefile.am: Add
$(VISIBILITY_CXXFLAGS).
* src/tgbaalgos/bfssteps.hh, src/tgbaalgos/compsusp.hh,
src/tgbaalgos/cutscc.hh, src/tgbaalgos/cycles.hh,
src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/nsheap.hh,
src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gtec/status.hh, src/tgbaalgos/gv04.hh,
src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.hh,
src/tgbaalgos/minimize.hh, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/postproc.hh, src/tgbaalgos/powerset.hh,
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reducerun.hh,
src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh,
src/tgbaalgos/safety.hh, src/tgbaalgos/save.hh, src/tgbaalgos/scc.hh,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/se05.hh,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.hh,
src/tgbaalgos/stripacc.hh, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.hh, src/tgbaalgos/translate.hh: Mark public
symbol with SPOT_API.
2013-07-29 01:14:03 +02:00
Alexandre Duret-Lutz
178ba87681 Improve documentation here and there.
* doc/Doxyfile.in: Update to Doxygen 1.8.4
* doc/footer.html: Point to the mailing list.
* doc/mainpage.dox: Point to spot::translator,
and spot::kripke.
* src/ta/tgta.hh: Do not use \emph.
* src/tgba/succiter.hh: Fix rendering of example.
* src/tgba/tgba.hh: Correct documentation.
* src/tgbaalgos/cycles.hh: Improve rendering of
documentation.
* src/tgbaalgos/lbtt.hh, src/tgbaalgos/minimize.hh:
Document missing arguments.
2013-06-09 15:55:57 +02:00
Alexandre Duret-Lutz
1ec9cebe58 Move \ingroup before \brief in all Doxygen comments.
Using \ingroup between \brief and the rest of the documentation causes
Doxygen to concatenate the brief with the rest of the doc.

* src/sanity/style.test: Warn when \ingroup is found
on the line after \brief.
* src/kripke/fairkripke.hh, src/kripke/kripke.hh,
src/kripke/kripkeprint.hh, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.hh, src/ltlast/binop.hh, src/ltlast/bunop.hh,
src/ltlast/constant.hh, src/ltlast/formula.hh, src/ltlast/multop.hh,
src/ltlast/refformula.hh, src/ltlast/unop.hh, src/ltlast/visitor.hh,
src/ltlenv/declenv.hh, src/ltlenv/defaultenv.hh,
src/ltlenv/environment.hh, src/ltlparse/ltlfile.hh,
src/ltlvisit/clone.hh, src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.hh, src/ltlvisit/length.hh, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/mark.hh, src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.hh,
src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh,
src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.hh, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.hh, src/misc/bddalloc.hh, src/misc/bddlt.hh,
src/misc/freelist.hh, src/misc/hash.hh, src/misc/ltstr.hh,
src/misc/minato.hh, src/misc/modgray.hh, src/misc/optionmap.hh,
src/misc/version.hh, src/saba/explicitstateconjunction.hh,
src/saba/saba.hh, src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
src/saba/sabasucciter.hh, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.hh, src/ta/ta.hh, src/ta/taproduct.hh,
src/ta/tgta.hh, src/taalgos/reachiter.hh, src/taalgos/tgba2ta.hh,
src/tgba/futurecondcol.hh, src/tgba/sba.hh, src/tgba/state.hh,
src/tgba/succiter.hh, src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbaproduct.hh, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.hh, src/tgba/tgbasgba.hh, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.hh, src/tgba/wdbacomp.hh, src/tgbaalgos/bfssteps.hh,
src/tgbaalgos/degen.hh, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.hh,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/powerset.hh, src/tgbaalgos/projrun.hh,
src/tgbaalgos/randomgraph.hh, src/tgbaalgos/reachiter.hh,
src/tgbaalgos/reducerun.hh, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/rundotdec.hh, src/tgbaalgos/save.hh,
src/tgbaalgos/stripacc.hh, src/tgbaalgos/translate.hh: Move \ingroup
before \brief.
2013-06-08 23:24:37 +02:00
Alexandre Duret-Lutz
eed7e2df8f lbtt: improve the LBTT output
Provide a way to output automata with state-based acceptance.  Also
print the guards using to_lbt_string() for consistency: as a
consequence, atomic proposition that do not match p[0-9]+ are now
double-quoted.

* src/tgbaalgos/lbtt.hh (lbtt_reachable): Add a sba option.
* src/tgbaalgos/lbtt.cc: Implement it, and use to_lbt_string().
* src/ltlvisit/lbt.cc (is_pnum): Reject 'p' without number.
* src/bin/ltl2tgba.cc: Activate the sba option of --ba was given.
Add an option --lbtt=t to get the old behavior.
* src/bin/man/ltl2tgba.x: Document the LBTT format we use with
some links and examples.
* src/tgbatest/lbttparse.test: More tests.
* src/tgbatest/ltlcross2.test: Add a check with --lbtt --ba.
* NEWS: Update.
2013-05-09 21:55:37 +02:00
Alexandre Duret-Lutz
c55bd831a8 Add a parser for automata in LBTT's format.
* src/tgbaalgos/lbtt.hh, src/tgbaalgos/lbtt.cc (lbtt_parse):
New function.
* src/tgba/tgbaexplicit.hh (get_acceptance_condition): Make it public.
* src/tgbatest/ltl2tgba.cc: Add a -XL option to read LBTT file.
* src/tgbatest/lbttparse.test: New file.
* src/tgbatest/Makefile.am: Add it.
2012-10-13 13:36:40 +02:00
Alexandre Duret-Lutz
1551c5d947 Upgrade GPL v2+ to GPL v3+.
* NEWS: Mention this.
* COPYING: Replace by GPL v3.
* src/sanity/style.test: Check files with the wrong license,
in case we forgot to update it during a merge.
* Makefile.am, bench/Makefile.am, bench/emptchk/Makefile.am,
bench/emptchk/defs.in, bench/emptchk/ltl-human.sh,
bench/emptchk/ltl-random.sh, bench/emptchk/pml-clserv.sh,
bench/emptchk/pml-eeaean.sh, bench/emptchk/pml2tgba.pl,
bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/known,
bench/ltl2tgba/lbtt2csv.pl, bench/ltl2tgba/ltl2baw.in,
bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small,
bench/ltlclasses/Makefile.am, bench/ltlclasses/defs.in,
bench/ltlclasses/run, bench/ltlcounter/Makefile.am,
bench/ltlcounter/defs.in, bench/ltlcounter/run,
bench/scc-stats/Makefile.am, bench/scc-stats/stats.cc,
bench/split-product/Makefile.am, bench/split-product/cutscc.cc,
bench/split-product/pml2tgba.pl, bench/wdba/Makefile.am,
bench/wdba/defs.in, bench/wdba/run, configure.ac, doc/Makefile.am,
doc/dot.in, doc/tl/Makefile.am, iface/Makefile.am,
iface/dve2/Makefile.am, iface/dve2/defs.in, iface/dve2/dve2.cc,
iface/dve2/dve2.hh, iface/dve2/dve2check.cc,
iface/dve2/dve2check.test, iface/dve2/finite.test,
iface/dve2/kripke.test, iface/gspn/Makefile.am, iface/gspn/common.cc,
iface/gspn/common.hh, iface/gspn/dcswave.test,
iface/gspn/dcswaveeltl.test, iface/gspn/dcswavefm.test,
iface/gspn/dcswaveltl.test, iface/gspn/dottygspn.cc,
iface/gspn/dottyssp.cc, iface/gspn/gspn.cc, iface/gspn/gspn.hh,
iface/gspn/ltlgspn.cc, iface/gspn/simple.test, iface/gspn/ssp.cc,
iface/gspn/ssp.hh, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test,
iface/gspn/udcsfm.test, iface/gspn/udcsltl.test, src/Makefile.am,
src/bin/Makefile.am, src/bin/common_cout.cc, src/bin/common_cout.hh,
src/bin/common_finput.cc, src/bin/common_finput.hh,
src/bin/common_output.cc, src/bin/common_output.hh,
src/bin/common_post.cc, src/bin/common_post.hh, src/bin/common_r.cc,
src/bin/common_r.hh, src/bin/common_range.cc, src/bin/common_range.hh,
src/bin/common_setup.cc, src/bin/common_setup.hh,
src/bin/common_sys.hh, src/bin/genltl.cc, src/bin/ltl2tgba.cc,
src/bin/ltl2tgta.cc, src/bin/ltlfilt.cc, src/bin/man/Makefile.am,
src/bin/randltl.cc, src/eltlparse/Makefile.am,
src/eltlparse/eltlparse.yy, src/eltlparse/eltlscan.ll,
src/eltlparse/fmterror.cc, src/eltlparse/parsedecl.hh,
src/eltlparse/public.hh, src/eltltest/Makefile.am,
src/eltltest/acc.cc, src/eltltest/acc.test, src/eltltest/defs.in,
src/eltltest/nfa.cc, src/eltltest/nfa.test, src/evtgba/Makefile.am,
src/evtgba/evtgba.cc, src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh,
src/evtgba/explicit.cc, src/evtgba/explicit.hh, src/evtgba/product.cc,
src/evtgba/product.hh, src/evtgba/symbol.cc, src/evtgba/symbol.hh,
src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc,
src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc,
src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc,
src/evtgbaalgos/save.hh, src/evtgbaalgos/tgba2evtgba.cc,
src/evtgbaalgos/tgba2evtgba.hh, src/evtgbaparse/Makefile.am,
src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am,
src/evtgbatest/defs.in, src/evtgbatest/explicit.cc,
src/evtgbatest/explicit.test, src/evtgbatest/ltl2evtgba.cc,
src/evtgbatest/ltl2evtgba.test, src/evtgbatest/product.cc,
src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
src/evtgbatest/readsave.test, src/kripke/Makefile.am,
src/kripke/fairkripke.cc, src/kripke/fairkripke.hh,
src/kripke/kripke.cc, src/kripke/kripke.hh,
src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh,
src/kripkeparse/Makefile.am, src/kripkeparse/fmterror.cc,
src/kripkeparse/kripkeparse.yy, src/kripkeparse/kripkescan.ll,
src/kripkeparse/parsedecl.hh, src/kripkeparse/public.hh,
src/kripkeparse/scankripke.ll, src/kripketest/Makefile.am,
src/kripketest/bad_parsing.test, src/kripketest/defs.in,
src/kripketest/kripke.test, src/kripketest/parse_print_test.cc,
src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/nfa.cc, src/ltlast/nfa.hh,
src/ltlast/predecl.hh, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/visitor.hh, src/ltlenv/Makefile.am, src/ltlenv/declenv.cc,
src/ltlenv/declenv.hh, src/ltlenv/defaultenv.cc,
src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh,
src/ltlparse/Makefile.am, src/ltlparse/fmterror.cc,
src/ltlparse/ltlfile.cc, src/ltlparse/ltlfile.hh,
src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll,
src/ltlparse/parsedecl.hh, src/ltlparse/public.hh,
src/ltltest/Makefile.am, src/ltltest/consterm.cc,
src/ltltest/consterm.test, src/ltltest/defs.in, src/ltltest/equals.cc,
src/ltltest/equals.test, src/ltltest/kind.cc, src/ltltest/kind.test,
src/ltltest/length.cc, src/ltltest/length.test,
src/ltltest/lunabbrev.test, src/ltltest/nenoform.test,
src/ltltest/parse.test, src/ltltest/parseerr.test,
src/ltltest/readltl.cc, src/ltltest/reduc.cc, src/ltltest/reduc.test,
src/ltltest/reduccmp.test, src/ltltest/reducpsl.test,
src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test,
src/ltltest/tostring.cc, src/ltltest/tostring.test,
src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
src/ltltest/utf8.test, src/ltltest/uwrm.test,
src/ltlvisit/Makefile.am, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/ltlvisit/destroy.cc,
src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh, src/ltlvisit/lbt.cc,
src/ltlvisit/lbt.hh, src/ltlvisit/length.cc, src/ltlvisit/length.hh,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/mark.cc, src/ltlvisit/mark.hh, src/ltlvisit/nenoform.cc,
src/ltlvisit/nenoform.hh, src/ltlvisit/postfix.cc,
src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.cc,
src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.cc,
src/ltlvisit/reduce.hh, src/ltlvisit/relabel.cc,
src/ltlvisit/relabel.hh, src/ltlvisit/simpfg.cc,
src/ltlvisit/simpfg.hh, src/ltlvisit/simplify.cc,
src/ltlvisit/simplify.hh, src/ltlvisit/snf.cc, src/ltlvisit/snf.hh,
src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh,
src/misc/Makefile.am, src/misc/acccompl.cc, src/misc/acccompl.hh,
src/misc/accconv.cc, src/misc/accconv.hh, src/misc/bareword.cc,
src/misc/bareword.hh, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
src/misc/bddlt.hh, src/misc/bddop.cc, src/misc/bddop.hh,
src/misc/casts.hh, src/misc/escape.cc, src/misc/escape.hh,
src/misc/fixpool.hh, src/misc/freelist.cc, src/misc/freelist.hh,
src/misc/hash.hh, src/misc/hashfunc.hh, src/misc/intvcmp2.cc,
src/misc/intvcmp2.hh, src/misc/intvcomp.cc, src/misc/intvcomp.hh,
src/misc/ltstr.hh, src/misc/memusage.cc, src/misc/memusage.hh,
src/misc/minato.cc, src/misc/minato.hh, src/misc/modgray.cc,
src/misc/modgray.hh, src/misc/mspool.hh, src/misc/optionmap.cc,
src/misc/optionmap.hh, src/misc/random.cc, src/misc/random.hh,
src/misc/timer.cc, src/misc/timer.hh, src/misc/unique_ptr.hh,
src/misc/version.cc, src/misc/version.hh, src/neverparse/Makefile.am,
src/neverparse/fmterror.cc, src/neverparse/neverclaimparse.yy,
src/neverparse/neverclaimscan.ll, src/neverparse/parsedecl.hh,
src/neverparse/public.hh, src/saba/Makefile.am,
src/saba/explicitstateconjunction.cc,
src/saba/explicitstateconjunction.hh, src/saba/saba.cc,
src/saba/saba.hh, src/saba/sabacomplementtgba.cc,
src/saba/sabacomplementtgba.hh, src/saba/sabastate.hh,
src/saba/sabasucciter.hh, src/sabaalgos/Makefile.am,
src/sabaalgos/sabadotty.cc, src/sabaalgos/sabadotty.hh,
src/sabaalgos/sabareachiter.cc, src/sabaalgos/sabareachiter.hh,
src/sabatest/Makefile.am, src/sabatest/defs.in,
src/sabatest/sabacomplementtgba.cc, src/sanity/Makefile.am,
src/sanity/readme.test, src/sanity/style.test, src/ta/Makefile.am,
src/ta/ta.cc, src/ta/ta.hh, src/ta/taexplicit.cc,
src/ta/taexplicit.hh, src/ta/taproduct.cc, src/ta/taproduct.hh,
src/ta/tgta.cc, src/ta/tgta.hh, src/ta/tgtaexplicit.cc,
src/ta/tgtaexplicit.hh, src/ta/tgtaproduct.cc, src/ta/tgtaproduct.hh,
src/taalgos/Makefile.am, src/taalgos/dotty.cc, src/taalgos/dotty.hh,
src/taalgos/emptinessta.cc, src/taalgos/emptinessta.hh,
src/taalgos/minimize.cc, src/taalgos/minimize.hh,
src/taalgos/reachiter.cc, src/taalgos/reachiter.hh,
src/taalgos/statessetbuilder.cc, src/taalgos/statessetbuilder.hh,
src/taalgos/stats.cc, src/taalgos/stats.hh, src/taalgos/tgba2ta.cc,
src/taalgos/tgba2ta.hh, src/tgba/Makefile.am, src/tgba/bdddict.cc,
src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh,
src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh,
src/tgba/public.hh, src/tgba/sba.hh, src/tgba/state.hh,
src/tgba/statebdd.cc, src/tgba/statebdd.hh, src/tgba/succiter.hh,
src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgba.cc,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
src/tgba/tgbakvcomplement.cc, src/tgba/tgbakvcomplement.hh,
src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbasafracomplement.hh,
src/tgba/tgbascc.cc, src/tgba/tgbascc.hh, src/tgba/tgbasgba.cc,
src/tgba/tgbasgba.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgba/tgbaunion.cc, src/tgba/tgbaunion.hh, src/tgba/wdbacomp.cc,
src/tgba/wdbacomp.hh, src/tgbaalgos/Makefile.am,
src/tgbaalgos/bfssteps.cc, src/tgbaalgos/bfssteps.hh,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh,
src/tgbaalgos/cycles.cc, src/tgbaalgos/cycles.hh,
src/tgbaalgos/degen.cc, src/tgbaalgos/degen.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/eltl2tgba_lacim.hh,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh,
src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/gtec/Makefile.am,
src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/isdet.cc,
src/tgbaalgos/isdet.hh, src/tgbaalgos/isweakscc.cc,
src/tgbaalgos/isweakscc.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2taa.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
src/tgbaalgos/magic.hh, src/tgbaalgos/minimize.cc,
src/tgbaalgos/minimize.hh, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh,
src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh,
src/tgbaalgos/projrun.cc, src/tgbaalgos/projrun.hh,
src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reachiter.cc, src/tgbaalgos/reachiter.hh,
src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh,
src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh,
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh,
src/tgbaalgos/safety.cc, src/tgbaalgos/safety.hh,
src/tgbaalgos/save.cc, src/tgbaalgos/save.hh, src/tgbaalgos/scc.cc,
src/tgbaalgos/scc.hh, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/se05.cc,
src/tgbaalgos/se05.hh, src/tgbaalgos/simulation.cc,
src/tgbaalgos/simulation.hh, src/tgbaalgos/stats.cc,
src/tgbaalgos/stats.hh, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/tau03opt.hh, src/tgbaalgos/weight.cc,
src/tgbaalgos/weight.hh, src/tgbaparse/Makefile.am,
src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbaparse/tgbascan.ll, src/tgbatest/Makefile.am,
src/tgbatest/babiak.test, src/tgbatest/bddprod.test,
src/tgbatest/complementation.cc, src/tgbatest/complementation.test,
src/tgbatest/cycles.test, src/tgbatest/defs.in,
src/tgbatest/degendet.test, src/tgbatest/degenid.test,
src/tgbatest/dfs.test, src/tgbatest/dupexp.test,
src/tgbatest/eltl2tgba.test, src/tgbatest/emptchk.test,
src/tgbatest/emptchke.test, src/tgbatest/emptchkr.test,
src/tgbatest/explicit.cc, src/tgbatest/explicit.test,
src/tgbatest/explicit2.cc, src/tgbatest/explicit2.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explpro4.test, src/tgbatest/explprod.cc,
src/tgbatest/explprod.test, src/tgbatest/intvcmp2.cc,
src/tgbatest/intvcomp.cc, src/tgbatest/intvcomp.test,
src/tgbatest/kv.test, src/tgbatest/ltl2neverclaim.test,
src/tgbatest/ltl2ta.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltl2tgba.test, src/tgbatest/ltlcounter.test,
src/tgbatest/ltlprod.cc, src/tgbatest/ltlprod.test,
src/tgbatest/mixprod.cc, src/tgbatest/mixprod.test,
src/tgbatest/neverclaimread.test, src/tgbatest/nondet.test,
src/tgbatest/obligation.test, src/tgbatest/powerset.cc,
src/tgbatest/randpsl.test, src/tgbatest/randtgba.cc,
src/tgbatest/randtgba.test, src/tgbatest/readsave.test,
src/tgbatest/renault.test, src/tgbatest/scc.test,
src/tgbatest/sccsimpl.test, src/tgbatest/spotlbtt.test,
src/tgbatest/spotlbtt2.test, src/tgbatest/taatgba.cc,
src/tgbatest/taatgba.test, src/tgbatest/tgbaread.cc,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.cc,
src/tgbatest/tripprod.test, src/tgbatest/wdba.test,
src/tgbatest/wdba2.test, wrap/Makefile.am, wrap/python/Makefile.am,
wrap/python/ajax/Makefile.am, wrap/python/ajax/spot.in,
wrap/python/buddy.i, wrap/python/spot.i,
wrap/python/tests/Makefile.am, wrap/python/tests/alarm.py,
wrap/python/tests/bddnqueen.py, wrap/python/tests/implies.py,
wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
wrap/python/tests/ltl2tgba.test, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py, wrap/python/tests/minato.py,
wrap/python/tests/modgray.py, wrap/python/tests/optionmap.py,
wrap/python/tests/parsetgba.py, wrap/python/tests/run.in,
wrap/python/tests/setxor.py: Update licence version, and replace the
FSF address by a URL.
2012-10-12 22:05:18 +02:00
Alexandre Duret-Lutz
c3e399c837 * src/tgba/tgba.hh, src/tgbaalgos/dotty.hh,
src/tgbaalgos/dottydec.hh, src/tgbaalgos/dupexp.hh,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh,
src/tgbaalgos/neverclaim.hh, src/tgbaalgos/powerset.hh,
src/tgbaalgos/projrun.hh, src/tgbaalgos/randomgraph.hh,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/replayrun.hh, src/tgbaalgos/rundotdec.hh
src/tgbaalgos/save.hh, src/tgbaalgos/stats.hh,
src/tgbaparse/public.hh: Add Doxygen groups for TGBA algorithms.
2004-11-17 16:56:36 +00:00
Alexandre Duret-Lutz
ad96e8fbad * iface/gspn/common.cc, iface/gspn/common.hh,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlparse/fmterror.cc, src/ltlparse/public.hh,
src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
src/misc/escape.cc, src/misc/escape.hh, src/tgba/bdddict.cc,
src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh: Include <iosfwd>
in headers, and prefer <ostream> in the body whenever possible.
* src/sanity/style.test, HACKING: Check and document this.
2004-08-09 16:32:25 +00:00
Alexandre Duret-Lutz
3b85646638 lbtt 1.1.0 supports TGBAs, use that and remove old workarounds.
* src/tgbaalgos/lbtt.cc (state_acc_pair, state_acc_pair_equal,
state_acc_pair_hash, acp_seen_map, todo_set, seen_map, fill_todo
lbtt_reachable): Remove.
(nonacceptant_lbtt_bfs): Rename as ...
(lbtt_bfs): ... this, and adjust to output acceptance conditions
on transitions.
(nonacceptant_lbtt_reachable): Rename as ...
(lbtt_reachable): ... this.
* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): Delete.
* src/tgbatest/ltl2tgba.cc: Suppress option "-T".
2004-07-08 16:42:00 +00:00
Alexandre Duret-Lutz
7069d5406b This should help getting accurate statistics (on both the
formula automaton and the synchronized product) from LBTT.
Idea from Jean-Michel Couvreur.

* src/tgbaalgos/lbtt.cc (nonacceptant_lbtt_bfs): New class.
(nonacceptant_lbtt_reachable): New function.
* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): New
function.
* src/tgbatest/ltl2tgba.cc (main): Call nonacceptant_lbtt_reachable
if the -T option is used.
* src/tgbatest/spotlbtt.test: Setup the -T variants, disabled by
default.
2004-02-07 23:49:28 +00:00
Alexandre Duret-Lutz
0816a4505f * src/tgbaalgos/lbtt.hh: Typos. 2004-02-05 18:44:09 +00:00
Alexandre Duret-Lutz
e341cc9ab6 * iface/gspn/eesrg.cc, iface/gspn/eesrg.hh, iface/gspn/gspn.cc,
iface/gspn/gspn.hh, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
src/tgba/bddprint.hh, src/tgba/succiter.hh,
src/tgba/succiterconcrete.cc, src/tgba/succiterconcrete.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.cc,
src/tgba/tgbabddconcrete.hh, src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbaexplicit.cc,
src/tgba/tgbaexplicit.hh, src/tgba/tgbaproduct.cc,
src/tgba/tgbaproduct.hh, src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/emptinesscheck.cc, src/tgbaalgos/emptinesscheck.hh,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/save.cc, src/tgbatest/explicit.cc,
src/tgbatest/ltl2tgba.cc, src/tgbaparse/tgbaparse.yy,
wrap/python/tests/ltl2tgba.py:
Rewrite `accepting condition' as `acceptance condition'.
The symbols which have been renamed are:
tgba::all_accepting_conditions
tgba::neg_accepting_conditions
succ_iterator::current_accepting_conditions
bdd_dict::register_accepting_variable
bdd_dict::register_accepting_variables
bdd_dict::is_registered_accepting_variable
tgba_bdd_concrete_factory::declare_accepting_condition
tgba_bdd_core_data::accepting_conditions
tgba_bdd_core_data::all_accepting_conditions
tgba_explicit::declare_accepting_condition
tgba_explicit::complement_all_accepting_conditions
tgba_explicit::has_accepting_condition
tgba_explicit::get_accepting_condition
tgba_explicit::add_accepting_condition
tgba_explicit::all_accepting_conditions
tgba_explicit::neg_accepting_conditions
state_tba_proxy::acceptance_cond
accepting_cond_splitter
2003-11-28 16:34:42 +00:00
Alexandre Duret-Lutz
43a91a152a * COPYING: New file.
* Makefile.am, configure.ac, doc/Makefile.am, iface/Makefile.am,
iface/gspn/Makefile.am, iface/gspn/common.cc,
iface/gspn/common.hh, iface/gspn/dottyeesrg.cc,
iface/gspn/dottygspn.cc, iface/gspn/eesrg.cc, iface/gspn/eesrg.hh,
iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/multop.hh,
src/ltlast/predecl.hh, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/visitor.hh, src/ltlenv/Makefile.am,
src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
src/ltlenv/environment.hh, src/ltlparse/Makefile.am,
src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/ltltest/Makefile.am,
src/ltltest/defs.in, src/ltltest/equals.cc,
src/ltltest/equals.test, src/ltltest/lunabbrev.test,
src/ltltest/nenoform.test, src/ltltest/parse.test,
src/ltltest/parseerr.test, src/ltltest/readltl.cc,
src/ltltest/tostring.cc, src/ltltest/tostring.test,
src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test,
src/ltlvisit/Makefile.am, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/destroy.cc,
src/ltlvisit/destroy.hh, src/ltlvisit/dotty.cc,
src/ltlvisit/dotty.hh, src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
src/misc/Makefile.am, src/misc/bddalloc.cc, src/misc/bddalloc.hh,
src/misc/bddlt.hh, src/misc/hash.hh, src/misc/minato.cc,
src/misc/minato.hh, src/misc/version.cc, src/misc/version.hh,
src/tgba/Makefile.am, src/tgba/bdddict.cc, src/tgba/bdddict.hh,
src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/public.hh,
src/tgba/state.hh, src/tgba/statebdd.cc, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.cc,
src/tgba/succiterconcrete.hh, src/tgba/tgba.cc, src/tgba/tgba.hh,
src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcretefactory.cc,
src/tgba/tgbabddconcretefactory.hh,
src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbabddconcreteproduct.hh, src/tgba/tgbabddcoredata.cc,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh,
src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh,
src/tgba/tgbatba.cc, src/tgba/tgbatba.hh,
src/tgbaalgos/Makefile.am, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dotty.hh, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptinesscheck.cc,
src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.cc,
src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/magic.cc,
src/tgbaalgos/magic.hh, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/reachiter.hh, src/tgbaalgos/save.cc,
src/tgbaalgos/save.hh, src/tgbaparse/Makefile.am,
src/tgbaparse/fmterror.cc, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbaparse/tgbascan.ll, src/tgbatest/Makefile.am,
src/tgbatest/bddprod.test, src/tgbatest/defs.in,
src/tgbatest/dupexp.test, src/tgbatest/emptchk.test,
src/tgbatest/emptchke.test, src/tgbatest/explicit.test,
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test,
src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test,
src/tgbatest/readsave.test, src/tgbatest/spotlbtt.test,
src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test,
wrap/Makefile.am, wrap/python/Makefile.am, wrap/python/buddy.i,
wrap/python/spot.i, wrap/python/cgi/Makefile.am,
wrap/python/cgi/ltl2tgba.in, wrap/python/tests/Makefile.am,
wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltl2tgba.test,
wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
wrap/python/tests/run.in: Add Copyright license.
2003-11-21 15:54:25 +00:00
Alexandre Duret-Lutz
66b1630c31 Homogenize passing of automata as pointers, not references.
Disallow copy for security.

* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy.
* src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise.
* src/tgba/tgbaexplicit.cc (tgba_explicit::operator=,
tgba_explicit::tgba_explicit(tgba_explicit)): Remove.
* src/tgba/tgbabddconcreteproduct.cc
(tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory,
product): Take operand automata as pointers.
* src/tgba/tgbabddconcreteproduct.hh (product): Likewise.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh:
(tgba_product): Disallow copy.
(tgba_product::tgba_product): Take operand automata as pointers.
* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable):
Take tgba arguments as pointer.
* src/tgbaalgos/dotty.hh (dotty_reachable): Likewise.
* src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise.
* src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba):
Likewise.
* src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise.
* src/tgbaalgos/save.hh (save): Likewise.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc,
src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc: Likewise.
2003-07-14 22:20:35 +00:00
Alexandre Duret-Lutz
9df8be4503 typo 2003-07-09 15:05:00 +00:00
Alexandre Duret-Lutz
2a8b1b7471 Make sure we only output one initial state in LBTT's output.
* src/tgbaalgos/lbtt.cc (fill_todo): Add the 'first' argument
to designate initial states.
(lbtt_reachable): Adjust calls to fill_todo.  Handle the
fake initial state accepting conditions specially.
* src/tgbaalgos/lbtt.hh: Update comments.
2003-07-09 14:03:43 +00:00
Alexandre Duret-Lutz
f9c8eb1cb7 * src/tgbatest/ltl2tgba.cc: Add option -t to output the LBTT automata.
* src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add lbtt.hh.
(libtgbaalgos_la_SOURCES): Add lbtt.cc.
* src/tgba/bddprint.cc (print_sat_handler): Put a space after "!".
* src/tgbatest/readsave.test: Adjust spaces after "!".
2003-07-08 15:45:11 +00:00