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

54 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
eef27f4496 * src/tgbatest/randtgba.cc: Do not include <string> twice. 2010-01-21 14:55:01 +01:00
Alexandre Duret-Lutz
77df39b4dd Deprecate ltl::destroy(f) in favor of f->destroy() 
* src/ltlast/formula.cc, src/ltlast/formula.hh (formula::clone):
Transform this static function into a member function.
* src/ltlvisit/destroy.hh (destroy): Document and declare as
deprecated.
* bench/split-product/cutscc.cc, iface/gspn/ltlgspn.cc,
src/eltlparse/eltlparse.yy, src/eltltest/acc.cc,
src/evtgbaalgos/tgba2evtgba.cc, src/evtgbatest/ltl2evtgba.cc,
src/ltlast/automatop.cc, src/ltlast/binop.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
src/ltlenv/declenv.hh, src/ltlparse/ltlparse.yy,
src/ltltest/equals.cc, src/ltltest/randltl.cc,
src/ltltest/readltl.cc, src/ltltest/reduc.cc,
src/ltltest/syntimpl.cc, src/ltltest/tostring.cc,
src/ltlvisit/destroy.cc src/ltlvisit/basicreduce.cc,
src/ltlvisit/contain.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/tgba/bdddict.cc,
src/tgba/bddprint.cc, src/tgba/taa.cc,
src/tgba/tgbabddconcretefactory.cc, src/tgba/tgbaexplicit.cc,
src/tgba/tgbafromfile.cc, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/eltl2tgba.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/randtgba.cc,
src/tgbatest/reductgba.cc, wrap/python/cgi/ltl2tgba.in,
wrap/python/tests/ltl2tgba.py, wrap/python/tests/ltlparse.py,
wrap/python/tests/ltlsimple.py: Adjust destroy() usage, and remove
the #include "destroy.hh" when appropriate.
 2009-11-09 07:13:31 +01:00
Alexandre Duret-Lutz
b0888257f8 Rename formula::ref and formula::unref as formula::clone 
and formula::destroy.

* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/formula.hh, src/ltlast/formula.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlenv/declenv.cc,
src/ltlvisit/basicreduce.cc, src/ltlvisit/clone.cc,
src/ltlvisit/destroy.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/reduce.cc,
src/tgbatest/randtgba.cc: Adjust.
 2009-11-09 07:13:31 +01:00
Alexandre Duret-Lutz
b1bfdee870 Revert everything related to Damien's work in 2008 (he will commit a new version soon). 
Here are the reverted patches:
8c0d1003b0,
25a3114287,
9afbaf6342,
dc0005f4e1,
543190f2bc.
 2009-03-25 16:44:05 +01:00
Alexandre Duret-Lutz
25a3114287 Merge all ltlast/ files into formula.hh. The forward declaration of visitor was causing error messages too cryptic for users. 2008-06-12 16:33:03 +02:00
Alexandre Duret-Lutz
d3b702a97c Make sure Spot compiles with g++-4.3. 
* src/ltlast/formula.hh (hash): Remove const from return type.
This kills a g++-4.3 warning.
* src/misc/hash.hh: Adjust to use unordered_set and unordered_map
from TR1 when g++-4.3 is used.
* src/evtgba/product.cc, src/ltltest/randltl.cc,
src/ltlvisit/randomltl.cc, src/ltlvisit/tostring.cc,
src/misc/freelist.hh, src/misc/optionmap.cc,
src/tgba/tgbareduc.hh, src/tgbaalgos/gv04.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/randomgraph.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc,
src/ltltest/equals.cc, src/ltltest/readltl.cc,
src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
src/ltltest/tostring.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/powerset.cc, src/tgbatest/explprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc,
src/tgbatest/reductgba.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc, src/evtgbatest/product.cc,
src/evtgbatest/readsave.cc, src/evtgbatest/ltl2evtgba.cc,
src/evtgbatest/readsave.cc: Add missing includes.
* src/tgbatest/explicit.test, src/tgbatest/explprod.test,
src/tgbatest/explpro2.test, src/tgbatest/troprod.test,
src/tgbatest/emptchk.test: Cope with different outputs.
 2008-03-14 22:45:37 +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
