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

*From*: Chris Ortiz <zitroomega@xxxxxxxxx>*Date*: Wed, 6 Dec 2023 11:10:00 -0800 (PST)*References*: <41e5f249-3277-483c-a78d-f1d97cfe0c8dn@googlegroups.com> <451db5cf-c9dd-4126-921a-f13a7ce5a0aen@googlegroups.com> <75eae0be-f016-4bc9-bcca-409d2eadb5c8@gmail.com>

Thank you very much Andrew and Hillel for the advices. I am still trying to express my simple state machines in math. My intent with a very simple and tiny model is:

2 possible initial states where

[ 0 :> [data |-> "a"] @@ 1 :> [data |-> Erased] ] and [ 0 :> [data |-> Erased] @@ 1 :> [data |-> "a" ] ]

Will transition via Relocate action into a single state

[ 0 :> [data |-> "a"] @@ 1 :> [data |-> "a"] ]

Any advice how to express this in both Init and Next formulas, I really appreciate it.

Best regards,

Zitro

On Tuesday, December 5, 2023 at 12:08:56 PM UTC-8 Hillel Wayne wrote:

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.

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/af172a90-7a84-406d-bc7f-ea01b1c8ba34n%40googlegroups.com.

**Follow-Ups**:

**References**:**[tlaplus] How to get all possible initial states from mutually exclusive sets of records?***From:*Chris Ortiz

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

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

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