diff --git a/NEWS b/NEWS index d19451793..33a40d185 100644 --- a/NEWS +++ b/NEWS @@ -89,6 +89,11 @@ New in spot 2.11.6.dev (not yet released) - b:b[*i..j] = b[*max(i,1)..j] - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1, j+l-1] + - The following new trivial simplifications have been implemented + for PSL operators: + - {[*]}[]->0 = 0 + - {[*]}<>->1 = 1 + - The HOA parser is a bit smarter when merging multiple initial states into a single initial state (Spot's automaton class supports only one): it now reuses the edges leaving initial states diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index e7c283bc6..141daa7b8 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -998,6 +998,8 @@ formula $b$, the following rewritings are systematically performed & \nsere{b} &\equiv \NOT b\\ \sere{r}\Asuffix \1&\equiv \1 & \sere{r}\Esuffix \0&\equiv \0 \\ + \sere{\STAR{}} \Asuffix \0 &\equiv \0 +& \sere{\STAR{}} \Esuffix \1 &\equiv \1 \\ \end{align*} \chapter{Grammar} diff --git a/spot/tl/formula.cc b/spot/tl/formula.cc index db4b32ec7..1a1a4fb47 100644 --- a/spot/tl/formula.cc +++ b/spot/tl/formula.cc @@ -1163,6 +1163,7 @@ namespace spot // - 1 <>-> Exp = Exp // - [*0] <>-> Exp = 0 // - Exp <>-> 0 = 0 + // - [*] <>-> 1 = 1 // - boolExp <>-> Exp = boolExp & Exp if (first->is_tt()) return second; @@ -1172,7 +1173,7 @@ namespace spot second->destroy(); return ff(); } - if (second->is_ff()) + if (second->is_ff() || (second->is_tt() && first == one_star())) { first->destroy(); return second; @@ -1185,6 +1186,7 @@ namespace spot // - 1 []-> Exp = Exp // - [*0] []-> Exp = 1 // - Exp []-> 1 = 1 + // - [*] []-> 0 = 0 // - boolExp []-> Exp = !boolExp | Exp if (first->is_tt()) return second; @@ -1194,7 +1196,7 @@ namespace spot second->destroy(); return tt(); } - if (second->is_tt()) + if (second->is_tt() || (second->is_ff() && first == one_star())) { first->destroy(); return second; diff --git a/tests/core/equals.test b/tests/core/equals.test index b36f9edc3..ffc400c83 100755 --- a/tests/core/equals.test +++ b/tests/core/equals.test @@ -55,6 +55,8 @@ GGGGGx, Gx !!!!!x, !x {[*0];x}<>->1, {x}<>->1 {x;[*0]}<>->1, {x}<>-> 1 +{[*]}[]->0, 0 +{[*]}<>->1, 1 {[*0];x;[*0];[*0]}<>->1, {x}<>->1 {[*0];x;[*0];x;[*0]}<>->1, {x;x}<>->1 {x;x;x;[*0];x;x}<>->1, {x;x;x;x;x}<>->1