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