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, A∩B 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 = {}
-Regards
Nikhila K N