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

1098 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
d2cf7199bc * iface/gspn/ltlgspn.cc (display_stats): New function. 
(main): Use it.
* iface/gspn/ssp.cc: Add more counters for statistics.
 2008-02-25 14:36:57 +01:00
Alexandre Duret-Lutz
723054ce80 * iface/gspn/ssp.cc (couvreur99_check_shy_ssp::find_state): Correctly 
update the emptiness statistics.

* m4/gspnlib.m4: Typo.
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
ffd47e425e * iface/gspn/ssp.cc: Pacify sanity.test. 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
a390fe0754 typos 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
2a843fab1a * iface/gspn/ssp.cc (spot): Typo. 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
236742aed8 * src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::check): 
Reorganize this function so that syntactically there is only one
loop over the successors, and not two.  Call reintroduce the call
to couvreur99_check_shy::state_index(), needed by SSP, and
suppress that to index_and_insert introduced on 2004-12-29.  Also
split the "group" option in two: "group" and "group2".  "group2"
is the equivalent of the older "group", while the new "group" is
weaker and faster.
(couvreur99_check_shy::state_index): Change prototype as needed by
the algorithm.
* src/tgbaalgos/gtec/gtec.hh: Adjust.
* src/tgbaalgos/gtec/nsheap.hh, src/tgbaalgos/gtec/nsheap.cc
(index_and_insert): Remove.
* iface/gspn/ssp.cc (couvreur99_check_shy_ssp::state_index): Adjust
to new prototype.
* bench/emptchk/README, bench/emptchk/algorithms: Adjust references
to group/group2.
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
d9d4804bc9 * NEWS, configure.ac: Bump version to 0.3a. 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
05d0353d04 * NEWS, README, configure.ac: Update for version 0.3. 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
3751960ac8 * wrap/python/cgi/ltl2tgba.in: Fix degeneralisation and output of 
accepting runs.
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
851ca0d807 * wrap/python/spot.i: Wrap spot::emptiness_check_instantiator. 
* wrap/python/cgi/ltl2tgba.in: Offers all 6 emptiness
check algorithms, and a text box for options.
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
396894f7a7 * src/tgbaalgos/ndfs_result.hxx (ndfs_result::construct_cycle): 
Initialize tmp to suppress a GCC 4.0.1 warning (seen on Darwin).
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
b47f4ab09b * src/tgbatest/defs.in (VALGRIND): Use --log-fd instead of 
--logfile-fd to please newer versions of Valgrind.
* src/ltltest/defs.in, src/evtgbatest/defs.in: Likewise.
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
89aff72523 * src/ltlparse/ltlparse.yy (result): Do not assign to $$, it's useless. 
Suggested by Akim.
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
f7fe379e60 * src/tgbatest/randtgba.cc: New option -H. 
* src/tgbaalgos/emptiness_stats.hh (unsigned_statistics_copy): New
class.
 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
d5fb32120f * src/tgbatest/randtgba.cc: New option -S. 2008-02-25 14:36:56 +01:00
Alexandre Duret-Lutz
8e00065d84 * src/tgbaalgos/lbtt.cc: Typo. 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
b343e16b51 * src/tgbatest/randtgba.cc (default_algos): Test the "ordering" 
heuristic.
 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
3f22bc17ff * src/tgbaalgos/tau03opt.cc: Include <vector>. 
(tau03_opt_search): Add option "ordering" (off by default).
If enabled, initialize an explicit ordering for acceptance
conditions into the new member "cond" (a vector of bdds).
(project_acc): New helper function for projecting a set of
acceptance conditions to a subset that maximizes the number
of initial consecutive conditions covered by the set in the
condition ordering.
(dfs_blue): Implement the ordering heuristic.
(dfs_red): Use a sentinel in condition_stack to avoid explicit
checks for the stack's emptiness.
Consider also the conditions in acc when checking for the
completion of an accepting cycle.
Fix the implementation of condition heuristic.
Implement the ordering heuristic.
Simplify the removal of elements from condition_stack (due to
the way in which elements are pushed on the stack, there can
be at most one element with a given depth in the stack at any
one time).
 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
