Thank you Stephan for clarification and correcting me on my nomenclature. The one I posted lastly is not an actual TLA+ but just the idea of what my spec intend to do, as I prematurely thought of but I found better insights from it.
Just a side note: I finally got my spec right by re-writing it as the following below. It took me days to write this simple TLA+ than writing a working program at work. The satisfaction of having a working TLA+ spec gives me a different sense of satisfaction than writing a program. The former gives me this sense of intelligence satisfaction and the latter gives me sense of deliverable accomplishment. Honestly, the former provided me a Eureka moment and an insights which I would have missed in my understanding of what I am trying to accomplish. I am starting to feel what Leslie is saying in those TLA+ videos that there is a benefit of working with TLA+, that is to think abstractly and think better. It hurts my brain but I am started to enjoy this.
EXTENDS Naturals, FiniteSets
CONSTANT JB, Data
ASSUME /\ Cardinality(JB) >= 2
VARIABLES jumboblock
vars == <<jumboblock>>
Invalid == CHOOSE d : d \notin Data
Erased == CHOOSE d : d \notin Data
\*This is possible initial states of jumboblocks which will be involved for relocation
AllPossibleInit == [ jbid: JB, data : (Data \cup {Erased})]
TypeOK ==
/\ jumboblock \in AllPossibleInit \X AllPossibleInit
\*Relocation is a tuple with direction from source to destination, not vice versa.
\*It is only possible if initial conditions below are met
Init ==
/\ jumboblock \in { <<s,d>> \in AllPossibleInit \X AllPossibleInit : /\ s.jbid # d.jbid \*Source and destination should not be same jbid
/\ s.data \in Data \*Source has valid user data
/\ d.data = Erased } \*Destination jbid should be erased
Relocate(s,d) ==
/\ jumboblock[1].jbid = s \*Enforce tuple should be source first
/\ jumboblock[2].jbid = d \*Enforce tuple should be destination second
/\ jumboblock[1].data \in Data
/\ jumboblock[2].data = Erased
/\ jumboblock' = [jumboblock EXCEPT ![2].data = jumboblock[1].data ] \*Relocation of valid user data to destination jumboblock
Next ==
\/ \E s,d \in JB : Relocate(s,d)
Thanks again Andrew, Hillel, and Stephan.
More power to TLA+ and to tlaplus group,
zitro