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

612 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
7819f14db2 * src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files. 
Cannot test them because the run returned by the emptiness checks
are currently incomplete (they lack the acceptance conditions, and
sometimes even the labels in the prefix).
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run
when the emptiness checks are fixed.
 2004-10-28 12:10:12 +00:00
Alexandre Duret-Lutz
6c815004c4 Introduce an emptiness-check interface, and modify the existing 
algorithms to conform to it, uniformly.  This will unfortunately
break third-party code that were using these algorithms.
* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
* src/tgbaalgos/Makefile.am: New files.
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
conform to the new emptiness-check interface.
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
Likewise.  The classes have been renamed are as following
  emptiness_check -> couvreur99_check
  emptiness_check_shy -> couvreur99_check_shy
  counter_example -> couvreur99_check_result
* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
iface/gspn/ssp.cc: Adjust to renaming and new interface.
 2004-10-27 16:47:54 +00:00
Alexandre Duret-Lutz
7010a02cd9 * src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh: 
New files.
* src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS,
libevtgbaalgos_la_SOURCES): Add them.
* src/evtgbatest/ltl2evtgba.cc, src/evtgbatest/ltl2evtgba.test:
New files.
* src/evtgbatest/Makefile.am (check_PROGRAMS, TESTS): Add them.
(ltl2evtgba_SOURCES): New variable.
 2004-10-27 11:18:13 +00:00
Alexandre Duret-Lutz
b89f1e252e * src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Do not assert 
that the true state has only one link when unobs is used.
 2004-10-27 11:13:52 +00:00
Alexandre Duret-Lutz
0864d1ca1e * src/evtgbatest/Makefile.am (CLEANFILES): New variable. 2004-10-23 07:49:08 +00:00
Alexandre Duret-Lutz
73ff928b6f Preliminary support for Event-based GBA. 
* src/evtgba/Makefile.am, src/evtgba/evtgba.cc,
src/evtgba/evtgba.hh, src/evtgba/evtgbaiter.hh,
src/evtgba/explicit.cc, src/evtgba/explicit.hh,
src/evtgba/product.cc, src/evtgba/product.hh,
src/evtgba/symbol.cc, src/evtgba/symbol.hh,
src/evtgbaalgos/Makefile.am, src/evtgbaalgos/dotty.cc,
src/evtgbaalgos/dotty.hh, src/evtgbaalgos/reachiter.cc,
src/evtgbaalgos/reachiter.hh, src/evtgbaalgos/save.cc,
src/evtgbaalgos/save.hh, src/evtgbaparse/Makefile.am,
src/evtgbaparse/evtgbaparse.yy, src/evtgbaparse/evtgbascan.ll,
src/evtgbaparse/fmterror.cc, src/evtgbaparse/parsedecl.hh,
src/evtgbaparse/public.hh, src/evtgbatest/Makefile.am,
src/evtgbatest/defs.in, src/evtgbatest/explicit.cc,
src/evtgbatest/explicit.test, src/evtgbatest/product.cc,
src/evtgbatest/product.test, src/evtgbatest/readsave.cc,
src/evtgbatest/readsave.test: New files.
* configure.ac: Create the Makefiles in these new subdirectories.
* src/Makefile.am: Recurse them.
 2004-10-22 16:22:31 +00:00
Alexandre Duret-Lutz
d9b29a0590 * src/misc/bareword.hh, src/misc/bareword.cc (quote_unless_bare_word): 
New function.
 2004-10-22 16:06:55 +00:00
Alexandre Duret-Lutz
38f7cac8dd * src/ltlvisit/tostring.cc (to_spin_string_visitor): Move to 
anonymous namespace.
 2004-10-22 12:29:13 +00:00
Alexandre Duret-Lutz
55b84b1a48 * src/misc/modgray.hh (loopless_modular_mixed_radix_gray_code::done, 
loopless_modular_mixed_radix_gray_code::last): Declare as const.
 2004-10-20 16:04:06 +00:00
Alexandre Duret-Lutz
4defec66b4 * src/misc/bareword.hh, src/misc/bareword.cc: New files. 
* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.
 2004-10-20 15:50:52 +00:00
Alexandre Duret-Lutz
094ddca665 * src/misc/modgray.hh, src/misc/modgray.cc: New files. 
* src/misc/Makefile.am (libmisc_la_SOURCES, misc_HEADERS): Add them.
* wrap/python/spot.i: Activate directors, and interface modgray.hh.
* wrap/python/tests/modgray.py: New file.
* wrap/python/tests/Makefile.am (TESTS): Add it.
 2004-10-20 15:46:56 +00:00
