[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Set operations and emptiness

Hi All,

I'm currently learning TLA+ and I met a problem that how can I check set emptiness?.

I have two sets A and B.
In every step, AB should be an empty set.
So after writing TLA specification, I would like to add this as an Invariant property. For doing this I wrote following code. But it doesn't work :-(

setInvariant == A \cap B = {}


Nikhila K N