6 Oct
2020
6 Oct
'20
4:21 p.m.
Dear Niklas,
On Tue, Oct 6, 2020 at 1:59 PM Niklas Metzger
<niklas.metzger(a)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