f59eeb75cd* src/tgbaalgos/powerset.cc, src/tgbaalgos/powerset.hh: New files. * src/tgbaalgos/Makefile.am: Add them. * src/tgbatest/powerset.cc: New file. * src/tgbatest/Makefile.am: Construct powerset and expldot from powerset.cc.
Alexandre Duret-Lutz
2004-01-05 17:29:36 +00:00
791c389080* src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::run) Reuse s->second to avoid a hash lookup. * src/tgbaalgos/save.cc (save_bfs::process_state): Delete dest.
Alexandre Duret-Lutz
2004-01-05 17:27:39 +00:00
95f6f2a639* src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::run) Reuse s->second to avoid a hash lookup. * src/tgbaalgos/save.cc (save_bfs::process_state): Delete dest.
Alexandre Duret-Lutz
2004-01-05 16:36:23 +00:00
5a5459f8be* src/ltlparse/Makefile.am ($(FROM_LTLPARSE_YY_MAIN)): Use $(FROM_LTLPARSE_YY_MAIN), not $@, because $@ can contains VPATH and we do not want Bison to see absolute paths. * src/tgbaparse/Makefile.am ($(FROM_TGBAPARSE_YY_MAIN)): Likewise.
Alexandre Duret-Lutz
2004-01-05 15:24:18 +00:00
a87c9d3d33* src/ltltest/parseerr.test: Adjust. * src/ltlparse/ltlparse.yy: Simplify error handling now that Bison will call destructors. Give each operator a full name, so that Bison uses it in error messages.
Alexandre Duret-Lutz
2004-01-05 12:17:38 +00:00
03704d635e* iface/gspn/ltleesrg.cc: New file. * iface/gspn/Makefile.am (check_PROGRAMS): Add ltleesrg. (ltleesrg_LDADD, ltleesrg_SOURCES): New variables.
Alexandre Duret-Lutz
2003-12-30 16:08:18 +00:00
6f88e518a9* src/ltltest/defs.in (run): New function, run valgrind. * src/ltltest/equals.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/ltltest/parse.test, src/ltltest/parseerr.test, src/ltltest/tostring.test, src/ltltest/tunabbrev.test, src/ltltest/tunenoform.test: Use run(). * Makefile.am (EXTRA_DIST): Don't list the m4/*.m4 files, Automake 1.8 find them automatically. * configure.ac: Require Automake 1.8, in gnits mode, and check for valgrind. * THANKS: New empty file.
Alexandre Duret-Lutz
2003-12-29 17:30:51 +00:00
c2892a8275* doc/Doxyfile.in: Upgrade to Doxygen 1.3.5. Build documentation for iface/. * dox/mainpage.dox: Fix reference to ltl_to_tgba. * src/ltlenv/environment.hh: Typo.
Alexandre Duret-Lutz
2003-12-29 12:14:04 +00:00
1b0fe66393* doc/texinfo.tex: New upstream version.
Alexandre Duret-Lutz
2003-12-29 10:57:51 +00:00
d07c66944e* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh (tgba_explicit::merge_transitions): New method. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Factorize all variables (not just Next and A) when computing prime implicants, and then call merge_transitions().
Alexandre Duret-Lutz
2003-12-03 13:29:11 +00:00
9b0ab316c2* configure.ac: Bump version to 0.0m.
Alexandre Duret-Lutz
2003-12-01 11:57:01 +00:00
0033466598* configure.ac, NEWS: Bump version to 0.0l. * doc/Makefile.am ($(srcdir)/spotref.pdf): Do not assume spot.latex is in the srcdir.
Alexandre Duret-Lutz
2003-12-01 11:48:58 +00:00
1811786597* src/tgbaparse/tgbaparse.yy (cond_list): Simplify into... (condition): ... this. We now accept only one condition, which is a formula. * src/tgba/tgbaexplicit.hh (tgba_explicit::add_neg_condition, tgba_explicit::get_condition): Remove, unused. * src/tgba/tgbaexplicit.cc: Likewise.
Alexandre Duret-Lutz
2003-11-28 16:57:55 +00:00
7e81306d45* src/tgba/bddprint.cc (print_accset_handler, bdd_print_accset): New functions. * src/tgba/bddprint.cc (bdd_print_accset): Declare it. * src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use it. * src/tgbatest/tgbaread.test, src/tgbatest/explicit.test: Adjust expected output.
Alexandre Duret-Lutz
2003-11-26 17:34:09 +00:00
6877f378bd* src/tgbaparse/tgbaparse.yy: Remove a random character. * src/tgba/formula2bdd.cc: Include cassert.
Alexandre Duret-Lutz
2003-11-25 14:19:14 +00:00
20289e4e7fExplicit automata can now have arbitrary logic formula on their arcs. ltl2tgba_fm benefits from this and join multiple arcs with the same destination and acceptance conditions. * src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh: New files. * src/tgba/Makefile.am (tgba_HEADERS, libtgba_la_SOURCES): Add them. * src/tgba/bddprint.cc, src/tgba/bddprint.hh (bdd_pring_formula, bdd_format_formula): New functions. * src/tgba/tgbaexplicit.hh (tgba_explicit::get_condition, tgba_explicit::add_condition, tgba_explicit::add_neg_condition, tgba_explicit::declare_accepting_condition, tgba_explicit::has_accepting_condition, tgba_explicit::get_accepting_condition, tgba_explicit::add_accepting_condition): Take a const formula*. * src/tgba/tgbaexplicit.cc (tgba_explicit::add_condition): Rewrite using formula_to_bdd. * src/tgbaalgos/dotty.cc (dotty_bfs::process_link): Use bdd_print_formula to display conditions. * src/tgbaalgos/save.cc (save_bfs::process_state): Likewise. * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict::bdd_to_formula): New function. (translate_dict::conj_bdd_to_atomic_props): Remove. (ltl_to_tgba_fm): Factor successors on accepting conditions and destinations, not conditions. Use bdd_to_formula to translate the conditions. * src/tgbaparse/tgbaparse.yy: Expect conditions as a formula in a string, call the LTL parser for this. * src/tgbaparse/tgbascan.ll: Process " and \ escapes in strings. * src/tgbatest/emptchke.test, src/tgbatest/explicit.test, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/mixprod.test, src/tgbatest/readsave.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Adjust to new syntax for explicit automata.
Alexandre Duret-Lutz
2003-11-24 18:30:09 +00:00
3126e49b28* src/misc/minato.hh (minato_isop(bdd,bdd)): New constructor variant. (minato_isop::local_vars::vars): New attribute. (minato_isop::local_vars::local_vars): Add the vars arguments. (minato_isop::todo, minato_isop::cube, minato_isop::ret): Rename as ... (minato_isop::todo_, minato_isop::cube_, minato_isop::ret_): ... these. * src/misc/minato.cc: Adjust to factorize only variables in vars.
Alexandre Duret-Lutz
2003-11-24 11:24:34 +00:00
e6c113f953* m4/devel.m4: Fix quoting and simplify default setting of enable_devel.
Alexandre Duret-Lutz
2003-11-24 10:48:53 +00:00
1b222106ab* src/ltlparse/ltlscan.ll: Include ltlparse/parsedecl.hh, not parsedecl.hh. * src/tgbaparse/tgbascan.ll: Likewise, include tgbaparse/parsedecl.hh.
Alexandre Duret-Lutz
2003-11-14 11:10:51 +00:00
f83a21cf94* src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Check whether the state is in the current SCC before passing it to h_filt().
Alexandre Duret-Lutz
2003-11-13 17:17:40 +00:00
10b2511dda* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::first_): New attribute. (tgba_succ_iterator_gspn_eesrg::step): Use first_. Loop until succ returns some successors. Report from Soheib Baarir.
Alexandre Duret-Lutz
2003-11-07 10:19:18 +00:00
f31caafb50* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::step): Fix the iteration logic. (tgba_succ_iterator_gspn_eesrg::tgba_succ_iterator_gspn_eesrg): Make sure not to free successors_ twice. (tgba_succ_iterator_gspn_eesrg::done): Fix definition.
Alexandre Duret-Lutz
2003-11-06 17:50:35 +00:00
f7851c17c0* iface/gspn/eesrg.cc (tgba_gspn_eesrg::get_init_state): Do not call get_init_state(), use 0 instead. (tgba_gspn_eesrg::format_state): Handle the case where s->left() == 0. Reported by Soheib Baarir.
Alexandre Duret-Lutz
2003-11-06 10:16:09 +00:00
e394b8e9f6* iface/gspn/gspn.cc (tgba_gspn_eesrg_private_::tgba_gspn_eesrg_private_): Show prop_index() and prop_kind() arguments on error.
Alexandre Duret-Lutz
2003-11-03 10:58:48 +00:00
c03626564a* iface/gspn/eesrg.cc (tgba_gspn_eesrg_private_::tgba_gspn_eesrg_private_): Show prop_index() argument on error.
Alexandre Duret-Lutz
2003-11-03 10:56:21 +00:00
747a4439ef* src/ltlparse/Makefile.am ($(FROM_LTLPARSE_YY_MAIN)): cd into $(srcdir) before running bison, so that bison does not put absolute filenames in generated files. * src/tgbaparse/Makefile.am ($(FROM_TGBAPARSE_YY_MAIN)): Likewise. Reported by Soheib Baarir.
Alexandre Duret-Lutz
2003-11-03 10:49:35 +00:00
dd720e9785* src/tgbaalgos/emptinesscheck.cc (emptiness_check::h_filt, emptiness_check::~emptiness_check) New methods. (emptiness_check::check): Release all iterators in todo on exit. (emptiness_check::counter_example): Rewrite the BFS logic. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::h_filt, emptiness_check::~emptiness_check): New methods.
Alexandre Duret-Lutz
2003-10-27 10:51:53 +00:00
071cb5d62c* src/tgbaalgos/emptinesscheck.cc (emptiness_check::check, emptiness_check::counter_example): Simplify access to hashes after calls to find() for the same element..
Alexandre Duret-Lutz
2003-10-23 16:05:51 +00:00
fb4873d92e* src/tgbaalgos/emptinesscheck.hh (connected_component::set_of_state): Rename as ... (connected_component::set_type): ... this, and define as a hash_set. (connected_component::has_state): New method. * src/tgbaalgos/emptinesscheck.cc (connected_component::has_state): New method. (emptiness_check::counter_example, emptiness_check::complete_cycle, emptiness_check::accepting_path): Simplify using has_state().
Alexandre Duret-Lutz
2003-10-23 15:49:29 +00:00
f0dd415f2f* src/tgbaalgos/emptinesscheck.hh (emptiness_check::seen_state_num): Rename as ... (emptiness_check::h): ... this, and define as a hash_map. (emptiness_check::remove_component): Remove superfluous state_map argument. * src/tgbaalgos/emptinesscheck.cc: Adjust.
Alexandre Duret-Lutz
2003-10-23 15:06:57 +00:00
90099e47a6* src/tgbaalgos/emptinesscheck.hh (emptiness_check::emptiness_check): New, take the automaton to work on, and store it ... (emptiness_check::aut_): ... in this new attribute. (emptiness_check::tgba_emptiness_check): Rename as ... (emptiness_check::check): ... this, and remove the automata argument. (emptiness_check::counter_example, emptiness_check::print_result, emptiness_check::remove_component, emptiness_check::accepting_path, emptiness_check::complete_cycle): Remove the automata argument. * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust.
Alexandre Duret-Lutz
2003-10-23 14:17:02 +00:00
b60722bc58* src/tgbaalgos/emptinesscheck.hh (connected_component::not_null, connected_component::transition_acc, connected_component::nb_transition, connected_component::nb_state): Remove these unused attributes. (connected_component::connected_component): Merge the two definitions into one. (connected_component::~connected_component): Remove. (connected_component::isAccepted): Delete, unused. * src/tgbaalgos/emptinesscheck.cc (connected_component::connected_component, connected_component::~connected_component): Adjust. (connected_component::isAccepted): Delete. (spot):
Alexandre Duret-Lutz
2003-10-23 13:50:15 +00:00
636f5238d3* src/tgbaalgos/emptinesscheck.hh (emptiness_check::remove_component, emptiness_check::root_component, emptiness_check::seen_state_num, emptiness_check::suffix): Move in private part. (emptiness_check::arc_accepting, emptiness_check::todo): Move ... * src/tgbaalgos/emptinesscheck.cc (emptiness_check::tgba_emptiness_check): ... as local variables of this function. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component): Move ... (emptiness_check::counter_example): ... as local variable of this function. * src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet): Move ... * src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet): ... here.
Alexandre Duret-Lutz
2003-10-23 13:05:35 +00:00
fda83b9c51* src/tgbaalgos/emptinesscheck.hh (emptiness_check::remove_component, emptiness_check::root_component, emptiness_check::seen_state_num, emptiness_check::suffix): Move in private part. (emptiness_check::arc_accepting, emptiness_check::todo): Move ... * src/tgbaalgos/emptinesscheck.cc (emptiness_check::tgba_emptiness_check): ... as local variables of this function. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::vec_component): Move ... (emptiness_check::counter_example): ... as local variable of this function. * src/tgbaalgos/emptinesscheck.hh (pair_state_iter, triplet): Move ... * src/tgbaalgos/emptinesscheck.cc (pair_state_iter, triplet): ... here.
Alexandre Duret-Lutz
2003-10-23 13:05:35 +00:00
008056f279* src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_result): Indent output as in the magic search.
Alexandre Duret-Lutz
2003-10-23 12:16:04 +00:00
46756c9589* src/tgbatest/spotlbtt.test: Add notice about long run time.
Alexandre Duret-Lutz
2003-10-23 12:09:34 +00:00
d46c63a21bMerge emptinesscheckexplicit into ltl2tgba. * src/tgbatest/Makefile.am (check_PROGRAMS): Remove emptinesscheckexplicit. (emptinesscheckexplicit_SOURCES): Remove. (TESTS): Replace emptinesscheckexplicit.test by emptchke.test. * src/tgbatest/emptinesscheckexplicit.cc, src/tgbatest/emptinesscheckexplicit.test: Delete. * src/tgbatest/empchke.test: New file. * src/tgbatest/ltl2tgba.cc: Add support for -X.
Alexandre Duret-Lutz
2003-10-23 11:58:11 +00:00
65f84e2c61Merge emptiness-checks tests into ltl2tgba. * src/tgbatest/Makefile (check_PRORGRAMS): Remove emptinesscheck and ltlmagic. (emptinesscheck_SOURCES, ltlmagic_SOURCES): Remove. (TESTS): Replace emptinesscheck.test and ltlmagic.test by emptchk.test. * src/tgbatest/emptinesscheck.test, src/tgbatest/ltlmagic.test: Delete. * src/tgbatest/emptchk.test: New file. * src/tgbatest/emptinesscheck.cc, src/tgbatest/ltlmagic.cc: Delete. * src/tgbatest/ltl2tgba.cc: Add support for -e, -E, -m, -M, and -n.
Alexandre Duret-Lutz
2003-10-23 11:37:07 +00:00
a11a29a1f7* src/tgbaalgos/emptinesscheck.cc (emptiness_check::tgba_emptiness_check): Do not print anything. (emptiness_check::counter_example): Assume that tgba_emptiness_check has already been called.
Alexandre Duret-Lutz
2003-10-23 09:40:55 +00:00
c7bbe60f4c* iface/gspn/ltlgspn.cc: Use command-line options to select algorithms, not #defines. * iface/gspn/Makefile.am (check_PROGRAMS): Remove eltlgspn-srg, efmgspn-srg, fmgspn-rg, and fmgspn-srg and their associated source variables. These are all replaced by ltlgspn-rg and ltlgspn-srg. * iface/gspn/dcswavefm.test, iface/gspn/dcswaveltl.test, iface/gspn/dcswaveeltl.test, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test, iface/gspn/udcsfm.test, iface/gspn/udcsltl.test: Adjust calls to ltlgspn-srg.
Alexandre Duret-Lutz
2003-10-08 17:27:20 +00:00
6920a1c30f* iface/gspn/ltlgspn.cc: We call tgba_emptiness_check before counter_example. And we print the prefix and the periode of counter_example's result.
rebiha
2003-10-07 12:13:30 +00:00
694ce34bc5* iface/gspn/udcsltl.test, iface/gspn/udcseltl.test, iface/gspn/dcswaveltl.test, iface/gspn/dcswaveeltl.test, iface/gspn/dcswavefm.test: Do not accept $? = 0 when a failure is expected.
Alexandre Duret-Lutz
2003-10-01 16:55:22 +00:00
7f3c113130* src/tgbatest/emptinesscheckexplicit.test (acc): New file.
rebiha
2003-09-25 15:12:44 +00:00
83565fb659* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh: Rename as ... * src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/ltl2tgba_lacim.hh: ... this, and rename ltl_to_tgba() as ltl_to_tgba_lacim as well. * iface/gspn/ltlgspn.cc, src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlmagic.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/tripprod.cc, wrap/python/spot.i, wrap/python/cgi/ltl2tgba.in, wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py: Adjust.
Alexandre Duret-Lutz
2003-09-22 15:54:34 +00:00
5439b2f4ee* src/tgba/state.hh: Include cassert.
Alexandre Duret-Lutz
2003-09-10 22:45:45 +00:00
f0de38680a* src/tgba/state.hh (state::hash): New method. (state_ptr_equal, state_ptr_hash): New functors. * src/tgba/statebdd.hh, src/tgba/statebdd.cc (state_bdd::hash): New method. * src/tgba/tgbaexplicit.hh, src/tgba/tgbaexplicit.cc (state_explicit::hash): New method. (ns_map, sn_map): Use Sgi::hash_map instead of std::map. * src/tgba/tgbaproduct.hh, src/tgba/tgbaproduct.cc (state_product::hash): New method. * src/tgba/tgbatba.cc (state_tba_proxy::hash): New method. * src/tgbaalgos/lbtt.cc (acp_seen, todo_set, seen_map): Redefine using Sgi::hash_map or Sgi::hash_set. (lbtt_reachable): Don't erase a key that is pointed to by an iterator. * src/tgbaalgos/reachiter.cc (tgba_reachable_iterator::~tgba_reachable_iterator): Likewise. * src/tgbaalgos/magic.cc (magic_search::~magic_search()): Likewise. * src/tgbaalgos/magic.hh (hash_type): Redefine using Sgi::hash_map. * src/tgbaalgos/reachiter.hh (seen_map): Redefine using Sgi::hash_map. * iface/gspn/gspn.cc (state_gspn::hash): New method. * src/misc/hash.hh (string_hash): New functor.
Alexandre Duret-Lutz
2003-08-29 15:54:31 +00:00
6da1f35641* src/tgba/tgbaexplicit.cc (tgba_explicit::all_accepting_conditions) Compute all_accepting_conditions_ from neg_accepting_conditions_, not by browsing the dictionary. The dictionary also contains accepting conditions from other automata... This bug was a consequence of the change from 2003-07-14. * src/tgbaalgos/save.cc (save_bfs::start()): Likewise, do not browse the dictionary to print accepting conditions. Call ->all_accepting_conditions() instead. * src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Typo from 2003-08-22 in the computation of all_accepting_conditions_. * src/tgbatest/explpro3.test: New file. * src/tgbatest/Makefile.am (TESTS): Add explpro3.test. * src/tgbatest/explprod.test, src/tgbatest/explpro2.test, src/tgbatest/tripprod.test: Sort the output using Perl.
Alexandre Duret-Lutz
2003-08-29 15:48:23 +00:00
1955150999Rewrite all std::map<const formula*, ...> as Sgi::hash_map<const formula*, ...>.
Alexandre Duret-Lutz
2003-08-28 16:59:11 +00:00
51094329d8* src/tgba/state.hh (state_ptr_less_than): Make sure left is non-null. Suggested by Denis Poitreneaud.
Alexandre Duret-Lutz
2003-08-25 19:21:02 +00:00
1ac0b08695* wrap/python/cgi/ltl2tgba.in: Fix display of relations for tgba_bdd_concrete automata.
Alexandre Duret-Lutz
2003-08-22 12:41:36 +00:00
7db71d9afeFix computation of product acceptance conditions, when the two operands share some acceptance conditions. * src/tgba/tgbaproduct.hh (tgba_product::left_acc_complement_, tgba_product::right_acc_complement_): New attribute. * src/tgba/tgbaproduct.cc (tgba_product::tgba_product): Set them. (tgba_product::succ_iter): Use them. * src/tgba/explpro2.test: New file. * src/tgba/Makefile.am (TESTS): Add it.
Alexandre Duret-Lutz
2003-08-22 10:07:02 +00:00
e238135bc1* iface/gspn/dcswavefm.test: New file. * iface/gspn/Makefile.am (check_PROGRAMS): Add fmgspn-rg and fmgspn-srg. (fmgspn_rg_SOURCES, fmgspn_rg_CPPFLAGS, fmgspn_rg_LDADD, fmgspn_srg_SOURCES, fmgspn_srg_CPPFLAGS, fmgspn_srg_LDADD): New variables. (TESTS): Add dcswavefm.test.
Alexandre Duret-Lutz
2003-08-20 09:56:12 +00:00
138ce95cca* src/ltlast/formula.hh: Make it clear that ref() and unref() deals with one node, not a entire formula.
Alexandre Duret-Lutz
2003-08-19 14:01:48 +00:00
2113d090bb* configure.ac: Bump version to 0.0i.
Alexandre Duret-Lutz
2003-08-18 15:35:38 +00:00
Alexandre Duret-Lutz
rebiha