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

589 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
3b693c5ca7 * configure.ac: Call AC_LIBTOOL_WIN32_DLL 
* src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined.
 2004-07-23 09:07:49 +00:00
Alexandre Duret-Lutz
89db9aa512 * src/Makefile.am (libbdd_la_LDFLAGS): Add -no-undefined. 2004-07-23 09:06:54 +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
f84dd2e72c * configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal 
definition visible even to non-GNU compilers.
 2004-07-19 08:54:37 +00:00
Alexandre Duret-Lutz
85d2b7b287 * configure.ac: Call AC_GNU_SOURCE to make glibc's strsignal 
definition visible even to non-GNU compilers.
 2004-07-16 16:25:38 +00:00
Alexandre Duret-Lutz
b4eda5e84d * m4/gccwarn.m4: Do not check nor use -Wstrict-prototypes. 
g++-3.4 complains it makes no sense in C++.
 2004-07-16 14:38:44 +00:00
Alexandre Duret-Lutz
bec7402a67 * iface/gspn/ssp.cc: Typos. 2004-07-16 11:52:19 +00:00
Alexandre Duret-Lutz
44ebe5a746 * iface/gspn/gspn.cc (tgba_succ_iterator_gspn::tgba_succ_iterator_gspn): 
Set size_ to 1 when stuttering is needed, so that done() does not
return true immediately.
 2004-07-16 11:19:28 +00:00
Alexandre Duret-Lutz
7abc2604f3 * examples/bddcalc/parser.yxx (actionSeq, varlist): Rewrite as 
left-recursive rules.
 2004-07-12 14:03:53 +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
c534bac478 * doc/footer.html: New file, link to RefDocComments on the wiki. 
* doc/Doxyfile.in (HTML_FOOTER): Use footer.html.
* doc/Makefile.am (EXTRA_DIST): Add footer.html.
 2004-07-09 14:51:56 +00:00
Alexandre Duret-Lutz
61a5ec760e typos 2004-07-09 13:08:42 +00:00
Alexandre Duret-Lutz
0f304df2ed * THANKS: Fill in. 2004-07-09 13:06:33 +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
cfdd81a919 Initial revision 2004-07-07 16:40:50 +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
Alexandre Duret-Lutz
f1c3af808f Merge BuDDy 2.3. 
* examples/calculator/, examples/internal/: Were renamed as ...
* examples/bddcalc/, examples/bddtest/: ... these.
* configure.ac: Adjust version and output Makefiles.
* examples/Makefile.am (SUBDIRS): Adjust subdir renaming.
* examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were
renamed as ...
* examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these.
* examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust
accordingly.
* src/Makefile.am (AM_CPPFLAGS): Define VERSION.
 2004-07-06 17:39:37 +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
Alexandre Duret-Lutz
7ff3898139 * configure.ac, NEWS: Bump version to 0.0w. 2004-06-29 18:24:17 +00:00
Alexandre Duret-Lutz
31b163dbf8 * configure.ac, NEWS: Bump version to 0.0v. 2004-06-29 18:22:13 +00:00
martinez
8be67c1976 * src/tgbatest/reduccmp.test: Bug. 
* src/tgbatest/reductgba.test: More Test.

* src/tgbatest/ltl2tgba.cc: Adjust ...
* src/tgbaalgos/reductgba_sim_del.cc, src/tgbaalgos/reductgba_sim.hh,
src/tgbaalgos/reductgba_sim.cc: try to optimize.

* src/tgba/tgbareduc.hh, src/tgba/tgbareduc.cc: Scc reduction
and we remove some acceptance condition in scc which are not accepting.
* src/ltlvisit/syntimpl.cc : Some case wasn't detect.
* src/ltlvisit/basicreduce.cc: Case FGa || FGb = F(Ga | Gb) added.
* src/ltltest/syntimpl.test: More Test.
* src/ltltest/syntimpl.cc: Put the formula in negative normal form.
 2004-06-28 15:53:20 +00:00
Alexandre Duret-Lutz
acee9e75a4 * buddy/: Merge buddy-2-3. 2004-06-28 15:25:13 +00:00
Alexandre Duret-Lutz
aa4a582f1b Merge BuDDy 2.3. 
* examples/calculator/, examples/internal/: Were renamed as ...
* examples/bddcalc/, examples/bddtest/: ... these.
* configure.ac: Adjust version and output Makefiles.
* examples/Makefile.am (SUBDIRS): Adjust subdir renaming.
* examples/cmilner/milner.c, examples/fdd/statespace.cxx: Were
renamed as ...
* examples/cmilner/cmilner.c, examples/fdd/fdd.cxx: ... these.
* examples/cmilner/Makefile.am, examples/fdd/Makefile.am: Adjust
accordingly.
* src/Makefile.am (AM_CPPFLAGS): Define VERSION.
 2004-06-28 15:22:11 +00:00
Alexandre Duret-Lutz
805b6fb70b Initial revision 2004-06-28 14:19:59 +00:00
Alexandre Duret-Lutz
0f79043b2a * src/tgbatest/ltl2tgba.cc (main): Degeneralize before 
the simulations.
 2004-06-25 11:33:48 +00:00
Alexandre Duret-Lutz
e9fd27e892 * src/ltlvisit/tostring.cc (is_bare_word): New function. 
(to_string_visitor::visitor(const atomic_prop*)): Use is_bare_word
to better check which atomic proposition need to be quoted.
* src/ltlparse/ltlscan.ll: Do not allow identifiers starting with F_
or G_.
* src/ltltest/equals.test, src/ltltest/tostring.test: More tests.
 2004-06-23 11:36:03 +00:00
