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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Tue, 5 Dec 2023 14:08:51 -0600*References*: <41e5f249-3277-483c-a78d-f1d97cfe0c8dn@googlegroups.com> <451db5cf-c9dd-4126-921a-f13a7ce5a0aen@googlegroups.com>*User-agent*: Mozilla Thunderbird

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/451db5cf-c9dd-4126-921a-f13a7ce5a0aen%40googlegroups.com.

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/75eae0be-f016-4bc9-bcca-409d2eadb5c8%40gmail.com.

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] Re: How to get all possible initial states from mutually exclusive sets of records?** - Next by Date:
**Re: [tlaplus] Re: How to get all possible initial states from mutually exclusive sets of records?** - Previous by thread:
**[tlaplus] Re: How to get all possible initial states from mutually exclusive sets of records?** - Next by thread:
**Re: [tlaplus] Re: How to get all possible initial states from mutually exclusive sets of records?** - Index(es):