alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Commit graph

  • 5d4affc5d7 * iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg, state_gspn_eesrg): Compute the array of all successors of the right state beforehand, pass it to Greatspn (left automata) at once, let it compute the resulting synchronized arcs, and iterate on that result. Alexandre Duret-Lutz 2004-04-14 13:00:03 +00:00
  • a2cd1de267 * src/tgbaalgos/gtec/nsheap.hh (numbered_state_heap_factory, numbered_state_heap_hash_map_factory): New class. * src/tgbaalgos/gtec/nsheap.cc (numbered_state_heap_hash_map_factory): Implement it. * src/tgbaalgos/gtec/gtec.hh (emptiness_check::emptiness_check, emptiness_check_shy::emptiness_check_shy): Take a numbered_state_heap_factory argument. * tgbaalgos/gtec/status.hh (emptiness_check_status::emptiness_check_status): Likewise. (emptiness_check_status::h): Make it a numbered_state_heap*. * src/tgbaalgos/gtec/ce.cc, tgbaalgos/gtec/gtec.cc, tgbaalgos/gtec/status.cc: Adjust uses of ecs_->h. Alexandre Duret-Lutz 2004-04-14 11:30:41 +00:00
  • 579c343e13 * src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc: Delete and split into ... * src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh, src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ... these new files. * src/tgbaalgos/gtec/Makefile.am: New file. * src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD): Recurse into gtec and link gtec/libgtec.la. (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh and emptinesscheck.cc. * configure.ac: Output src/tgbalagos/gtec/Makefile. * iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes. * README: Update tree description. Alexandre Duret-Lutz 2004-04-14 10:56:36 +00:00
  • d8f5bf608a * tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator, numbered_state_heap, numbered_state_heap_hash_map): New classes. * tgbaalgos/emptinesscheck.cc (numbered_state_heap_hash_map_const_iterator): New class. (numbered_state_heap_hash_map): Implement it. Alexandre Duret-Lutz 2004-04-13 15:32:10 +00:00
  • 7305dbb658 * src/tgbaalgos/emptinesscheck.hh (explicit_connected_component_factory, connected_component_hash_set_factory): New classes. (counter_example::counter_example): Take an explicit_connected_component_factory factory argument. * src/tgbaalgos/emptinesscheck.cc: Adjust. Alexandre Duret-Lutz 2004-04-13 13:57:59 +00:00
  • 3e63c1a0ca * src/tgbaalgos/emptinesscheck.hh (explicit_connected_component): New class. (counter_example::connected_component_set): Rename as ... (connected_component_hash_set): ... this, and inherit from explicit_connected_component. (counter_example::accepting_path, counter_example::complete_cycle): Alexandre Duret-Lutz 2004-04-13 13:25:19 +00:00
  • 1ea3c2ce5a * src/tgbaalgos/emptinesscheck.hh (counter_example::connected_component_set::has_state): Return a const state* and behave like h_filt. * src/tgbaalgos/emptinesscheck.cc: Adjust. Alexandre Duret-Lutz 2004-04-13 12:16:33 +00:00
  • b85e930232 * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Move into ... (emptiness_check_shy): This new subclass of emptiness_check. * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust. Alexandre Duret-Lutz 2004-04-13 11:44:42 +00:00
  • be17fc19f5 * src/tgba/bdddict.hh (bdd_dict::annon_free_list): Hide from Swig. Alexandre Duret-Lutz 2004-04-13 09:56:44 +00:00
  • 8a84cc6fb3 * src/tgbaalgo/semptinesscheck.hh (counter_example): New class, extracted from ... (emptiness_check): ... here. * src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc: Adjust. Alexandre Duret-Lutz 2004-04-13 09:39:30 +00:00
  • 80b7cbcf45 * wrap/python/Makefile.am ($(srcdir)/spot_wrap.cxx) ($(srcdir)/buddy_wrap.cxx): Use -noruntime instead of -c. Alexandre Duret-Lutz 2004-04-13 09:38:49 +00:00
  • 5eb2cf2cac * src/tgbaalgo/semptinesscheck.hh (emptiness_check_status): New class, extracted from ... (emptiness_check): ... here. * src/tgbaalgos/emptinesscheck.cc: Adjust. Alexandre Duret-Lutz 2004-04-13 08:53:10 +00:00
  • f8321633b7 * src/tgbaalgo/semptinesscheck.hh (scc_stack): New class, extracted from ... (emptiness_check): ... here. (emptiness_check::root): Redefined as a scc_stack object. * src/tgbaalgos/emptinesscheck.cc: Adjust. Alexandre Duret-Lutz 2004-04-13 08:33:24 +00:00
  • 7fd9459a63 * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Do not visit a state more than once. Report from Soheib Baarir. Alexandre Duret-Lutz 2004-04-05 12:43:06 +00:00
  • fa6ac39cfb * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict): Reuse Acc and Var variables from a shared bdd_dict. Register Next variables as anonymous variables. (translate_dict::translate_dict, translate_dict::~translate_dict, translate_dict::register_proposition, translate_dict::register_a_variable, translate_dict::register_next_variable, translate_dict::dump, translate_dict::var_to_formula, ltl_to_tgba_fm): Adjust. (translate_dict::dict): New attribute. (translate_dict::a_map, translate_dict::a_formula_map, translate_dict::var_map, translate_dict::var_formula_map): Delete. Alexandre Duret-Lutz 2004-03-25 16:24:05 +00:00
  • 3c3b23bfa4 * src/misc/freelist.cc (free_list::remove): Work around invalidated iterators. * tgba/bdddict.cc (unregister_variable): New methods, extracted from ... (bdd_dict::unregister_all_my_variables): ... here. * tgba/bdddict.hh (unregister_variable): Declare them. Alexandre Duret-Lutz 2004-03-25 15:02:57 +00:00
  • 784ccafb1b * src/misc/freelist.hh (free_list::remove, free_list::insert): New methods. * src/misc/freelist.cc (free_list::register_n, free_list::releases_n): Rewrite using free_list::remove and free_list::insert. (free_list::remove, free_list::insert): New methods. * src/tgba/bdddict.hh (bdd_dict::register_anonymous_variables): New method. (bdd_dict::annon_free_list): New subclass. (bdd_dict::free_annonymous_list_of_type_of): New attribute. * src/tgba/bdddict.cc (bdd_dict::register_all_variables_of, bdd_dict::unregister_all_my_variables): Handle anonymous variables too. (bdd_dict::register_anonymous_variables, bdd_dict::annon_free_list::annon_free_list, bdd_dict::annon_free_list::extend): New methods. Alexandre Duret-Lutz 2004-03-23 09:39:38 +00:00
  • aba2dc75d7 * src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path) Fix handling of PATH when backtracking. Report from Soheib Baarir. Alexandre Duret-Lutz 2004-03-23 09:33:27 +00:00
  • cf6602a3be Move the free_list management into a separate class for reuse. Alexandre Duret-Lutz 2004-03-18 15:43:10 +00:00
  • b84e6a6440 * src/Makefile.am (EXTRA_lbtt_SOURCES): Remove Config-parse.h, it is automatically distributed. (EXTRA_lbtt_translate_SOURCES): Likewise, remove NeverClaim-parse.h. Alexandre Duret-Lutz 2004-03-09 09:49:48 +00:00
  • 0bd6f72690 * configure.ac, NEWS: Bump version to 0.0s. Alexandre Duret-Lutz 2004-03-08 22:30:45 +00:00
  • b9b3c1ca25 * configure.ac, NEWS: Bump version to 0.0r. Alexandre Duret-Lutz 2004-03-08 22:23:04 +00:00
  • 1d411fa3c1 * configure.ac (YACC): Do not add `-d' here... * src/Makefile.am (AM_YFLAGS): ... do it here. (BUILT_SOURCES): New variable. Alexandre Duret-Lutz 2004-03-08 17:53:54 +00:00
  • 249a114f29 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm) <exprop>: Do not blindly enumerate all combinations of atomic properties; initially set all_props to the set of all possibly satisfiable combinations. Alexandre Duret-Lutz 2004-03-08 17:24:17 +00:00
  • 3aec630540 * doc/texinfo.tex: New upstream version. Alexandre Duret-Lutz 2004-03-08 17:23:36 +00:00
  • 4aea8548d3 * lbtt/src/Makefile.am (lbtt_translate_SOURCES): Fix leftover from 1.0.3 merge. Alexandre Duret-Lutz 2004-02-20 23:19:09 +00:00
  • 9e269dadc2 * wrap/python/cgi/ltl2tgba.in: Process ltl2tgba.opt if it exists. Alexandre Duret-Lutz 2004-02-20 23:15:04 +00:00
  • ab26065f4c * wrap/python/cgi/ltl2tgba.in: Color translators and their options. Alexandre Duret-Lutz 2004-02-20 22:51:13 +00:00
  • 153962aa9d * wrap/python/cgi/ltl2tgba.in: Present the options in a table. Alexandre Duret-Lutz 2004-02-20 21:51:39 +00:00
  • 0a1fc73eed * wrap/python/cgi/ltl2tgba.in: Remove the "print dot" options, add a "dot source" source behind each picture instead. Do not run `dot' on big automata. Alexandre Duret-Lutz 2004-02-20 21:00:06 +00:00
  • af27439d87 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Fix example in comment. Skip false transitions, and do not compute sub-formulae reachable only via false transitions. Alexandre Duret-Lutz 2004-02-20 14:18:54 +00:00
  • 0f7625b17d * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Revert yesterday's change. This optimization is NOT covered by exprop. In fact it could be generalized. Alexandre Duret-Lutz 2004-02-20 09:29:00 +00:00
  • 1ca1c39ec5 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Remove the cond_for_true optimization. It is covered by exprop. Alexandre Duret-Lutz 2004-02-19 15:47:31 +00:00
  • 3350ff7176 * src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator::current_state): Fix reference to Oddoux's thesis. Alexandre Duret-Lutz 2004-02-19 15:46:30 +00:00
  • 4e793ef418 * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Add the symb_merge argument. * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Likewise. * src/tgbatest/ltl2tgba.cc (main): Rename -fx as -x, and add -y to unset symb_merge. * wrap/python/cgi/ltl2tgba.in: Remove the exprop version of the FM translator, make exprop and symb_merge options. Alexandre Duret-Lutz 2004-02-16 16:07:47 +00:00
  • 5cb4048120 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_trad_visitor::visit) <unop::G>: suppress the GFy optimisation introduced on 2003-11-26, it is generalized by the identification of states with same symbolic rewriting introduced on 2004-02-02. Alexandre Duret-Lutz 2004-02-16 12:25:59 +00:00
  • 4741dc02bf * lbtt/: Merge lbtt 1.0.3. Alexandre Duret-Lutz 2004-02-16 12:09:29 +00:00
  • f4708a0179 Initial revision Alexandre Duret-Lutz 2004-02-16 11:36:00 +00:00
  • 15618b84ea Import of lbtt 1.0.3 Alexandre Duret-Lutz 2004-02-16 11:35:59 +00:00
  • 373be36cae * src/tgbatest/ltl2baw.pl (END): Ensure LTL2TGBA is always closed. Alexandre Duret-Lutz 2004-02-13 14:47:34 +00:00
  • 665216b0c2 * src/ExternalTranslator.cc: Include sys/wait.h. Alexandre Duret-Lutz 2004-02-12 14:16:55 +00:00
  • 2c10510e87 * src/tgbatest/ltl2tgba.cc (syntax): Recognize "-" as input filename for the formula. Merge the transitions of automata read with -X. * src/tgbatest/spotlbtt.test: Add many disabled algorithms. It is convenient to reuse the `config' file created by this test when making statistics. * src/tgbatest/ltl2baw.pl: New file. * src/tgbatest/Makefile.am (EXTRA_DIST): Add ltl2baw.pl. Alexandre Duret-Lutz 2004-02-11 15:45:54 +00:00
  • 2b7c9ea395 * src/SpotWrapper.cc (SpotWrapper::SPOT_AND, SpotWrapper::SPOT_OR): Define as && and || as in Spin. * src/SpotWrapper.hh: Update by email. Alexandre Duret-Lutz 2004-02-11 15:20:45 +00:00
  • 53a0cc7a54 * wrap/python/libpy.c: Update from Swig 1.3.21. * HACKING: Update versions. Alexandre Duret-Lutz 2004-02-10 10:15:20 +00:00
  • 07ba321e0a * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Take an exprop argument. Consider all possible combinations of propositions when generating arcs. Suggested by Jean-Michel Couvreur. * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Adjust. * src/tgbatest/ltl2tgba.cc: Honor -fx. * src/tgbatest/spotlbtt.test: Exercise -fx. * wrap/python/cgi/ltl2tgba.in: Support Couvreur/FM with exploded properties. Alexandre Duret-Lutz 2004-02-09 23:23:29 +00:00
  • f2c6db6d49 * src/ltlparse/ltlparse.yy: Typo. Alexandre Duret-Lutz 2004-02-09 21:01:34 +00:00
  • faaa117e02 * wrap/python/cgi/ltl2tgba.in: Use render_dot when showing formula. * wrap/python/cgi/README: Mention unique_id. Alexandre Duret-Lutz 2004-02-09 09:24:33 +00:00
  • 7069d5406b This should help getting accurate statistics (on both the formula automaton and the synchronized product) from LBTT. Idea from Jean-Michel Couvreur. Alexandre Duret-Lutz 2004-02-07 23:49:28 +00:00
  • 0816a4505f * src/tgbaalgos/lbtt.hh: Typos. Alexandre Duret-Lutz 2004-02-05 18:44:09 +00:00
  • b253881336 * src/tgbatest/spotlbtt.test: Typo. Alexandre Duret-Lutz 2004-02-05 13:08:57 +00:00
  • c38a3428f3 * wrap/python/spot.i (unblock_signal): New function. * wrap/python/cgi/ltl2tgba.in (print_footer, alarm_handler) (reset_alarm): New functions. Kill the script and its children if it runs for too long. (render_dot): Call reset_alarm. Alexandre Duret-Lutz 2004-02-04 22:56:06 +00:00
  • 44b351d23c * configure.ac, NEWS: Bump version to 0.0p. Alexandre Duret-Lutz 2004-02-03 14:18:33 +00:00
  • 1db08f494b * wrap/python/cgi/ltl2tgba.in: Fix <table> setting to cope with IE, Safari, konqueror, ... None of these support rules="groups" frame="border" properly (Mozilla is OK). Alexandre Duret-Lutz 2004-02-03 10:16:00 +00:00
  • 6dc59fa7fa * wrap/python/cgi/ltl2tgba.in: Output a description of the syntax. Alexandre Duret-Lutz 2004-02-02 23:30:08 +00:00
  • cfcc5e857b * wrap/python/cgi/ltl2tgba.in: Import spot and redirect stderr to stdout early. Alexandre Duret-Lutz 2004-02-02 22:04:38 +00:00
  • 59125b2a6c * wrap/python/cgi/ltl2tgba.in (print_stats): Compute and display the number of acceptance conditions. Alexandre Duret-Lutz 2004-02-02 22:02:00 +00:00
  • 49192cc35f * wrap/python/tests/bddnqueen.py, wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py: Specify coding system to accommodate newer Python versions. Alexandre Duret-Lutz 2004-02-02 21:43:41 +00:00
  • c46204dfad * src/misc/bddalloc.hh: Make all methods public. * wrap/python/spot.i: Include misc/bddalloc.hh and misc/minato.hh. * wrap/python/tests/minato.py: New file. * wrap/python/tests/Makefile.am (TESTS): Add minato.py. Alexandre Duret-Lutz 2004-02-02 21:39:25 +00:00
  • e0b15c6f67 * src/tgbatest/explicit.cc, src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc, src/tgbatest/readsave.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc: Add missing copyright license. Alexandre Duret-Lutz 2004-02-02 20:40:32 +00:00
  • 550e7acdb2 * wrap/python/cgi/ltl2tgba.in (render_dot): Render .png directly with dot, without using convert. * wrap/python/cgi/README: Do not mention convert. Alexandre Duret-Lutz 2004-02-02 20:17:05 +00:00
  • 47489236dc * wrap/python/cgi/ltl2tgba.in (render_dot, render_automaton) (render_bdd): New functions, extracted from the rest of the code. Alexandre Duret-Lutz 2004-02-02 20:11:31 +00:00
  • dae794aad3 * wrap/python/cgi/ltl2tgba.in (default_translator): Default to trans_fm. (translators): Show trans_fm before trans_lacim. Alexandre Duret-Lutz 2004-02-02 19:31:58 +00:00
  • 26cf0145b7 * wrap/python/cgi/ltl2tgba.in (print_stats): New function. Call it to display the size of the generalized and degeneralized automata. Alexandre Duret-Lutz 2004-02-02 19:29:56 +00:00
  • 834ce05235 * src/tgbalagos/stats.hh, src/tgbalagos/stats.cc: New files. * src/tgbalagos/Makefile.am: Add them. * wrap/python/spot.i: Include src/tgbalagos/dupexp.hh and src/tgbalagos/stats.hh Alexandre Duret-Lutz 2004-02-02 17:32:01 +00:00
  • d13c9c179b * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Identify states with identical successors. This optimizes the translation of `a R (b R c)', for instance. * src/tgbatest/ltl2tgba.test: Add two new tests. Alexandre Duret-Lutz 2004-02-02 16:26:15 +00:00
  • 872f7efbeb * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Identify states with identical successors. This optimizes the translation of `a R (b R c)', for instance. * src/tgbatest/ltl2tgba.test: Add two new tests. Alexandre Duret-Lutz 2004-02-02 16:12:13 +00:00
  • 0dd81f7d16 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Identify states with identical successors. This optimizes the translation of `a R (b R c)', for instance. * src/tgbatest/ltl2tgba.test: Add two new tests. Alexandre Duret-Lutz 2004-02-02 16:12:13 +00:00
  • 9d9ba1bed7 Hide the tgba_gspn and tgba_gspn_eesrg classes. Offer the corresponding automaton via the automaton() method of the gspn_interface and gspn_eesrg_interface classes. Alexandre Duret-Lutz 2004-02-02 09:55:48 +00:00
  • 2f7d46d719 * src/ltlvisit/tostring.cc: Fix output of F0, F1, G0, G1, X0, and X1. * src/ltltest/tostring.test: Test these. Alexandre Duret-Lutz 2004-01-30 16:55:12 +00:00
  • 1d72cdc86e * src/tgba/tgbaexplicit.cc (tgba_explicit::get_acceptance_condition): Do not treat true and false specially. Otherwise it breaks translation of F(false). * src/tgbatest/explprod.test, src/tgbatest/tripprod.test: Do not use true as acceptance condition. Alexandre Duret-Lutz 2004-01-29 17:05:19 +00:00
  • 440029c1b5 After this changes, degeneralized automata are 40% smaller in LBTT's statistics. Alexandre Duret-Lutz 2004-01-29 13:02:55 +00:00
  • bdbaa8356c * src/tgbaalgos/magic.cc (magic_search::~magic_search): Release all iterators on the stack. (magic_search::check): Release iterators that are popped off the stack. Alexandre Duret-Lutz 2004-01-26 12:46:39 +00:00
  • 57ddf52df0 * src/tgbatest/explpro2.test: Fix reordering regex. Alexandre Duret-Lutz 2004-01-26 10:16:18 +00:00
  • 468a32ea6e * src/tgbatest/defs.in (run): Use libtool --mode=execute. Alexandre Duret-Lutz 2004-01-26 08:37:58 +00:00
  • e434ccbec0 * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Merge transitions with same destination and acceptance conditions directly, without calling a->merge_transition(). If one transitions goes to "True", subtract its conditions from all other transitions; this optimizes a U b. Alexandre Duret-Lutz 2004-01-23 17:36:04 +00:00
  • 314768bf28 * src/ltlast/refformula.hh (ref_formula::ref_count_): New method. * src/ltlast/refformula.cc (ref_formula::ref_count_): New method. * src/ltlast/atomic_prop.hh (atomic_prop::dump_instance): New method. * src/ltlast/atomic_prop.cc (atomic_prop::dump_instance): New method. Alexandre Duret-Lutz 2004-01-23 17:08:45 +00:00
  • e73ce85cfc * src/tgbaalgos/ltl2tgba_fm.cc: Typos in comments. Alexandre Duret-Lutz 2004-01-23 13:01:43 +00:00
  • 4b4b640ec4 * src/TestOperations.cc: Include sys/wait.h. Alexandre Duret-Lutz 2004-01-16 16:04:04 +00:00
  • 7c1ac7bb67 * src/Alloc.h: Rename as ... * src/ObstackAlloc.h: ... this. The problem is that alloc.h is a system header in g++ < 3.0, and Darwin has a case-insensitive filesystem. System headers that include alloc.h pick the local Alloc.h version. * BuchiAutomaton.h, Configuration.h, DispUtil.cc, ExternalTranslator.h, FormulaRandomizer.h, Graph.h.in, LtlFormula.h, Makefile.am, NeverClaimAutomaton.h, PathEvaluator.h, ProductAutomaton.h, SccIterator.h, SharedTestData.h, StatDisplay.h, StateSpace.h, StateSpaceRandomizer.cc, StringUtil.h, TestOperations.h, TestRoundInfo.h, TestStatistics.h, UserCommandReader.h, UserCommands.h, main.cc: Adjust includes. Alexandre Duret-Lutz 2004-01-16 13:30:42 +00:00
  • b9b365e731 * configure.ac, NEWS: Bump version to 0.0o. Alexandre Duret-Lutz 2004-01-13 17:57:07 +00:00
  • 770943adc3 * configure.ac: Bump version to 0.0n. * NEWS: Update. Alexandre Duret-Lutz 2004-01-13 17:37:06 +00:00
  • 5b8ff7fb35 new upstream version Alexandre Duret-Lutz 2004-01-13 17:08:46 +00:00
  • 90d139db24 * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check, emptiness_check::check2): Document them. Alexandre Duret-Lutz 2004-01-13 16:45:55 +00:00
  • e481e1218e * iface/gspn/ltlgspn.cc (main): Typo, use MIN_ARG. Alexandre Duret-Lutz 2004-01-12 10:24:13 +00:00
  • c9d438aef4 * iface/gspn/dcswaveeltl.test, iface/gspn/udcsefm.test, iface/gspn/udcseltl.test: Exercize -e2. Alexandre Duret-Lutz 2004-01-09 17:33:23 +00:00
  • 93f1cc0d47 * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check2): New function, variant of emptiness_check::check(). * src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Likewise. * src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Exercize -e2. * src/tgbatest/ltl2tgba.cc: Support -e2, for emptiness_check::check2(). * iface/gspn/Makefile.am [WITH_GSPN_EESRG] (check_PROGRAMS): Compile ltlgspn-eesrg instead of ltleesrg. (ltleesrg_SOURCES, ltleesrg_LDADD): Replace by... (ltlgspn_eesrg_SOURCES, ltlgspn_eesrg_LDADD, LIBGSPNESRG_LDFLAGS): ... these. * iface/gspn/ltleesrg.cc: Delete. * iface/gspn/ltlgspn.cc [EESRG]: Support EESRG conditionally. Support -e2. Alexandre Duret-Lutz 2004-01-09 17:22:09 +00:00
  • a1f990b125 * src/tgbaalgos/ltl2tgba_lacim.cc: Typo in comment. Alexandre Duret-Lutz 2004-01-09 16:19:12 +00:00
  • 036cfd30f8 * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check): Typos in comment. Alexandre Duret-Lutz 2004-01-09 13:34:14 +00:00
  • f01267f36f * src/tgbaalgos/emptinesscheck.cc (emptiness_check::check): Typos in comment. Alexandre Duret-Lutz 2004-01-09 13:34:14 +00:00
  • 06877eac24 * m4/gspnlib.m4 (AX_CHECK_GSPNLIB): Do not warn about a missing library for eesrg. Define the WITH_GSPN_EESRG conditional. * iface/gspn/Makefile.am (gspn_HEADERS, check_PROGRAMS): Add the eesrg items in condition WITH_GSPN_EESRG. (libspotgspneesrg_la_LIBADD, libspotgspneesrg_la_CPPFLAGS) (libspotgspneesrg_la_SOURCES): Define only in condition WITH_GSPN_EESRG. Alexandre Duret-Lutz 2004-01-09 12:12:48 +00:00
  • 7a54e04800 * src/tgbaalgos/emptinesscheck.cc (emptiness_check::print_stats): New function. * src/tgbaalgos/emptinesscheck.hh (emptiness_check::print_stats): Likewise. * iface/gspn/ltlgspn.cc (main) <Couvreur>: Call print_stats(). * iface/gspn/ltleesrg.cc (main): Likewise. Alexandre Duret-Lutz 2004-01-09 10:56:56 +00:00
  • 4732d165db * iface/gspn/ltlgspn.cc: Add option -P. Alexandre Duret-Lutz 2004-01-09 10:31:01 +00:00
  • 92cc5f9b9f Run valgrind in test cases. * src/tgbatest/defs.in (VALGRIND, run): Define. * src/tgbatest/bddprod.test, src/tgbatest/dupexp.test, src/tgbatest/emptchk.test, src/tgbatest/emptchke.test, src/tgbatest/explicit.test, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/ltl2tgba.test, src/tgbatest/ltlprod.test, src/tgbatest/mixprod.test, src/tgbatest/readsave.test, src/tgbatest/tgbaread.test, src/tgbatest/tripprod.test: Use run(). Alexandre Duret-Lutz 2004-01-08 15:44:27 +00:00
  • 7aecf4ad09 * src/bddop.c (bdd_support): Free supportSet if it needs to be reallocated. This fixes a memory leak reported by Souheib.Baarir@lip6.fr. Alexandre Duret-Lutz 2004-01-07 16:05:21 +00:00
  • 9297d6dd9f * iface/gspn/eesrg.cc (format_state): Do not rewrite n's, just strip the last one. Escaping must be done at output. * iface/gspn/gspm.cc (format_state): Likewise. * src/misc/escape.hh, src/misc/escape.cc: New files. * src/misc/Makefile.am: Add them. * src/tgba/bddprint.cc (bdd_format_accset): New function. * src/tgba/bddprint.hh (bdd_format_accset): New function. * src/tgbaalgos/dotty.cc (dotty_bfs::process_state): Escape the state name using escape_str(). (dotty_bfs::process_link): Escape conditions and acceptance conditions using escape_str(). * src/tgbaalgos/save.cc (save_bfs::start): Call print_acc(). (save_bfs::print_acc): New function extracted from save_bfs::start(). Escape each acceptance condition. (save_bfs::process_state): Use escape_str() and print_acc() Alexandre Duret-Lutz 2004-01-06 16:56:07 +00:00
  • 8008deeddd * src/ltlvisit/tostring.cc (to_string_visitor::visit(const atomic_prop*)): Quote propositions that start with F, G, or X. * src/ltltest/tostring.test: Test quoted propositions. * src/tgbaalgos/save.cc (save_bfs::process_state): Escape " and + characters in formulae. * src/tgbatest/readsave.test: Test for this. Alexandre Duret-Lutz 2004-01-06 15:45:00 +00:00
  • a7ab42e422 * src/tgbaalgos/reachiter.hh: Typos in comments. Alexandre Duret-Lutz 2004-01-06 12:34:24 +00:00
  • c0210abb55 * iface/gspn/eesrg.cc (tgba_gspn_eesrg::all_acceptance_conditions, tgba_gspn_eesrg::neg_acceptance_conditions): Forward to data_->operand. Alexandre Duret-Lutz 2004-01-06 11:59:24 +00:00
  • 24fec22e52 * src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle): Do not skip this computation if from == to but the period is empty. Alexandre Duret-Lutz 2004-01-06 11:52:16 +00:00
  • 3c363aa11a * iface/gspn/eesrg.cc (state_gspn_eesrg::clone): Clone the right state. Alexandre Duret-Lutz 2004-01-06 11:34:41 +00:00