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

Commit graph

  • 207735900d * src/tl/dot.cc: Fix assumption about call orders. Alexandre Duret-Lutz 2015-09-30 14:46:44 +02:00
  • 4a43e24afa * iface/ltsmin/kripke.test: Fix paths to test binaries. Alexandre Duret-Lutz 2015-09-30 11:08:34 +02:00
  • 0bbcd6e85e dupexp: rename to copy, and preserve named states on request Alexandre Duret-Lutz 2015-09-30 10:59:13 +02:00
  • dcb9d7e8a8 doxygen: improve formula documentation Alexandre Duret-Lutz 2015-09-29 22:59:05 +02:00
  • ca95e4d1d2 bddprint: do not store a global shared_ptr to the bdd_dict Alexandre Duret-Lutz 2015-09-29 19:59:02 +02:00
  • c67540db14 doc: more examples of the formula interface Alexandre Duret-Lutz 2015-09-28 23:17:04 +02:00
  • cb39210166 kill the ltl namespace Alexandre Duret-Lutz 2015-09-28 16:20:53 +02:00
  • 6ded5e75c4 merge ltlvisit/ ltlast/ ltlenv/ into a single tl/ directory Alexandre Duret-Lutz 2015-09-28 15:15:55 +02:00
  • 3e10dba978 python: work around old swig version Alexandre Duret-Lutz 2015-09-28 14:00:34 +02:00
  • 8b4ec5ded0 formula: rename the constants for consistency Alexandre Duret-Lutz 2015-09-27 22:47:17 +02:00
  • fad05632a2 python: implement the map and transform functions for formulas Alexandre Duret-Lutz 2015-09-27 22:02:49 +02:00
  • 2369389850 formula: replace nth() by operator[]() Alexandre Duret-Lutz 2015-09-27 21:06:24 +02:00
  • 533268000d python: implement __getitem__ for formula Alexandre Duret-Lutz 2015-09-27 20:36:07 +02:00
  • 5711d34489 formula: hide initializer lists from swig Alexandre Duret-Lutz 2015-09-27 20:35:21 +02:00
  • 96806681e0 simplify: save some work using a temporary variable. Alexandre Duret-Lutz 2015-09-27 17:58:41 +02:00
  • 3ad002be5f formula: speedup == and != Alexandre Duret-Lutz 2015-09-27 16:40:09 +02:00
  • 6a3c30951e ltl2tgba_fm: simplify some constant checks Alexandre Duret-Lutz 2015-09-27 10:35:57 +02:00
  • 1729a79ac7 nullptr cleanup for -Wzero-as-null-pointer-constant Alexandre Duret-Lutz 2015-09-26 22:14:27 +02:00
  • 51a3cfcede product: add a product_or variant Alexandre Duret-Lutz 2015-09-26 19:14:08 +02:00
  • b77f7e24c3 revamp the formula hierarchy (montro-patch) Alexandre Duret-Lutz 2015-09-24 19:44:00 +02:00
  • 1628b188fe Remove useless register_propositions method Etienne Renault 2015-09-24 14:19:48 +02:00
  • 11b9ada2bb Ease atomic proposition manipulation for twa. Etienne Renault 2015-07-21 17:30:56 +02:00
  • 953181bbb7 parseaut: store names from states in the dstar format Alexandre Duret-Lutz 2015-09-09 01:07:16 +02:00
  • a26dd5af1d parseaut: better recovery from dstar errors Alexandre Duret-Lutz 2015-09-09 00:44:39 +02:00
  • 6f99829a1d help git --status by ignoring more files Alexandre Duret-Lutz 2015-09-09 00:12:11 +02:00
  • 3b72826e6d parseaut: better error recovery for dstar automata Alexandre Duret-Lutz 2015-09-08 00:51:04 +02:00
  • 17a18f2890 adjust documentation for the merge of the dstar parser Alexandre Duret-Lutz 2015-09-07 22:46:39 +02:00
  • c59e994a2c parseaut: support multiple dstar automata Alexandre Duret-Lutz 2015-09-07 22:27:07 +02:00
  • 209e89a94c parseaut: swallow the dstarparser Alexandre Duret-Lutz 2015-09-07 09:25:44 +02:00
  • e7ecab93ff dstarparse: preparation before merge with parse_aut Alexandre Duret-Lutz 2015-09-06 18:44:54 +02:00
  • 5098c91bd4 parseaut: fix typo in error message Alexandre Duret-Lutz 2015-09-06 17:23:19 +02:00
  • 14c0577650 parseaut: keep track of the format of each parsed automaton Alexandre Duret-Lutz 2015-09-06 17:07:32 +02:00
  • 6079b1dcdf sanity: soften the class.*{ check Alexandre Duret-Lutz 2015-09-07 22:52:39 +02:00
  • 767e0522c9 tl: fix two typo in the bibliography Alexandre Duret-Lutz 2015-09-06 16:38:19 +02:00
  • 3378d72a88 dtgbasat: add a colored option Alexandre Duret-Lutz 2015-09-03 17:26:55 +02:00
  • 6b3de8afa0 * tools/man2html.pl: Fix copyright. Alexandre Duret-Lutz 2015-08-26 23:27:42 +02:00
  • 1f17b59360 debian: add licenses for lib/* Alexandre Duret-Lutz 2015-08-26 18:27:15 +02:00
  • 22974c7b7b * configure.ac, NEWS: Bump version to 1.99.3a. Alexandre Duret-Lutz 2015-08-26 18:05:21 +02:00
  • 5498f1335a Release Spot 1.99.3 Alexandre Duret-Lutz 2015-08-26 08:14:53 +02:00
  • 1fc3bf1a1a * doc/org/index.org: Avoid a "download it here" link. Alexandre Duret-Lutz 2015-08-25 23:30:48 +02:00
  • 05cfbaad1f * doc/org/install.org: Suggest using the stable packages with Ubuntu. Alexandre Duret-Lutz 2015-08-25 23:28:31 +02:00
  • daf5a2be05 org: link to tl.pdf Alexandre Duret-Lutz 2015-08-25 23:23:11 +02:00
  • 0dbdff59b8 * NEWS: Fix some typos. Alexandre Duret-Lutz 2015-08-25 23:07:44 +02:00
  • c2f0a5f02c Fix bitvect.test. Alexandre Duret-Lutz 2015-08-25 22:51:25 +02:00
  • 0510e4dfe8 ltlcross: recover from out-of-memory during state-space product Alexandre Duret-Lutz 2015-08-24 00:23:51 +02:00
  • 63969b13fa Fix spurious uniq.test failure. Alexandre Duret-Lutz 2015-08-23 17:38:30 +02:00
  • c8df1ae85d * doc/org/ltldo.org: Another typo. Alexandre Duret-Lutz 2015-08-21 23:17:08 +02:00
  • 596de181be * doc/org/ltldo.org: Improve English. Alexandre Duret-Lutz 2015-08-21 22:11:10 +02:00
  • 782edb9a69 * src/ltlvisit/unabbrev.cc: Missing break. Alexandre Duret-Lutz 2015-08-21 17:35:46 +02:00
  • 8d38587da8 * NEWS: mention the translate() typo. Alexandre Duret-Lutz 2015-08-21 16:06:29 +02:00
  • 308833788b unabbreviate: enable removal of R Alexandre Duret-Lutz 2015-08-21 16:02:52 +02:00
  • 0b8c418c94 * wrap/python/spot.py: Typo. Alexandre Duret-Lutz 2015-08-21 11:23:11 +02:00
  • 9c922252a6 * src/tests/ltl2dstar.test: Fix for recent change to ltlcross. Alexandre Duret-Lutz 2015-08-21 10:51:29 +02:00
  • 60bd1400c3 * NEWS: summarize recent changes. Alexandre Duret-Lutz 2015-08-20 23:20:33 +02:00
  • 7615a57dab dstar2tgba: rewrite using common_aoutput Alexandre Duret-Lutz 2015-08-20 22:54:40 +02:00
  • f831f729e1 homogenize dstar_parse() and parse_aut() outputs Alexandre Duret-Lutz 2015-08-20 22:33:25 +02:00
  • 62f5b9769b remove algorithms that where only used by dstar's dra2ba conversion Alexandre Duret-Lutz 2015-08-20 21:31:07 +02:00
  • 9b5340b90a dstarparse: get rid of the deticated data structures and conversions Alexandre Duret-Lutz 2015-08-20 19:50:03 +02:00
  • 5f0b6dc36c remfin: deal with almost-Rabin automata Alexandre Duret-Lutz 2015-08-20 16:47:30 +02:00
  • ef1bbfc659 remfin: make sure Rabin automata are always converted to Büchi Alexandre Duret-Lutz 2015-08-20 13:40:10 +02:00
  • 4bef219d8f remfin: implement the BA-type check Alexandre Duret-Lutz 2015-08-19 18:23:31 +02:00
  • 8a3a07d8a4 * doc/tl/tl.tex: Refine note about {r} vs. r in PSL. Alexandre Duret-Lutz 2015-08-19 14:20:17 +02:00
  • c5541a2189 * src/twaalgos/mask.hh: Cleanup comments. Alexandre Duret-Lutz 2015-08-19 11:00:01 +02:00
  • 5f76f34607 * doc/tl/tl.bib: Properly quote PSL. Alexandre Duret-Lutz 2015-08-19 10:59:09 +02:00
  • 818b58ec70 ltl: allow \" and \\ in double-quoted atomic propositions Alexandre Duret-Lutz 2015-08-18 14:55:53 +02:00
  • 47824bead6 tl: reorganize section 5 Alexandre Duret-Lutz 2015-08-18 11:14:53 +02:00
  • ce9b2369ed more final keywords Alexandre Duret-Lutz 2015-08-18 09:46:13 +02:00
  • 0689aa165b silence diagnostics from gcc-snapshot Alexandre Duret-Lutz 2015-08-17 18:54:49 +02:00
  • 56cbc3c813 ltlfilt: add --unabbreviate Alexandre Duret-Lutz 2015-08-17 16:07:00 +02:00
  • d1f915c748 merge tunnabrev/lunnabrev/wmunabbrev into a single function Alexandre Duret-Lutz 2015-08-17 15:26:42 +02:00
  • 314a016547 * doc/org/spot.css: improve style for printing. Alexandre Duret-Lutz 2015-08-17 11:06:02 +02:00
  • 59202bd5de do not rewrite <-> and -> for Spin LTL output Alexandre Duret-Lutz 2015-08-14 17:28:01 +02:00
  • ac6b042e2c remove a GCC 4.6 workaround Alexandre Duret-Lutz 2015-08-14 15:34:28 +02:00
  • 304f2496ea bdddict: remove register_clone_acc Alexandre Duret-Lutz 2015-08-14 15:16:26 +02:00
  • c50d5a82ac fix a spurious assertion Alexandre Duret-Lutz 2015-08-14 14:13:57 +02:00
  • 0143f0d435 sccsimpl: Remove Fin sets between SCCs Alexandre Duret-Lutz 2015-08-14 11:31:25 +02:00
  • 2eab0344b9 fix latex escaping Alexandre Duret-Lutz 2015-08-13 17:25:00 +02:00
  • 21ff2d0415 org: Add link to the Python notebooks. Alexandre Duret-Lutz 2015-08-13 16:44:31 +02:00
  • 868cabe4f6 * src/bin/man/ltlcross.x: Document %N, %T, %H. Alexandre Duret-Lutz 2015-08-13 15:56:00 +02:00
  • 546304eabc * doc/org/spot.css: Add padding at the bottom of man pages. Alexandre Duret-Lutz 2015-08-13 15:34:53 +02:00
  • b8445846ce * tools/man2html.pl: Fix interlinking of man pages. Alexandre Duret-Lutz 2015-08-13 15:34:30 +02:00
  • 490b0b1584 * doc/org/tools.org: Add links to man pages. Alexandre Duret-Lutz 2015-08-13 15:14:04 +02:00
  • 288a4ff33c * src/bin/man/ltl2tgba.x: Remove superfluous directory. Alexandre Duret-Lutz 2015-08-13 15:13:44 +02:00
  • d2c0105224 * HACKING: Mention that we now need groff. Alexandre Duret-Lutz 2015-08-13 12:05:18 +02:00
  • 3897c8dc9a org: include the man pages in the generated userdoc Alexandre Duret-Lutz 2015-08-13 00:33:24 +02:00
  • f7b65001e9 man: improve typesetting and prepare for html output Alexandre Duret-Lutz 2015-08-12 19:13:45 +02:00
  • 5b75ad5abd fix detection of ipython Alexandre Duret-Lutz 2015-08-08 16:44:52 +02:00
  • 29fc0f5caa org: use optipng to compress png files Alexandre Duret-Lutz 2015-08-07 18:23:54 +02:00
  • 659dfe95e1 org: cleanup css files Alexandre Duret-Lutz 2015-08-07 16:28:37 +02:00
  • 86e16af97c debian: Distribute the html version of the ipython notebooks Alexandre Duret-Lutz 2015-08-07 14:20:32 +02:00
  • fb8a16ffcc * wrap/python/ajax/spotcgi.in: Output .hoa as text/x-hoa. Alexandre Duret-Lutz 2015-08-07 12:06:01 +02:00
  • be847372de * NEWS: Summarize recent changes. Alexandre Duret-Lutz 2015-08-07 11:21:55 +02:00
  • 62fb48ea6e cgi: add a HOA output Alexandre Duret-Lutz 2015-08-07 11:19:12 +02:00
  • 33afd9f0e2 cgi: Display a message for weak TGBA. Alexandre Duret-Lutz 2015-08-07 10:49:32 +02:00
  • 7efe8c1c6c cgi: force transition-based acceptance output for TGBA Alexandre Duret-Lutz 2015-08-07 10:42:34 +02:00
  • 254910ed7c * wrap/python/ajax/trans.html: Remove some debugging statements. Alexandre Duret-Lutz 2015-08-07 10:30:33 +02:00
  • c0b77b2e62 cgi: do not display Inf(0) for state-based BA Alexandre Duret-Lutz 2015-08-06 16:29:55 +02:00
  • 3edd55fcd5 print_hoa: diagnose unknown options Alexandre Duret-Lutz 2015-07-24 23:23:55 +02:00
  • 5cd8c1b8cc * src/twa/twasafracomplement.cc: Remove two unused methods. Alexandre Duret-Lutz 2015-07-23 18:05:32 +02:00
  • e76596e1bf acc: fix detection of generalized-Rabin Alexandre Duret-Lutz 2015-07-23 17:53:58 +02:00