[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



  1. 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
  2. Same thing in your Init, remove the enclosing curly braces.
  3. 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.