Alexandre Duret-Lutz
7d27fd3796 * iface/gspn/gspn.cc, src/ltlvisit/basicreduce.cc, 
src/ltlvisit/destroy.cc, src/ltlvisit/dotty.cc,
src/ltlvisit/dump.cc, src/ltlvisit/length.cc,
src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc,
src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc,
src/tgba/formula2bdd.cc, src/tgba/tgbabddconcreteproduct.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/dotty.cc,
src/tgbaalgos/dupexp.cc, src/tgbaalgos/lbtt.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/neverclaim.cc,
src/tgbaalgos/save.cc, src/tgbaalgos/stats.cc,
src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh:
Declare private classes and helper function in anonymous namespaces.
* HACKING, src/sanity/style.test: Document and check this.
Also check for trailing { after namespace or class.
* src/ltlast/predecl.hh, src/ltlast/visitor.hh,
src/tgba/tgbareduc.hh: Fix trailing {.
 2004-10-18 13:56:31 +00:00
Alexandre Duret-Lutz
5176caf4d2 * src/tgbaalgos/gtec/ce.cc: Reinstall change from 2004-09-21. 2004-10-15 13:33:50 +00:00
Alexandre Duret-Lutz
ed6db92642 Back out all Thomas's changes on emptiness checks since 
2004-08-23.  Some of these will need to be reintegrated more
slowly and cleanly.

* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am,
src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert.
* src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh,
src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh,
src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh,
src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh:
Delete.
 2004-10-15 10:33:55 +00:00
Alexandre Duret-Lutz
01987350b7 * src/ltltest/reduc.test: Do source ./defs. Revert mistaken 
change from 2004-09-13.
 2004-10-14 12:57:12 +00:00
Alexandre Duret-Lutz
2a2c630bfa * src/tgbatest/explicit.test: Typo. 2004-10-14 12:21:48 +00:00
Alexandre Duret-Lutz
e8e2bec243 The computation of the counter example fails the valgrind tests 
and is wrong into two ways: the search stack is generally not a
path, and does not run until the end of the STL container.
Remove it.
* src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh
(tarjan_on_fly): Do not inherit from the emptiness_search class,
because the check method will no longer return a counter example.
(tarjan_on_fly::check): Return only a boolean.
(tarjan_on_fly::build_counter): Delete.
* src/tgbatest/ltl2tgba.cc: Adjust.
 2004-10-13 17:39:27 +00:00
Alexandre Duret-Lutz
ca27267c69 * src/tgba/tgbaexplicit.cc (tgba_explicit_succ_iterator::current_state, 
tgba_explicit_succ_iterator::current_condition,
tgba_explicit_succ_iterator::current_accepting_conditions): Assert
the iteration is not finished.
 2004-10-13 14:32:05 +00:00
Alexandre Duret-Lutz
8b3bfaacdb * src/sanity/style.test: Suggest using "x->y", not "(*x).y". 
* src/tgbaalgos/tarjan_on_fly.cc: Fix.
 2004-09-27 14:57:37 +00:00
Alexandre Duret-Lutz
3f2cba6304 * src/sanity/style.test: Suggest ++i over i++ when it does not 
matter, for consistency.
* src/tgbaalgos/tarjan_on_fly.cc, iface/gspn/ssp.cc,
src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/minimalce.cc, src/tgba/tgbareduc.cc: Adjust.
 2004-09-23 12:20:10 +00:00
Alexandre Duret-Lutz
3780650ea0 * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): New unobs argument. 
* src/tgbaalgos/ltl2tgba_fm.cc (ltl_to_tgba_fm): Handle unobs.
* src/tgbatest/ltl2tgba.cc (syntax, main): New -U option.
 2004-09-23 11:56:43 +00:00
Alexandre Duret-Lutz
a59b9aa7f4 * src/tgbaalgos/colordfs.hh, src/tgbaalgos/minimalce.cc, 
src/tgbaalgos/minimalce.hh, src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/tarjan_on_fly.hh, src/tgbatest/ltl2tgba.cc: Rename
emptyness_search to emptiness_search.
 2004-09-21 15:19:26 +00:00
Alexandre Duret-Lutz
c30823f7be * src/sanity/style.test: Warn about places where size() is used 
instead of empty().
* src/misc/bddalloc.cc (bdd_allocator::extend): Use empty() rather
than size() when checking emptiness of lists.
* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/minimalce.cc,
src/ltlvisit/basicreduce.cc, src/ltlvisit/reduce.cc,
src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/misc/minato.cc: Likewise.
* src/ltlast/multop.cc (multop::instance): Call ->size() only once.
 2004-09-21 13:01:27 +00:00
martinez
314f51ac55 * src/tgbatest/emptchk.test 
src/tgbaalgos/tarjan_on_fly.hh,
src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh,
src/tgbaalgos/minimalce.cc: To correct a bug.
 2004-09-14 16:11:14 +00:00
martinez
ad71da0042 * src/ltltest/reduc.test (FICH): bad file name. 2004-09-14 11:51:56 +00:00
martinez
0e5ca8a586 * src/tgbaalgos/nesteddfsgen.hh src/tgbaalgos/nesteddfsgen.cc: 
New algorithm for emptiness check.
 2004-09-13 15:47:33 +00:00
martinez
5af687b2c8 * src/tgbatest/spotlbtt.test, 
src/tgbatest/reductgba.cc,
src/tgbatest/ltl2tgba.cc:
Add option for reduction of TGBA.

* src/tgbatest/emptchk.test, src/tgbaalgos/Makefile.am,
src/tgbaalgos/tarjan_on_fly.hh, src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh, src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh, src/tgbaalgos/minimalce.cc,
src/tgbaalgos/colordfs.hh, src/tgbaalgos/colordfs.cc:
Remove some bugs.

src/tgbaalgos/gtec/ce.cc:
Modification of construction of counter example.

* src/tgbaalgos/reductgba_sim.hh src/tgbaalgos/reductgba_sim.cc,
src/tgbaalgos/reductgba_sim_del.cc,
src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc:
Modification for delayed simulation.


* src/tgbaalgos/gtec/ce.hh,
* src/tgbatest/ltl2tgba.cc,
 2004-09-13 15:25:13 +00:00
martinez
2d1151e018 * src/tgbaalgos/tarjan_on_fly.hh, 
src/tgbaalgos/tarjan_on_fly.cc,
src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfs.cc,
src/tgbaalgos/minimalce.hh,
src/tgbaalgos/minimalce.cc,
src/tgbaalgos/colordfs.hh,
src/tgbaalgos/colordfs.cc: four new algorithms for emptyness check.

src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/ce.cc: Adapt the counter exemple for the ce
object in minimalce.hh.

src/tgbatest/ltl2tgba.cc,
src/tgbatest/emptchk.test,
src/tgbaalgos/Makefile.am: Add files for emptyness-check.


* src/tgbaalgos/reductgba_sim_del.cc: Restrict to degeneralize automata.
* src/tgba/tgbareduc.hh: src/tgba/tgbareduc.cc: Merge transition
for scc reduce.
 2004-08-23 12:48:33 +00:00
Alexandre Duret-Lutz
8f502a8e32 * src/tgbatest/ltl2tgba.cc (syntax): Typo. 2004-08-12 14:45:07 +00:00
Alexandre Duret-Lutz
59947d11cf * src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/ltl2tgba_lacim.hh: 
Typos in Doxygen comments.
 2004-08-11 09:05:27 +00:00
Alexandre Duret-Lutz
42fc2b772f * src/ltlvisit/apcollect.hh: Fix include guard. Report from Denis. 
* src/sanity/includes.test: Include files twice to check include
guards.
 2004-08-10 18:07:20 +00:00
Alexandre Duret-Lutz
11762deafc * src/tgbatest/ltl2tgba.cc (main): Fix another gcc warning in case 
assert() is disabled.
 2004-08-10 16:01:14 +00:00
Alexandre Duret-Lutz
7818321589 * src/Makefile.am (nodist_EXTRA_libspot_la_SOURCES): New variable, 
to force C++ linking.
 2004-08-10 15:52:21 +00:00
Alexandre Duret-Lutz
79ef47dbf1 * src/ltlvisit/apcollect.cc, src/ltlvisit/apcollect.hh: New files, 
based on code from <Denis.Poitrenaud@lip6.fr>.
* src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES, ltlvisit_HEADERS):
Add them.
 2004-08-09 16:55:08 +00:00
