alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
2278 commits 6 branches 0 tags 36 MiB
Commit graph

2278 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
8c2d7fcb7f Use the same location.hh and position.hh in all parsers. 
* src/misc/location.hh, src/misc/position.hh: New files,
from Bison 2.7.
* src/misc/Makefile.am: Distribute them.
* src/eltlparse/Makefile.am, src/eltlparse/eltlparse.yy,
src/eltlparse/parsedecl.hh, src/eltlparse/public.hh,
src/kripkeparse/Makefile.am, src/kripkeparse/kripkeparse.yy,
src/kripkeparse/parsedecl.hh, src/kripkeparse/public.hh,
src/ltlparse/Makefile.am, src/ltlparse/fmterror.cc,
src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/neverparse/Makefile.am,
src/neverparse/neverclaimparse.yy, src/neverparse/parsedecl.hh,
src/neverparse/public.hh, src/tgbaparse/Makefile.am,
src/tgbaparse/parsedecl.hh, src/tgbaparse/public.hh,
src/tgbaparse/tgbaparse.yy: Adjust to use and include
misc/location.hh.
* NEWS: Mention this change.
 2013-07-29 01:14:34 +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
dab51a9dd0 Use -fvisibility=hidden in src/kripke/, src/saba/, and src/sabaalgos/ 
* src/kripke/Makefile.am, src/saba/Makefile.am,
src/sabaalgos/Makefile.am: Use $(VISIBILITY_CXXFLAGS).
* src/kripke/fairkripke.hh, src/kripke/kripke.hh,
src/kripke/kripkeexplicit.hh, src/kripke/kripkeprint.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: Mark exported symbols
with SPOT_API.
 2013-07-29 01:14:03 +02:00
Alexandre Duret-Lutz
a12922b331 Use -fvisibility=hidden in src/tgba/. 
* src/tgba/Makefile.am: Use $(VISIBILITY_CXXFLAGS).
* src/tgba/bdddict.hh, src/tgba/bddprint.hh, src/tgba/formula2bdd.hh,
src/tgba/futurecondcol.hh, src/tgba/state.hh, src/tgba/statebdd.hh,
src/tgba/succiter.hh, src/tgba/succiterconcrete.hh, src/tgba/taatgba.hh,
src/tgba/tgba.hh, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddconcretefactory.hh, src/tgba/tgbabddconcreteproduct.hh,
src/tgba/tgbabddcoredata.hh, src/tgba/tgbabddfactory.hh,
src/tgba/tgbaexplicit.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: Mark exported symbols with
SPOT_API.
* src/tgba/public.hh: Mark the file as deprecated.
* src/tgbaalgos/cutscc.hh: Adjust.
 2013-07-29 01:14:03 +02:00
Alexandre Duret-Lutz
8ba3e64f0a Use -fvisibility=hidden in src/ltlast/, src/ltlvisit/, and src/ltlenv/. 
* src/ltlast/Makefile.am, src/ltlenv/Makefile.am,
src/ltlvisit/Makefile.am: Use $(VISIBILITY_CXXFLAGS).
* src/misc/common.hh (SPOT_DEPRECATED): New macro.
* 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/formula_tree.hh,
src/ltlast/multop.hh, src/ltlast/nfa.hh, src/ltlast/refformula.hh,
src/ltlast/unop.hh, src/ltlast/visitor.hh, src/ltlenv/declenv.hh,
src/ltlenv/defaultenv.hh, src/ltlvisit/apcollect.hh,
src/ltlvisit/clone.hh, src/ltlvisit/contain.hh,
src/ltlvisit/destroy.hh, src/ltlvisit/dotty.hh, src/ltlvisit/dump.hh,
src/ltlvisit/lbt.hh, src/ltlvisit/length.hh,
src/ltlvisit/lunabbrev.hh, src/ltlvisit/nenoform.hh,
src/ltlvisit/postfix.hh, src/ltlvisit/randomltl.hh,
src/ltlvisit/reduce.hh, src/ltlvisit/relabel.hh,
src/ltlvisit/remove_x.hh, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.hh, src/ltlvisit/snf.hh,
src/ltlvisit/tostring.hh, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.hh: Add SPOT_API in fron of
exported symbols.
* src/ltlvisit/nenoform.cc, src/ltlvisit/remove_x.cc: Add missing
include of the corresponding header file.
 2013-07-29 01:14:03 +02:00
