diff --git a/NEWS b/NEWS index 0a53c0e2b..67bf9bcd1 100644 --- a/NEWS +++ b/NEWS @@ -13,8 +13,9 @@ New in spot 1.99.2a (not yet released) * All the unabbreviation functions (unabbreviate_ltl(), unabbreviate_logic(), unabbreviate_wm()) have been merged into a single unabbreviate() function that takes a string representing - the list of rewritting rules to enable. This function is also - available via ltlfilt --unabbreviate. + the list of operators to remove among "eFGiMRW^" where 'e', 'i', + and '^' stand respectively for <->, ->, and xor. + This feature is also available via ltlfilt --unabbreviate. * In LTL formulas, atomic propositions specified using double-quotes can now include \" and \\. (This is more consistent with the HOA diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 44b8ad1a0..e9e1ff8ec 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1262,19 +1262,25 @@ occurrences of $\XOR$, $\EQUIV$ and $\IMPLIES$. ``\texttt{\^{}e}" & f\XOR g &\equiv& (f\AND\NOT g)\OR (g\AND\NOT f)\\ ``\texttt{\^{}}"\text{~without~}``\texttt{e}" & f\XOR g &\equiv& \NOT(f\EQUIV g)\\ ``\texttt{F}" & \F f&\equiv& \1\U f\\ -``\texttt{G}" & \G f&\equiv& \0\R f \\ -``\texttt{W}" & f \W g&\equiv& g \R (g \OR f)\\ -``\texttt{M}" & f \M g&\equiv& g \U (g \AND f) +``\texttt{G}"\text{~without~}``\texttt{R}" & \G f&\equiv& \0\R f \\ +``\texttt{GR}"\text{~without~}``\texttt{W}" & \G f&\equiv& f \W \0 \\ +``\texttt{GRW}" & \G f&\equiv& \NOT\F\NOT f \\ +``\texttt{M}" & f \M g&\equiv& g \U (g \AND f) \\ +``\texttt{R}"\text{~without~}``\texttt{W}" & f \R g&\equiv& g\W (f \AND g)\\ +``\texttt{RW}" & f \R g&\equiv& g\U ((f \AND g) \OR \G g) \\ +``\texttt{W}"\text{~without~}``\texttt{R}" & f \W g&\equiv& g \R (g \OR f)\\ +``\texttt{WR}" & f \W g&\equiv& f \U (g \OR \G f)\\ \end{array} \] Among all the possible rewritings (see Appendix~\ref{sec:ltl-equiv}) -for $\W$ and $\M$, those two were chosen because they are easier to -translate in a tableau construction~\cite[Fig.~11]{duret.11.vecos}. +the default rules for $\R$, $\W$ and $\M$, those were chosen because +they are easier to translate in a tableau +construction~\cite[Fig.~11]{duret.11.vecos}. Besides the `\verb=unabbreviate()=' function, there is also a class -`\verb=unabbreviator()= that implement the same functionality, but -maintain a cache of abbreviated subformulas. This is preferable if +`\verb=unabbreviator()= that implements the same functionality, but +maintains a cache of abbreviated subformulas. This is preferable if you plan to abbreviate many formulas sharing identical subformulas. \section{LTL simplifier} diff --git a/src/bin/ltlfilt.cc b/src/bin/ltlfilt.cc index 62ea85baf..cd783cdcd 100644 --- a/src/bin/ltlfilt.cc +++ b/src/bin/ltlfilt.cc @@ -129,9 +129,9 @@ static const argp_option options[] = 0 }, { "unabbreviate", OPT_UNABBREVIATE, "STR", OPTION_ARG_OPTIONAL, "remove all occurrences of the operators specified by STR, which " - "must be a substring of \"eFGiMW^\", where 'e', 'i', and '^' stand " - "respectively for <->, ->, and xor. If no argument is passed, all " - "rewriting rules are applied.", 0 }, + "must be a substring of \"eFGiMRW^\", where 'e', 'i', and '^' stand " + "respectively for <->, ->, and xor. If no argument is passed, " + "the subset \"eFGiMW^\" is used.", 0 }, { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0, "if any of those APs occur in the formula, add a term ensuring " "two of them may not be true at the same time. Use this option " diff --git a/src/ltlvisit/unabbrev.cc b/src/ltlvisit/unabbrev.cc index 80ae9424f..626fe5ffc 100644 --- a/src/ltlvisit/unabbrev.cc +++ b/src/ltlvisit/unabbrev.cc @@ -51,6 +51,9 @@ namespace spot re_m_ = true; re_some_other_ = true; break; + case 'R': + re_r_ = true; + re_some_other_ = true; case 'W': re_w_ = true; re_some_other_ = true; @@ -109,18 +112,44 @@ namespace spot auto c = run(uo->child()); switch (auto op = uo->op()) { - // F f1 = true U f1 + // F f = true U f case unop::F: if (!re_f_) goto unop_clone; out = binop::instance(binop::U, constant::true_instance(), c); break; - // G f1 = false R f1 + // G f = false R f + // G f = f W false + // G f = !F!f + // G f = !(true U !f) case unop::G: if (!re_g_) goto unop_clone; - out = binop::instance(binop::R, constant::false_instance(), c); - break; + if (!re_r_) + { + out = binop::instance(binop::R, + constant::false_instance(), c); + break; + } + if (!re_w_) + { + out = binop::instance(binop::W, + c, constant::false_instance()); + break; + } + { + auto nc = unop::instance(unop::Not, c); + if (!re_f_) + { + out = unop::instance(unop::Not, + unop::instance(unop::F, nc)); + break; + } + auto u = binop::instance(binop::U, + constant::true_instance(), nc); + out = unop::instance(unop::Not, u); + break; + } case unop::Not: case unop::X: case unop::Closure: @@ -182,12 +211,29 @@ namespace spot break; } // f1 W f2 = f2 R (f2 | f1) + // f1 W f2 = f1 U (f2 | G f1) + // f1 W f2 = f1 U (f2 | !F !f1) + // f1 W f2 = f1 U (f2 | !(1 U !f1)) case binop::W: if (!re_w_) goto binop_clone; - out = binop::instance(binop::R, f2, - multop::instance(multop::Or, - f2->clone(), f1)); + if (!re_r_) + { + out = binop::instance(binop::R, f2, + multop::instance(multop::Or, + f2->clone(), f1)); + break; + } + f1->clone(); + out = unop::instance(unop::G, f1); + if (re_g_) + { + auto tmp = out; + out = run(out); + tmp->destroy(); + } + out = binop::instance(binop::U, f1, + multop::instance(multop::Or, f2, out)); break; // f1 M f2 = f2 U (g2 & f1) case binop::M: @@ -197,8 +243,32 @@ namespace spot multop::instance(multop::And, f2->clone(), f1)); break; - case binop::U: + // f1 R f2 = f2 W (f1 & f2) + // f1 R f2 = f2 U ((f1 & f2) | Gf2) + // f1 R f2 = f2 U ((f1 & f2) | !F!f2) + // f1 R f2 = f2 U ((f1 & f2) | !(1 U !f2)) case binop::R: + if (!re_r_) + goto binop_clone; + { + auto f12 = multop::instance(multop::And, f1, f2->clone()); + if (!re_w_) + { + out = binop::instance(binop::W, f2, f12); + break; + } + out = unop::instance(unop::G, f2->clone()); + if (re_g_) + { + auto tmp = out; + out = run(tmp); + tmp->destroy(); + } + out = binop::instance(binop::U, f2, + multop::instance(multop::Or, f12, out)); + } + break; + case binop::U: case binop::UConcat: case binop::EConcat: case binop::EConcatMarked: diff --git a/src/ltlvisit/unabbrev.hh b/src/ltlvisit/unabbrev.hh index 047866b91..0cb30c123 100644 --- a/src/ltlvisit/unabbrev.hh +++ b/src/ltlvisit/unabbrev.hh @@ -40,11 +40,12 @@ namespace spot bool re_g_ = false; bool re_i_ = false; bool re_m_ = false; + bool re_r_ = false; bool re_w_ = false; bool re_xor_ = false; bool re_some_bool_ = false; // rewrite xor, i, or e bool re_some_f_g_ = false; // rewrite F or G - bool re_some_other_ = false; // rewrite W or M + bool re_some_other_ = false; // rewrite W, M, or R // Cache of rewritten subformulas std::unordered_map cache_; public: diff --git a/src/tests/unabbrevwm.test b/src/tests/unabbrevwm.test index ab5cbf3fa..fff7c357f 100755 --- a/src/tests/unabbrevwm.test +++ b/src/tests/unabbrevwm.test @@ -25,8 +25,10 @@ set -e +ltlfilt=../../bin/ltlfilt + # Removing W,M in this formula caused a segfault at some point. -run 0 ../../bin/ltlfilt --remove-wm >out <out <