* 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.
(to_string_visitor::visitor(const atomic_prop*)): Use is_bare_word
to better check which atomic proposition need to be quoted.
* src/ltlparse/ltlscan.ll: Do not allow identifiers starting with F_
or G_.
* src/ltltest/equals.test, src/ltltest/tostring.test: More tests.
extracted from ...
* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
again.
* src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call
simplify_f_g() in addition to unabbreviate_logic().
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
Add simpfg.cc and simpfg.hh.
* 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.
with scc and delayed simulation.
* src/tgbatest/ltl2tgba.cc: Adjust parameters.
* src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test.
* src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs.
* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
Remove some useless comments.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC.
* src/ltlvisit/reducform.cc: Correct some bug for multop.
* src/ltltest/reduccmp.test: More Test.
* src/ltltest/reduc.cc: Thinko
* src/ltltest/equals.cc: Reduction compare
automata.
* src/tgbatest/spotlbtt.test, src/tgbatest/Makefile.am: Add some
test for reduction of automata.
* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim.hh: Compute some simulation relation
to reduce a tgba.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: A implementation
of tgba for the reduction.
* src/tgbaalgos/Makefile.am, src/tgba/Makefile.am:
Add the reduction of automata.
* src/ltlvisit/syntimpl.cc, src/ltlvisit/basereduc.cc:
Lot of mistake are corrected.
* src/ltlvisit/syntimpl.hh, src/ltlvisit/reducform.cc,
src/ltlvisit/reducform.hh, src/ltltest/reduc.cc: Adjust.
* src/ltltest/equals.cc, src/ltltest/reduccmp.test,
src/ltltest/Makefile.am: Add a test for reduction.
class gspn_environment, and move it to ...
* src/ltlenv/declenv.cc, src/ltlenv/declenv.hh: .. this new file
as class declarative_environment.
* src/ltlenv/Makefile.am (ltlenv_HEADERS): Add declenv.hh.
(libltlenv_la_SOURCES): Add declenv.cc.
* iface/gspn/dottygspn.cc, iface/gspn/dottyssp.cc,
iface/gspn/gspn.cc, iface/gspn/gspn.hh, iface/gspn/ltlgspn.cc,
iface/gspn/ssp.cc, iface/gspn/ssp.hh: Adjust references
to declarative_environment.
dynamic_cast instead of node_type_form_visitor, this is usually
smaller.
* src/ltlvisit/reducform.hh,
src/ltlvisit/forminf.cc (node_type_form_visitor): Delete.
* src/sanity/style.test: Two more checks.
(reduce_options): ... this, and use it as a bit field so
option can be combined easily.
(reduce): Adjust argument.
(reduce_form): Remove, not needed anymore.
* src/ltlvisit/reducform.cc, src/ltltest/reduc.cc,
src/tgbatest/ltl2tgba.cc: Adjust.
the `inclusion' flag.
* iface/gspn/ssp.cc (gspn_ssp_interface::gspn_ssp_interface): Call
inclusion_version when inclusion is set.
* iface/gspn/ltlgspn.cc (main) [SSP]: Turn on inclusion for -e3,
-e4, and -e5.
and dead_prop from the dead argument passed to the constructor.
(tgba_succ_iterator_gspn): Stutter on dead transitions.
(tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_.
(gspn_interface::gspn_interface): Hand dead to tgba_gspn.
* iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a
dead argument.
* iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the
dead property.
* iface/gspn/udcseltl.test: Try option -d.
