You can also stick two functions together with the TLC module:
EXTENDS TLC
Data' = Data @@ Erased
On 12/5/2023 10:13 AM, Andrew Helwer wrote:
- 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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/451db5cf-c9dd-4126-921a-f13a7ce5a0aen%40googlegroups.com.