Alexandre Duret-Lutz
cbfbf14297 * NEWS: summarize recent changes 2013-07-29 01:13:57 +02:00
Alexandre Duret-Lutz
1ed43038e8 Move bdd_allocator to src/priv/. 
* src/misc/bddalloc.cc, src/misc/bddalloc.hh,
src/misc/freelist.cc, src/misc/freelist.hh: Move ...
* src/priv/bddalloc.cc, src/priv/bddalloc.hh,
src/priv/freelist.cc, src/priv/freelist.hh: ... here.
* src/misc/Makefile.am, src/priv/Makefile.am: Adjust.
* src/tgba/bdddict.cc: Adjust include.
* src/tgbaalgos/ltl2tgba_fm.cc: Remove useless include.
 2013-07-29 01:12:13 +02:00
Alexandre Duret-Lutz
9775dfdd4b Hide the only use of bdd_allocator. 
* src/tgba/bdddict.cc, src/tgba/bdddict.hh:  Hide the bdd_allocator
dependency in a bdd_dict_priv class that is not defined publicly.
 2013-07-29 01:12:13 +02:00
Alexandre Duret-Lutz
1581a94c65 * src/misc/unique_ptr.hh: Add missing operator->() const. 2013-07-29 01:12:13 +02:00
Alexandre Duret-Lutz
882097a2ce Remove modgray, it's not used. 
* src/misc/modgray.cc, src/misc/modgray.hh: Delete.
* src/misc/Makefile.am: Adjust.
* wrap/python/tests/modgray.py: Delete.
* wrap/python/tests/Makefile.am: Adjust.
* wrap/python/spot.i: Remove binding.
 2013-07-29 01:12:12 +02:00
Alexandre Duret-Lutz
f2078ac325 Create a new src/priv/ directory for private algorithms. 
* README: Document it.
* configure.ac: Generate src/priv/Makefile.
* src/Makefile.am: Recurse into priv/.
* src/priv/Makefile.am: New file.
* src/misc/acccompl.cc, src/misc/acccompl.hh,
src/misc/accconv.cc, src/misc/accconv.hh: Move to...
* src/priv/acccompl.cc, src/priv/acccompl.hh,
src/priv/accconv.cc, src/priv/accconv.hh: ... here.
* src/misc/Makefile.am: Adjust.
* src/tgbaalgos/scc.cc, src/tgbaalgos/simulation.cc: Adjust
includes.
* src/sanity/style.test: Make sure no public header
file include a private one.
 2013-07-29 01:12:12 +02:00
Alexandre Duret-Lutz
2ef8917ba5 Enable -fvisibility=hidden for src/misc/. 
* configure.ac: Check for -fvisibility support.
* m4/ax_check_compile_flag.m4: New file.
* src/misc/common.hh: New file.
* src/misc/Makefile.am: Add common.hh, and adjust to use -fvisibility.
* src/misc/bareword.hh, src/misc/escape.hh, src/misc/formater.hh,
src/misc/intvcmp2.hh, src/misc/intvcomp.hh, src/misc/memusage.hh,
src/misc/minato.hh, src/misc/optionmap.hh, src/misc/random.hh,
src/misc/timer.hh, src/misc/version.hh, src/misc/bddop.hh: Include
common.hh and add SPOT_API tags.
* src/misc/acccompl.hh, src/misc/accconv.hh: Prepare for upcoming
move.
* src/sanity/style.test: Ignore SPOT_API tags.
* wrap/python/Makefile.am: Ignore SPOT_API.
* wrap/python/spot.i: Do not emit binding for bddalloc.hh.
* wrap/python/tests/minato.py: Do not use bdd_allocator.
 2013-07-29 01:12:12 +02:00
