[tlaplus] How to get all possible initial states from mutually exclusive sets of records?

[Chris Ortiz <zitroomega@xxxxxxxxx>]

Hello TLAPlus Group,

I need help as I am trying to understand why I am getting this error below.

Attempted to enumerate S \cup T when S:
<<[data |-> "a"]>>
and T:
(0 :> [data |-> Erased])
are not both enumerable
While working on the initial state:
jumboblock = {<<[data |-> "a"]>> \cup (0 :> [data |-> Erased])}

Here is the Module I am working on where I am getting this problem. I appreciate any help or tips to make me understand what I am missing on my spec or make it better.

-------------------------------

EXTENDS Naturals, FiniteSets

CONSTANT JB, Data

VARIABLES jumboblock
vars == <<jumboblock>>


Invalid == CHOOSE d : d \notin Data
Erased == CHOOSE d : d \notin Data

TypeOK ==
    /\ jumboblock \in {[ JB -> [data : (Data \cup {Erased})]]}
                               

Init ==
    /\ \E s, d \in (SUBSET JB), z \in Data:
            /\ s # {} /\ d # {} /\ s \cap d = {}
            /\ jumboblock = {[ x \in s |-> [ data |-> z]] \cup [ y \in d |-> [ data |-> Erased ]]}

Relocate(s,d) ==
    /\ jumboblock[s].data \in Data
    /\ jumboblock[d].data = "" />    /\ jumboblock' = [jumboblock EXCEPT ![d].data = "" />
Next ==
    \/ \E s, d \in JB : Relocate(s, d)


Spec == Init /\ [][Next]_vars

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

Thanks,

Zitro

-- 
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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/41e5f249-3277-483c-a78d-f1d97cfe0c8dn%40googlegroups.com.