On Tue, Oct 6, 2020 at 5:09 PM Niklas Metzger <niklas.metzger@cispa.saarland> wrote:

Hi Alexandre,

thank you for your fast response! I’m a bit confused on the meaning of creation time:

...

...

...

import spot f = spot.formula("Fa") ff = spot.formula("Ga") spot.formula.Or([f, ff]) spot.formula("Fa | Ga") f = spot.formula("Ga") ff = spot.formula("Fa") spot.formula.Or([f, ff]) spot.formula("Fa | Ga") n = spot.formula("Ga") nn = spot.formula("Fa") spot.formula.Or([n, nn]) spot.formula("Fa | Ga")

Is there some internal representation that does not create new objects if seen before?

Yes. You can also use print(f.id()) to display the "serial number" of formula f. That's an identifier incremented for each new formula (new in the sense "not seen before"). This value is used to sort formulas (e.g., order the operands), or as hash value. But it is not necessarily unique in the case that so many formulas are created that the counter loops. -- Alexandre Duret-Lutz