If the input is a tgba_explicit_formula we can output a
tgba_explicit_formula too, and we want to do that because it is
more space efficient.
* src/tgba/tgbaexplicit.hh (get_label): New method.
* src/tgbaalgos/sccfilter.cc (create_transition): New function,
to handle tgba_explicit_formula and tgba_explicit_string output
differently.
(filter_iter): Template it on the output tgba type, and adjust
to call create_transition.
(scc_filter): Use filter_iter<tgba_explicit_formula> or
filter_iter<tgba_explicit_string> depending on the input tgba
type.
A useless acceptance conditions is one that is always implied by
another.
* src/misc/bddop.hh, src/misc/bddop.cc
(compute_neg_acceptance_conditions): New function.
* src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc
(set_acceptance_conditions): New function.
* src/tgbaalgos/scc.cc (build_map, build_scc_stats, dump_scc_dot):
Keep track of useful acceptance conditions.
(useful_acc_of): New function.
* src/tgbaalgos/scc.hh (scc_stats, scc_map::scc::useful_scc): New
attributes.
* src/tgbaalgos/sccfilter.cc (filter_iter): Adjust to filter
useless acceptance conditions.
(scc_filter): Compute useful acceptance conditions and pass them
to filter_iter.
* src/tgbaalgos/ltl2taa.cc: Do NOT use the same bdd_dict for both
the translation and the language containment checker.
* src/tgbatest/spotlbtt.test: Update TAA related tests.
tgba_explicit instances labelled by other objects than strings.
* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh:
Split tgba_explicit in two levels: tgba_explicit with unlabelled
states, and tgba_explicit_labelled templated by the type of
the label. Define tgba_explicit_string (with the interface
of the former tgba_explicit class) and tgba_explicit_formula
for future use in ltl2tgba.cc.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgbaalgos/cutscc.cc, src/tgbaalgos/dupexp.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/powerset.cc, src/tgbaalgos/randomgraph.cc,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy,
src/tgbatest/explicit.cc, src/tgbatest/ltl2tgba.cc: Adjust to
use tgba_explicit_string when appropriate.
constructor. It does the same thing as the default copy
constructor, and g++ 4.2.3 complained that the copy constructor
of spot::state was not called. Reported by Denis Poitrenaud.
* src/tgba/taa.cc, src/tgba/taa.hh: taa_succ_iterator is not
on-the-fly anymore allowing some redundant transitions to be
removed. Also a new function to output a TAA.
* src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: Add the
refined rules from Tauriainen.
* src/tgbatest/ltl2tgba.cc: Use -c to activate refined rules in
ltl_to_taa.
* src/tgbatest/spotlbtt.test: More tests.
* misc/Makefile.am, misc/bbop.cc, misc/bddop.hh: Factorize some
code on BDDs to compute all_acceptance_conditions from
neg_acceptance_condition.
* src/tgba/Makefile.am, src/tgbatest/Makefile.am: Adjust.
* src/tgba/taa.cc, src/tgba/taa.hh: The TAA class.
* src/tgba/tgbaexplicit.hh: Use the factorized code in bddop.hh.
* src/tgbatest/taa.cc, src/tgbatest/taa.test: Some test cases.
the original automaton has no acceptance condition.
* src/tgba/tgbasgba.cc, src/tgba/tgbasgba.hh: New option:
when the original automaton has no accepting condition, it
explicitly considers that every state is accepting.
shared_ptr on states...
* src/tgba/state.hh: ... here.
* src/tgbatest/complementation.test: Do not apply some tests on
the new algorithm because it takes to much time to run.
* src/tgba/tgbacomplement.cc, src/tgba/tgbacomplement.hh: The
construction.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/complementation.cc: Add options to support this
construction in addition to Safra construction.
* src/tgba/Makefile.am: Adjust.
* src/tgbatest/complementation.test: Adjust to test also this
complementation.
* src/tgba/tgbasgba.hh, src/tgba/tgbasgba.hh: Here.
* src/tgbatest/ltl2tgba.cc: New option `-lS' for state-labeled
automata.
* src/tgba/Makefile.am: Adjust and sort files in tgba_HEADERS
and libtgba_la_SOURCES.
size of TGBAs represented as BDDs by deleting unaccepting SCCs.
* src/eltlparse/eltlparse.yy: Remove a warning.
* src/tgba/tgbabddconcrete.cc, src/tgba/tgbabddconcrete.hh,
src/tgba/tgbabddcoredata.cc, src/tgba/tgbabddcoredata.hh: Add a
new function delete_unaccepting_scc in both classes.
* src/tgbatest/eltl2tgba.cc, src/tgbatest/spotlbtt.test: Use this
new function in LaCIM for ELTL and bench it.
* src/tgbatest/defs.in: Fix it.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/defs.in: Add LaCIM for
ELTL in benchs.
Add an algorithm to split an automaton in several automata.
* bench/scc-stats: New directory. Contains input files and test
program for computing statistics.
* bench/split-product: New directory. Contains test program for
synchronised product on splitted automata.
* bench/split-product/models: New directory. Contains Promela
files and LTL formulae that should be verified by the models.
* src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh:
New files. Small class to avoid long initializations with numerous
constants when translating to TGBA many LTL formulae from a
given file.
* src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh:
New file. From a single automaton, create, at most,
X sub automata.
* src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh:
Adjust to compute self-loops count.
into a TGBA instead of a TBA.
* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc:
Adjust the transformation from Streett to Büchi to support
generalized acceptance conditions.
* src/tgbatest/complementation.cc: Improve output messages.
* src/tgbatest/complementation.test: New tests.
* src/tgba/tgbacomplement.hh, src/tgba/tgbacomplement.cc: New
files. The complementation algorithm.
* src/tgba/Makefile.am: Adjust.
* src/tgbatest/complementation.test,
src/tgbatest/complementation.cc: New files. Test suite for the
complementation algorithm.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbaalgos/Makefile.am: Reformat the header using 80
columns.
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.
a new tgba_scc class.
* src/tgba/futurecondcol.cc, src/tgba/futurecondcol.hh: Move
all delegation functions and scc_map into ...
* src/tgba/tgbascc.cc, src/tgba/tgbascc.hh: ... these new files.
for ELTL. This is a new version of the work started in 2008 with
LTL and ELTL formulae now sharing the same class hierarchy.
* configure.ac: Adjust for src/eltlparse/ and src/eltltest/
directories, and call AX_BOOST_BASE.
* m4/boost.m4: New file defining AX_BOOST_BASE([MINIMUM-VERSION]).
* src/Makefile.am: Add eltlparse and eltltest.
* src/eltlparse/: New directory. Contains the ELTL parser.
* src/eltltest/: New directory. Contains tests related to
ELTL (parser and AST).
* src/ltlast/Makefile.am: Adjust for ELTL AST files.
* src/ltlast/automatop.cc, src/ltlast/automatop.hh: New files.
Represent automaton operators nodes used in ELTL ASTs.
* src/ltlast/nfa.cc, src/ltlast/nfa.hh: New files. Represent
simple NFAs used internally by automatop nodes.
* src/ltlast/allnode.hh, src/ltlast/predecl.hh,
src/ltlast/visitor.hh: Adjust for automatop.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
src/ltlvisit/dotty.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc: Because LTL and ELTL formulae share the
same class hierarchy, LTL visitors need to handle automatop nodes
to compile. When it's meaningful the visitor applies on automatop
nodes or simply assert(0) otherwise.
* src/tgba/tgbabddconcretefactory.cc (create_anonymous_state),
src/tgba/tgbabddconcretefactory.hh (create_anonymous_state): New
function used by the LaCIM translation algorithm for ELTL.
* src/tgbaalgos/Makefile.am: Adjust for eltl2tgba_lacim* files.
* src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/eltl2tgba_lacim.hh: New files. Implementation of
the LaCIM translation algorithm for ELTL.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Handle automatop nodes in the translation by an assert(0).
* src/tgbatest/Makefile.am: Adjust for eltl2tgba.* files.
* src/src/tgbatest/eltl2tgba.cc, src/tgbatest/eltl2tgba.test: New
files
* src/ltlenv/environment.hh, src/ltlvisit/basicreduce.cc: Remove
useless FIXMEs.
* src/ltlvisit/reduce.cc (reduce_visitor::visit(binop)): Compute
syntactic implications only when needed.
* src/tgbaalgos/reductgba_sim_del.cc
(build_recurse_successor_spoiler): Remplace the FIXME by an assert.
* src/tgba/tgbareduc.cc: Reword some comments, discard old
commented code.
New function.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh: Use it to
distinguish acceptance conditions that are identical in both
operands.
* src/tgbatest/explpro4.test: New file.
* src/tgbatest/explpro2.test, src/tgbatest/Makefile.am: Adjust.
Rename as ...
(free_anonymous_list_of): ... this, and correct their update on
release. Also correct yesterday's the correction (ahem!).
(dump): Improve verbosity.
* src/misc/freelist.cc (free_list::remove, free_list::insert): Fix
longstanding thinkos.
(free_list::free_count): New function.
