Commit graph

17 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
98604c754f * src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ...
* 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.
2004-06-22 22:54:35 +00:00
Alexandre Duret-Lutz
47e9ac108f * src/ltlvisit/basicreduce.hh: New file, extracted from ...
* src/ltlvisit/reducform.hh: ... here.
* src/ltlvisit/basereduc.cc: Rename as ...
* src/ltlvisit/basicreduce.cc: ... this, to match the function name.
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
Adjust filenames.
* src/ltlvisit/reducform.cc: Adjust includes.
2004-06-22 22:27:53 +00:00
martinez
2f1a67d927 * src/ltlvisit/reducform.cc, src/tgba/tgbareduc.cc,
src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh
src/tgbaalgos/reductgba_sim_del.cc, src/tgbatest/reduccmp.test,
src/tgbatest/reductgba.cc: 80 columns and style.
2004-06-22 17:24:46 +00:00
martinez
c769f74750 * src/tgbatest/spotlbtt.test: We don't check the post-reduction
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
2004-06-17 16:27:36 +00:00
martinez
8d3606ff07 * src/tgbatest/ltl2tgba.cc: Add some option for the reduction of
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.
2004-06-15 16:24:02 +00:00
Alexandre Duret-Lutz
8e324fa2a2 * HACKING, src/sanity/style.test: NULL is not portable, prohibit it.
* iface/gspn/ssp.cc, src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
src/ltlvisit/syntimpl.cc: Use 0 instead of NULL.
2004-06-02 15:16:47 +00:00
Alexandre Duret-Lutz
6e3fd873ba * src/ltltest/inf.cc, src/ltltest/inf.test: Rename as ...
* src/ltltest/syntimpl.cc, src/ltltest/syntimpl.test: ... these.
* src/ltltest/Makefile.am: Adjust.
* src/ltlvisit/forminf.cc: Rename as...
* src/ltlvisit/syntimpl.cc: ... this.
* src/ltlvisit/syntimpl.hh: New file with definitions extracted
from ...
* src/ltlvisit/reducform.hh: ... this one.
* src/ltlvisit/Makefile.am, src/ltlvisit/reducform.cc: Adjust.
2004-06-01 20:43:00 +00:00
Alexandre Duret-Lutz
121a55c48f * src/ltlvisit/forminf.cc (form_eventual_universal_visitor,
inf_form_right_recurse_visitor, inf_form_left_recurse_visitor): Rename
as ...
(eventual_universal_visitor, inf_right_recurse_visitor,
inf_left_recurse_visitor): ... these.
(is_GF, is_FG): Move ...
* src/ltlvisit/basereduc.cc (is_GF, is_FG): ... here, since they
are only used here.
(basic_reduce_form, basic_reduce_form_visitor): Rename as ...
(basic_reduce, basic_reduce_visitor): ... these.
* src/ltlvisit/reducform.cc (reduce_form_visitor): Rename as ...
(reduce_visitor): ... this.
* src/ltltest/inf.cc: Adjust calls.
* src/sanity/style.test: Improve missing-space after coma detection.
2004-05-30 12:33:35 +00:00
Alexandre Duret-Lutz
cdbb199c4d * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc: Use
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.
2004-05-26 12:48:22 +00:00
Alexandre Duret-Lutz
8f82f1d5f3 * src/ltlvisit/reducform.hh (option): Rename as ...
(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.
2004-05-25 12:46:56 +00:00
Alexandre Duret-Lutz
3426ece95c * src/ltlvisit/basereduc.cc, src/ltlvisit/reducform.cc,
src/ltlvisit/forminf.cc: Remove superfluous spot::ltl:: prefixes.
2004-05-25 09:14:51 +00:00
Alexandre Duret-Lutz
1245d19d23 * src/sanity/style.test: Catch `;'-not-followed-by-space.
* src/ltlvisit/reducform.cc, src/ltlvisit/forminf.cc: Fix style.
2004-05-24 18:16:27 +00:00
martinez
788ed772c2 * src/ltlvisit/basereduc.cc (spot): 80 columns.
* src/ltlvisit/reducform.cc (spot), src/ltltest/inf.cc,
src/ltltest/reduc.cc (main), src/ltlvisit/reducform.hh,
src/tgbatest/ltl2tgba.cc (main): More option.
* src/ltltest/inf.test: More test.
2004-05-17 14:50:17 +00:00
Alexandre Duret-Lutz
f2f10852c6 * ltltest/inf.cc, ltltest/reduc.cc, ltlvisit/reducform.cc: Fix style.
* sanity/style.test: More tests.
2004-05-14 14:09:01 +00:00
martinez
4cd10c3dfc * src/ltlvisit/Makefile.am: Copyright 2004.
* src/ltltest/inf.test: More test.
* src/ltlvisit/basereduc.cc, src/ltlvisit/forminf.cc (spot):
Use dynamic_cast.
* src/ltlvisit/reducform.cc, src/ltlvisit/reducform.hh,
src/ltltest/reduc.test, src/ltltest/reduc.cc: Add an option
to choose which rules applies to simplify the formula.
2004-05-13 16:00:15 +00:00
Alexandre Duret-Lutz
69169970a2 * src/ltltest/inf.cc, src/ltltest/inf.test, src/ltltest/reduc.test,
src/ltlvisit/formlength.cc, src/ltlvisit/reducform.cc,
src/ltlvisit/reducform.hh: Fix copyright year, these files were
created in 2004.
2004-05-10 17:26:32 +00:00
martinez
bafc92d0b8 *** empty log message *** 2004-05-10 15:43:18 +00:00