5b6e79ad96 * src/tgbaalgos/ndfs_result.hxx (ndfs_result::construct_prefix): 
Initialize tmp to suppress a GCC 4.0 warning.
* src/ltltest/randltl.cc (main): Likewise with another variable.
 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
048a5825de * src/ltlast/visitor.hh (visitor, const_visitor): Add empty 
virtual destructors.
* src/tgba/tgbabddfactory.hh (tgba_bdd_factory): Likewise.
* src/misc/hash.hh: Use the std namespace only with GCC 3.0,
not with all compiler versions with minor version 0.
* src/tgba/tgbatba.cc (tgba_tba_proxy_succ_iterator): Fix
friend declaration of ::spot::tgba_tba_proxy.
 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
6bcc8c3ce1 * src/tgbaalgos/magic.hh: fixme is not a doxygen command. Use bug. 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
98fd480506 * README: Update lbtt references. 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
cc4137e5ba * iface/gspn/ssp.cc: Typo in comment. 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
17f76e371f * lbtt/: Merge lbtt 1.2.0. 2005-08-31 15:30:38 +00:00
Alexandre Duret-Lutz
8a5fd909b3 * src/tgbaalgos/reductgba_sim_del.cc 
(parity_game_graph_delayed::get_relation): Disable for generalized
automata, it's wrong.
 2005-06-06 13:53:56 +00:00
Alexandre Duret-Lutz
fc4f4f7288 * src/tgbaalgos/reductgba_sim_del.cc 
(parity_game_graph_delayed::nb_set_acc_cond): Simplify.
 2005-05-25 09:00:19 +00:00
Alexandre Duret-Lutz
35aa277164 * sanity/style.test: Catch misuses of Sgi::. 
* tgba/tgbareduc.hh, tgbaalgos/reductgba_sim.cc,
tgbaalgos/reductgba_sim.hh, tgbaalgos/reductgba_sim_del.cc: Fix them.
 2005-05-25 08:56:15 +00:00
Denis Poitrenaud
64d5de8fe1 * src/ltlvisit/syntimpl.cc: Fix a typo. 2005-05-16 15:19:13 +00:00
Alexandre Duret-Lutz
5a39d40b2c * src/ltlvisit/syntimpl.cc: Fix detection of purely eventual formulae. 2005-05-14 20:56:19 +00:00
Alexandre Duret-Lutz
2e15a93525 * src/tgbaalgos/ltl2tgba_fm.cc: Fix handling of fair_loop_approx. 2005-05-12 18:01:27 +00:00
Alexandre Duret-Lutz
814ec7c2d0 * src/misc/hashfunc.hh (knuth32_hash): New function. 
* src/misc/hash.hh (ptr_hash): Use knuth32_hash.
* src/tgba/tgbabddconcretefactory.hh (tgba_bdd_concrete_factory): Use
ltl::formula_ptr_hash for acc_map_.
 2005-05-04 16:09:41 +00:00
Alexandre Duret-Lutz
9063c5abb4 * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_fm.cc: Add 
the reduce_ltl argument.
* src/tgbatest/ltl2tgba.cc: Add options -fr1, -fr2, -fr3, and -fr4.
* src/tgbatest/spotlbtt.test, bench/ltl2tgba/algorithms: Test -fr4.
* bench/ltl2tgba/parseout.pl: Suppress Perl warnings on disabled
algorithms.
 2005-05-04 13:47:38 +00:00
Alexandre Duret-Lutz
7ef117e3dc * bench/ltl2tgba/README: More instructions. 
* bench/Makefile.am (SUBDIRS): Add ltl2tgba.
* README: Mention bench/ltl2tgba.
 2005-04-19 09:04:22 +00:00
Alexandre Duret-Lutz
a7cf769a24 * bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README, 
bench/ltl2tgba/algorithms, bench/ltl2tgba/big,
bench/ltl2tgba/defs.in, bench/ltl2tgba/formulae.ltl,
bench/ltl2tgba/known, bench/ltl2tgba/parseout.pl,
bench/ltl2tgba/small: New files.
* src/tgbatest/ltl2baw.pl: Move ...
* bench/ltl2tgba/ltl2baw.in: ... here.
* src/tgbatest/Makefile.am: Adjust.
* configure.ac: Adjust.
 2005-04-15 13:38:23 +00:00
