alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
814 commits 6 branches 0 tags 36 MiB
Commit graph

814 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
db6973aaa8 * bench/emptchk/Makefile.am (dist_noinst_SCRIPTS): Add pml-clserv.sh 
and pml-eeaean.sh.
* bench/emptchk/ltl-human.sh: Typo in densities.
Reported by Denis.
 2005-01-30 10:18:24 +00:00
Alexandre Duret-Lutz
9e7138d9ab * doc/mainpage.dox: More text, and a link to "Modules". 2005-01-29 16:47:01 +00:00
Alexandre Duret-Lutz
5c6471daca * src/tgbatest/ltl2tgba.cc (main): Silence the "filename.tgba read" 
message if -0 is used.
 2005-01-29 16:05:28 +00:00
Alexandre Duret-Lutz
cddca67fda * bench/emptchk/formulae.ltl: New file. 2005-01-29 00:13:58 +00:00
Alexandre Duret-Lutz
de472c74b4 * src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Document poprem. 2005-01-29 00:07:21 +00:00
Alexandre Duret-Lutz
29548f695d * bench/emptchk/README: Make clearer that spin is needed. 2005-01-29 00:00:06 +00:00
Alexandre Duret-Lutz
c8a9c2d48a * src/tgbatest/randtgba.cc (syntax): Missing std::endl. 2005-01-28 23:57:41 +00:00
Alexandre Duret-Lutz
7bba6dc63d * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. 
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check, couvreur99_check_shy):
Add the poprem option.
* src/tgbaalgos/gtec/gtec.cc: Implement it.
* src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh
(scc_stack::rem, scc_stack::clear_rem,
scc_stack::connected_component::rem): New.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Add rem variants.
 2005-01-28 23:55:33 +00:00
Alexandre Duret-Lutz
5fb5b68407 * src/tgbaalgos/emptiness_stats.hh: Make sure depth() >= 0. 
* src/tgbaalgos/gtec/gtec.hh (couvreur99_check, couvreur99_check_shy):
Add the poprem option.
* src/tgbaalgos/gtec/gtec.cc: Implement it.
* src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh
(scc_stack::rem, scc_stack::clear_rem,
scc_stack::connected_component::rem): New.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Add rem variants.
 2005-01-28 17:17:54 +00:00
Denis Poitrenaud
b1800e382c * src/tgbatest/dfs.test, src/tgbatest/emptchk.test, 
src/tgbatest/emptchke.test, src/tgbatest/ltl2tgba.cc,
src/tgbatest/randtgba.cc, src/tgbatest/tba_samples_from_spin.test:
Adjust names of emptiness check algorithms.
 2005-01-28 15:57:52 +00:00
Denis Poitrenaud
40ce79c733 * src/tgbaalgos/gtec/gtec.cc: Adjust statistics count to match 
how the algorithm will behave once remove_component() is revamped. From
Alexandre.
 2005-01-27 13:46:18 +00:00
Alexandre Duret-Lutz
311e1ba759 * src/tgbaalgos/gtec/ce.cc (couvreur99_check_result::accepting_cycle): 
More ref in comment.
 2005-01-27 12:35:33 +00:00
Alexandre Duret-Lutz
acead199f5 * src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx, 
src/tgbaalgos/gtec/ce.cc: Do not account for states that are
computed but not visited by the BFS&DFS used to construct
accepting runs.
 2005-01-26 17:31:21 +00:00
Denis Poitrenaud
68c0aa2e38 * src/tgbatest/randtgba.cc: Complete performance measurements. 
* src/tgbatest/ltl2tgba.cc: Typo.

* src/tgbaalgos/magic.hh: Correct pseudo-code.

dedicated to display of stats.
 2005-01-25 12:31:05 +00:00
Alexandre Duret-Lutz
1072b2dd99 * src/tgbaalgos/tau03opt.hh, src/tgbaalgos/se05.hh: Correct 
pseudo-code.  From Denis.
 2005-01-24 18:57:08 +00:00
Alexandre Duret-Lutz
42bc594193 * src/tgbaalgos/gtec/gtec.cc: Fake statistics count to match 
how the algorithm will behave once remove_component() is revamped.
 2005-01-24 15:25:56 +00:00
