Hi!
I’m currently using Spot to manipulate LTL formulas (using Python) and encountered the following behaviour: The result of "spot.formula.Or([x,y])” possibly changes the order of the subformulas, e.g. globally will appear in front of finally. Is there a way to build formulas that stick to the given order?
Best and thanks in advance Niklas
Dear Niklas,
On Tue, Oct 6, 2020 at 1:59 PM Niklas Metzger niklas.metzger@cispa.saarland wrote:
"spot.formula.Or([x,y])” possibly changes the order of the subformulas, e.g. globally will appear in front of finally. Is there a way to build formulas that stick to the given order?
Not really. The operands of all operators that are associative and commutative are always sorted (to improve sharing of subformulas, cache hits, equality checks, etc.)
The order ensures that Boolean operands always come first (i.e., the present before the future), and the rest is sorted by creation order. If you have the impression that some G(x) comes before F(x), it's just because that G(x) was created before F(x).
import spot fx = spot.formula('F(x)') gy = spot.formula('G(y)') fz = spot.formula('F(z)') spot.formula_Or([gy, fz, fx])
spot.formula("Fx | Gy | Fz")
-- Alexandre Duret-Lutz
-
Alexandre Duret-Lutz -
Niklas Metzger