diff --git a/NEWS b/NEWS index 6e577b1d5..6c9dfab6b 100644 --- a/NEWS +++ b/NEWS @@ -36,7 +36,9 @@ New in spot 0.8.3a: configured and built. This helps on systems (such as MinGW) where LBTT cannot be built. The test-suite will skip any LBTT-based test if LBTT is missing. - * Interface chances: + * Interface changes: + - Operators ->, <->, U, W, R, and M are no parsed as + right-associative to better match the PSL standard. - The new entry point for LTL/PSL simplifications is the function ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh. The ltl_simplifier class implements a cache. diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index c645d1fd5..efac4bfd0 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -873,51 +873,46 @@ operator, even if the operator has multiple synonyms (like \samp{|}, \section{Operator precedence} -\spottodo[inline]{The following operator precedence describe the - current parser of Spot, but this is not what we want eventually. - For instance $\IMPLIES$ should be right associative. $\U$ and $\W$ - would probably make more sense as right associative operators too.\\ - % - Tools that have $\U$, $\R$, $\W$, and $\M$ operators as left - associative: Spin, ltl2ba (same parser as spin), Wring, psl2ba, - Spot, Modella, NuSMV.\\ - % - Tools (and doc) that have these operators as right associative: Goal - (hence Büchi Store), PSL reference manual, LTL2AUT, LTL2Büchi (from - JavaPathFinder).\\ - % - Tools that have these operators as non-associative (parentheses are - required): Vis, LBTT.\\ - % - While compiling these lists I have also discovered that not all - people aggreed on the associativity of $\IMPLIES$ and $\EQUIV$. - Some have both left-assoc, or both right-assoc, other have only - $\IMPLIES$ as right-assoc.\\ - % - We want to get closer to the PSL standard eventually.} +The following operator precedence describes the current parser of +Spot. It has not always been this way. Especially, all operators +were left associative until version 0.9, when we changed the +associativity of $\IMPLIES$, $\EQUIV$, $\U$, $\R$, $\W$, and $\M$ to get closer +to the PSL standard~\cite{psl.04.lrm,eisner.06.psl}. \begin{center} \begin{tabular}{clc} - assoc. & operators & priority \\ + assoc. & operators & priority \\ \midrule -left & $\Asuffix,\,\AsuffixEQ,\,\Esuffix,\,\EsuffixEQ$ & \tikz[remember picture,baseline]\node (lowest){lowest}; \\ -left & $\CONCAT,\,\FUSION$ & \\ -left & $\IMPLIES,\,\EQUIV$ & \\ -left & $\XOR$ & \\ -left & $\OR$ & \\ -left & $\AND,\,\ANDALT$ & \\ -left & $\U,\,\W,\,\M,\,\R$ & \\ - & $\F,\,\G$ & \\ - & $\X$ & \\ - & $\STAR{\mvar{i}..\mvar{j}},\,\PLUS,\,\EQUAL{\mvar{i}..\mvar{j}},\,\GOTO{\mvar{i}..\mvar{j}}$ & \\ - & $\NOT$ & \\ - & $\code{=0},\,\code{=1}$ & \tikz[remember picture,baseline]\node (highest){highest}; \\ +right & $\Asuffix,\,\AsuffixEQ,\,\Esuffix,\,\EsuffixEQ$ & \tikz[remember picture,baseline]\node (lowest){lowest}; \\ +left & $\CONCAT$ & \\ +left & $\FUSION$ & \\ +right & $\IMPLIES,\,\EQUIV$ & \\ +left & $\XOR$ & \\ +left & $\OR$ & \\ +left & $\AND,\,\ANDALT$ & \\ +right & $\U,\,\W,\,\M,\,\R$ & \\ + & $\F,\,\G$ & \\ + & $\X$ & \\ + & $\STAR{\mvar{i}..\mvar{j}},\,\PLUS,\,\EQUAL{\mvar{i}..\mvar{j}},\,\GOTO{\mvar{i}..\mvar{j}}$ & \\ + & $\NOT$ & \\ + & $\code{=0},\,\code{=1}$ & \tikz[remember picture,baseline]\node (highest){highest}; \\ \end{tabular} \end{center} \begin{tikzpicture}[remember picture,overlay,>=stealth',semithick] \draw[->] (lowest) -- (highest); \end{tikzpicture} +Beware that not all tools agree on the associativity of these +operators. For instance Spin, ltl2ba (same parser as spin), Wring, +psl2ba, Modella, and NuSMV all have $\U$ and $\R$ as left-associative, +while Goal (hence Büchi store), LTL2AUT, and LTL2Büchi (from +JavaPathFinder) have $\U$ and $\R$ as right-associative. Vis and LBTT +have these two operators as non-associative (parentheses required). +Similarly the tools do not aggree on the associativity of $\IMPLIES$ +and $\EQUIV$: some tools handle both operators as left-associative, or +both right-associative, other have only $\IMPLIES$ as right-associative. + + \chapter{Properties} When Spot builds a formula (represented by an AST with shared diff --git a/src/ltlparse/ltlparse.yy b/src/ltlparse/ltlparse.yy index 0f4b51e4c..066acc716 100644 --- a/src/ltlparse/ltlparse.yy +++ b/src/ltlparse/ltlparse.yy @@ -111,19 +111,20 @@ using namespace spot::ltl; /* Priorities. */ -/* Low priority regex operator. */ -%left OP_UCONCAT OP_ECONCAT OP_UCONCAT_NONO OP_ECONCAT_NONO +/* Low priority SERE-LTL binding operator. */ +%right OP_UCONCAT OP_ECONCAT OP_UCONCAT_NONO OP_ECONCAT_NONO -%left OP_CONCAT OP_FUSION +%left OP_CONCAT +%left OP_FUSION /* Logical operators. */ -%left OP_IMPLIES OP_EQUIV +%right OP_IMPLIES OP_EQUIV %left OP_OR %left OP_XOR %left OP_AND OP_SHORT_AND /* LTL operators. */ -%left OP_U OP_R OP_M OP_W +%right OP_U OP_R OP_M OP_W %nonassoc OP_F OP_G %nonassoc OP_X diff --git a/src/ltltest/reduccmp.test b/src/ltltest/reduccmp.test index 8028d9ef9..931117426 100755 --- a/src/ltltest/reduccmp.test +++ b/src/ltltest/reduccmp.test @@ -263,13 +263,13 @@ for x in ../reduccmp ../reductaustr; do run 0 $x '{a && b && d[->2..4]} <>-> d' '0' run 0 $x '{a && { c* : b* : (g|h)*}} <>-> d' 'a & c & b & (g | h) & d' run 0 $x '{a && {b;c}} <>-> d' '0' - run 0 $x '{a && {b;c:e}} <>-> d' '0' + run 0 $x '{a && {(b;c):e}} <>-> d' '0' run 0 $x '{a && {b*;c*}} <>-> d' '{a && {b*|c*}} <>-> d' # until better - run 0 $x '{a && {b*;c*:e}} <>-> d' '{a && {b*|c*} && e} <>-> d' # idem + run 0 $x '{a && {(b*;c*):e}} <>-> d' '{a && {b*|c*} && e} <>-> d' # idem run 0 $x '{a && {b*;c}} <>-> d' 'a & c & d' - run 0 $x '{a && {b*;c:e}} <>-> d' 'a & c & d & e' + run 0 $x '{a && {(b*;c):e}} <>-> d' 'a & c & d & e' run 0 $x '{a && {b;c*}} <>-> d' 'a & b & d' - run 0 $x '{a && {b;c*:e}} <>-> d' 'a & b & d & e' + run 0 $x '{a && {(b;c*):e}} <>-> d' 'a & b & d & e' run 0 $x '{{{b1;r1*}&&{b2;r2*}};c}' 'b1&b2&X{{r1*&&r2*};c}' run 0 $x '{{b1:r1*}&&{b2:r2*}}' '{{b1&&b2}:{r1*&&r2*}}' run 0 $x '{{r1*;b1}&&{r2*;b2}}' '{{r1*&&r2*};{b1&&b2}}'