You can also stick two functions together with the TLC module:
EXTENDS TLC
Data' = Data @@ Erased
--
- In your TypeOK, remove the curly braces enclosing the right hand side; all that's doing is making a set with a single element, that single element being a set of functions
- Same thing in your Init, remove the enclosing curly braces.
- You can't stick two functions together by taking their union. If you want to do that you have to define a function over the union of the domains of your two functions.
Andrew
--On Monday, December 4, 2023 at 7:28:32 PM UTC-5 Chris Ortiz wrote:
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/451db5cf-c9dd-4126-921a-f13a7ce5a0aen%40googlegroups.com.