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

894 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Alexandre Duret-Lutz
ad9eec60f1 * src/tgbaalgos/gtec/gtec.hh (couvreur99_check): Add pseudo code. 2005-02-03 14:40:14 +00:00
Alexandre Duret-Lutz
5533e9dc35 * src/tgbaalgos/randomgraph.cc (random_graph): Make sure n > 0. 
* src/tgbatest/randtgba.cc: Check the range of all arguments.
 2005-02-02 16:03:31 +00:00
Alexandre Duret-Lutz
f22b59bf95 * bench/emptchk/models/eeaean1.pml: New file, from schwoon.05.tacas. 
* bench/emptchk/Makefile.am: Distribute models/eeaean1.pml
and build models/eeaean1.tgba.
* bench/emptchk/pml-eeaean.sh: Check models/eeaean1.pml.
* bench/emptchk/README: Adjust.
* bench/emptchk/defs.in (RANDTGBA, LTL2TGBA): These tools are in
the build tree, not the source tree...
 2005-02-02 12:58:08 +00:00
Alexandre Duret-Lutz
2b68284dba These tests are huge, and are obsoleted by randtgba-based checks, 
and by bench/emptchk/.
* src/tgbatest/tba_samples_from_spin.test: Delete.
* src/tgbatest/tba_samples_from_spin/: Delete.
* src/tgbatest/Makefile.am: Adjust.
 2005-02-02 10:30:39 +00:00
Alexandre Duret-Lutz
5cd58f9aaf * src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll, 
src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
src/evtgbaparse/public.hh, src/evtgbatest/product.cc,
src/evtgbatest/readsave.cc, src/ltlparse/fmterror.cc,
src/ltlparse/ltlparse.yy, src/ltlparse/parsedecl.hh,
src/ltlparse/public.hh, src/tgbaparse/parsedecl.hh,
src/tgbaparse/public.hh, src/tgbaparse/tgbaparse.yy: Update
to Bison 2.0.
 2005-02-01 18:03:00 +00:00
Alexandre Duret-Lutz
461fcd3732 * bench/emptchk/pml2tgba.pl (usage): Correct description. From Denis. 2005-02-01 16:52:22 +00:00
Alexandre Duret-Lutz
ce871f2f2e * bench/emptchk/README: Timing info from Denis. 2005-02-01 13:23:34 +00:00
Alexandre Duret-Lutz
516350ddc0 * src/tgbatest/randtgba.cc (main): Skip empty lines. 
(syntax): Categorize options.
 2005-02-01 13:19:11 +00:00
Alexandre Duret-Lutz
42cd2e05b5 * src/tgbatest/explicit.test, src/tgbatest/explpro2.test, 
src/tgbatest/explprod.test, src/tgbatest/tripprod.test,
src/evtgbatest/explicit.test: Do not reorder the output.
It's pointless since 2005-01-20.
 2005-01-31 17:24:42 +00:00
Alexandre Duret-Lutz
885097ae62 * configure.ac, NEWS: Bump version to 0.1a. 2005-01-31 13:01:08 +00:00
Alexandre Duret-Lutz
f07aba5ac3 * configure.ac, NEWS: Bump version to 0.1. 2005-01-31 12:54:47 +00:00
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