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

Commit graph

  • da2ccdb2ed * src/tgbaalgos/hoa.cc: Use is_buchi() and is_true(). Alexandre Duret-Lutz 2015-02-25 22:40:03 +01:00
  • 5b2c7b55ed acc: refactor strip() routines Alexandre Duret-Lutz 2015-02-25 22:36:13 +01:00
  • 717c857794 ltlcross: adjust to work with generic acceptance Alexandre Duret-Lutz 2015-02-25 08:57:49 +01:00
  • 9ccbc34964 remfin: introduce less acceptance sets for interferences Alexandre Duret-Lutz 2015-02-25 08:55:54 +01:00
  • 83dfb4a971 remfin: cleanup acceptance Alexandre Duret-Lutz 2015-02-24 21:51:20 +01:00
  • d597050f6d Make it easy to complement an acceptance condition Alexandre Duret-Lutz 2015-02-24 21:50:00 +01:00
  • 659107a000 Add a cleanup_acceptance() algorithm Alexandre Duret-Lutz 2015-02-24 20:02:44 +01:00
  • 85508a0ea6 Add a remove_fin() algorithm Alexandre Duret-Lutz 2015-02-24 09:10:20 +01:00
  • 1441c4fe34 acc: add a to_dnf() method Alexandre Duret-Lutz 2015-02-22 23:10:31 +01:00
  • de586dd2f0 stats: use %g to print the (generic) acceptance condition Alexandre Duret-Lutz 2015-02-22 18:05:57 +01:00
  • 33c496a4bb acc: Add operators == and != for acc_code Alexandre Duret-Lutz 2015-02-20 13:16:46 +01:00
  • 039274b238 sbacc: Make sure it also work for non-TGBA Alexandre Duret-Lutz 2015-02-20 08:54:01 +01:00
  • f325cddc1c acc: avoid superfluous parentheses when printing acceptance Alexandre Duret-Lutz 2015-02-20 08:53:01 +01:00
  • 76c676dba0 rename set_acceptance_conditions as set_generalized_buchi Alexandre Duret-Lutz 2015-02-19 18:47:15 +01:00
  • fd1f6c4d61 Preliminirary support for generic acceptance. Alexandre Duret-Lutz 2015-02-18 11:28:03 +01:00
  • c61f053e2d transform: copy and accessible versions Alexandre Lewkowicz 2015-02-19 16:23:59 +01:00
  • 223d41d26b autfilt: fix destruction order for static variables Alexandre Duret-Lutz 2015-02-18 12:45:09 +01:00
  • dcad10fc68 maskkeep: Add a tgba_digraph version Alexandre Lewkowicz 2015-02-12 14:49:37 +01:00
  • 727c351657 common_conv: Parse comma and space separated numbers Alexandre Lewkowicz 2015-02-12 14:46:33 +01:00
  • 78def4f8ca bin: add the --output to tools that output formulas Alexandre Duret-Lutz 2015-02-15 23:50:48 +01:00
  • e22a800fe4 ltlfilt: add a --count option, like autfilt Alexandre Duret-Lutz 2015-02-15 23:13:47 +01:00
  • 1e7c1e5cdd bin: implement --output for automata Alexandre Duret-Lutz 2015-02-15 12:23:28 +01:00
  • d17d7469c3 ltlcross: allow appending to files via >>FILENAME Alexandre Duret-Lutz 2015-02-14 17:39:51 +01:00
  • 7daea8d3cb bitvect: Fix routines for 64-width vectors Alexandre Duret-Lutz 2015-02-13 18:44:46 +01:00
  • be40885010 * doc/org/ltlfilt.org: Update description of --stutter-invariant. Alexandre Duret-Lutz 2015-02-13 17:07:48 +01:00
  • e900488e13 bench/stutter: add a "user" benchmark Alexandre Duret-Lutz 2015-02-13 16:58:42 +01:00
  • 204af40b09 stutter: Improve sl2. Alexandre Duret-Lutz 2015-02-07 12:59:55 +01:00
  • bd414d4d4c bench/stutter: Update Alexandre Duret-Lutz 2015-01-22 11:31:20 +01:00
  • 5d31094029 dtgba_complement: take a tgba_digraph_ptr as input Alexandre Duret-Lutz 2015-02-10 16:58:08 +01:00
  • afc8773de1 ltlcross: Add --ignore-execution-failures. Alexandre Duret-Lutz 2015-02-10 11:14:56 +01:00
  • 2786d0c652 hoaparse: Fix non-posix warnings. Etienne Renault 2015-02-09 10:10:06 +01:00
  • 87f51e28e0 ltldo: cleanup temporary files Alexandre Duret-Lutz 2015-02-06 22:31:39 +01:00
  • db34207084 graph: Make perfect forwarding imperfect. Alexandre Duret-Lutz 2015-02-06 13:55:25 +01:00
  • f2ba94f4d4 Add (void) casts for variables used only in assert()s. Alexandre Duret-Lutz 2015-02-06 11:57:27 +01:00
  • 78e63d0324 nra2nba: Fix initial state construction. Alexandre Duret-Lutz 2015-02-05 18:55:52 +01:00
  • 856adef9a8 acc: do not store a bdd_dict Alexandre Duret-Lutz 2015-02-04 21:14:07 +01:00
  • 2a3c126c15 Make the compiler requirement clearer. Alexandre Duret-Lutz 2015-02-04 15:55:52 +01:00
  • ee0b8e4ea8 autfilt: add a --strip-acceptance option Alexandre Duret-Lutz 2015-02-03 23:02:37 +01:00
  • acb67c1bf6 autfilt: add a --sbacc option Alexandre Duret-Lutz 2015-02-03 20:53:29 +01:00
  • cbee5c1a3f hoaparse: detect duplicate atomic propositions Alexandre Duret-Lutz 2015-02-03 09:21:13 +01:00
  • d7dc584992 hoaparse: fix parsing of LBTT with non 0-based states Alexandre Duret-Lutz 2015-02-02 18:48:33 +01:00
  • 08fbe27136 bin: diagnose empty automata in ltlcross and ltldo Alexandre Duret-Lutz 2015-02-02 17:46:38 +01:00
  • de935d40ca autfilt: improve documentation Alexandre Duret-Lutz 2015-02-01 20:31:21 +01:00
  • 57cda2d9c3 * src/dstarparse/nra2nba.cc: Simplify construction of initial state. Alexandre Duret-Lutz 2015-02-01 17:16:24 +01:00
  • 847270b480 ltlcross: replace %H,%T,%N by %O Alexandre Duret-Lutz 2015-02-01 01:54:39 +01:00
  • dbd824c539 save: remove Alexandre Duret-Lutz 2015-01-31 21:13:44 +01:00
  • a246c3b8ba tgbaparse: remove this parser Alexandre Duret-Lutz 2015-01-31 20:44:33 +01:00
  • d0f0be234d maskacc: Add a tgba_digraph version Alexandre Duret-Lutz 2015-01-31 20:28:47 +01:00
  • a0a035e0e1 tgbatest: remove the unused powerset source Alexandre Duret-Lutz 2015-01-31 17:55:38 +01:00
  • 7b5f80d46d tgbatest: get rid of tgbaread Alexandre Duret-Lutz 2015-01-31 17:49:02 +01:00
  • 33a944705c tgbatest: drop support of Spot's legacy format from ltl2tgba Alexandre Duret-Lutz 2015-01-31 17:43:16 +01:00
  • 5852292c9f hoa: correctly deal with "Acceptance: 1 t" Alexandre Duret-Lutz 2015-01-28 22:35:11 +01:00
  • 44f98219d3 python: use hoa_parse instead of tgba_parse Alexandre Duret-Lutz 2015-01-27 22:44:01 +01:00
  • 6819cee682 bin: fix compilation on mingw Alexandre Duret-Lutz 2015-01-27 21:29:34 +01:00
  • 48d508420b ltldo: rounds start at 1 Alexandre Duret-Lutz 2015-01-27 16:02:13 +01:00
  • a24a021964 bin: add shorthands for ltlcross and ltldo Alexandre Duret-Lutz 2015-01-27 15:06:58 +01:00
  • 259c9faaae ltldo: automatic renaming of AP Alexandre Duret-Lutz 2015-01-27 13:59:02 +01:00
  • a4a0cf3bb2 ltl: keep track of spin-compatible AP Alexandre Duret-Lutz 2015-01-27 10:21:17 +01:00
  • 16a8c03143 ltldo: new binary Alexandre Duret-Lutz 2015-01-26 19:28:11 +01:00
  • e5294aac21 never: use state-names as comments Alexandre Duret-Lutz 2015-01-25 13:02:28 +01:00
  • c44b158716 org: declare utf8 everwhere and fix some typos Alexandre Duret-Lutz 2015-01-25 12:03:15 +01:00
  • 25af8e7eff update to ltl3ba 1.1.1 Alexandre Duret-Lutz 2015-01-25 11:44:00 +01:00
  • d9045d131c bin: factor common conversion functions Alexandre Duret-Lutz 2015-01-24 22:55:57 +01:00
  • 06d1c1ea96 * wrap/python/ajax/spot.in: Replace call to dupex by ensure_digraph. Alexandre Duret-Lutz 2015-01-24 16:52:08 +01:00
  • 49701ca3bc dotty: get rid of the decorated version Alexandre Duret-Lutz 2015-01-24 11:54:39 +01:00
  • 947ab17b12 autfilt: add an --intersect filter Alexandre Duret-Lutz 2015-01-23 22:48:15 +01:00
  • 8dc6776c24 postproc: fix handling of --complete Alexandre Duret-Lutz 2015-01-23 18:40:46 +01:00
  • 93271bed6f randomize: reorder state names Alexandre Duret-Lutz 2015-01-23 18:36:45 +01:00
  • 9add895ba7 hoa,dot: propagate state names Alexandre Duret-Lutz 2015-01-23 18:34:57 +01:00
  • ae50155297 dotty: output label for unreachable state even if SCCs are shown Alexandre Duret-Lutz 2015-01-23 17:29:35 +01:00
  • a4b6faba20 ltl2tgba.html: Adjust for ltl3ba 1.1.0 Alexandre Duret-Lutz 2015-01-23 11:38:10 +01:00
  • ef6d175ace ltltest: speed kind.test and consterm.test up Alexandre Duret-Lutz 2015-01-22 20:43:21 +01:00
  • 2fc816c8a7 hoa: make the scanner interactive when reading from a pipe Alexandre Duret-Lutz 2015-01-22 16:47:58 +01:00
  • 46d967945b simulation: do not mark codeterministic automata as deterministic Alexandre Duret-Lutz 2015-01-22 15:51:12 +01:00
  • a89b9d3678 hoa: do not add a fake initial state when possible Alexandre Duret-Lutz 2015-01-21 23:28:35 +01:00
  • 58b088128d dot: output marked states only for SBA Alexandre Duret-Lutz 2015-01-20 11:35:34 +01:00
  • dd948bc1a7 hoa: validate trans-acc and state-acc Alexandre Duret-Lutz 2015-01-20 09:45:16 +01:00
  • c6110a884c hoa: fix parsing of label-expr with parentheses Alexandre Duret-Lutz 2015-01-20 08:31:48 +01:00
  • 8c83c8a81e dupexp: remove the version that fills a vector Alexandre Duret-Lutz 2015-01-19 18:16:23 +01:00
  • 64469f3dbd simulation: take a tgba_digraph as input Alexandre Duret-Lutz 2015-01-19 18:07:59 +01:00
  • 0159027395 simulation: get rid of the "don't care" simulation reductions Alexandre Duret-Lutz 2015-01-19 16:43:58 +01:00
  • 1d724beabd ltl2tgba.html: document [:*i..j] Alexandre Duret-Lutz 2015-01-19 14:38:09 +01:00
  • 34f1601b9b ltl: rename is_X_free() into is_syntactic_stutter_invariant() Alexandre Duret-Lutz 2015-01-15 23:09:24 +01:00
  • a79db4eefe psl: add support for the [:*i..j] operator Alexandre Duret-Lutz 2015-01-15 18:50:32 +01:00
  • eebbcac281 tl: formul\ae -> formulas Alexandre Duret-Lutz 2015-01-15 10:32:18 +01:00
  • 731561cdac scc: get rid of scc_stats Alexandre Duret-Lutz 2015-01-18 21:24:11 +01:00
  • 5b74160abb test: simplify scc.test Alexandre Duret-Lutz 2015-01-18 20:02:26 +01:00
  • 1411fa6063 cycles: rewrite using the tgba_digraph interface Alexandre Duret-Lutz 2015-01-18 14:03:16 +01:00
  • 8fd594f5d0 ltlfilt: add a --max-count/-n option Alexandre Duret-Lutz 2015-01-14 18:49:00 +01:00
  • ae234d2e12 ltlfilt: remove -n. Alexandre Duret-Lutz 2015-01-14 18:24:31 +01:00
  • 7c55500d0e never: fix output of accepting initial states Alexandre Duret-Lutz 2015-01-13 18:02:13 +01:00
  • f3f4305150 use ltl2tgba -Ds instead of ltl2tgba -sD in the test suite Alexandre Duret-Lutz 2015-01-13 17:13:58 +01:00
  • 1578cdf837 minimize: cosmetics Alexandre Duret-Lutz 2015-01-13 17:13:03 +01:00
  • f958c51991 powerset: rewrite the determinization construction using bitvectors Alexandre Duret-Lutz 2015-01-13 08:54:36 +01:00
  • 0d1c08e6e1 powerset: tiny speedup Alexandre Duret-Lutz 2015-01-12 23:23:47 +01:00
  • 2377523c02 powerset: simplify an implication check Alexandre Duret-Lutz 2015-01-11 19:14:32 +01:00
  • 6f7f9ef8bc isdet: rewrite using the tgba_digraph interface Alexandre Duret-Lutz 2015-01-11 13:58:52 +01:00
  • c85ba787e8 ltltest: get rid of equals.cc Alexandre Duret-Lutz 2015-01-09 23:18:55 +01:00
  • 6a2aad6259 never: add an option to output in Spin's 6.2.4 style Alexandre Duret-Lutz 2015-01-09 22:25:18 +01:00
  • 604971d651 postproc: use scc_filter_states on SBA Alexandre Duret-Lutz 2015-01-09 22:23:55 +01:00