Alexandre Duret-Lutz
3802528bfd * src/tgba/tgbatba.cc (tgba_tba_proxy::format_state): Use 
bdd_format_accset to print the acceptance condition part of the state.
That produces more readable output.
 2004-06-23 08:51:32 +00:00
Alexandre Duret-Lutz
bd69b16e46 * wrap/python/cgi/ltl2tgba.in: Add "Formula Simplications" options. 
* wrap/python/spot.i: Wrap src/ltlvisite/reduce.hh.
 2004-06-23 08:28:50 +00:00
Alexandre Duret-Lutz
b42cdc0d8f * src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh: New files, 
extracted from ...
* src/ltlvisit/lunabbrev.cc: ... this one, which now work as documented
again.
* src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc: Adjust to call
simplify_f_g() in addition to unabbreviate_logic().
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
Add simpfg.cc and simpfg.hh.
 2004-06-23 08:09:19 +00:00
Alexandre Duret-Lutz
839837a69e more files to ignore 2004-06-22 22:58:09 +00:00
Alexandre Duret-Lutz
98604c754f * src/ltlvisit/reducform.hh, src/ltlvisit/reducform.cc: Rename to ... 
* src/ltlvisit/reduce.hh, src/ltlvisit/reduce.cc: ... this, to match
the function name.
* ltltest/equals.cc, ltltest/reduc.cc, ltlvisit/Makefile.am,
tgbatest/ltl2tgba.cc, tgbatest/reductgba.cc: Adjust filenames.
 2004-06-22 22:54:35 +00:00
Alexandre Duret-Lutz
473af5bb1d * src/ltlvisit/basicreduce.cc (basic_reduce_visitor::visit(binop*)): 
Factorize.
 2004-06-22 22:48:34 +00:00
Alexandre Duret-Lutz
47e9ac108f * src/ltlvisit/basicreduce.hh: New file, extracted from ... 
* src/ltlvisit/reducform.hh: ... here.
* src/ltlvisit/basereduc.cc: Rename as ...
* src/ltlvisit/basicreduce.cc: ... this, to match the function name.
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS, libltlvisit_la_SOURCES):
Adjust filenames.
* src/ltlvisit/reducform.cc: Adjust includes.
 2004-06-22 22:27:53 +00:00
Alexandre Duret-Lutz
a57c619ed5 * src/ltlvisit/lunabbrev.hh: Revert superfluous change from 
2004-05-10.
 2004-06-22 22:06:28 +00:00
martinez
2f1a67d927 * src/ltlvisit/reducform.cc, src/tgba/tgbareduc.cc, 
src/tgbaalgos/reductgba_sim.cc, src/tgbaalgos/reductgba_sim.hh
src/tgbaalgos/reductgba_sim_del.cc, src/tgbatest/reduccmp.test,
src/tgbatest/reductgba.cc: 80 columns and style.
 2004-06-22 17:24:46 +00:00
Alexandre Duret-Lutz
f61b69ef3d * src/sanity/style.test: Typo. 2004-06-22 17:12:14 +00:00
martinez
eb0852257f * src/tgbatest/ltl2tgba.cc, src/tgbaalgos/reductgba_sim_del.cc, 
src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
bug in delayed simulation.

* src/tgbatest/reduccmp.test, src/tgbatest/reductgba.test,
src/tgba/tgbareduc.cc: bug in scc reduction.
 2004-06-22 15:30:12 +00:00
martinez
6d5593ae48 * src/tgbatest/reductgba.test, src/tgba/tgbareduc.cc: 
There is bug in reduction with scc.
* src/tgbatest/reduccmp.test: More test.

* src/tgbatest/reductgba.test: Wrong test are removed.
 2004-06-21 12:15:19 +00:00
martinez
f680eb0d80 * src/tgbatest/reductgba.test, src/ltltest/reduccmp.test: Wrong test are removed. 2004-06-17 17:00:29 +00:00
martinez
cc93a6d6ac * src/ltltest/reduccmp.test: Wrong test are removed. 2004-06-17 16:48:22 +00:00
martinez
c769f74750 * src/tgbatest/spotlbtt.test: We don't check the post-reduction 
with scc and delayed simulation.

* src/tgbatest/ltl2tgba.cc: Adjust parameters.
* src/tgbatest/reductgba.cc, src/tgbatest/Makefile.am: More Test.
* src/tgbaalgos/reductgba_sim_del.cc: Not finish, lot of bugs.
* src/tgbaalgos/reductgba_sim.hh, src/tgbaalgos/reductgba_sim.cc:
Remove some useless comments.
* src/tgba/tgbareduc.cc, src/tgba/tgbareduc.hh: Bug in SCC.

* src/ltlvisit/reducform.cc: Correct some bug for multop.
* src/ltltest/reduccmp.test: More Test.
* src/ltltest/reduc.cc: Thinko
* src/ltltest/equals.cc: Reduction compare
 2004-06-17 16:27:36 +00:00
Alexandre Duret-Lutz
84e72c8764 * iface/gspn/ssp.cc (emptiness_check_shy_ssp::find_state): Free s. 
This fixes a memory leak observed by Soheib Baarir.
 2004-06-17 09:07:36 +00:00
martinez
525c8918ca * src/tgbatest/reductgba.cc, src/tgbatest/reductgba.test: Test for 
reduction of tgba.
 2004-06-16 09:31:43 +00:00