GitLab

(couvreur99_check_shy::couvreur99_check_shy): Add the group option,
and redefine todo as a list so it can be iterated over.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Introduce
couvreur99_shy- (for group=false) in addition to couvreur99_shy
(for group=true).
* iface/gspn/ssp.cc (couvreur99_check_ssp_shy_semi,
couvreur99_check_ssp_shy): Use group=true;

(set_init_state): Return a pointer to the initial state.

(tgba_run_to_tgba): New function.

(minimize_run): Rename as ...
* src/tgbaalgos/reducerun.cc, src/tgbaalgos/reducerun.hh:
(reduce_run): ... this.
* src/tgbaalgos/Makefile.am, src/tgbatest/ltl2tgba.cc,
src/tgbatest/randtgba.cc: Adjust all references.

files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them/
* src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add option -m.
* src/tgbatest/emptchkr.test: Use -m.

based on Thomas Martinez's src/tgbaalgos/tarjan_on_fly.cc and
src/tgbaalgos/tarjan_on_fly.hh former implementation.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
tgbaalgos_HEADERS): Add them.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Bind the
new algorithm.
* src/tgbatest/emptchk.test: Test it.

src/tgbaalgos/weight.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc,
src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics
capability.
* src/tgbatest/randtgba.cc: Print these statistics.
* src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance
condition.
* src/tgbatest/emptchk.test: Test tau03opt search.

* src/tgbaalgos/tau03.cc: Suppress optimisations, the algorithm is now
the original one.
* src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03opt.cc: New files
implementing most of all the optimisations of tau03.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Make them public.
* src/tgbatest/tba_samples_from_spin.test: Test them.

* src/tgbaalgos/magic.cc: Fix a comment.
* src/tgbaalgos/se05.hh: New file.
* src/tgbaalgos/se05.cc: Fix a comment.
* src/tgbaalgos/tau03.hh: New file.
* src/tgbaalgos/tau03.cc: New file.
* src/tgbaalgos/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc: Add tau03 new emptiness check.
* src/tgbatest/randtgba.cc: Add tau03 new emptiness check.
* src/tgbatest/emptchkr: Fix a comment.
* src/tgbatest/tba_samples_from_spin/explicit1_1.tba,
src/tgbatest/tba_samples_from_spin/explicit1_2.tba,
src/tgbatest/tba_samples_from_spin/explicit1_3.tba,
src/tgbatest/tba_samples_from_spin/explicit1_4.tba,
src/tgbatest/tba_samples_from_spin/explicit1_5.tba,
src/tgbatest/tba_samples_from_spin/explicit1_6.tba,
src/tgbatest/tba_samples_from_spin/explicit1_7.tba,
src/tgbatest/tba_samples_from_spin/explicit1_8.tba,
src/tgbatest/tba_samples_from_spin/explicit1_9.tba,
src/tgbatest/tba_samples_from_spin/explicit2_1.tba,
src/tgbatest/tba_samples_from_spin/explicit2_2.tba,
src/tgbatest/tba_samples_from_spin/explicit2_3.tba,
src/tgbatest/tba_samples_from_spin/explicit2_4.tba,
src/tgbatest/tba_samples_from_spin/explicit2_5.tba,
src/tgbatest/tba_samples_from_spin/explicit2_6.tba,
src/tgbatest/tba_samples_from_spin/explicit2_7.tba,
src/tgbatest/tba_samples_from_spin/explicit2_8.tba,
src/tgbatest/tba_samples_from_spin/explicit2_9.tba: New files
* src/tgbatest/tba_samples_from_spin.test : New test.
* src/tgbatest/Makefile.am: Add it.

functionality of the old tgba_tba_proxy.
* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator,
tgba_tba_proxy): Rewrite to produce TBA with at most N copies of
each state, skipping the `bddtrue' stage now used only in
tgba_sba_proxy.  Doing so removes approximately 6% of states in
the degeneralized tests of spotlbtt.test.
(tgba_sba_proxy): Implement it.
* src/tgbaalgos/neverclaim.hh, src/tgbaalgos/neverclaim.cc: Adjust
to take a tgba_sba_proxy.
* src/tgbatest/ltl2tgba.cc: Add option -DS and adjust call to
never_claim_reachable().

check, degeneralize the automaton only if it has too much
acceptance conditions.  This makes it easier to reproduce runs
of randtgba.
* src/tgbatest/emptchk.test: Adjust.

* src/tgbaalgos/se05.cc: Add a bit state hashing version.
* src/tgbaalgos/magic.hh: Make them public.
* src/tgbatest/ltl2tgba.cc: Add the two new emptiness checks.
* src/tgbatest/emptchk.test: Incorporate tests of src/tgbatest/dfs.test.
* src/tgbatest/dfs.test: Introduce new characteristic explicit tests.

src/tgbaalgos/replayrun.cc (replay_tgba_run): Take a `debug'
option to decide whether the output should look like that of
print_tgba_run() or a complete debug trace.
* src/tgbatest/ltl2tgba.cc (main): Call replay_tgba_run() with
debug=true.

some help strings.

prepare it to a bit state hashing version.
* src/tgbaalgos/magic.hh: adapt to the new interface of
magic_search and se05_search.
* src/tgbaalgos/se05.cc: new file.
* src/tgbaalgos/Makefile.am: Add it.
* src/tgbatest/ltl2tgba.cc: Add new emptiness check.
* src/tgbatest/emptchk.test: more tests.
* src/tgbatest/dfs.test: new file.
* src/tgbatest/Makefile.am: Add it.