Alexandre Duret-Lutz
8f0135ebb0 * src/tgbaalgos/emptiness_stats.hh (ars_statistics): Distinguish 
states visited to compute the prefix and those for the cycle.
* src/tgbaalgos/gv04.cc, src/tgbaalgos/ndfs_result.hxx,
src/tgbaalgos/gtec/ce.cc: Adjust.
* src/tgbatest/randtgba.cc: Print both statistics.
 2005-01-24 15:21:41 +00:00
Denis Poitrenaud
f56abf58b8 * src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add options 2005-01-24 14:41:27 +00:00
Alexandre Duret-Lutz
7d0b3fe297 * src/tgbatest/randtgba.cc: Some fixes from Denis for ratio stats. 2005-01-24 14:35:44 +00:00
Alexandre Duret-Lutz
55cc650bfe * src/ltlast/formula.hh (formula_ptr_less_than): Two 
formulae with the same hash key are not necessary equal!
 2005-01-20 21:35:10 +00:00
Alexandre Duret-Lutz
5069a565b6 * src/ltlast/formula.hh (hash, dump, dump_, hash_key_): New members. 
(formula_ptr_less_than, formula_ptr_hash): New class.
* src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
src/ltlast/constant.cc, src/ltlast/formula.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc: Adjust to handle dump_.
* src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh:
Sort the set using formula_ptr_less_than.
* src/ltlvisit/dump.cc: Simplify using ->dump().
* src/tgbaalgos/ltl2tgba_fm.cc: Sort all maps to get deterministic
results.
 2005-01-20 17:33:55 +00:00
Alexandre Duret-Lutz
8a5e31f00e * src/tgbaalgos/tau03opt.hh (explicit_tau03_opt_search): Doco. 2005-01-18 16:10:49 +00:00
Alexandre Duret-Lutz
48dfd73cca * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::clear_todo, 
couvreur99_check_shy::check): Sum all successors in the
todo stack AND all items on the stack.
 2005-01-18 10:52:23 +00:00
Alexandre Duret-Lutz
2604b27008 * src/tgbaalgos/emptiness_stats.hh (ec_statistics::depth): New function. 
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::clear_todo,
couvreur99_check_shy::check): Count all successors in the
todo stack rather than all items on the stack.
 2005-01-17 18:48:59 +00:00
Denis Poitrenaud
addb3a30cd * src/tgbatest/randtgba.cc: Close the formula file and remove a trace. 2005-01-13 18:16:32 +00:00
Denis Poitrenaud
2653b35ba7 * src/tgbatest/randtgba.cc: Add products with formulae issued of a file 
and more statistics.
* src/tgbatest/readsave.test: Undo previous change.
 2005-01-13 18:00:25 +00:00
Denis Poitrenaud
4e6ce2e739 * src/tgbatest/readsave.test: Fix parameter of randtgba call. 
more statistics.
the heap used for bit state hashing version and adjust the prototype of
* src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc: adjust the
prototype of has_been_visited and pop_notify.
 2005-01-13 09:21:22 +00:00
Denis Poitrenaud
333ee43f00 * src/tgbatest/randtgba.cc: Add products with randomized formulae and 2005-01-12 18:38:25 +00:00
Alexandre Duret-Lutz
0ff7f3ba2f * src/tgbaalgos/gv04.cc (result): Implement the acss_statistics, 
and ars_statistics interfaces.
 2005-01-11 14:42:00 +00:00
Denis Poitrenaud
81423bb743 * src/ltltest/randltl.cc: Typo. 2005-01-11 12:37:43 +00:00
Denis Poitrenaud
86b7f26960 * src/tgbaparse/tgbaparse.yy: Accept automaton without state. 
* src/ltltest/randltl.cc: Typo.
 2005-01-11 12:27:37 +00:00
Denis Poitrenaud
3f2790061a * src/tgbatest/randtgba.cc: Typo. 2005-01-10 18:26:14 +00:00
Alexandre Duret-Lutz
1cc003ec38 * src/tgbatest/ltl2tgba.cc: Typo. 2005-01-10 17:26:11 +00:00
Alexandre Duret-Lutz
6a0ab6c081 * src/tgbatest/randtgba.cc: Add option -P. 2005-01-10 17:22:25 +00:00
Denis Poitrenaud
a4b9b791ef * src/tgbaalgos/tau03.cc: Typo. 
* src/tgbatest/ltl2tgba.cc: Add option -b.
 2005-01-10 17:17:19 +00:00