Alexandre Duret-Lutz
ad96e8fbad * iface/gspn/common.cc, iface/gspn/common.hh, 
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlparse/fmterror.cc, src/ltlparse/public.hh,
src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
src/ltlvisit/tostring.cc, src/ltlvisit/tostring.hh,
src/misc/escape.cc, src/misc/escape.hh, src/tgba/bdddict.cc,
src/tgba/bdddict.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh,
src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh,
src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/neverclaim.hh,
src/tgbaalgos/save.cc, src/tgbaalgos/save.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh,
src/tgbaparse/fmterror.cc, src/tgbaparse/public.hh: Include <iosfwd>
in headers, and prefer <ostream> in the body whenever possible.
* src/sanity/style.test, HACKING: Check and document this.
 2004-08-09 16:32:25 +00:00
Alexandre Duret-Lutz
6853977be2 * src/ltlast/allnodes.hh, src/ltlast/atomic_prop.hh, 
src/ltlast/binop.hh, src/ltlast/constant.hh,
src/ltlast/formula.hh, src/ltlast/multop.hh,
src/ltlast/predecl.hh, src/ltlast/refformula.hh,
src/ltlast/unop.hh, src/ltlast/visitor.hh: Use file to introduce
each file.
 2004-08-09 13:43:55 +00:00
