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

Commit graph

  • 6dd2749c25 delete two unused files Alexandre Duret-Lutz 2014-12-06 23:41:50 +01:00
  • d2597854c8 Merge branch 'master' into next Alexandre Duret-Lutz 2014-12-06 14:02:38 +01:00
  • 84902fd690 * NEWS, configure.ac: Bump version to 1.2.6a. Alexandre Duret-Lutz 2014-12-06 13:26:12 +01:00
  • 44b374d1b9 Release Spot 1.2.6. Alexandre Duret-Lutz 2014-12-06 12:35:05 +01:00
  • 8c9bca9405 * HACKING: Mention the new gitlab page and repository. Alexandre Duret-Lutz 2014-12-05 20:25:13 +01:00
  • ff03ab4f56 work around BSD sed not interpreting \r in s/$/\r/ Alexandre Duret-Lutz 2014-12-05 10:25:33 +01:00
  • 1156866630 simplify: remove an incorect SERE simplification Alexandre Duret-Lutz 2014-12-04 22:50:43 +01:00
  • 88da1ad84d work around BSD sed not interpreting \r in s/$/\r/ Alexandre Duret-Lutz 2014-12-05 10:25:33 +01:00
  • 7619a5a062 simplify: remove an incorect SERE simplification Alexandre Duret-Lutz 2014-12-04 22:50:43 +01:00
  • 2731c9be67 * src/tgbaalgos/hoaf.hh: Fix comment. Alexandre Duret-Lutz 2014-12-04 18:20:05 +01:00
  • a0d9268fda ltl: remove the useless Finish operator Alexandre Duret-Lutz 2014-12-04 17:48:42 +01:00
  • ad77145496 how: fix multi-line incomplete strings Alexandre Duret-Lutz 2014-12-04 09:55:00 +01:00
  • ebc3d64927 neverclaim: fix reporting of parse_boolean() errors Alexandre Duret-Lutz 2014-12-04 08:36:59 +01:00
  • d0525871ed neverclaim: fix parsing of aliased states Alexandre Duret-Lutz 2014-12-03 22:20:14 +01:00
  • e1bba50047 hoa: swallow the neverclaim parser Alexandre Duret-Lutz 2014-12-03 18:20:35 +01:00
  • bc9cb1e5bb * configure.ac: Prefer swig-3.0 when available. Alexandre Duret-Lutz 2014-10-28 23:53:04 +01:00
  • 39eefd0c6e * src/misc/random.cc: Declare the generator as static. Alexandre Duret-Lutz 2014-12-03 14:19:59 +01:00
  • c0e9891246 randomize: new function Alexandre Duret-Lutz 2014-12-03 14:16:45 +01:00
  • 0db0eca14e graph: store the source indices in the transition vector Alexandre Duret-Lutz 2014-12-02 20:16:06 +01:00
  • 80ce0e2129 satminimization: do not assume the initial state is 0 Alexandre Duret-Lutz 2014-12-02 20:14:57 +01:00
  • 5d8f16da99 countstates: remove unused file Alexandre Duret-Lutz 2014-12-01 17:51:57 +01:00
  • a95693906a bddop: remove unused file Alexandre Duret-Lutz 2014-12-01 17:48:39 +01:00
  • 202b960994 accconv, acccompl: remove unused files Alexandre Duret-Lutz 2014-12-01 17:38:22 +01:00
  • 12401fe91a ltlfile: remove unused file Alexandre Duret-Lutz 2014-12-01 17:34:13 +01:00
  • 4f1535c8fe defaultenv: simplify usage Alexandre Duret-Lutz 2014-11-30 19:53:14 +01:00
  • 946f7e80dd * src/bin/randltl.cc: Fix typos in examples. Alexandre Duret-Lutz 2014-11-29 15:45:16 +01:00
  • e6e416e1e1 document autfilt and randaut Alexandre Duret-Lutz 2014-11-29 18:03:56 +01:00
  • c5842c3a0a randaut: new binary Alexandre Duret-Lutz 2014-11-29 16:04:26 +01:00
  • 61dc1203ca * src/bin/randltl.cc: Fix typos in examples. Alexandre Duret-Lutz 2014-11-29 15:45:16 +01:00
  • 6400ec852b Add documentation for is_stutter_invariant. Thibaud Michaud 2014-11-17 12:04:45 +01:00
  • 10c4a92ddb python: fix spot.py script for new acceptance interface Alexandre Duret-Lutz 2014-11-27 19:09:06 +01:00
  • c494a347c9 stutter: fiddle with the benchmark Alexandre Duret-Lutz 2014-11-23 21:47:12 +01:00
  • 0beb148b6a * src/tgbaalgos/closure.cc: Fix invalid read. Alexandre Duret-Lutz 2014-11-23 21:45:20 +01:00
  • ad3ea61ac2 Adding README in bench/stutter/. Thibaud Michaud 2014-11-17 09:57:26 +01:00
  • 94854ac7be Adding ipython notebook to visualize stutter-invariance benchmarks. Thibaud Michaud 2014-11-14 14:33:13 +01:00
  • 0250a32747 export a create_atomic_prop_set() function Alexandre Duret-Lutz 2014-11-26 10:27:59 +01:00
  • f08a26f7b9 hoa: rename hoaf_reachable() to hoa_reachable() Alexandre Duret-Lutz 2014-11-25 22:02:59 +01:00
  • 5b5c5edcf8 * src/ltlparse/ltlscan.ll: Mark as non-interactive. Alexandre Duret-Lutz 2014-11-25 21:46:27 +01:00
  • ef5b0417e7 hoa: fix handling of escaped characters in atomic propositions Alexandre Duret-Lutz 2014-11-25 11:37:29 +01:00
  • 2a71517f5c hoa: more coverage for the parser Alexandre Duret-Lutz 2014-11-25 14:28:03 +01:00
  • 12389adf4f hoa: check parsing from stdin Alexandre Duret-Lutz 2014-11-25 11:52:42 +01:00
  • fa2ad77078 hoa: test DOS-style input Alexandre Duret-Lutz 2014-11-25 11:44:58 +01:00
  • 0d59e55f4d hoa: fix handling of escaped characters in atomic propositions Alexandre Duret-Lutz 2014-11-25 11:37:29 +01:00
  • a9fa7d33c5 autfilt: diagnose non-existant files Alexandre Duret-Lutz 2014-11-25 08:59:26 +01:00
  • e7e21ae58f hoa: improve parser and scanner Alexandre Duret-Lutz 2014-11-25 08:51:55 +01:00
  • 0a21db5c30 * NEWS: Mention the HOA parser. Alexandre Duret-Lutz 2014-11-21 16:26:54 +01:00
  • 1c8b58d69f hoa: add some error recovery Alexandre Duret-Lutz 2014-11-21 17:43:17 +01:00
  • 4043ad2ccf hoa: diagnose unsupported Headers Alexandre Duret-Lutz 2014-11-21 16:39:33 +01:00
  • 8004dca157 hoa: add support for multiple initial states Alexandre Duret-Lutz 2014-11-21 16:05:28 +01:00
  • 63abfed108 ltlcross: report aborted HOA files Alexandre Duret-Lutz 2014-11-21 15:21:23 +01:00
  • c12b2d63b3 hoa: add support for --ABORT-- Alexandre Duret-Lutz 2014-11-21 15:03:11 +01:00
  • 8c8c2f0b7c hoa: allocate the states once, after parsing the header Alexandre Duret-Lutz 2014-11-21 14:00:19 +01:00
  • 71d21b378b hoa: support Inf(!x) Alexandre Duret-Lutz 2014-11-21 13:37:25 +01:00
  • 7a03228880 hoa: add alias support Alexandre Duret-Lutz 2014-11-21 11:05:24 +01:00
  • 691ab05926 hoa: catch redefinition of states Alexandre Duret-Lutz 2014-11-21 10:49:58 +01:00
  • 69678152b6 hoa: add support for unlabeled transitions Alexandre Duret-Lutz 2014-11-20 19:44:56 +01:00
  • 1d962f79ac hoa: make the parser more resilient to errors Alexandre Duret-Lutz 2014-11-20 12:29:18 +01:00
  • 392c527d31 monitor: add a few tests Alexandre Duret-Lutz 2014-11-20 10:59:56 +01:00
  • 6eeb74e15f autfilt, dstar2tgba: fix --help Alexandre Duret-Lutz 2014-11-20 10:02:29 +01:00
  • 131299d03e hoa: make it possible to read a stream of automata Alexandre Duret-Lutz 2014-11-19 18:50:51 +01:00
  • 5aff262844 autfilt: first stub Alexandre Duret-Lutz 2014-11-19 17:46:44 +01:00
  • fb0849f43b * src/bin/dstar2tgba.cc: Remove a useless include. Alexandre Duret-Lutz 2014-11-19 16:54:12 +01:00
  • 622fe08f00 ltlcross: add support for reading TGBA as HOA Alexandre Duret-Lutz 2014-11-19 16:38:14 +01:00
  • e55bcd95aa hoa: preliminary implementation of a parser Alexandre Duret-Lutz 2014-11-18 18:48:36 +01:00
  • e1d4522ca9 hoa: fix output Alexandre Duret-Lutz 2014-11-18 18:51:58 +01:00
  • f8cf2aa9b3 fix line number tracking in files with DOS newlines Alexandre Duret-Lutz 2014-11-18 11:07:02 +01:00
  • 45e9b96b66 fix line number tracking in files with DOS newlines Alexandre Duret-Lutz 2014-11-18 11:07:02 +01:00
  • 881afd67ba * NEWS: Mention the new stutter invariance check Alexandre Duret-Lutz 2014-11-14 13:23:30 +01:00
  • d92ca23da3 * src/ltltest/remove_x.test: More tests. Alexandre Duret-Lutz 2014-11-12 19:03:32 +01:00
  • 9effca6907 Remove the stutter test from tgbatest/. Alexandre Duret-Lutz 2014-11-12 18:41:22 +01:00
  • f412fee6f3 stutter check: cleanup and add test cases Alexandre Duret-Lutz 2014-11-12 18:29:54 +01:00
  • fcf6e25132 Optimizing closure and sl. Thibaud Michaud 2014-10-29 10:47:52 +01:00
  • 5817a3c11b Remove const qualifier in translator::run return type Thibaud Michaud 2014-10-29 11:00:48 +01:00
  • 37bcb5d959 Adding tgba-based stutter-invariance checking Thibaud Michaud 2014-10-01 12:58:16 +02:00
  • beafcf4e3d Adding trans_storage methods to tgbagraph.hh Thibaud Michaud 2014-10-29 14:15:06 +01:00
  • c9618f9137 random_graph: add option to generate complete deterministic automaton Thibaud Michaud 2014-10-13 16:36:57 +02:00
  • 24d60edc84 Adding option to filter by number of atomic propositions in ltlfilt. Thibaud Michaud 2014-10-16 23:59:34 +02:00
  • b012621357 * NEWS: Mention the std::set assignment workaround. Alexandre Duret-Lutz 2014-11-14 08:38:16 +01:00
  • 11aa708a81 ltl2tgba_fm: fix non-deterministic output Alexandre Duret-Lutz 2014-11-13 18:03:15 +01:00
  • becfcbcf79 * NEWS: Mention the std::set assignment workaround. Alexandre Duret-Lutz 2014-11-14 08:38:16 +01:00
  • 6e2151dc18 futurecondcol: avoid gcc-snapshot bug Alexandre Duret-Lutz 2014-11-13 23:41:07 +01:00
  • 4ea63f8404 ltl2tgba_fm: fix non-deterministic output Alexandre Duret-Lutz 2014-11-13 18:03:15 +01:00
  • 2745381097 tgbasafracomplement: avoid some std::set copies Alexandre Duret-Lutz 2014-10-31 11:47:03 +01:00
  • 63da386a66 ltl: use "final" and "override" in the AST classes Alexandre Duret-Lutz 2014-10-28 23:39:08 +01:00
  • 6f572ebcc8 * configure.ac: Prefer swig-3.0 when available. Alexandre Duret-Lutz 2014-10-28 23:53:04 +01:00
  • b8a792248a tgbasafracomplement: avoid some std::set copies Alexandre Duret-Lutz 2014-10-31 11:47:03 +01:00
  • ad8d24222a buddy: rename libbdd to libbddx Alexandre Duret-Lutz 2014-10-30 17:29:27 +01:00
  • f35be908c8 tgba_digraph: speedup purge_unreachable_states slightly Alexandre Duret-Lutz 2014-10-30 09:59:57 +01:00
  • f0fd654c1f misc: define SPOT_LIKELY and SPOT_UNLIKELY Alexandre Duret-Lutz 2014-10-30 09:58:12 +01:00
  • 923785f76a tgba_digraph: add a copy constructor, and obsolete dupexp Alexandre Duret-Lutz 2014-10-28 18:47:19 +01:00
  • 971788fdbe [buddy] pack cache entry on 16 bytes, not 20. Alexandre Duret-Lutz 2014-10-28 09:57:55 +01:00
  • c189875daf ltl: get rid of formula_ptr_hash Alexandre Duret-Lutz 2014-10-26 21:42:28 +01:00
  • 3d9ffaec83 fix compilation with clang++-3.6 -Wdocumentation Alexandre Duret-Lutz 2014-10-26 20:50:38 +01:00
  • 15710e7b1d lib: remove the gethrxtime module Alexandre Duret-Lutz 2014-10-26 13:58:29 +01:00
  • a4f951facc timer: add a stopwatch for timing a simple operation Alexandre Duret-Lutz 2014-10-26 13:44:47 +01:00
  • 8d947a8782 ltl: get rid of ltl::ref_formula Alexandre Duret-Lutz 2014-10-25 16:47:44 +02:00
  • d79da2e941 ltl: rename formula::count_ as formula::serial_. Alexandre Duret-Lutz 2014-10-25 01:11:26 +02:00
  • 2553c29ca7 tgba_digraph: add a purge_dead_states() method Alexandre Duret-Lutz 2014-10-24 00:37:18 +02:00
  • 09242d3f78 org: compatibility with org 8 Alexandre Duret-Lutz 2014-10-24 10:47:49 +02:00
  • 63708ddcc7 org: compatibility with org 8 Alexandre Duret-Lutz 2014-10-24 10:47:49 +02:00