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

881 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
760945e678 update 2008-02-25 14:36:55 +01:00
Alexandre Duret-Lutz
9517cde264 Merge commit 'origin/lbtt-orig' into new-master 
Conflicts:

	lbtt/INSTALL
	lbtt/doc/texinfo.tex
	lbtt/src/LbttAlloc.h

Finish merge
 2008-02-25 14:34:25 +01:00
Alexandre Duret-Lutz
91df6cab77 fix status of lbtt's subtree. Apparently it was messed up during the cvsimport 2008-02-25 14:30:09 +01:00
Alexandre Duret-Lutz
17f76e371f * lbtt/: Merge lbtt 1.2.0. 2005-08-31 15:30:38 +00:00
Alexandre Duret-Lutz
0a12b942a4 Import of lbtt 1.2.0 2005-08-31 15:14:51 +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
Alexandre Duret-Lutz
3b3a196526 * src/tgbatest/ltl2tgba.cc: Simplify using 
emptiness_check_instantiator.
* src/tgba/tgba.cc, src/tgba/tgba.hh
(tgba::number_of_acceptance_conditions): Return an unsigned.
* bench/emptchk/algorithms, bench/emptchk/README,
src/tgbatest/emptchk.test, src/tgbatest/emptchke.test: Adjust
references to algorithms.
* bench/emptchk/pml-clserv.sh, bench/emptchk/pml-eeaean.sh: Quote
variables properly.
 2005-02-18 10:03:01 +00:00
Alexandre Duret-Lutz
4e1916ec50 * src/tgbaalgos/emptiness.hh, src/tgbaalgos/emptiness.cc 
(emptiness_check_instantiator): New class.
* src/misc/optionmap.hh (set (const option_map&)): New method.
* src/tgbatest/randtgba.cc: Create every emptiness check via
emptiness_check_instantiator.
 2005-02-17 19:14:03 +00:00
Alexandre Duret-Lutz
435b03c2b2 * src/tgbaalgos/emptiness.hh, 
src/tgbaalgos/emptiness.cc (emptiness_check::safe): New method.
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Implement it.
* src/tgbatest/randtgba.cc: Simplify.
 2005-02-17 16:48:35 +00:00
Alexandre Duret-Lutz
c1d0cab3af * src/tgbaalgos/magic.hh, src/tgbaalgos/magic.cc, 
src/tgbaalgos/se05.hh, src/tgbaalgos/se05.cc: Provide wrapper
functions that read the hash-map size from a "bsh" option.
* src/tgbatest/randtgba.cc: Simplify.
 2005-02-17 16:09:56 +00:00
Alexandre Duret-Lutz
fed4b6f05c * src/misc/optionmap.hh, src/misc/optionmap.cc 
(option_map::parse_options): Rewrite.  Do not modify the input
string, allow !foo as a shorthand for foo=0, and support K and
M suffixes for values.
* src/tgbatest/randtgba.cc (cons_emptiness_check): Simplify.
* wrap/python/spot.i: Process optionmap.hh.
* wrap/python/tests/optionmap.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
 2005-02-17 15:01:51 +00:00
Alexandre Duret-Lutz
f3effb9da0 * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map::get, 
option_map::set): Handle default values.
(anonymous::to_int): Do not print anything.
* src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/ce.cc, src/tgbaalgos/ce.hh: Take an option_map in
the constructor.
* src/tgbaalgos/gtec.cc, src/tgbaalgos/gtec.hh: Likewise.  Handle
the "poprem", "group", and "shy" options via the option_map.
Supply a couvreur99() wrapper to the shy/non-shy variant.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
iface/gspn/ssp.cc: Adjust.
 2005-02-16 18:53:18 +00:00
Alexandre Duret-Lutz
77888e9293 * src/tgbatest/randtgba.cc: Factorize more code using the 
unsigned_statistics interface.
* bench/emptchk/README: Adjust description of output.
 2005-02-08 18:33:14 +00:00
Alexandre Duret-Lutz
5cceccca06 * src/sanity/style.test: Strip all strings before checking the 
file, so that strings are not checked for our C++ style.
Reported by Denis (with a chainsaw).
 2005-02-07 15:56:35 +00:00
Denis Poitrenaud
b10727f139 * src/misc/optionmap.cc, src/misc/optionmap.hh: Typo (Hummm). 2005-02-07 15:47:36 +00:00
Denis Poitrenaud
661dee8633 * src/misc/optionmap.cc, src/misc/optionmap.hh (option_map): New class. 
* src/misc/Makefile.am: Add it.
* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: Add option
facilities to the classes emptiness_check and emptiness_result
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh,
src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh: Compute optionnaly
accepting runs from stack.
* src/tgbatest/randtgba.cc: Make this option public.
 2005-02-07 15:18:41 +00:00
Alexandre Duret-Lutz
e812e1926f * src/misc/ltstr.hh: Include <functional> 2005-02-05 10:18:31 +00:00
Alexandre Duret-Lutz
a5e9fb9df4 * src/tgbatest/randtgba.cc (stat_collector): New class, replacing... 
(ec_stat, acss_stat, ars_stat, print_ec_stats, print_acss_stats,
print_ars_stats): ... these.
* tgbaalgos/emptiness_stats.hh (unsigned_statistics): Make the
map public.
 2005-02-04 17:47:05 +00:00
Alexandre Duret-Lutz
081bdad5b4 * src/tgbaalgos/emptiness_stats.hh (unsigned_statistics::stats_map_): 
Use char_ptr_less_than.
 2005-02-04 16:16:05 +00:00
Alexandre Duret-Lutz
117aaf6772 * src/misc/ltstr.hh: New file. 
* src/misc/Makefile.am (misc_HEADERS): Add it.
 2005-02-04 15:27:24 +00:00
Alexandre Duret-Lutz
479c4833e0 * src/tgbaalgos/emptiness_stats.hh (unsigned_statistics::stats_map_): 
Use char* for keys, not std::string.
 2005-02-04 11:55:45 +00:00
Alexandre Duret-Lutz
9c2c3926c7 * tgbaalgos/emptiness_stats.hh (unsigned_statistics): New base 
class for ec_statistics and ars_statistics.
(acss_statistics): Inherit from ars_statistics.
* tgbaalgos/emptiness.cc, tgbaalgos/emptiness.hh:
(emptiness_check::statistics, emptiness_check_result::statistics):
New methods.
* tgbatest/randtgba.cc: Adjust to use the above.
* tgbaalgos/gv04.cc, tgbaalgos/ndfs_result.hxx, tgbaalgos/gtec/ce.cc,
tgbaalgos/gtec/ce.hh: Do not inherit from ars_statistics if
acss_statistics is used.
 2005-02-03 17:37:11 +00:00