alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Commit graph

  • f22b5ae371 * configure.ac: Switch to Automake 1.11 and enable color-tests. Alexandre Duret-Lutz 2009-08-28 17:29:59 +02:00
  • 43ba3f8378 [buddy] configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and add an AC_CONFIG_MACRO_DIR call. Alexandre Duret-Lutz 2009-08-28 17:01:01 +02:00
  • 9eecd6aed5 * configure.ac: Switch from Libtool 1.5.x to Libtool 2.x, and add an AC_CONFIG_MACRO_DIR call. * m4/libtool.m4, tools/ltmain.sh: Remove. Alexandre Duret-Lutz 2009-08-28 17:00:50 +02:00
  • b19ea79f43 Add TGBA union implementation. Félix Abecassis 2009-07-30 16:02:59 +02:00
  • afeaf287e9 * m4/intel.m4: Fix to support the cache. Guillaume Sadegh 2009-07-09 21:29:50 +02:00
  • fd9ec01743 * src/tgba/tgbacomplement.cc: Stay on 80 columns. Guillaume Sadegh 2009-07-08 18:09:21 +02:00
  • 414956c51e Add 2 benchmarks directories. Add an algorithm to split an automaton in several automata. Félix Abecassis 2009-07-06 17:27:16 +02:00
  • a160b3504b * src/tgba/tgbacomplement.cc: Fix the transformation from Streett to TGBA. * src/tgbatest/complementation.test: Modify tests. Guillaume Sadegh 2009-07-07 14:07:52 +02:00
  • 9c7201c3b1 * bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.0. Alexandre Duret-Lutz 2009-06-17 16:28:00 +02:00
  • b3e8797c51 [lbtt] Adjust to support the Intel compiler (icpc). Guillaume Sadegh 2009-06-12 16:20:08 +02:00
  • bf925aaeeb [buddy] Adjust to support the Intel compiler (icc). Guillaume Sadegh 2009-06-12 16:17:44 +02:00
  • 7ac816f38e Adjust the build system for ICC. Guillaume Sadegh 2009-06-12 16:14:05 +02:00
  • d1cf819540 Kill a g++-4.2 warning. Alexandre Duret-Lutz 2009-06-11 18:35:01 +02:00
  • e0a8114f06 During the complementation, transform the auxiliary Streett automaton into a TGBA instead of a TBA. Guillaume Sadegh 2009-06-07 17:22:46 +02:00
  • 4d4fc641b5 * src/tgba/tgbacomplement.cc, src/tgbatest/complementation.cc: Fix style. Guillaume Sadegh 2009-06-09 18:59:53 +02:00
  • 7817f325eb More files to ignore. Guillaume Sadegh 2009-06-07 18:38:56 +02:00
  • 3a3e5d4bff * src/tgba/tgbacomplement.cc (state_complement::hash): Improve the hash function. Guillaume Sadegh 2009-06-07 18:26:26 +02:00
  • 8fe11196bd * src/eltlparse/eltlparse.yy: Fix a memory leak. * src/eltltest/nfa.cc: Adjust. * src/tgbaalgos/eltl2tgba_lacim.cc: Fix a memory leak. Damien Lefortier 2009-06-09 21:18:43 +02:00
  • 78f8f1640c Remove generated files that git follows. Guillaume Sadegh 2009-04-15 21:00:51 +02:00
  • c5f8eafb01 Add an algorithm to complement Büchi automata. Guillaume Sadegh 2009-02-24 15:01:29 +01:00
  • e48338e8d8 Modify the ELTL parser to be able to support PSL operators. Add a new keyword in the ELTL format: finish, which applies to an automaton operator and tells whether it just completed. Damien Lefortier 2009-06-05 01:17:19 +02:00
  • 4de885afb1 * src/tgbatest/scc.test: Redirect stdout into file stdout' instead of out', to conform to other tests, and add a missing call to diff. Alexandre Duret-Lutz 2009-06-02 17:30:52 +02:00
  • a40f362e99 Introduce some experimental kripke classes to simplify writing interfaces. Alexandre Duret-Lutz 2009-06-02 17:26:49 +02:00
  • a2b6bef003 * src/tgbatest/scc.test: New file. * src/tgbatest/Makefile.am: Adjust. * src/tgbaalgos/scc.hh: More documentation. * src/tgbaalgos/scc.cc (scc_recurse): Fix computation of acc_paths and dead_paths. Prevent recursions in states that have already been visited. Alexandre Duret-Lutz 2009-06-02 15:47:01 +02:00
  • 642c2b1a71 Lift the SCC computation off future_condition_collectors, into a new tgba_scc class. Alexandre Duret-Lutz 2009-05-31 21:46:05 +02:00
  • 2cc7c253f1 [lbtt] Adjust parser to Bison 2.4.1. Alexandre Duret-Lutz 2009-05-31 21:26:25 +02:00
  • 352984293a Test "ltl2tgba -FC" and plug the memory leaks of scc_map. Alexandre Duret-Lutz 2009-05-28 18:18:00 +02:00
  • d74578ef6e Implement spot::future_conditions_collector. Alexandre Duret-Lutz 2009-05-28 17:42:52 +02:00
  • a375972f5c * src/tgbaalgos/scc.cc (dump_scc_dot): Use a bit vector instead of a map to track visited SCC since they are sequentially numbered. Alexandre Duret-Lutz 2009-05-28 16:22:41 +02:00
  • 15b3b9e07d Number states using negative values and SCCs using nonnegative values. Alexandre Duret-Lutz 2009-05-28 14:02:42 +02:00
  • 96a7a49c52 Store the scc_map_ as a vector instead of a std::map. There is no point in using a map since the SCC are numbered in sequence. Alexandre Duret-Lutz 2009-05-28 13:32:36 +02:00
  • 07ead6134e Keep track of conditions in SCC, and add a more verbose dump. Alexandre Duret-Lutz 2009-05-28 13:08:20 +02:00
  • cbfdcca1f9 Fix assertion in scc.cc Alexandre Duret-Lutz 2009-05-28 11:45:16 +02:00
  • 6142441f01 * src/tgba/tgba.hh (format_state): s/automata who/automata that/. * src/evtgba/evtgba.hh (format_state): Likewise. * src/evtgba/product.hh (format_state): Likewise. Alexandre Duret-Lutz 2009-05-26 23:15:52 +02:00
  • b06c9cd563 Extend the ELTL parser to support more complex aliases of automaton operators such as Strong=G(F($0))->G(F($1)) and G=R(false, $0). Damien Lefortier 2009-04-18 16:24:18 +02:00
  • bbbc1acc14 Minor fixes to compile with GCC 4.4. Guillaume Sadegh 2009-04-09 17:14:32 +02:00
  • 7643c49cbd Correct LaCIM for ELTL and make it work with LBTT. Damien Lefortier 2009-04-08 19:57:27 +02:00
  • 355461ae99 Extend the ELTL parser to support basic aliases of automaton operators such as F=U(true,$0) or R=!U(!$0,!$1), and infix notation for binary automaton operators. Damien Lefortier 2009-04-04 21:54:01 +02:00
  • 2fbcd7e52f Add support for ELTL (AST & parser), and an adaptation of LaCIM for ELTL. This is a new version of the work started in 2008 with LTL and ELTL formulae now sharing the same class hierarchy. Damien Lefortier 2009-03-02 17:31:12 +01:00
  • 90332d8d77 * src/evtgbaparse/evtgbaparse.yy: Stay on 80 columns. Alexandre Duret-Lutz 2009-03-25 17:43:55 +01:00
  • efbdc08d9f Update parsers to work with Bison 2.4.1. Alexandre Duret-Lutz 2009-03-25 17:11:33 +01:00
  • 1f6087953b Also revert b28d7ba804 as it was a follow-up to Damien's work. Alexandre Duret-Lutz 2009-03-25 17:26:25 +01:00
  • 70b6bcf8eb * src/tgbaalgos/scc.hh: Add missing misc/hash.hh inclusion. Alexandre Duret-Lutz 2009-03-25 16:36:23 +01:00
  • b1bfdee870 Revert everything related to Damien's work in 2008 (he will commit a new version soon). Alexandre Duret-Lutz 2009-03-25 13:58:18 +01:00
  • 3d278663cd typo Alexandre Duret-Lutz 2009-02-23 19:06:46 +01:00
  • ab8b2cbceb typos Alexandre Duret-Lutz 2009-02-23 15:05:52 +01:00
  • 6e4110fabb Typos Alexandre Duret-Lutz 2009-02-18 09:59:41 +01:00
  • 33652acd62 Update to compile with GCC 4.4.0 (trunk). Guillaume Sadegh 2008-12-18 23:49:01 +01:00
  • 1d58493be3 Update to compile with the Intel compiler. Guillaume SADEGH 2008-12-07 02:31:15 +01:00
  • 7998fff056 Compute more statistics about SCCs. Alexandre Duret-Lutz 2008-12-11 13:06:58 +01:00
  • b2f7c2d76d Fix tracking of SCCs on the search stack Alexandre Duret-Lutz 2008-12-11 12:56:34 +01:00
  • c44d6277f2 Introduce scc.cc to compute SCC stats and map. Alexandre Duret-Lutz 2008-12-05 12:04:31 +01:00
  • d5235c6901 Add option -k to ltl2tgba Alexandre Duret-Lutz 2008-12-05 11:21:38 +01:00
  • d1ca1e31aa Add missing bench/gspn-ssp/README file to the repository Alexandre Duret-Lutz 2008-12-02 11:30:40 +01:00
  • 6a2cfc43d5 Fix and simplify the generation of the gspn-ssp Makefile Alexandre Duret-Lutz 2008-08-29 17:06:05 +02:00
  • e6904d0a4c Use the TMPDIR variable in the gspn-ssp benchmark Alexandre Duret-Lutz 2008-08-29 17:02:24 +02:00
  • 0b1f869891 minor gspn-ssp/tools/sum tweaks Alexandre Duret-Lutz 2008-08-29 16:28:24 +02:00
  • 111b408da4 Add bench/gspn-ssp/README Alexandre Duret-Lutz 2008-08-27 17:15:48 +02:00
  • 360a5729be Have bench/gspn-ssp/tools/sum working directly from the *.log files, and improve its output. Alexandre Duret-Lutz 2008-08-27 16:04:34 +02:00
  • 56d1dbc610 Build the benchmark in bench/gspn-ssp/ using makefiles Alexandre Duret-Lutz 2008-08-08 10:26:21 +02:00
  • b83349d416 more files to ignore Alexandre Duret-Lutz 2008-08-07 15:41:24 +02:00
  • 40c4476ce4 Keep track of the number of inclusions detected in ssp_semi Alexandre Duret-Lutz 2008-08-18 17:19:19 +02:00
  • 35bf9b5345 bench/gspn-ssp/: New directory. Alexandre Duret-Lutz 2008-08-07 15:37:57 +02:00
  • d3b5e5bdad Add option -e54 to ltlgspn-ssp Alexandre Duret-Lutz 2008-08-07 14:10:28 +02:00
  • 8c0d1003b0 Start the ELTL translation (LACIM). Merge all eltlast/ files into formula.hh (except automatop.hh). Damien Lefortier 2008-06-18 15:11:25 +02:00
  • 862302590c Prefix bytecode filenames with $srcdir so the tests work in VPATH builds. Alexandre Duret-Lutz 2008-06-12 17:23:22 +02:00
  • b28d7ba804 adjust #includes in python/ Alexandre Duret-Lutz 2008-06-12 16:56:40 +02:00
  • 25a3114287 Merge all ltlast/ files into formula.hh. The forward declaration of visitor was causing error messages too cryptic for users. Alexandre Duret-Lutz 2008-06-12 16:31:59 +02:00
  • 9afbaf6342 Delete useless *.cc files in ltlast/ Alexandre Duret-Lutz 2008-06-12 14:28:29 +02:00
  • 994482ed2c dottynips.cc, emptiness_check.cc: Include ctsdlib for exit() Alexandre Duret-Lutz 2008-06-11 17:14:44 +02:00
  • dc0005f4e1 src/eltlparse/eltlparse.yy: Include limits.h for INT_MIN and INT_MAX. Alexandre Duret-Lutz 2008-06-11 17:01:42 +02:00
  • 34d81cd807 src/sanity/includes.test: Remove empty line at beginning of file. Alexandre Duret-Lutz 2008-06-11 16:58:44 +02:00
  • 9cadc24173 Remove the const qualifier from the return type of formula::hash(), GCC complains. Alexandre Duret-Lutz 2008-06-11 16:57:01 +02:00
  • 0129018b58 Fix the previous patch. Guillaume Sadegh 2008-06-11 16:14:51 +02:00
  • a33c1894c3 Test suite for the NipsVM front-end. Guillaume Sadegh 2008-06-10 03:34:40 +02:00
  • f56721107b src/sanity/includes.test (INCDIR): Remove any trailing slash. Alexandre Duret-Lutz 2008-06-03 12:45:17 +02:00
  • 40dc725116 Install interfaces' headers in the spot/iface/ directory, not directly in the spot/ directory. Alexandre Duret-Lutz 2008-06-03 12:44:09 +02:00
  • 664f84796f do not install nips VM Alexandre Duret-Lutz 2008-06-02 15:32:12 +02:00
  • 73b286cfcb factorize linking of libnipsvm.la Alexandre Duret-Lutz 2008-06-02 15:31:37 +02:00
  • ed589d8c5a more files to ignore Alexandre Duret-Lutz 2008-05-30 17:03:07 +02:00
  • ff134eb81e 2008-05-29 Guillaume SADEGH <sadegh@lrde.epita.fr> Guillaume Sadegh 2008-05-31 14:43:28 +02:00
  • a48a10e82e 2008-05-31 Guillaume SADEGH <sadegh@lrde.epita.fr> Guillaume Sadegh 2008-05-31 14:04:55 +02:00
  • bc5f13bb4e NIPS VM added to the SPOT distribution. Guillaume Sadegh 2008-04-02 17:43:54 +02:00
  • 543190f2bc Template ltlast/ & ltlenv/ classes in internal/ & Add ELTL parser. Damien Lefortier 2008-03-25 16:52:06 +01:00
  • 21c98c0a01 Kill some FIXMEs. Alexandre Duret-Lutz 2008-04-14 11:35:57 +02:00
  • 6b9acabe76 ignore libtool generated files Alexandre Duret-Lutz 2008-04-10 17:03:50 +02:00
  • 6c2bdf4512 Update to LBTT 1.2.1 Alexandre Duret-Lutz 2008-04-10 10:20:40 +02:00
  • 43c9c6faaa * src/evtgbaparse/Makefile.am (AM_CXXFLAGS): Remove -Werror so we tolerate more flex versions. * src/ltlparse/Makefile.am (AM_CXXFLAGS): Likewise. * src/tgbaparse/Makefile.am (AM_CXXFLAGS): Likewise. Alexandre Duret-Lutz 2008-03-28 17:22:23 +01:00
  • 323e326c7d Second thinko in #if/#else. Alexandre Duret-Lutz 2008-03-25 16:26:50 +01:00
  • 07fd0377e6 Thinko in #if/#else. Alexandre Duret-Lutz 2008-03-25 15:35:03 +01:00
  • b1ee7c64e7 typo Alexandre Duret-Lutz 2008-03-21 21:39:18 +01:00
  • b71360ae44 Avoid <iostream> in headers, better use <iosfwd>. Damien Lefortier 2008-03-21 21:59:34 +01:00
  • c764b2021d * src/tgbatest/ltl2tgba.cc, src/misc/hash.hh: Reformat the header using 80 columns. Alexandre Duret-Lutz 2008-03-21 17:02:57 +01:00
  • d3b702a97c Make sure Spot compiles with g++-4.3. Alexandre Duret-Lutz 2008-03-13 17:42:42 +01:00
  • f217ff374c * src/bddtest.cxx: Include <cstdlib> to compile with g++-4.3. Alexandre Duret-Lutz 2008-03-13 18:20:47 +01:00
  • ab1a2ae5d7 * src/main.cc: Include <climits> for LONG_MAX. lbtt won't compile with g++-4.3 otherwise. * src/Ltl-parse.yy (matchCharactersFromStream): Declare the chars as const to kill a g++ warning. * src/NeverClaim-parse.yy (yyerror): Declare the error message as const to kill a g++ warning. Alexandre Duret-Lutz 2008-03-13 11:28:18 +01:00
  • 5ef7084b61 Add .gitignore files Alexandre Duret-Lutz 2008-03-13 10:45:48 +01:00
  • c06c95c4f1 * doc/Doxyfile.in (LATEX_HIDE_INDICES): Do not generate indices until Doxygen is fixed. Doxygen 1.5.5 generate incorrect LaTeX code. Alexandre Duret-Lutz 2008-03-11 15:07:09 +01:00
  • 8c829cf3e1 * src/tgbaalgos/reachiter.hh: Typos in comments. Alexandre Duret-Lutz 2008-02-27 16:14:45 +01:00
  • cc9c08b6cf * src/tgba/tgbabddconcretefactory.hh (create_state): Clarify comments. Alexandre Duret-Lutz 2008-02-22 09:22:19 +00:00