does not leak on errors.
* src/tgbatest/ltl2tgba.cc: Free the automata if it could not be
fully parsed.

src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: New files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbaalgos/dotty.hh (dotty_reachable): Take a dotty_decorator
as third parameter.
* src/tgbaalgos/dotty.cc (dotty_bfs::process_state,
dotty_bfs::process_link): Use the decorator.
* src/tgbatest/ltl2tgba.cc: Graph the accepting run if the -g option
is given.
* src/tgbatest/emptchk.test: Exercize -g.

src/tgbaalgos/emptiness.hh (print_tgba_run): Take the tgba*
argument before the tgba_run* argument (for consistency with
replay_tgba_run).
* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust
calls to print_tgba_run().

src/tgbaalgos/gtec/gtec.hh (couvreur99_check::print_stats): New.
* src/tgbatest/ltl2tgba.cc: Print emptiness-check statistics.

as `if (x) delete x;'.
* iface/gspn/gspn.cc, iface/gspn/ssp.cc, src/ltlvisit/basicreduce.cc,
src/tgba/tgba.cc, src/tgba/tgbaproduct.cc, src/tgbaalgos/magic.cc,
src/tgbatest/ltl2tgba.cc: Remove such constructs.

-eALGO and -EALGO to ease the addition of new algorithms.
* src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust.

* src/sanity/80columns.test: Use expand to untabify, the previous
recipe was incomplete.

couvreur99_check_result::complete_cycle,
couvreur99_check_result::accepting_path): Record conditions and
acceptance conditions in the accepting run.  Simplify the
todo BFS stack for accepting_run and complete_cycle.
* src/tgbatest/ltl2tgba.cc (main): Do use replay_tgba_run
now everything works.
* src/tgbaalgos/replayrun.cc (replay_tgba_run): Be more verbose
when an outgoing transition is not found.

Cannot test them because the run returned by the emptiness checks
are currently incomplete (they lack the acceptance conditions, and
sometimes even the labels in the prefix).
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run
when the emptiness checks are fixed.

algorithms to conform to it, uniformly.  This will unfortunately
break third-party code that were using these algorithms.
* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
* src/tgbaalgos/Makefile.am: New files.
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
conform to the new emptiness-check interface.
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
Likewise.  The classes have been renamed are as following
  emptiness_check -> couvreur99_check
  emptiness_check_shy -> couvreur99_check_shy
  counter_example -> couvreur99_check_result
* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
iface/gspn/ssp.cc: Adjust to renaming and new interface.

2004-08-23.  Some of these will need to be reintegrated more
slowly and cleanly.

* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am,
src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert.
* src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh,
src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh,
src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh,
src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh:
Delete.

and is wrong into two ways: the search stack is generally not a
path, and does not run until the end of the STL container.
Remove it.
* src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh
(tarjan_on_fly): Do not inherit from the emptiness_search class,
because the check method will no longer return a counter example.
(tarjan_on_fly::check): Return only a boolean.
(tarjan_on_fly::build_counter): Delete.
* src/tgbatest/ltl2tgba.cc: Adjust.

matter, for consistency.
* src/tgbaalgos/tarjan_on_fly.cc, iface/gspn/ssp.cc,
src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/minimalce.cc, src/tgba/tgbareduc.cc: Adjust.

* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs.
* src/tgbatest/ltl2tgba.cc (syntax, main): New -U option.

src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename
emptyness_search to emptiness_search.

src/tgbatest/reductgba.cc,
src/tgbatest/ltl2tgba.cc:
Add option for reduction of TGBA.

* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc,
src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
Remove some bugs.

src/tgbaalgos/gtec/ce.cc:
Modification of construction of counter example.

* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim_del.cc,
src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
Modification for delayed simulation.


* src/tgbaalgos/gtec/ce.hh,
* src/tgbatest/ltl2tgba.cc,

src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh,
src/tgbaalgos/minimalce.cc,
src/tgbaalgos/colordfs.hh,
src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check.

src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
object in minimalce.hh.

src/tgbatest/ltl2tgba.cc,
src/tgbatest/emptchk.test,
src/tgbaalgos/Makefile.am: Add files for emptyness-check.


* src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata.
* src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition
for scc reduce.

assert() is disabled.

* 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".

src/tgbaalgos/reductgba_sim.cc,	src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim_del.cc: Remove some comments.

* src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ...
* src/tgbatest/spotlbtt.test: More test (delayed simulation)

* src/tgbatest/reductgba.test: More Test.

* src/tgbatest/ltl2tgba.cc: Adjust ...
* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim.cc: try to optimize.

* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Scc reduction
and we remove some acceptance condition in scc which are not accepting.
* src/ltlvisit/syntimpl.cc : Some case wasn't detect.
* src/ltlvisit/basicreduce.cc: Case FGa || FGb = F(Ga | Gb) added.
* src/ltltest/syntimpl.test: More Test.
* src/ltltest/syntimpl.cc: Put the formula in negative normal form.

the simulations.

* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match
the function name.
* ltltest/equals.cc, ltltest/reduc.cc, ltlvisit/Makefile.am,
tgbatest/ltl2tgba.cc, tgbatest/reductgba.cc: Adjust filenames.

src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
bug in delayed simulation.

* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test,
src/tgba/tgbareduc.cc: bug in scc reduction.