Alexandre Duret-Lutz
576e00099d * src/tgbaalgos/ltl2tgba_fm.hh (ltl_to_tgba_fm): Document all 
parameters.
* src/tgbaalgos/ltl2tgba_lacim.hh (ltl_to_tgba_lacim): Likewise.
 2004-08-09 08:50:42 +00:00
Alexandre Duret-Lutz
9bdefd34e7 * configure.ac: Call AC_LIBTOOL_WIN32_DLL 
* src/Makefile.am (libspot_la_LDFLAGS): Add -no-undefined.
 2004-07-23 09:08:45 +00:00
Alexandre Duret-Lutz
f6174b7f5e * src/tgbatest/explicit.test: Do not use `-i', it's not needed 
and it is wrong to put it after `-e'.  Caught by Denis too.
 2004-07-22 14:26:51 +00:00
Alexandre Duret-Lutz
3ec8a99b24 * src/ltltest/reduc.test: Use test a = b' not test a == b'. 
Reported by <Denis.Poitrenaud@lip6.fr> (failure on Cygwin).
 2004-07-22 13:53:51 +00:00
Alexandre Duret-Lutz
df75d35a5a * src/tgbatest/defs.in (VALGRIND): Specify --tool=memcheck for 
compatibility with valgrind 2.1.x.
* src/ltltest/defs.in (VALGRIND): Likewise.
 2004-07-20 15:47:30 +00:00
Alexandre Duret-Lutz
4cbc1d8856 * src/tgbaalgos/gtec/gtec.hh: Typos in comments. 2004-07-12 11:16:12 +00:00
Alexandre Duret-Lutz
844b17a211 * src/tgba/state.hh (state_ptr_equal, state_ptr_hash): Fix Doxygen 
example.
 2004-07-09 15:17:41 +00:00
Alexandre Duret-Lutz
1aad1ffbfd * src/tgbaalgos/reductgba_sim.hh (parity_game_graph_delayed, 
reduc_tgba_sim): Fix warnings about Doxygen comment.
* src/ltlvisit/reduce.hh (reduce): Likewise.
 2004-07-09 15:12:35 +00:00
Alexandre Duret-Lutz
019bdef8ff * src/tgbatest/ltl2baw.pl: Do not use -T anymore. Fix comments. 2004-07-09 12:54:08 +00:00
Alexandre Duret-Lutz
3b85646638 lbtt 1.1.0 supports TGBAs, use that and remove old workarounds. 
* src/tgbaalgos/lbtt.cc (state_acc_pair, state_acc_pair_equal,
state_acc_pair_hash, acp_seen_map, todo_set, seen_map, fill_todo
lbtt_reachable): Remove.
(nonacceptant_lbtt_bfs): Rename as ...
(lbtt_bfs): ... this, and adjust to output acceptance conditions
on transitions.
(nonacceptant_lbtt_reachable): Rename as ...
(lbtt_reachable): ... this.
* src/tgbaalgos/lbtt.hh (nonacceptant_lbtt_reachable): Delete.
* src/tgbatest/ltl2tgba.cc: Suppress option "-T".
 2004-07-08 16:42:00 +00:00
Alexandre Duret-Lutz
59df610023 Patch from Heikki Tauriainen <heikki.tauriainen@hut.fi>. 
* src/tgbaalgos/gtec/ce.cc (counter_example::counter_example): Do
not parenthesize the type after the new operator (g++ 3.4 complains).
* src/tgbaalgos/dupexp.cc (dupexp_iter::process_state,
dupexp_iter::declare_state): Use this->automata_ instead of
automata_.    Local member automata_ inherited from template base
classes must be prefixed or g++ 3.4 will not look them
up (conforming to §14.6.2.3).
 2004-07-08 14:50:46 +00:00
Alexandre Duret-Lutz
e11da2e3af * lbtt/: Merge lbtt 1.1.0. 
* src/tgbatest/spotlbtt.test: Adjust config file syntax to
please lbtt 1.1.0.
 2004-07-07 17:41:42 +00:00
Alexandre Duret-Lutz
478844dad8 * src/tgbaalgos/gtec/gtec.hh (emptiness_check_shy::find_state): Add 
comments.
* iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Likewise.
Soheib and I had a hard time figuring why we did this...
 2004-07-07 12:00:11 +00:00
martinez
9ce6888872 * src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh, 
src/tgbaalgos/reductgba_sim.cc,	src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim_del.cc: Remove some comments.

* src/tgbatest/ltl2tgba.cc, src/tgbatest/reductgba.cc: Adjust ...
* src/tgbatest/spotlbtt.test: More test (delayed simulation)
 2004-07-05 16:03:26 +00:00