- 03 Jan, 2005 7 commits
-
-
Alexandre Duret-Lutz authored
emptiness_check_stats. * src/tgbaalgos/emptiness_stats.hh: Use it.
-
Alexandre Duret-Lutz authored
DOT_MULTI_TARGETS, and disable GROUP_GRAPH (it causes segfault). * src/tgbaparse/public.hh (format_tgba_parse_errors): Complete Doxygen comment.
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/ndfs_result.hh (ndfs_result): Inherit from ars_statistics. (ndfs_result::dfs): Call inc_ars_states(). (ndfs_result::test_path, ndfs_result::min_path): Update ars_statistics. * tgbaalgos/gtec/ce.hh (couvreur99_check_result): Inherit from ars_statistics. * tgbaalgos/gtec/ce.cc (shortest_path, couvreur99_check_result::accepting_cycle::scc_bfs): Update ars_statistics. * src/tgbatest/randtgba.cc: Display statistics about accepting run search.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh (couvreur99_check_result): Inherit from acss_statistics. (couvreur99_check_result::acss_states): Implement it. * src/tgbatest/randtgba.cc: Display statistics about accepting cycle search space.
-
Alexandre Duret-Lutz authored
erase() after splice(), splice() already removes the elements.
-
Alexandre Duret-Lutz authored
src/ltlast/refformula.hh, src/ltlenv/defaultenv.hh, src/misc/bareword.hh, src/tgba/succiter.hh, src/tgba/tgbabddfactory.hh, src/tgba/tgbareduc.hh, src/tgbaalgos/dupexp.hh, src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh, src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/tau03opt.hh: Add or fix include guards. * src/sanity/includes.test: Check the presence of the include guard.
-
- 29 Dec, 2004 1 commit
-
-
Alexandre Duret-Lutz authored
(index_and_insert): New function. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check): Rewrite. (couvreur99_check_shy::clear_todo): New method. * src/tgbaalgos/gtec/gtec.hh (couvreur99_check_shy::todo_item): New struct. * iface/gspn/ssp.cc (numbered_state_heap_ssp_semi::index_and_insert): New method.
-
- 20 Dec, 2004 2 commits
-
-
Alexandre Duret-Lutz authored
legitimate symlink in our source tree. Requested by Akim Demaille.
-
Denis Poitrenaud authored
runs. * src/tgbaalgos/bfssteps.hh, src/tgbaalgos/bfssteps.cc: Add the method finalize witch compute (by default) the traversed path. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc: Fix a bug concerning the heap used for bit state hashing version and ajust the prototype of has_been_visited and pop_notify. * src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: ajust the prototype of has_been_visited and pop_notify.
-
- 17 Dec, 2004 2 commits
-
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
splice(), splice() already remove the elements. * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_run): Likewise.
-
- 16 Dec, 2004 2 commits
-
-
Alexandre Duret-Lutz authored
emptiness-check on its own.
-
Alexandre Duret-Lutz authored
so it doesn't have to compute it. * src/tgbaparse/tgbascan.ll: Likewise. (YY_USER_INIT, current_file): Remove, it is too costly to use yy::Location::filename in the current implementation of yy::Location (this attribute is duplicated for each token). Leaving it empty divides the parsing time by 3. * src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh (format_tgba_parse_errors): Take the filename as argument. * src/tgbatest/explprod.cc, src/tgbatest/ltl2tgba.cc, src/tgbatest/mixprod.cc, src/tgbatest/powerset.cc, src/tgbatest/readsave.cc, src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc, src/tgbatest/tripprod.cc, iface/gspn/dottyssp.cc, iface/gspn/ltlgspn.cc: Adjust calls to format_tgba_parse_errors.
-
- 15 Dec, 2004 3 commits
-
-
Alexandre Duret-Lutz authored
reading of TGBAs with lots of identical conditions.
-
Alexandre Duret-Lutz authored
vr_map, free_annonymous_list_of_type>: Redeclare as std::map, instead of Sgi::hash_map. It proved to be faster. * src/tgbaalgos/ltl2tgba_fm.cc (translate_dict) <fv_map, vf_map>: Use the same definition as in bdd_dict. * tgbaalgos/reachiter.hh, tgbaalgos/replayrun.cc: Explicitly include misc/hash.hh.
-
Alexandre Duret-Lutz authored
Compiling the runtime in a separate modules is no longer required, and actually it does not work anymore... * wrap/python/swigpy.i: Remove. * wrap/python/Makefile.am (_swigpy.la): Remove all references. ($(srcdir)/spot_wrap.cxx, $(srcdir)/buddy_wrap.cxx): Do not use -noruntime.
-
- 14 Dec, 2004 2 commits
-
-
Alexandre Duret-Lutz authored
-
Denis Poitrenaud authored
-
- 13 Dec, 2004 1 commit
-
-
Denis Poitrenaud authored
accepting runs for ndfs emptiness check algoritms. * src/tgbaalgos/Makefile.am: Add it. * src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: Remove the old result classes and use the new one.
-
- 10 Dec, 2004 7 commits
-
-
Alexandre Duret-Lutz authored
(couvreur99_check_status::cycle_seed): New attribute. * src/tgbaalgos/gtec/gtec.cc (couvreur99_check::check, couvreur99_check_shy::check): Fill cycle_seed. * src/tgbaalgos/gtec/ce.hh, src/tgbaalgos/gtec/ce.cc: (couvreur99_check_result::accepting_run, couvreur99_check_result::accepting_cycle): Revamp to compute a cycle from the cycle_start, and then the shortest prefix to this cycle.
-
Alexandre Duret-Lutz authored
comment.
-
Alexandre Duret-Lutz authored
not tgbaalgos/gtec/status.hh.
-
Denis Poitrenaud authored
-
Alexandre Duret-Lutz authored
so it actually explore some accepting automata.
-
Alexandre Duret-Lutz authored
(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;
-
Alexandre Duret-Lutz authored
pointer of the state created as keys in sets; otherwise the graph created depends on the memory layout.
-
- 09 Dec, 2004 1 commit
-
-
Alexandre Duret-Lutz authored
Make sure to create the source state before the destination state.
-
- 08 Dec, 2004 5 commits
-
-
Denis Poitrenaud authored
-
Denis Poitrenaud authored
(set_init_state): Return a pointer to the initial state. (tgba_run_to_tgba): New function.
-
Alexandre Duret-Lutz authored
-
Alexandre Duret-Lutz authored
(tgba_explicit::create_transition(state*, const state*)): New function. * src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh: (random_graph): Revamp the algorithm to call rand() less often. * src/tgbatest/randtgba.cc: Add option -0 to easy profiling.
-
Alexandre Duret-Lutz authored
-
- 07 Dec, 2004 3 commits
-
-
Alexandre Duret-Lutz authored
(barand): New class. * src/misc/random.cc (nrand, bmrand, prand): New functions. * wrap/python/spot.i: Process src/misc/random.hh.
-
Alexandre Duret-Lutz authored
-
Denis Poitrenaud authored
accepting runs * src/misc/timer.hh: Include cassert.
-
- 06 Dec, 2004 1 commit
-
-
Alexandre Duret-Lutz authored
-
- 29 Nov, 2004 3 commits
-
-
Alexandre Duret-Lutz authored
* src/misc/Makefile.am (misc_HEADERS, libmisc_la_SOURCES): Add them. * src/tgbatest/randtgba.cc: Use time_map to measure the algorithms. Add the -R option. * src/sanity/style.sh: Let me use `for (.*;;)'.
-
Denis Poitrenaud authored
accepting runs
-
Alexandre Duret-Lutz authored
(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.
-