Alexandre Duret-Lutz
b5710663f4 [buddy] Restrict the number of exported symbols. 
* src/bdd.h, src/bvec.h, src/fdd.h: Declare all exported
symbols using BUDDY_API, a new macro that sets visibility=default.
* src/Makefile.am: Compile with -fvisibility=hidden by default,
and compile the C++ part with -fvisibility-inlines-hidden as well.
 2013-07-29 01:12:12 +02:00
Alexandre Duret-Lutz
9ed2d7a1dc Bump version to 1.1.4a. 
* NEWS: Bump version.
* configure.ac: Bump version, and add a banner
about this being a development version at the end.
 2013-07-29 01:11:32 +02:00
Alexandre Duret-Lutz
9d6d53ed92 Release Spot 1.1.4. 
* NEWS, configure.ac, doc/org/tools.org: Update version.
 2013-07-29 00:27:59 +02:00
Alexandre Duret-Lutz
ce6114f461 * THANKS: Jan should have been added earlier... 2013-07-29 00:25:13 +02:00
Alexandre Duret-Lutz
cb7bdf8c1f Fix interpretation of {e[*]} and !{e[*]}. 
This follows from a discussion with Ernesto Posse.

The semantics for the {...} operator we use in Spot comes from the
cl(...) operator defined by Dax et al. (ATVA'09).  This is slightly
different from the the way the PSL spec interprets a SERE used in the
context of a temporal formula (appendix B.3.1.1.2, item 7).

cl({a;b}[*]) would match any infinite word that starts with a;b, while
in PSL {a;b}[*] would match any infinite word that alternates a and b.

Spot documents that {SERE} in a temporal formula is interpreted like
cl(SERE) however it failed to ignore the empty prefix of SERE.  So
{{a;b}[*]} would match anything, because the empty word is a prefix of
any word, and is also accepted by {a;b}[*].  Some trivial identities
and basic rewritings were also wrongly considering these empty
prefixes as well.

This patch therefore fixes the translation and syntactic
simplification rules, to really ignore these empty prefixes.

In some future version it should probably be wise to rename this {...}
operator as cl(...), and use {...} for the semantics given in appendix
B.3.1.1.2 (item 7) of the PSL specs.

* src/ltlast/unop.cc: Fix trivial identities.  We have
{[*0]} = 0 and !{[*0]} = 1.
* src/ltlvisit/simplify.cc: Fix basic rewriting rules.
{e[*]} = {e} and !{e[*]} = !{e}.
* doc/tl/tl.tex: Adjust documentation.
* doc/tl/tl.bib (dax.09.atva): New entry.
* src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
infinite word for {e[*]} just because the empty
prefix is matched by e[*].
* src/tgbatest/ltl2tgba.test: Add a test case.
* NEWS: Mention it.
* THANKS: Add Ernesto.
 2013-07-29 00:25:13 +02:00
Alexandre Duret-Lutz
4f986400f1 * src/bin/man/ltlcross.x: Typo. 2013-07-27 12:31:52 +02:00
Alexandre Duret-Lutz
027836f431 neverparse: accept more unparenthesised guards 
Also accept guards of the form (a) || !(b) or (a) && !(b).

* src/neverparse/neverclaimscan.ll: Adjust.
* src/tgbatest/neverclaimread.test: Add a test case.
 2013-07-26 12:04:45 +02:00
Alexandre Duret-Lutz
e598175fca neverparse: Remove superfluous %expect-rr in grammar. 
* src/neverparse/neverclaimparse.yy: Remove %expect-rr, that's only for
GLR parsers.
 2013-07-26 11:51:30 +02:00
Alexandre Duret-Lutz
734e203b65 ltlcross: missing newline in error message. 
* src/bin/ltlcross.cc: Add that missing new line.
* NEWS: Mention it.
 2013-07-25 18:37:04 +02:00
Alexandre Duret-Lutz
5046f6d9db * src/tgbaalgos/isweakscc.cc: Remove useless guards. 2013-07-23 10:32:15 +02:00
Alexandre Duret-Lutz
84c9f03767 neverpase: fix parsing of neverclaim produced by ltl2ba and ltl3ba 
These translator may output guards such as (a) || (b), but with the
changes in Spot 1.1.3 it would only work with ((a) || (b)).

Furthermore when ltlcross would fail to parse a neverclaim containing
such a guard, it would fail to parse all later neverclaims, because
the lexer was not properly reset.

* src/neverparse/neverclaimscan.ll: Scan (a) || (b) as a single
token.
(neverclaimyyopen): Reset the lexer.
* src/tgbatest/neverclaimread.test: Add a test for (a) || (b).
* NEWS: Update.
 2013-07-20 20:21:39 +02:00
Alexandre Duret-Lutz
365d0ead94 * src/tgbaalgos/reducerun.hh: Typos in documentation. 2013-07-20 20:18:26 +02:00
Alexandre Duret-Lutz
b26b910358 * src/bin/ltlcross.cc: Typo. 2013-07-20 20:16:51 +02:00
Alexandre Duret-Lutz
00bf8d1641 * doc/org/ioltl.org: Typos. 2013-07-09 21:08:28 +02:00
Alexandre Duret-Lutz
9bd49cfcfc * NEWS, configure.ac: Bump version to 1.1.3a. 2013-07-09 15:53:44 +02:00
Alexandre Duret-Lutz
026830d159 Release Spot 1.1.3. 
* configure.ac, doc/org/tools.org, NEWS: Set version to 1.1.3.
 2013-07-09 14:03:07 +02:00
Alexandre Duret-Lutz
a9a96ee4ff ltlcross: do not use f after it has been destroyed. 
Reported by Joachim Klein.

* src/bin/ltlcross.cc: Here.
* NEWS, THANKS: Update.
 2013-07-09 14:00:49 +02:00
Alexandre Duret-Lutz
168265bdf0 * NEWS: Summarize recent changes. 2013-07-09 13:59:04 +02:00
Alexandre Duret-Lutz
327bd2d621 Support reading the new style of neverclaim output by Spin 6.24+. 
* src/neverparse/neverclaimparse.yy, src/neverparse/neverclaimscan.ll:
Allow transitions between do..od, recognize atomic and assert.
* src/neverparse/parsedecl.hh: Pass the error_list to the lexer.
* src/tgbatest/neverclaimread.test: Add a test case.
 2013-07-09 06:25:44 +02:00
Alexandre Duret-Lutz
ff102d3d94 Fix non-standard use of the date command. 
Reported by Étienne Renault.

* bench/spin13/run.sh: Here.
 2013-06-25 10:36:55 +02:00
Alexandre Duret-Lutz
fc5d4e1a41 Fix "BDD Error" in scc_filter(). 
If all the acceptance set of an SCC but the first one were useless, the
scc_filter() algorithm could abort with a BDD error because of a bug in
the logic.

* src/tgbaalgos/sccfilter.cc (scc_filter): Fix.
* src/tgbatest/sccsimpl.test: Add a test case supplied by Étienne
Renault.
 2013-06-19 21:21:16 +02:00
Alexandre Duret-Lutz
372a086cb7 Improve ltlfilt.org 
* doc/org/ltlfilt.org: Mention that the --stutter-invariant check
use automata.  Fix a typo.
 2013-06-09 18:55:57 +02:00
Alexandre Duret-Lutz
644b5f0152 * configure.ac, NEWS: Bump version to 1.1.2a. 2013-06-09 18:44:42 +02:00
Alexandre Duret-Lutz
424f04ca11 Release Spot 1.1.2. 
* configure.ac, NEWS, doc/org/tools.org: Bump version to 1.1.2.
 2013-06-09 18:05:20 +02:00
Alexandre Duret-Lutz
ecc8b8c79c * NEWS: Summarize recent changes. 2013-06-09 16:01:34 +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
1cd9b204ed Fix verbatim blocks of Doxygen comments. 
* src/ltlast/formula.hh, src/ltlvisit/contain.hh,
src/ltlvisit/randomltl.hh, src/ltlvisit/reduce.hh,
src/ltlvisit/remove_x.hh, src/ltlvisit/simplify.hh, src/ltlvisit/snf.hh,
src/misc/minato.hh, src/misc/optionmap.hh,
src/saba/sabacomplementtgba.hh, src/taalgos/emptinessta.hh,
src/taalgos/minimize.hh, src/taalgos/tgba2ta.hh,
src/tgba/tgbakvcomplement.hh, src/tgbaalgos/cycles.hh,
src/tgbaalgos/eltl2tgba_lacim.hh, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gv04.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/randomgraph.hh, src/tgbaalgos/se05.hh,
src/tgbaalgos/simulation.hh, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.hh: Surround verbatim blocks with /** ... */
instead of using /// on each line.  Otherwise Doxygen will output the
leading "///" tokens -- apparently this is a feature.
* src/sanity/style.test: Strip multi-line comments before checking
code style.
 2013-06-09 15:55:03 +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
0ec3f7843a simulation: fix compilation with g++ < 4.5. 
* src/tgbaalgos/simulation.cc: Pass template arguments to base-class
initializer to fix compilation with g++ < 4.5.  Reported by Sonali
Dutta.
 2013-05-22 20:06:26 +02:00
Alexandre Duret-Lutz
4c1a9fdb10 More files to ignore. 2013-05-17 11:11:19 +02:00
Alexandre Duret-Lutz
330b6ddac0 * src/bin/ltlcross.cc (statistics): Initialize all members. 2013-05-17 10:58:44 +02:00
Alexandre Duret-Lutz
57d25f0e21 * NEWS, configure.ac: Bump version to 1.1.1a. 2013-05-13 20:04:04 +02:00
Alexandre Duret-Lutz
27a18a0410 Release Spot 1.1.1 
* NEWS, configure.ac, doc/org/tools.org: Bump version.
 2013-05-13 16:20:29 +02:00
Alexandre Duret-Lutz
5a6b50acbb org: Augment the load-path. 
* doc/org/init.el.in: Add emacs-goodies-el to the load-path, so that
org-mode has a better chance to find htmlize.
 2013-05-13 16:12:32 +02:00
Alexandre Duret-Lutz
b457e78fb0 * doc/org/ltlfilt.org: Add an example with --stutter-invariant. 2013-05-13 16:10:09 +02:00
Alexandre Duret-Lutz
54b25b8c8e ltlcross: more documentation 
* doc/org/ltlcross.org: Describe statistics, and mention --products=N.
 2013-05-13 16:09:50 +02:00
Alexandre Duret-Lutz
9b82d7557c ltlcross: add a --products=N option 
* src/bin/ltlcross.cc: Implement the new option.  Average the product
statistics on all products.
* src/tgbatest/basimul.test, src/tgbatest/ltlcross.test,
src/tgbatest/ltlcross2.test, bench/ltl2tgba/tools: Use the new option.
* NEWS: Mention it.
 2013-05-12 21:22:46 +02:00
Alexandre Duret-Lutz
b4670f85f1 bdddict: add an unregister_all_typed_variables() method 
* src/tgba/bdddict.cc, src/tgba/bdddict.hh
(unregister_all_typed_variables): New method.
* src/tgbaalgos/degen.cc (degeneralize): Use it.
* NEWS: Mention it.
 2013-05-12 21:05:05 +02:00