b343e16b51 * src/tgbatest/randtgba.cc (default_algos): Test the "ordering" 
heuristic.
 2008-02-25 14:36:55 +01: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
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
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
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
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
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
516350ddc0 * src/tgbatest/randtgba.cc (main): Skip empty lines. 
(syntax): Categorize options.
 2005-02-01 13:19:11 +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
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
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
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
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
333ee43f00 * src/tgbatest/randtgba.cc: Add products with randomized formulae and 2005-01-12 18:38:25 +00:00
Denis Poitrenaud
3f2790061a * src/tgbatest/randtgba.cc: Typo. 2005-01-10 18:26:14 +00:00
Alexandre Duret-Lutz
6a0ab6c081 * src/tgbatest/randtgba.cc: Add option -P. 2005-01-10 17:22:25 +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
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
58aff37db9 * src/tgbatest/randtgba.cc: Add option -O, so we can profile each 
emptiness-check on its own.
 2004-12-16 21:49:46 +00:00
Denis Poitrenaud
0222c5e186 * src/misc/timer.cc, src/tgbatest/randtgba.cc: Format the statistics. 2004-12-10 18:15:20 +00:00
Alexandre Duret-Lutz
9782b822f0 * src/tgbaalgos/gtec/gtec.hh, src/tgbaalgos/gtec/gtec.cc 
(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;
 2004-12-10 16:16:38 +00:00
Alexandre Duret-Lutz
688587d700 * src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh 
(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.
 2004-12-08 15:39:15 +00:00
Alexandre Duret-Lutz
668666d246 * src/misc/timer.hh, src/misc/timer.cc: New files. 
* 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 (.*;;)'.
 2004-11-29 16:50:49 +00:00
Alexandre Duret-Lutz
e58743dbb7 * src/tgbaalgos/minimizerun.cc, src/tgbaalgos/minimizerun.hh 
(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.
 2004-11-29 10:01:08 +00:00
Alexandre Duret-Lutz
3c9f4c6d0d * src/tgbatest/emptchkr.test: Try degeneralized automata. 
* src/tgbatest/randtgba.cc (main): Pass the correct automaton to
minimize_run().
 2004-11-29 09:48:01 +00:00
Alexandre Duret-Lutz
896dc5afec * src/tgbatest/randtgba.cc (to_float): Use strtod() instead of 
strtof() to please Solaris 9.
 2004-11-28 19:42:10 +00:00
Alexandre Duret-Lutz
6724f4bfbb * src/tgbaalgos/minimizerun.hh, src/tgbaalgos/minimizerun.cc: New 
files.
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them/
* src/tgbatest/randtgba.cc, src/tgbatest/ltl2tgba.cc: Add option -m.
* src/tgbatest/emptchkr.test: Use -m.
 2004-11-26 23:54:53 +00:00
Denis Poitrenaud
15329c5618 * src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh, 
src/tgbaalgos/se05.cc, src/tgbaalgos/se05.hh,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.hh,
src/tgbaalgos/tau03opt.cc: Fix comments and debug traces

* src/tgbatest/randtgba.cc: Adjust names of algorithms.
 2004-11-25 14:40:17 +00:00
Alexandre Duret-Lutz
2143d6c4b6 * src/tgbatest/randtgba.cc: Add option -D. 2004-11-25 12:52:01 +00:00
Alexandre Duret-Lutz
6cce60bed7 * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh: New files, partly 
based on Thomas Martinez's src/tgbaalgos/tarjan_on_fly.cc and
src/tgbaalgos/tarjan_on_fly.hh former implementation.
* src/tgbaalgos/Makefile.am (libtgbaalgos_la_SOURCES,
tgbaalgos_HEADERS): Add them.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc: Bind the
new algorithm.
* src/tgbatest/emptchk.test: Test it.
 2004-11-22 16:57:31 +00:00
Denis Poitrenaud
0f15d28fe8 * src/tgbaalgos/emptiness_stats.hh, src/tgbaalgos/weight.cc, 
src/tgbaalgos/weight.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03opt.cc,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/status.cc,
src/tgbaalgos/gtec/status.hh, : Add emptiness check statistics
capability.
* src/tgbatest/randtgba.cc: Print these statistics.
* src/tgbatest/ltl2tgba.cc: tau03opt search can deal without acceptance
condition.
* src/tgbatest/emptchk.test: Test tau03opt search.
 2004-11-22 12:06:03 +00:00
Alexandre Duret-Lutz
8068a54e38 * src/tgbatest/randtgba.cc (main): Add options -z and -Z for statistics. 
(ce_stat): New struct.
 2004-11-18 19:05:41 +00:00