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

Commit graph

  • 88cd81c547 * src/misc/satsolver.cc: Report when SAT-solver terminate by signal. Alexandre Duret-Lutz 2013-09-04 16:20:51 +02:00
  • 22f944ad56 sat: catch write errors Alexandre Duret-Lutz 2013-09-04 13:58:40 +02:00
  • 1f3b7e8002 sat: catch cases where nbclause > INT_MAX and report them Alexandre Duret-Lutz 2013-09-03 10:34:50 +02:00
  • ba5bddec78 degen: use the initial state heuristic when entering SCCs Alexandre Duret-Lutz 2013-09-02 18:09:03 +02:00
  • 3eb993e224 postproc: make it possible to force sat-minimization Alexandre Duret-Lutz 2013-09-02 12:10:19 +02:00
  • 8e30fcd84b postproc: two fixes for sat-minimize Alexandre Duret-Lutz 2013-08-30 19:03:11 +02:00
  • 484c56c6ea sat: skip reference transitions that are out of any cycle Alexandre Duret-Lutz 2013-08-29 17:42:15 +02:00
  • e9f60df857 sat: implement partial symmetry breaking Alexandre Duret-Lutz 2013-08-29 17:10:07 +02:00
  • 9cfe1a3496 tostring: add LaTeX output Alexandre Duret-Lutz 2013-08-28 18:52:59 +02:00
  • 90c106f8a8 sat: generalize the code for reading the solution Alexandre Duret-Lutz 2013-08-28 15:24:16 +02:00
  • 1ab46b0864 postproc: Add option to output Complete automata. Alexandre Duret-Lutz 2013-08-26 15:46:51 +02:00
  • b31facffb1 * NEWS: Summarize recent changes Alexandre Duret-Lutz 2013-08-26 14:38:10 +02:00
  • 7a7ed8a632 rename dba_complement() to dtgba_complement() Alexandre Duret-Lutz 2013-08-26 14:00:04 +02:00
  • fdb157bf94 satmin: cleanup interfaces and minimization loops Alexandre Duret-Lutz 2013-08-22 15:49:30 +02:00
  • b09ef5bea9 postproc: disable WDBA-minimization on request Alexandre Duret-Lutz 2013-08-21 17:53:01 +02:00
  • bfbe5b448b stats: add %r to display run-time Alexandre Duret-Lutz 2013-08-21 16:30:26 +02:00
  • 4dd8d80292 isdet: simplify is_deterministic(), add is_complete(). Alexandre Duret-Lutz 2013-08-21 14:23:11 +02:00
  • bcd794c608 sat: improve our algorithms Alexandre Duret-Lutz 2013-08-20 18:27:35 +02:00
  • 1029d08a77 ltlcross: Complement deterministic automata. Alexandre Duret-Lutz 2013-08-18 22:37:25 +02:00
  • 2dda2c9122 minimize_obligation: can complement the input TGBA if deterministic Alexandre Duret-Lutz 2013-08-18 00:58:01 +02:00
  • 3b10bb3b8c satsolver: new function Alexandre Duret-Lutz 2013-07-19 17:59:28 +02:00
  • 6ce005b2d0 * .gitignore: More files to ignore. Alexandre Duret-Lutz 2013-07-19 15:08:59 +02:00
  • 679df4eee1 Implement dtgba_sat_minimize(). Alexandre Duret-Lutz 2013-07-17 10:14:00 +02:00
  • 260ab53cb5 * src/tgba/tgbatba.cc: Register the variables of the source automaton. Alexandre Duret-Lutz 2013-05-22 17:48:12 +02:00
  • 84dabae374 Add some test of the SAT-based minimization. Alexandre Duret-Lutz 2013-05-16 17:58:35 +02:00
  • b679adadf9 postproc: Add a sat-minimize option. Alexandre Duret-Lutz 2013-05-10 18:29:02 +02:00
  • d9f3ca71c0 dtbasat: implement dba_sat_minimize() Alexandre Duret-Lutz 2013-07-18 22:29:06 +02:00
  • 3fd49da159 complete: new algorithm for TGBAs Alexandre Duret-Lutz 2013-02-22 18:01:32 +01:00
  • 78e76eb07d dbacomp: connect only back-links and generalize to tgba Alexandre Duret-Lutz 2013-02-03 00:16:32 +01:00
  • 63b7cdb6c8 tba_determinize: add a cycle_threshold Alexandre Duret-Lutz 2013-01-22 18:53:45 +01:00
  • 0117fc2c36 postproc: use tba_determinize_check() Alexandre Duret-Lutz 2013-01-21 19:18:14 +01:00
  • 07ab225cc4 dba_determinize: Add a threshold argument. Alexandre Duret-Lutz 2013-07-17 10:35:23 +02:00
  • 4ac6468bfc Implement tba_determinize_check(), following Dax et al. (ATVA'07). Alexandre Duret-Lutz 2013-01-21 16:01:45 +01:00
  • bd2e78c1ed Introduce a dba_complement() function. Alexandre Duret-Lutz 2013-01-21 14:45:44 +01:00
  • ec5bbf4fcf Implementent tba_determinize(), based on Dax et al (ATVA'07). Alexandre Duret-Lutz 2013-01-21 11:14:08 +01:00
  • 29bc087d56 reachiter: fix the DFS, and add a version with on_stack() Alexandre Duret-Lutz 2013-02-01 08:26:59 +01:00
  • 57f712fcbd ltlcross: Allow %D, %N, or %T to be used multiple time Alexandre Duret-Lutz 2013-08-19 16:23:44 +02:00
  • f704513b6b org: document dstar2tgba. Alexandre Duret-Lutz 2013-08-19 15:42:08 +02:00
  • d561dfb7e0 * src/bin/ltlcross.cc: Use dstar_to_tgba(). Alexandre Duret-Lutz 2013-08-17 14:37:32 +02:00
  • d7027c34d3 dstar: Improve conversion from DRA to BA. Alexandre Duret-Lutz 2013-08-17 13:10:41 +02:00
  • c58bfbd2ee * src/kripkeparse/Makefile.am: Add missing include directory. Alexandre Duret-Lutz 2013-08-16 23:36:18 +02:00
  • d3b81809c8 dstar2tgba: new command. Alexandre Duret-Lutz 2013-08-16 20:21:30 +02:00
  • 9a7590a646 dstar: implement dra_to_dba() Alexandre Duret-Lutz 2013-08-16 17:01:44 +02:00
  • ce0aec604c Introduce some masked tgba. Alexandre Duret-Lutz 2013-08-14 18:12:06 +02:00
  • 68ce9980d1 Introduce spot::state_set. Alexandre Duret-Lutz 2013-08-14 18:08:19 +02:00
  • d2560944b6 * src/tgbatest/ltl2tgba.cc: Accept reading LBTT files from stdin. Alexandre Duret-Lutz 2013-07-27 00:57:45 +02:00
  • 337aeefcc3 ltlcross: add support for ltl2dstar's output. Alexandre Duret-Lutz 2013-07-25 18:27:51 +02:00
  • 2da0053c53 dstarparse: Preliminary work on a parser for ltl2dstar. Alexandre Duret-Lutz 2013-07-24 19:16:18 +02:00
  • 5a3b1a9905 bitvect: implement a dynamic bit-vector class. Alexandre Duret-Lutz 2013-07-24 19:21:08 +02:00
  • dfc5ff95e5 degen: Improve when initial state is accepting without self-loop. Alexandre Duret-Lutz 2013-08-23 13:23:59 +02:00
  • 67a4833576 Fix --enable-optimization, not to reset CXXFLAGS. Alexandre Duret-Lutz 2013-08-21 23:05:18 +02:00
  • a30a59582c Fix builds for older versions of g++. Alexandre Duret-Lutz 2013-08-21 18:40:22 +02:00
  • e7522056ca ltlcross: give an example of accepted word for nonempty cross-products Alexandre Duret-Lutz 2013-07-20 18:55:45 +02:00
  • 4bafa4e1b0 tmpfile: Honor SPOT_TMPFILE and SPOT_TMPKEEP. Alexandre Duret-Lutz 2013-07-20 16:12:19 +02:00
  • 1bb5cbd90c Test driver for Teamcity. Alexandre Duret-Lutz 2013-07-21 13:00:22 +02:00
  • 9894b81775 ltlcross: use tmpfile. Alexandre Duret-Lutz 2013-07-17 00:05:38 +02:00
  • c0e7f9de58 gnulib: import module mkstemps Alexandre Duret-Lutz 2013-07-18 20:04:42 +02:00
  • 16b7206dd9 Fix gnulib to not replace gmtime() and localtime() Alexandre Duret-Lutz 2013-07-18 19:55:45 +02:00
  • 96f32c73fb Update to gnulib 312af25ba220ccff068245f0dc698e9bcc8f03f8 Alexandre Duret-Lutz 2013-07-18 17:27:53 +02:00
  • 904ff6a555 misc: Include config.h in *.cc files Alexandre Duret-Lutz 2013-07-18 15:00:29 +02:00
  • e7d09f4fd0 tmpfile: new module to create and keep track of temporary files. Alexandre Duret-Lutz 2013-07-17 00:03:50 +02:00
  • ab3a4f54c2 gnulib: add module stpcpy Alexandre Duret-Lutz 2013-07-17 11:35:43 +02:00
  • 5b0bf8ef09 ltlcross: Add a --color option. Alexandre Duret-Lutz 2013-05-17 14:04:09 +02:00
  • 35129e5a5a gnulib: Add modules argmatch and isatty. Alexandre Duret-Lutz 2013-05-17 11:39:42 +02:00
  • 542050bab4 * doc/Doxyfile.in: Hide private functions and member. Enable search. Alexandre Duret-Lutz 2013-07-10 13:05:30 +02:00
  • 7f31d70345 * src/tgbaalgos/cutscc.cc: Cosmetics. Alexandre Duret-Lutz 2013-07-10 08:34:34 +02:00
  • 26f48b1df2 * src/taalgos/tgba2ta.cc: Cosmetics. Alexandre Duret-Lutz 2013-07-10 08:27:40 +02:00
  • 92a3366488 * src/taalgos/minimize.cc: Cosmetics. Alexandre Duret-Lutz 2013-07-10 08:15:23 +02:00
  • f00d97b4ba Use the count_state() function instead of stats_reachable(). Alexandre Duret-Lutz 2013-07-10 07:57:24 +02:00
  • 43b3df0ef0 Use -fvisibility=hidden globally. Alexandre Duret-Lutz 2013-07-04 19:20:29 +02:00
  • f8cdaf0c12 gnulib: Upgrade and build as a libtool library. Alexandre Duret-Lutz 2013-07-04 18:56:29 +02:00
  • cee552689a [buddy] Probe for -fvisibility and -fvisibility-inlines-hidden. Alexandre Duret-Lutz 2013-07-04 18:46:07 +02:00
  • e4abcfddfc Add missing copyright blurbs to sanity tests. Alexandre Duret-Lutz 2013-06-29 09:58:30 +02:00
  • 17c31fdee2 * HACKING: Some doc on exporting symbols with SPOT_API. Alexandre Duret-Lutz 2013-06-29 00:39:26 +02:00
  • aeca44e0b1 Add a sanity check for installed private headers. Alexandre Duret-Lutz 2013-06-28 23:45:25 +02:00
  • cfbd31384f Use -fvisibility=hidden in src/ta/ and src/taalgos/. Alexandre Duret-Lutz 2013-06-28 18:39:17 +02:00
  • f53328a8c7 Use -fvisibility=hidden for all parsers. Alexandre Duret-Lutz 2013-06-28 18:28:35 +02:00
  • 8c2d7fcb7f Use the same location.hh and position.hh in all parsers. Alexandre Duret-Lutz 2013-06-28 18:12:10 +02:00
  • a0f5d53ea4 Use -fvisibility=hidden in src/tgbaalgos/. Alexandre Duret-Lutz 2013-06-28 17:34:20 +02:00
  • dab51a9dd0 Use -fvisibility=hidden in src/kripke/, src/saba/, and src/sabaalgos/ Alexandre Duret-Lutz 2013-06-26 23:09:53 +02:00
  • a12922b331 Use -fvisibility=hidden in src/tgba/. Alexandre Duret-Lutz 2013-06-26 22:46:23 +02:00
  • 8ba3e64f0a Use -fvisibility=hidden in src/ltlast/, src/ltlvisit/, and src/ltlenv/. Alexandre Duret-Lutz 2013-06-26 18:55:17 +02:00
  • cbfbf14297 * NEWS: summarize recent changes Alexandre Duret-Lutz 2013-06-25 11:35:20 +02:00
  • 1ed43038e8 Move bdd_allocator to src/priv/. Alexandre Duret-Lutz 2013-06-24 23:45:06 +02:00
  • 9775dfdd4b Hide the only use of bdd_allocator. Alexandre Duret-Lutz 2013-06-24 23:36:34 +02:00
  • 1581a94c65 * src/misc/unique_ptr.hh: Add missing operator->() const. Alexandre Duret-Lutz 2013-06-24 23:34:07 +02:00
  • 882097a2ce Remove modgray, it's not used. Alexandre Duret-Lutz 2013-06-24 21:59:52 +02:00
  • f2078ac325 Create a new src/priv/ directory for private algorithms. Alexandre Duret-Lutz 2013-06-24 20:55:40 +02:00
  • 2ef8917ba5 Enable -fvisibility=hidden for src/misc/. Alexandre Duret-Lutz 2013-06-24 21:39:22 +02:00
  • b5710663f4 [buddy] Restrict the number of exported symbols. Alexandre Duret-Lutz 2013-06-23 23:46:57 +02:00
  • 9ed2d7a1dc Bump version to 1.1.4a. Alexandre Duret-Lutz 2013-07-29 01:08:25 +02:00
  • 9d6d53ed92 Release Spot 1.1.4. Alexandre Duret-Lutz 2013-07-28 01:46:28 +02:00
  • ce6114f461 * THANKS: Jan should have been added earlier... Alexandre Duret-Lutz 2013-07-28 21:54:05 +02:00
  • cb7bdf8c1f Fix interpretation of {e[*]} and !{e[*]}. Alexandre Duret-Lutz 2013-07-28 21:04:10 +02:00
  • 4f986400f1 * src/bin/man/ltlcross.x: Typo. Alexandre Duret-Lutz 2013-07-27 12:23:22 +02:00
  • 027836f431 neverparse: accept more unparenthesised guards Alexandre Duret-Lutz 2013-07-26 12:02:04 +02:00
  • e598175fca neverparse: Remove superfluous %expect-rr in grammar. Alexandre Duret-Lutz 2013-07-26 11:51:30 +02:00
  • 734e203b65 ltlcross: missing newline in error message. Alexandre Duret-Lutz 2013-07-25 18:34:48 +02:00
  • 5046f6d9db * src/tgbaalgos/isweakscc.cc: Remove useless guards. Alexandre Duret-Lutz 2013-03-21 10:54:04 +01:00
  • 84c9f03767 neverpase: fix parsing of neverclaim produced by ltl2ba and ltl3ba Alexandre Duret-Lutz 2013-07-20 19:38:14 +02:00