Re: [Spot] Explicit order of sub-formulas in formula constructor - Spot

6 Oct 2020

On Tue, Oct 6, 2020 at 5:09 PM Niklas Metzger
&lt;niklas.metzger(a)cispa.saarland&gt; 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