options -C and -CR for that.
* src/tgbatest/ltl2tgba.cc: Add option -C and -CR to control
whether we want the accepting run to be printed or replayed.
* src/tgbatest/dfs.test, src/tgbatest/eltl2tgba.test,
src/tgbatest/emptchk.test, src/tgbatest/emptchke.test,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlcounter.test: Use -CR.
* src/ltlast/binop.cc, src/ltlast/binop.cc: Add support for
these new operators.
* src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse them.
* src/ltltest/reduccmp.test: Add new tests for W and M.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/contain.cc,
src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/reduce.cc, src/ltlvisite/simpfg.cc,
src/ltlvisit/simpfg.hh, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/tgba/formula2bdd.cc,
src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc:
Add support for W and M.
* src/tgbatest/ltl2neverclaim.test: Test never claim output
using LBTT, this is more thorough. Also we cannot use -N
any more in the spotlbtt.test.
* src/tgbatests/ltl2tgba.cc: Define M and W for ELTL.
* src/tgbatest/ltl2neverclaim.test: Test W and M, and use
-DS instead of -N, because lbtt-translate does not want
to translate these operators for tools that masquerade as Spin.
by default in scc_filter().
Doing so helps the degeneralization algorithm, because it will
have more opportunity to be in an accepting level when it reaches
the accepting SCCs.
* src/tgbaalgos/sccfilter.cc (filter_iter::filter_iter): Take a
remove_all_useless argument.
(filter_iter::process_link): Use the flag to decide whether to
filter acceptance conditions going to accepting SCCs.
(scc_filter): Take a remove_all_useless argument and pass it to
filter_iter.
* src/tgbaalgos/sccfilter.hh (filter_iter): Add the new argument
and document the function.
* src/tgbatest/tgbatests/ltl2tgba.cc (main): Add option use -R3
for remove_all_useless=false and add -R3f for
remove_all_useless=true.
* src/tgbatest/ltl2tgba.test: Show one case where -R3f makes
the degeneralization worse than -R3.
* src/tgbatest/ltl2tgba.cc (main): Call scc_filter() before the
degeneralization, because it might remove useless acceptance
conditions. I realized this while looking at experiments from
Rüdiger Ehlers.
* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh:
Remove the containment option.
* src/tgbafromfile.cc, src/tgbafromfile.hh: Remove the
containment_ member.
* src/tgbatest/ltl2tgba.cc (syntax): Remove -c option for
FM algorithm, use it exclusively for TAA.
* src/tgbatest/ltl2tgba.cc (syntax, main): Introduce -le to select
this algorithm and -lo to add the default LTL operators. This
replace the undocumented hack to add LTL operators when the
formula with read for command-line, or the automaton was output
for LBTT.
* src/tgbatest/eltl2tgba.test, src/tgbatest/spotlbtt.test: Update
call syntax.
* NEWS: Mention -le, -lo, and -taa.
* src/tgbatest/ltl2tgba.cc (syntax): Move -R3b with the other
LaCIM options.
(main): Speak of "symbolic SCC pruning" instead of "deleting
unaccepting SCC", and do that right after the translation, before
degeneralization. Also error out when -R3b is used on non
symbolic automata.
* src/tgbatest/eltl2tgba.cc: Remove.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: New option: -xltl to translate an
extended LTL instead of an LTL, a feature previously offered by
eltl2tgba.cc. Also: -R3b to use delete_unaccepting_scc.
* src/tgbatest/spotlbtt.test: Adjust.
* src/misc/timer.hh (time_info::running): New attribute.
(time_info::start, time_info::stop): Update and check
time_info::running.
* src/misc/timer.cc (timer_map::print): Mark running timers with
a "+" in the output.
* src/tgbatest/ltl2tgba.cc (main): Rename the name of the timers
for SCC and simulation reduction, and actually stop the SCC timer.
prune_scc() leaked memory and failed to remove chains of useless SCCs.
* src/tgbaalgos/reductgba_sim.cc (reduc_tgba_sim): Call
scc_filter() instead of prune_scc(), and do it before running
any simulation-based reduction.
* src/tgbaalgos/reductgba_sim.hh (reduc_tgba_sim): Return a const
tgba*.
* src/tgbatest/ltl2tgba.cc: Call scc_filter() instead of
prune_scc().
* src/tgbatest/scc.test: Add two more tests that failed with
prune_scc().
* src/tgbatest/ltl2tgba.cc (syntax): Reorganize the help text, so
that we can find options without resorting to grep... Also
cleanup the program name if it is a libtool wrapper.
translation. It still is the default translation.
(opt_fm, opt_taa): Replace these two variables by ...
(translation): ... this enum. And use a switch to call the
correct translation.
much time when the formula is large, and it is useless when the
purpose is model-checking with Spin.
* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Add the
comments option.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs,
never_claim_reachable): Honor the comment option.
* src/tgba/tests/ltl2tgba.cc (-N): Do not comment states.
(-NN) New option to output a commented never claim.
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.
* src/ltlast/automatop.hh, src/ltlast/automatop.cc: Add missing
instance_count() functions.
* src/tgbatests/eltl2tgba.cc: Add missing instance_count()
assertions at the end.
* src/tgbatests/ltl2tgba.cc: Also call automatop::instance_count(),
even if automatop are not used in ltl2tgba yet. This way we won't
forget once eltl2tgba and ltl2tgba are merged.
* 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.
TGBA which uses TAA as an intermediate representation. This is a
basic version, optimizations and enhancements will come later.
* src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2taa.hh: The algortihm.
* src/tgbaalgos/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba: New option: -taa, which uses this new
translation algorithm.
* src/tgbatest/spotlbtt.test: Add ltl2tgba -taa.
* 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.
* src/tgbaalgos/scc.hh (scc_map::scc_of_state,
scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
New functions.
(scc_map::scc::conds): New attribute.
(dump_scc_dot): Take an optional VERBOSE argument.
* src/tgbaalgos/scc.cc (scc_map::scc_of_state,
scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of):
Implement these new functions.
(dump_scc_dot): Display number of states, conditions and
acceptance conditions, with VERBOSE is set.
(build_map): Fill the new scc_map::scc::cond field.
* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.hh:
Add Reduce_Containment_Checks and Reduce_Containment_Checks_Stronger
flags, and call reduce_tau03.
* src/ltlvisit/contain.hh (reduce_tau03): Make "stronger" the
default.
* src/ltlvisit/contain.cc: Style.
* src/ltltest/reduc.cc: Simplify using the reduce() interface
instead of reduce_tau03.
* src/tgbatest/ltl2tgba.cc: Likewise. Add -fr5, -fr6, and -fr7
options.
* src/tgbatest/spotlbtt.test: Remove cases using "-c", since its
current implementation is not always correct (and apparently
reduces less than -fr7).
New function, performing LTL reduction a la tauriainen.03.a83.
* src/ltltest/equals.cc, src/ltltest/reduc.cc: Add support for
the new reduction.
* src/ltltest/reduc.test: Cut the test in half, and additionally
test the new reduction.
* src/ltltest/reduccmp.test: Run on the new reduction.
* src/ltltest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: Add new options to apply the reduction.
* src/tgbatest/spotlbtt.test: Use them.
(ltl_to_tgba_fm): Add a new option "containment_checks" to enable
some language containment checks (via emptiness checks) during the
translation. This first attempt currently only use containment
checks to merge states bisimulating each other.
* src/tgbatest/ltl2tgba.cc: Bind this to option "-c".
* src/tgbatest/spotlbtt.test: Check it.
instead of one : one for the atomic propositions, and one
for the acceptance conditions. This way it's easy for
the tools in iface/gspn/ to require some atomic proposition
to be declared and allow any acceptance conditions (there is nothing
to adjust in this files because of the default value of the argument).
* src/tgbaparse/tgbaparse.yy: Adjust.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/readsave.cc,
src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc: Adjust calls.
option_map::set): Handle default values.
(anonymous::to_int): Do not print anything.
* src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/ce.cc, src/tgbaalgos/ce.hh: Take an option_map in
the constructor.
* src/tgbaalgos/gtec.cc, src/tgbaalgos/gtec.hh: Likewise. Handle
the "poprem", "group", and "shy" options via the option_map.
Supply a couvreur99() wrapper to the shy/non-shy variant.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
iface/gspn/ssp.cc: Adjust.