Alexandre Duret-Lutz
7753938fe9 * src/tgbatest/ltl2tgba.cc (main): Delete the reduced automaton 
before the degeneralized automaton.
 2005-04-14 09:21:59 +00:00
Alexandre Duret-Lutz
98236cf656 * doc/Makefile.am (doc, $(srcdir)/stamp): Ignore rm's errors. 2005-04-13 16:28:10 +00:00
Alexandre Duret-Lutz
acf61d1a46 * README: Typos. 2005-04-12 09:18:54 +00:00
Alexandre Duret-Lutz
8721f65bdc * NEWS, configure.ac: Bump version to 0.2a. 2005-04-08 22:44:26 +00:00
Alexandre Duret-Lutz
e00aadce5b * NEWS, configure.ac: Bump version to 0.2. 2005-04-08 22:41:09 +00:00
Alexandre Duret-Lutz
751424c9ec * bench/emptchk/README: Mention 
http://spot.lip6.fr/wiki/EmptinessCheckOptions for the syntax.
 2005-04-08 19:00:08 +00:00
Alexandre Duret-Lutz
5d0f702383 * src/tgbaparse/tgbaparse.yy (acc_list): Do not explicitly delete 
an undeclared acceptance condition.
* src/tgbaalgos/save.cc (print_acc): Unquote atomic propositions.
 2005-04-06 17:23:29 +00:00
Alexandre Duret-Lutz
d309c01941 * bench/emptchk/Makefile.am: Create reduced versions of the graphs. 
* bench/emptchk/pml2tgba.pl: Add option -r.
* bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh:
Also run on reduced graphs (this is fast).
* bench/emptchk/README: Adjust.
 2005-04-06 16:31:32 +00:00
Alexandre Duret-Lutz
ecaedbba4c * src/ltlvisit/length.cc (length_visitor): Rewrite using 
postfix_visitor.
 2005-02-23 00:35:45 +00:00
Alexandre Duret-Lutz
dd1bc78786 * src/tgbaalgos/tau03opt.cc (tau03_opt_search): Add options "weights" 
and "redweights" (on by default).
 2005-02-22 17:37:33 +00:00
Alexandre Duret-Lutz
fa9614e997 * src/tgbaalgos/tau03opt.cc (tau03_opt_search): Do not 
account for the size of condition_stack.
 2005-02-22 13:43:47 +00:00
Alexandre Duret-Lutz
a2cbe9cab8 * src/sanity/style.test: Catch occurrences of "accepting condition". 
* bench/emptchk/ltl-human.sh, bench/emptchk/ltl-random.sh,
src/sanity/style.test, src/tgba/bdddict.cc,
src/tgba/succiterconcrete.hh, src/tgba/tgbabddcoredata.hh,
src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh,
src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbatest/dfs.test: Replace them by "acceptance condition".
 2005-02-20 22:41:11 +00:00
Alexandre Duret-Lutz
7bbe3f5573 * src/tgbaalgos/tau03opt.hh, src/tgbaalgos/tau03.hh: Include 
misc/optionmap.hh.
 2005-02-20 22:19:15 +00:00
Alexandre Duret-Lutz
89c33952c9 * bench/emptchk/README: Document the file `algorithms'. 2005-02-18 14:34:17 +00:00
Alexandre Duret-Lutz
ff8fe6802b * src/tgbaalgos/tau03opt.cc (tau03_opt_search): Implement the 
"condition heuristic".  Suggested by Heikki Tauriainen.
* src/tgbatest/randtgba.cc: Test it.
 2005-02-18 14:13:26 +00:00
Alexandre Duret-Lutz
6314b682ba * src/tgbatest/randtgba.cc: Remplace the -O option by -A, reading 
all algorithms from a file.  Use the emptiness_check_instantiator
syntax as name in the output.
* bench/emptchk/defs.in: DEfine ALGORITHMS here.
* bench/emptchk/ltl-human.sh, bench/emptchk/ltl-random.sh,
bench/emptchk/pml-clserv.sh, bench/emptchk/pml-clserv.sh: Use
$ALGORITHMS.
* src/misc/timer.cc: Truncate long keys in display.
 2005-02-18 12:28:42 +00:00