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

Commit graph

  • 39417037d7 to_string: abbreviate [->i..j] and [=i..j] expressed using [*i..j] Alexandre Duret-Lutz 2012-04-13 23:01:28 +02:00
  • e109f21ce4 Factor the code of ltl::to_string and ltl::to_spin_string. Alexandre Duret-Lutz 2012-04-13 17:50:23 +02:00
  • 3d41bf9ff1 ltl2tgba.html: Display properties of formulas. Alexandre Duret-Lutz 2012-03-19 19:03:43 +01:00
  • 62bf41cdb4 Prefer "xor" over "^" when outputing formulae. Alexandre Duret-Lutz 2012-03-14 16:34:49 +01:00
  • 5ce59c011c ltl2tgba.html: Provide a link to an SVG output. Suggested by Denis. Alexandre Duret-Lutz 2012-03-14 12:03:28 +01:00
  • 277ae7ddfb ltl::dotty: Number children for Concat and Fusion. Alexandre Duret-Lutz 2012-03-13 16:00:20 +01:00
  • 266bd25ba5 ltl2tgba.html: lists PSL operators in the help text. Alexandre Duret-Lutz 2012-03-12 19:28:43 +01:00
  • 412f946ac0 Use []=> and <>=> as sugar in the output when possible. Alexandre Duret-Lutz 2012-02-16 19:24:44 +01:00
  • 5e7c0add49 Move helper functions from simplify.cc to the AST files. Alexandre Duret-Lutz 2012-02-16 19:05:20 +01:00
  • aa4b68fcfc Simplify some simplification code using but_all(). Alexandre Duret-Lutz 2012-02-15 13:49:59 +01:00
  • 955fc041ca Reduce 'a|(b&X(b U a))' to 'b U a', plus three simular rules. Alexandre Duret-Lutz 2012-02-13 19:14:33 +01:00
  • bb56c26d1c Rewrite "(Xc) M b" as "b & X(b U c)", plus three similar rules. Alexandre Duret-Lutz 2012-02-13 17:58:57 +01:00
  • c9b34d684a * src/ltlvisit/tostring.cc: Output <-> and -> instead of <=> and =>. Alexandre Duret-Lutz 2011-06-16 11:55:05 +02:00
  • 1ddafc1cb4 Move the U,W,R,M equivalences to an appendix. Alexandre Duret-Lutz 2012-02-07 16:46:05 +01:00
  • e6e85999de Add new simplification rules like: "a | (Xa R b)" gives "b U a". Alexandre Duret-Lutz 2012-02-07 15:36:18 +01:00
  • 005988530e Augment the Syntactic Hierarchy Classes grammar with ->, <-> and xor. Alexandre Duret-Lutz 2012-02-07 10:19:43 +01:00
  • 54fd973a90 Fix computation of syntactic classes for Implies. Alexandre Duret-Lutz 2012-02-06 13:18:52 +01:00
  • 395793d986 Rewrite a&XGa as Ga, and a|XFa as Fa. Alexandre Duret-Lutz 2012-01-17 11:50:32 +01:00
  • 58f99203ad * doc/tl/Makefile.am: Fix timestamp issue causing distcheck failure. Alexandre Duret-Lutz 2012-01-12 14:35:39 +01:00
  • 54d4a0a093 Rewrite F(a M b) as F(a & b), and G(a W b) as G(a | b). Alexandre Duret-Lutz 2012-01-11 11:15:54 +01:00
  • 212c7ebdd7 Add implication-based rewritings from Babiak et al. (TACAS'12) Alexandre Duret-Lutz 2012-01-10 19:34:41 +01:00
  • ed0dd0b48d Add a new length_boolone() function to fix an assert in randpsl. Alexandre Duret-Lutz 2012-01-06 11:32:44 +01:00
  • c2ab4e781b Rewrite "a U (a&b)" as "b M a", and "a W (a&b)" as "b R a". Alexandre Duret-Lutz 2012-01-05 13:13:32 +01:00
  • 55a1c6c12f Fix compilation of tl.tex in VPATH builds. Alexandre Duret-Lutz 2011-12-18 15:32:34 +01:00
  • 0536cdfb9b Fix a g++ warning about possibly uninitialized variable. Alexandre Duret-Lutz 2011-12-08 10:12:43 +01:00
  • dd52768932 Support the PSL syntax [*1:inf], as a synonym for [*1:]. Alexandre Duret-Lutz 2011-12-07 17:02:05 +01:00
  • d0a8e6d6f5 * doc/tl/Makefile.am (LATEXMK): Support an older version of latexmk. Alexandre Duret-Lutz 2011-12-07 15:30:19 +01:00
  • 8c077b662d * doc/tl/tl.tex: Various minor improvements. Alexandre Duret-Lutz 2011-12-07 15:24:12 +01:00
  • 2c37367075 * doc/tl/tl.tex: More text for the temporal hierarchy. Alexandre Duret-Lutz 2011-12-07 12:23:26 +01:00
  • dc5a0620b7 * doc/tl/tl.tex: Fix trivial identities for AndNLM. Alexandre Duret-Lutz 2011-12-05 19:42:17 +01:00
  • 72609185b8 Fix drawing a bonup operators in the AST. Alexandre Duret-Lutz 2011-12-05 19:16:31 +01:00
  • fa44383efb Replace reference to RATEXP in the parser, by reference to SERE. Alexandre Duret-Lutz 2011-12-05 19:14:03 +01:00
  • 3d183d68c8 Make sure PSL formulae are translated with the FM translation online. Alexandre Duret-Lutz 2011-12-05 18:48:42 +01:00
  • 3dfde9e85f Make sure PSL formulae are translated with the FM translation. Alexandre Duret-Lutz 2011-12-05 17:29:39 +01:00
  • 9e92267c70 more files to ignore Alexandre Duret-Lutz 2011-12-05 17:12:55 +01:00
  • fef1547bc3 Use `SERE' consistently. Add more references. Alexandre Duret-Lutz 2011-12-05 17:11:01 +01:00
  • b03935a4cf Simplify {r1;b1}&&{r2;b2} or {b1:r1}&&{b2:r2}, or similar. Alexandre Duret-Lutz 2011-12-05 15:41:45 +01:00
  • 2f9f274a5f Diagnose reversed ranges like [=2..1], [->..0] or [*8..4]. Alexandre Duret-Lutz 2011-12-02 12:27:44 +01:00
  • ec9a3f96cb * src/ltlvisit/postfix.cc: Fix recursion on bunop formulae. Alexandre Duret-Lutz 2011-12-01 21:18:27 +01:00
  • 2a4f181737 * doc/tl/tl.tex: Fix footnote the the property table. Alexandre Duret-Lutz 2011-12-01 19:07:18 +01:00
  • 775438422d Remove a dynamic_cast. Alexandre Duret-Lutz 2011-12-01 18:42:59 +01:00
  • 614810c0db Simplify {b && {r1;...;rn}}. Alexandre Duret-Lutz 2011-12-01 18:41:00 +01:00
  • d0cfd44ba6 Simplify {b && {r1:...:rn}} as {b && r1 && ... && rn}. Alexandre Duret-Lutz 2011-12-01 17:48:15 +01:00
  • 77084747b9 Simplify {b && r[*]} as {b && r}; likewise for [->] and [=]. Alexandre Duret-Lutz 2011-12-01 16:39:15 +01:00
  • e61c01b826 * doc/tl/tl.tex: Document operator precedence. Alexandre Duret-Lutz 2011-11-29 18:51:51 +01:00
  • 2f46267117 Use latexmk to build tl.tex. Alexandre Duret-Lutz 2011-11-29 18:09:49 +01:00
  • 0f11e5fe0e Speedup mark_concat_ops() and simplify_mark() with a cache. Alexandre Duret-Lutz 2011-11-13 19:44:40 +01:00
  • f68f639e68 Rewrite {b}<>->f as (!b)|f instead of b->f. Alexandre Duret-Lutz 2011-11-13 18:12:53 +01:00
  • 098e121a36 Ignore sub-"SERE" that have been proved useless already. Alexandre Duret-Lutz 2011-11-12 23:10:40 +01:00
  • b6702fc23a [buddy] Speedup hash functions. Alexandre Duret-Lutz 2011-11-12 01:26:17 +01:00
  • 4ba60dad28 Speedup construction of transitions in ltl_to_tgba_fm. Alexandre Duret-Lutz 2011-11-12 00:16:44 +01:00
  • b67852a5ff Reuse Boolean->BDD translations performed during simplification. Alexandre Duret-Lutz 2011-11-11 15:53:05 +01:00
  • f590ca4e96 Cache the LTL->BDD translation for every subformulae. Alexandre Duret-Lutz 2011-11-11 15:36:22 +01:00
  • 77d704ea9e Add trivial identity {b}=b and !{b}=!b for any Boolean formula b. Alexandre Duret-Lutz 2011-11-07 11:30:27 +01:00
  • 98f67973eb Speedup minimize_obligation() when f->is_syntactic_obligation(). Alexandre Duret-Lutz 2011-11-07 10:03:50 +01:00
  • c483053a85 Add documentation for temporal logic operators. Alexandre Duret-Lutz 2011-05-28 15:22:12 +02:00
  • b3cc033e92 Trim DFAs used when translating PSL's closure operators. Alexandre Duret-Lutz 2011-11-06 16:15:31 +01:00
  • d1530de125 Setup machinery to build DFA when translating some PSL operators. Alexandre Duret-Lutz 2011-11-06 14:05:19 +01:00
  • 2f03649324 Generalize syntactic implication for event. and univ. formulae. Alexandre Duret-Lutz 2011-10-31 17:47:08 +01:00
  • 07e40e706a Translate Boolean formulae as BDD using the ltl_simplifier cache. Alexandre Duret-Lutz 2011-10-30 18:59:17 +01:00
  • 369ad87e50 Rewrite syntactic implication using a single function. Alexandre Duret-Lutz 2011-10-30 18:48:27 +01:00
  • 7514cc15ee Decrease the maximum bound used in random BUnOps. Alexandre Duret-Lutz 2011-10-30 18:40:33 +01:00
  • c54627bebd Avoid containment checks on equal formulae. Alexandre Duret-Lutz 2011-10-30 18:37:42 +01:00
  • 58bbaa0859 Fix translation of '{(c&!c)[->0..1]}!'. Alexandre Duret-Lutz 2011-10-30 18:34:49 +01:00
  • 1507dbc63a Fix a Clang-2.9 warning. Alexandre Duret-Lutz 2011-10-30 18:30:26 +01:00
  • 7f7627bf22 Check that reductions are legitimates with containment. Alexandre Duret-Lutz 2011-10-30 18:28:47 +01:00
  • cd9369c186 Fix universal and eventual rules for M and W. Alexandre Duret-Lutz 2011-10-30 18:15:20 +01:00
  • c9a659c8d4 Compare Boolean LTL formulae using BDDs. Alexandre Duret-Lutz 2011-10-12 11:06:26 +08:00
  • fea49630f6 Merge the syntactic implication code with ltl_simplifier. Alexandre Duret-Lutz 2011-10-12 08:16:45 +08:00
  • 3db13a6f97 * src/ltlvisit/simplify.cc: More comments. Alexandre Duret-Lutz 2011-09-25 22:48:24 +02:00
  • 03fd46a13b Rewrite xor, =>, and <=> in negative_normal_form(). Alexandre Duret-Lutz 2011-09-18 22:19:37 +02:00
  • b89f86edcf Mark reduce_tau03() as deprecated. Alexandre Duret-Lutz 2011-08-25 12:30:55 +02:00
  • 5c1729d6e4 Remove basicreduce files. ltl_simplifier does all the work. Alexandre Duret-Lutz 2011-08-25 12:15:33 +02:00
  • 67f4e8b5ce Deprecate reduce() in favor of ltl_simplifier. Alexandre Duret-Lutz 2011-08-24 19:16:15 +02:00
  • c0085a8f30 Move the remaining reduce() logic into ltl_simplifier. Alexandre Duret-Lutz 2011-08-24 17:40:22 +02:00
  • d4d4c0e7d3 Typo in the code rewriting "a M 1 = Fa". Alexandre Duret-Lutz 2011-08-24 16:59:50 +02:00
  • c2335edb57 Remove the negative_normal_form call from reduce(). Alexandre Duret-Lutz 2011-08-24 16:08:40 +02:00
  • 1087c62356 Move language containment into ltl_simplifier. Alexandre Duret-Lutz 2011-08-24 15:54:06 +02:00
  • 82b42494db Generalize G,&,| rewritings to deal with event. and univ. terms. Alexandre Duret-Lutz 2011-08-23 16:51:02 +02:00
  • ab7a1c7aa9 More rewritings or multop::And and multop::Or. Alexandre Duret-Lutz 2011-08-23 14:18:59 +02:00
  • 09d9696995 Make sure 'a U XXXFb' reduces to 'XXXFb'. Spot 0.7.1 missed that. Alexandre Duret-Lutz 2011-08-23 09:06:03 +02:00
  • 47fb449198 * src/ltlvisit/reduce.hh: 80 columns. Alexandre Duret-Lutz 2011-08-22 23:08:00 +02:00
  • ca686cb07e Fix a case caught by the random formula generator. Alexandre Duret-Lutz 2011-08-22 22:14:36 +02:00
  • ca2fe4f3f8 Reimplement basic_reduce()'s rules in ltl_simplifier. Alexandre Duret-Lutz 2011-08-22 19:34:09 +02:00
  • e3e0f913b6 * src/ltlvisit/simplify.hh (ltl_simplifier): Disallow copy. Alexandre Duret-Lutz 2011-08-19 18:08:00 +02:00
  • dd1cd89a73 event./univ. and syntactic implications rewriting in ltl_simplifier. Alexandre Duret-Lutz 2011-08-19 18:07:48 +02:00
  • 503bdb5bbf Adjust kind.test Adjust after the change of 2011-05-23. Alexandre Duret-Lutz 2011-08-19 17:42:33 +02:00
  • aa5c2f606b Take trivial identities into account to simplify basicreduce. Alexandre Duret-Lutz 2011-05-28 15:01:22 +02:00
  • bd720488b4 * src/ltlast/formula.hh: Typos in comments. Alexandre Duret-Lutz 2011-05-23 15:08:24 +02:00
  • 8ecf57e832 Generalize computation of is.eventual and is.universal. Alexandre Duret-Lutz 2011-05-23 15:06:57 +02:00
  • 9f7ef5d0c3 Introduce ltl_simplifier. Alexandre Duret-Lutz 2011-05-17 19:30:34 +02:00
  • 0caa631c0d Speedup randpsl.test. Alexandre Duret-Lutz 2011-02-27 15:21:41 +01:00
  • fb386209aa Track finite formulae. Alexandre Duret-Lutz 2011-02-27 13:29:14 +01:00
  • df760a4597 Track syntactic classes. Alexandre Duret-Lutz 2011-02-25 18:07:48 +01:00
  • 2669df1c96 Combine Boolean formulae in Fusion arguments. Alexandre Duret-Lutz 2011-02-23 16:24:45 +01:00
  • a2da5184b5 Add trivial identities for &&, <>->, []-> and Boolean arguments. Alexandre Duret-Lutz 2011-02-23 15:11:44 +01:00
  • 0e4e2a79b2 Cosmetic change to please sanity checks. Alexandre Duret-Lutz 2011-02-20 17:40:55 +01:00
  • 6e6b6b1e01 Disable LTL reductions on SERE formulae. Alexandre Duret-Lutz 2011-02-20 17:15:37 +01:00
  • 459921ef60 Track SERE formulas. Alexandre Duret-Lutz 2011-02-20 17:08:39 +01:00
  • fdd73d5123 Add support for the {SERE}! PSL operator. Alexandre Duret-Lutz 2011-02-17 18:47:21 +01:00