Alexandre Duret-Lutz
7c07f3149f * src/tgbaalgos/ndfs_result.hxx (ndfs_result, acss_interface): 
Conditionally inherit from acss_statistics.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc: Define Has_Size in all heaps.
 2005-01-07 10:27:17 +00:00
Denis Poitrenaud
603b49e216 * src/ltltest/randltl.cc: Include cassert. 
* src/tgbaalgos/ndfs_result.hxx: Implement the spot::acss_statistics
interface.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc: Add to each heap class a method returning its
size.
 2005-01-06 15:54:48 +00:00
Alexandre Duret-Lutz
174b531f82 * src/ltltest/randltl.cc: Add options -r and -u. 
* src/ltltest/reduc.test: Use randltl -u, and run it through valgrind.
 2005-01-06 12:29:56 +00:00
Alexandre Duret-Lutz
e366b081a8 * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: New files. 
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS,
libltlvisit_la_SOURCES): Distribute them.
* src/ltltest/randltl.cc: New file.
* src/ltltest/Makefile.am (LDADD): Link with ../libspot.la directly.
(noinst_PROGRAMS, randltl_SOURCES): New.
(EXTRA_DIST, CLEANFILES): The list of random formulae is now generated.
* src/ltltest/formulae.txt: Delete.
* src/ltltest/reduc.test: Use randltl to generate formulae.
* src/ltlvisit/length.cc (length_visitor): Fix computation
of the length of multops.
* src/ltlvisit/length.hh (length): Document the length of multops.
 2005-01-05 16:20:21 +00:00
Alexandre Duret-Lutz
7216701631 * src/sanity/includes.test: Also check *.hxx files. 
* src/tgbaalgos/ndfs_result.hxx: Rename the include guard.
 2005-01-04 13:32:53 +00:00
Alexandre Duret-Lutz
e9beca0d56 fix eof, truncated by last commit 2005-01-04 13:20:50 +00:00
Alexandre Duret-Lutz
b054139e6d * doc/Doxyfile.in (FILE_PATTERNS): Remove *.hxx. 
* src/sanity/80columns.test, src/sanity/style.test: Process *.hxx files.
* src/tgbaalgos/ndfs_result.hh: Rename as ..
* src/tgbaalgos/ndfs_result.hxx: ... this, so it does not get
documented (and so Doxygen do not complain).
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc: Adjust include.
* src/tgbaalgos/Makefile.am: Rename ndfs_result.hh as ndfs_result.hxx
and do not install it, this is a private header.
 2005-01-03 17:39:43 +00:00
Alexandre Duret-Lutz
a9ab303859 * src/tgbaalgos/emptiness.hh: Declare Doxygen group 
emptiness_check_stats.
* src/tgbaalgos/emptiness_stats.hh: Use it.
 2005-01-03 16:59:53 +00:00
Alexandre Duret-Lutz
685c23a756 * doc/Doxyfile.in: Update for Doxygen 1.4.0, set 
DOT_MULTI_TARGETS, and disable GROUP_GRAPH (it causes segfault).
* src/tgbaparse/public.hh (format_tgba_parse_errors): Complete
Doxygen comment.
 2005-01-03 16:40:15 +00:00
Alexandre Duret-Lutz
55c08790fd * src/tgbaalgos/emptiness_stats.hh (ars_statistics): New class. 
* 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.
 2005-01-03 15:49:50 +00:00
Alexandre Duret-Lutz
6feb92090d * src/tgbaalgos/bfssteps.hh (bfs_steps::finalize): Document. 2005-01-03 14:20:08 +00:00
Alexandre Duret-Lutz
ca2fe6c711 * src/tgbaalgos/emptiness_stats.hh (accs_statistics): New class. 
* 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.
 2005-01-03 13:10:35 +00:00
Alexandre Duret-Lutz
13183893dd * src/tgbaalgos/ndfs_result.hh (construct_prefix): Do not call 
erase() after splice(), splice() already removes the elements.
 2005-01-03 12:11:28 +00:00
Alexandre Duret-Lutz
000c041a95 * src/evtgba/evtgbaiter.hh, src/ltlast/formula.hh, 
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.
 2005-01-03 10:20:26 +00:00
Alexandre Duret-Lutz
93f77c5782 * src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc 
(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.
 2004-12-29 15:29:26 +00:00