Set operations and emptiness

[knnik...@gmail.com]

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

[Stephan Merz]

Hello,

what you have done so far looks good. In order for TLC to check the invariant, "setInvariant" should be added to the invariants to be verified (with the box checked) in "Model Overview" -> "What to check?" -> "Invariants".

If that doesn't help, could you explain what doesn't work and perhaps share your specification?

Regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Nikhila K N]

Thanks, Stephan

But it doesn't work for me. PFA for model checking error result. If the invariant is violated, the error reporter shows the error message and the state, which invariant violated. The following is my TLA spec:

-------------------------------- MODULE ACP --------------------------------

VARIABLE permissions, restrictions

Users == {"u1", "u2"}

DataTypes == {"T1", "T2"}

Init ==

  /\ permissions = [u1 |-> {"T1"}, u2 |-> {"T2"}]

  /\ restrictions = [u1 |-> {"T2"}, u2 |-> {}]

  

setInvariant == permissions \cap restrictions = {}

AssignPermissions(from, to) ==

  /\ permissions' = [permissions EXCEPT ![to] = @ \cup permissions[from]]

  /\ UNCHANGED <<restrictions>>

  

Next ==

  \/ \E u, v \in Users:

    \/ AssignPermissions(u, v)

Spec == Init /\ [][Next]_<<permissions, restrictions>>

=============================================================================

\* Modification History

\* Last modified Thu Mar 08 18:02:43 IST 2018 by nikhila

\* Created Thu Mar 01 23:34:51 IST 2018 by nikhila

Regards,

Nikhila K N

PhD Scholar,

International Institute of Information Technology,

Bangalore

India

On Thu, Mar 8, 2018 at 1:01 PM, Stephan Merz <stepha...@gmail.com> wrote:

Hello,

what you have done so far looks good. In order for TLC to check the invariant, "setInvariant" should be added to the invariants to be verified (with the box checked) in "Model Overview" -> "What to check?" -> "Invariants".

If that doesn't help, could you explain what doesn't work and perhaps share your specification?

Regards,

Stephan

On 8 Mar 2018, at 07:42, knnik...@gmail.com wrote:

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/2mM6x0Hgrtc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.

[Stephan Merz]

In your specification, the variables permissions and restrictions hold functions (actually, records), not sets.

Perhaps you are used to how functions are represented in the Z or B methods, but in TLA+, functions are primitive values, not sets of pairs. Therefore set operations cannot be used with functions.

Perhaps you want to check the invariant

\A u \in Users : permissions[u] \cap restrictions[u] = {}

Regards,

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

<tla_spec.png>