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

Commit graph

  • f40925f67b ltlcheck: disable timeout handling when kill() or alarm() are missing Alexandre Duret-Lutz 2012-10-14 12:49:26 +02:00
  • e46ae2799f ltlcheck: use kill instead of killpg Alexandre Duret-Lutz 2012-10-14 09:12:06 +02:00
  • a62a04670c more files to ignore Alexandre Duret-Lutz 2012-10-14 09:11:49 +02:00
  • 7e79fcb4e3 gnulib: add module sys_wait, for compilation on MinGW Alexandre Duret-Lutz 2012-10-13 18:13:52 +02:00
  • d22fb0b61f * src/ltlvisit/lbt.cc: Add missing case for Xor. Alexandre Duret-Lutz 2012-10-13 17:56:15 +02:00
  • a7d7d8d0ef lbtt_parse: add support for state-based acceptance Alexandre Duret-Lutz 2012-10-13 17:38:32 +02:00
  • 37b0809c44 * src/misc/formater.hh: Add virtual destructors to please g++-4.0. Alexandre Duret-Lutz 2012-10-13 15:59:08 +02:00
  • 852603416f to_spin_string: fix output of false and true Alexandre Duret-Lutz 2012-10-09 12:08:37 +02:00
  • 6167526548 * src/bin/ltlcheck.cc: Fix exit status and error reporting. Alexandre Duret-Lutz 2012-10-09 12:07:58 +02:00
  • d0a04f9410 ltlcheck: Add a timeout option. Alexandre Duret-Lutz 2012-10-09 09:16:22 +02:00
  • 82babb9d38 ltlcheck: Record translation time. Alexandre Duret-Lutz 2012-10-08 23:22:42 +02:00
  • 756319739b Import the gethrxtime module from gnulib. Alexandre Duret-Lutz 2012-10-08 21:59:59 +02:00
  • d7e8684d38 * src/bin/ltlcheck.cc: Improve example in --help. Alexandre Duret-Lutz 2012-10-05 16:38:35 +02:00
  • 122d34cce4 * src/bin/ltlcheck.cc: Compute statistics and print them in JSON. Alexandre Duret-Lutz 2012-10-05 16:32:33 +02:00
  • e99fdfb650 Pick the most readable format available for displaying formulas. Alexandre Duret-Lutz 2012-10-05 14:11:03 +02:00
  • 3f5e6102dc Clean up the misc/formater.hh file. Alexandre Duret-Lutz 2012-10-05 13:52:54 +02:00
  • f6dc6412d3 Use the spot::formater class in ltlcheck to format output commands. Alexandre Duret-Lutz 2012-10-05 13:38:36 +02:00
  • a303c8603c Factor the %-formating machinery. Alexandre Duret-Lutz 2012-10-04 09:05:23 +02:00
  • 62af20d39f * src/bin/ltlcheck.cc: Add support for LBTT's output as %T. Alexandre Duret-Lutz 2012-10-03 17:21:31 +02:00
  • 1017350110 * src/ltlparse/ltlscan.ll: Reset the starting condition to 0 initially. Alexandre Duret-Lutz 2012-10-03 17:19:08 +02:00
  • c55bd831a8 Add a parser for automata in LBTT's format. Alexandre Duret-Lutz 2012-10-02 18:01:35 +02:00
  • df743e5057 Preliminary implementation of an LBTT clone. Alexandre Duret-Lutz 2012-09-30 20:15:50 +02:00
  • f38405002a gnulib: upgrade and install the mkstemp module. Alexandre Duret-Lutz 2012-09-30 16:44:32 +02:00
  • 8ecf2ab1fd * src/tgbatest/kv.test: Fix the test comparison. Alexandre Duret-Lutz 2012-10-12 22:09:16 +02:00
  • 1551c5d947 Upgrade GPL v2+ to GPL v3+. Alexandre Duret-Lutz 2012-10-12 21:57:10 +02:00
  • 8cd6e1c6d2 * src/tgbatest/kv.test: Rewrite the sed command more portably. Alexandre Duret-Lutz 2012-10-12 10:13:29 +02:00
  • 08175025c9 scc_map: fix computation of ap_set_of, and (indirectly) aprec_set_of Alexandre Duret-Lutz 2012-10-12 09:39:29 +02:00
  • 561b852106 * src/tgba/tgbaexplicit.hh: Fix definition of the new alias_ map. Alexandre Duret-Lutz 2012-10-03 09:30:04 +02:00
  • fb38fe56aa * src/sanity/includes.test: Work around a bug in Bison 2.6. Alexandre Duret-Lutz 2012-10-02 18:20:53 +02:00
  • c05ec36dd0 * src/neverparse/neverclaimparse.yy: Prefer accepting labels in aliases. Alexandre Duret-Lutz 2012-09-30 22:21:32 +02:00
  • dd4d03e3a9 tgba_explicit: fix support for aliases Alexandre Duret-Lutz 2012-09-30 22:19:48 +02:00
  • 0fed46b796 Add a string version of to_lbt_string(). Alexandre Duret-Lutz 2012-09-30 16:21:10 +02:00
  • 902dadb898 * src/tgbaalgos/cycles.cc (nocycle): Fix a comment. Alexandre Duret-Lutz 2012-09-30 15:39:06 +02:00
  • dd16f58ef4 enumerate_cycles: fix memory management. Alexandre Duret-Lutz 2012-09-30 15:19:05 +02:00
  • 4ed4e4d2a8 Fix return of is_deterministic(), it was inverted. Alexandre Duret-Lutz 2012-09-30 09:57:20 +02:00
  • 7854f629e5 bin: factor version display. Alexandre Duret-Lutz 2012-09-29 17:34:53 +02:00
  • 489f719dc1 bin: factor the calls to set_program_name(). Alexandre Duret-Lutz 2012-09-29 17:09:26 +02:00
  • ecca4ba53e bin: factor the code to read LTL formulas from -f or -F. Alexandre Duret-Lutz 2012-09-29 15:42:33 +02:00
  • 467bf378a8 simulation: Fix a bug reported by Étienne Renault. Thomas Badie 2012-09-26 17:09:43 +02:00
  • f01d30eb91 Create unique_ptr for Spot. Thomas Badie 2012-09-04 16:19:59 +02:00
  • b23296cf61 Allow lbtt not to be built, and skip relevant tests. Alexandre Duret-Lutz 2012-04-27 11:09:13 +02:00
  • b5b3cd9d0c * src/bin/ltlfilt.cc (--psl): Remove this option. Alexandre Duret-Lutz 2012-09-25 09:52:34 +02:00
  • b5da11ed24 * src/tgbaalgos/minimize.hh: Typo in comment. Alexandre Duret-Lutz 2012-09-24 15:52:11 +02:00
  • 1f0c765547 ltl2tgta: new tool Alexandre Duret-Lutz 2012-09-24 15:41:53 +02:00
  • b0678a21a2 Fix prototype of atomic_prop_collect_as_bdd(). Alexandre Duret-Lutz 2012-09-24 14:52:18 +02:00
  • d138853676 * HACKING: Document the Gettext.pm and LaTeX dependencies Alexandre Duret-Lutz 2012-09-24 11:35:40 +02:00
  • 45e3f7fc2a Add two event_univ rewriting rules. Alexandre Duret-Lutz 2012-09-24 10:42:20 +02:00
  • 45ba8c3ef6 Add 11 implication-based simplification rules for U,W,R,M. Alexandre Duret-Lutz 2012-09-21 18:39:13 +02:00
  • f711f9d097 Fix failures detected on MacOS X with g++ 4.0. Alexandre Duret-Lutz 2012-09-22 13:06:10 +02:00
  • c6840d81e4 Work around old g++ versions. Alexandre Duret-Lutz 2012-09-22 01:26:33 +02:00
  • 13025d6cc8 * src/tgbaalgos/cycles.hh: Add virtual destructor. Alexandre Duret-Lutz 2012-09-22 01:14:07 +02:00
  • 3c17c418a2 Speedup is_weak_scc() if all transitions in the SCC are accepting. Alexandre Duret-Lutz 2012-09-21 15:09:08 +02:00
  • d228784c39 Don't pass the automaton to enumerate_cycle and is_weak_scc. Alexandre Duret-Lutz 2012-09-21 14:30:34 +02:00
  • 40de47f159 dve2: use postprocessor to simplify the code. Alexandre Duret-Lutz 2012-09-21 14:16:07 +02:00
  • 09b540315a * NEWS: Reorganize and update recent changes. Alexandre Duret-Lutz 2012-09-21 13:12:22 +02:00
  • 92e37998b2 Better documentation for the cycle enumeration algorithms. Alexandre Duret-Lutz 2012-09-21 11:15:12 +02:00
  • 420fcd62e4 Add a is_weak_scc() function based on cycle enumeration. Alexandre Duret-Lutz 2012-09-20 18:05:34 +02:00
  • 374a489e3f Implement Loizou & Thanisch's algorithm for enumerating cycles. Alexandre Duret-Lutz 2012-09-20 16:09:53 +02:00
  • 379e0d5eb4 * src/tgba/tgbascc.cc: Cosmetics. Alexandre Duret-Lutz 2012-09-19 22:13:58 +02:00
  • 64f0f653e3 * src/bin/ltl2tgba.cc: Fix cases where --stats is not used... Alexandre Duret-Lutz 2012-09-19 22:13:41 +02:00
  • f3a2675588 * src/bin/ltl2tgba.cc: Improve documentation. Alexandre Duret-Lutz 2012-09-19 10:29:10 +02:00
  • 26ad32d561 ltl2tgba: Add a --stats option. Alexandre Duret-Lutz 2012-09-19 00:28:23 +02:00
  • f4381d59ce Add option --lbt-input to ltl2tgba. Factor it with ltlfilt. Alexandre Duret-Lutz 2012-09-18 21:44:58 +02:00
  • f02156ebff Various utf-8 fixes. Alexandre Duret-Lutz 2012-09-18 20:57:47 +02:00
  • 4ed153a247 * src/bin/ltl2tgba.cc: Fix display of BA. Alexandre Duret-Lutz 2012-09-18 16:04:48 +02:00
  • 10189b2d61 * src/tgbaalgos/postproc.cc: Misplaced call to scc_filter(). Alexandre Duret-Lutz 2012-09-17 18:47:04 +02:00
  • 675fc0bc67 * src/bin/genltl.cc (parse_opt): Add OPT_U_LEFT and OPT_U_RIGHT cases. Alexandre Duret-Lutz 2012-09-17 18:03:04 +02:00
  • 0c005c8159 More fixes for the OS X builds. Alexandre Duret-Lutz 2012-09-17 11:51:44 +02:00
  • 42665b87b0 * src/bin/ltlfilt.cc: Add a --remove-wm option. Alexandre Duret-Lutz 2012-09-17 11:08:10 +02:00
  • 28e7d9aa4d Fix sanity failure on Mac OS X. Alexandre Duret-Lutz 2012-09-17 08:15:23 +02:00
  • d9dc1f489d Add a visitor to relabel the atomic proposition in formulas. Alexandre Duret-Lutz 2012-09-16 21:30:54 +02:00
  • 1a84c17ece Add an LTL printer in LBT's syntax. Alexandre Duret-Lutz 2012-09-14 18:52:59 +02:00
  • 106a14f8db Implement a parser for LBT's prefix syntax for LTL. Alexandre Duret-Lutz 2012-09-14 17:43:13 +02:00
  • a010ebc805 Use more sba_explicit more often. Alexandre Duret-Lutz 2012-09-14 15:10:12 +02:00
  • 807834ec41 Detect fail conditions on std::cout in user's tools. Alexandre Duret-Lutz 2012-09-14 09:45:40 +02:00
  • 70f51b2786 * src/tgbatest/wdba2.test: Adjust to yesterday's change to -kt. Alexandre Duret-Lutz 2012-09-12 18:02:59 +02:00
  • 6a3cf7538c bin/ltl2tgba: New user binary. Alexandre Duret-Lutz 2012-09-12 17:54:14 +02:00
  • 26deb56a9c Fix multiple inclusions of config.h. Alexandre Duret-Lutz 2012-09-12 13:19:17 +02:00
  • 04b5e37055 Add count_nondet_states(aut) and is_deterministic(aut). Alexandre Duret-Lutz 2012-09-11 15:10:49 +02:00
  • 45e93ea16c * NEWS: Summarize recent changes. Alexandre Duret-Lutz 2012-09-07 14:55:26 +02:00
  • 2d1460a2bd Kill the gspn-ssp benchmark (it was not working anymore). Alexandre Duret-Lutz 2012-09-07 14:28:38 +02:00
  • 649e8e2def Kill src/ltltest/randltl and replace it by src/bin/randltl. Alexandre Duret-Lutz 2012-09-07 14:24:06 +02:00
  • 1257893fb2 Kill src/ltltest/genltl now that src/bin/genltl does everything it did. Alexandre Duret-Lutz 2012-09-07 13:53:09 +02:00
  • 0990de50df Fix missing spaces after comma. Alexandre Duret-Lutz 2012-09-07 13:20:42 +02:00
  • f19526a93f randltl: Output unique formulae by default. Alexandre Duret-Lutz 2012-09-07 12:20:27 +02:00
  • bc6fa22b13 * src/bin/randltl.cc: Add a --weak-fairness option. Alexandre Duret-Lutz 2012-09-07 12:15:14 +02:00
  • 134fbd203d * src/bin/Makefile.am: Use a static library for all common functions. Alexandre Duret-Lutz 2012-09-07 11:39:17 +02:00
  • e43bc893fd randltl: add option to simplify formulas Alexandre Duret-Lutz 2012-09-07 11:30:48 +02:00
  • 7274ca2bb7 Fix prototype of ltl_simplifier::ltl_simplifier. Alexandre Duret-Lutz 2012-09-07 11:31:23 +02:00
  • a80356e440 * src/ltlvisit/apcollect.hh: Improve doc. Alexandre Duret-Lutz 2012-09-05 15:44:08 +02:00
  • 760d75cc44 randltl: first stage of the reimplementation Alexandre Duret-Lutz 2012-09-05 12:03:24 +02:00
  • a3e54af924 * src/bin/common_output.hh, src/bin/common_output.cc: Fix includes. Alexandre Duret-Lutz 2012-09-05 11:51:50 +02:00
  • c96513b6b8 help2man: generate man pages for genltl and ltlfilt Alexandre Duret-Lutz 2012-09-04 13:49:40 +02:00
  • e0873cc7d6 ltlfilt, genltl: factor the common output options. Alexandre Duret-Lutz 2012-09-03 19:31:29 +02:00
  • 267183bda7 ltlfilt: update the exit status in the same way as grep Alexandre Duret-Lutz 2012-09-03 17:44:39 +02:00
  • 24a8c03192 ltlfilt: add option to filter by implication or equivalence Alexandre Duret-Lutz 2012-09-03 17:13:25 +02:00
  • d1b8537f98 genltl: reimplement using argp, and allowing ranges. Alexandre Duret-Lutz 2012-08-31 19:00:40 +02:00
  • 90279bd40c ltlfilt: use error() to report errors. Alexandre Duret-Lutz 2012-08-31 15:28:58 +02:00
  • 8132f91867 ltlfilt: Call set_program_name(). Alexandre Duret-Lutz 2012-08-31 14:58:18 +02:00
  • 93f6e21759 Install gnulib to make sure we can use argp in ltlfilt. Alexandre Duret-Lutz 2012-08-31 14:47:50 +02:00