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

11 commits

Author SHA1 Message Date
Guillaume Sadegh
d037008cdc * src/ltltest/randltl.cc, src/ltltest/reduc.test, 
src/tgbatest/dfs.test: Adjust headers to 80 columns.
 2009-10-01 00:32:06 +02:00
Alexandre Duret-Lutz
058bb83c6d Fix a memory leak in randltl. 
* src/ltltest/randltl.cc: Free the atomic properties from AP
before exit.
 2009-09-07 14:35:35 +02: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
5b6e79ad96 * src/tgbaalgos/ndfs_result.hxx (ndfs_result::construct_prefix): 
Initialize tmp to suppress a GCC 4.0 warning.
* src/ltltest/randltl.cc (main): Likewise with another variable.
 2008-02-25 14:36:55 +01:00
Denis Poitrenaud
81423bb743 * src/ltltest/randltl.cc: Typo. 2005-01-11 12:37:43 +00:00
Denis Poitrenaud
86b7f26960 * src/tgbaparse/tgbaparse.yy: Accept automaton without state. 
* src/ltltest/randltl.cc: Typo.
 2005-01-11 12:27:37 +00:00
Denis Poitrenaud
603b49e216 * src/ltltest/randltl.cc: Include cassert. 
* src/tgbaalgos/ndfs_result.hxx: Implement the spot::acss_statistics
interface.
* src/tgbaalgos/magic.cc, src/tgbaalgos/se05.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc: Add to each heap class a method returning its
size.
 2005-01-06 15:54:48 +00:00
Alexandre Duret-Lutz
174b531f82 * src/ltltest/randltl.cc: Add options -r and -u. 
* src/ltltest/reduc.test: Use randltl -u, and run it through valgrind.
 2005-01-06 12:29:56 +00:00
Alexandre Duret-Lutz
e366b081a8 * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: New files. 
* src/ltlvisit/Makefile.am (ltlvisit_HEADERS,
libltlvisit_la_SOURCES): Distribute them.
* src/ltltest/randltl.cc: New file.
* src/ltltest/Makefile.am (LDADD): Link with ../libspot.la directly.
(noinst_PROGRAMS, randltl_SOURCES): New.
(EXTRA_DIST, CLEANFILES): The list of random formulae is now generated.
* src/ltltest/formulae.txt: Delete.
* src/ltltest/reduc.test: Use randltl to generate formulae.
* src/ltlvisit/length.cc (length_visitor): Fix computation
of the length of multops.
* src/ltlvisit/length.hh (length): Document the length of multops.
 2005-01-05 16:20:21 +00:00