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

*From*: Chris Ortiz <zitroomega@xxxxxxxxx>*Date*: Thu, 7 Dec 2023 09:54:32 -0800 (PST)*References*: <41e5f249-3277-483c-a78d-f1d97cfe0c8dn@googlegroups.com> <451db5cf-c9dd-4126-921a-f13a7ce5a0aen@googlegroups.com> <75eae0be-f016-4bc9-bcca-409d2eadb5c8@gmail.com> <af172a90-7a84-406d-bc7f-ea01b1c8ba34n@googlegroups.com> <4EC0D2BE-DE1B-493D-8DFD-909FA05B2DDB@gmail.com>

Thank you Stephan for clarification and correcting me on my nomenclature. The one I posted lastly is not an actual TLA+ but just the idea of what my spec intend to do, as I prematurely thought of but I found better insights from it.

Just a side note: I finally got my spec right by re-writing it as the following below. It took me days to write this simple TLA+ than writing a working program at work. The satisfaction of having a working TLA+ spec gives me a different sense of satisfaction than writing a program. The former gives me this sense of intelligence satisfaction and the latter gives me sense of deliverable accomplishment. Honestly, the former provided me a Eureka moment and an insights which I would have missed in my understanding of what I am trying to accomplish. I am starting to feel what Leslie is saying in those TLA+ videos that there is a benefit of working with TLA+, that is to think abstractly and think better. It hurts my brain but I am started to enjoy this.

EXTENDS Naturals, FiniteSets

CONSTANT JB, Data

ASSUME /\ Cardinality(JB) >= 2

VARIABLES jumboblock

vars == <<jumboblock>>

Invalid == CHOOSE d : d \notin Data

Erased == CHOOSE d : d \notin Data

\*This is possible initial states of jumboblocks which will be involved for relocation

AllPossibleInit == [ jbid: JB, data : (Data \cup {Erased})]

TypeOK ==

/\ jumboblock \in AllPossibleInit \X AllPossibleInit

\*Relocation is a tuple with direction from source to destination, not vice versa.

\*It is only possible if initial conditions below are met

Init ==

/\ jumboblock \in { <<s,d>> \in AllPossibleInit \X AllPossibleInit : /\ s.jbid # d.jbid \*Source and destination should not be same jbid

/\ s.data \in Data \*Source has valid user data

/\ d.data = "" } \*Destination jbid should be erased

Relocate(s,d) ==

/\ jumboblock[1].jbid = s \*Enforce tuple should be source first

/\ jumboblock[2].jbid = d \*Enforce tuple should be destination second

/\ jumboblock[1].data \in Data

/\ jumboblock[2].data = "" /> /\ jumboblock' = [jumboblock EXCEPT ![2].data = "" ] \*Relocation of valid user data to destination jumboblock

Next ==

\/ \E s,d \in JB : Relocate(s,d)

CONSTANT JB, Data

ASSUME /\ Cardinality(JB) >= 2

VARIABLES jumboblock

vars == <<jumboblock>>

Invalid == CHOOSE d : d \notin Data

Erased == CHOOSE d : d \notin Data

\*This is possible initial states of jumboblocks which will be involved for relocation

AllPossibleInit == [ jbid: JB, data : (Data \cup {Erased})]

TypeOK ==

/\ jumboblock \in AllPossibleInit \X AllPossibleInit

\*Relocation is a tuple with direction from source to destination, not vice versa.

\*It is only possible if initial conditions below are met

Init ==

/\ jumboblock \in { <<s,d>> \in AllPossibleInit \X AllPossibleInit : /\ s.jbid # d.jbid \*Source and destination should not be same jbid

/\ s.data \in Data \*Source has valid user data

/\ d.data = "" } \*Destination jbid should be erased

Relocate(s,d) ==

/\ jumboblock[1].jbid = s \*Enforce tuple should be source first

/\ jumboblock[2].jbid = d \*Enforce tuple should be destination second

/\ jumboblock[1].data \in Data

/\ jumboblock[2].data = "" /> /\ jumboblock' = [jumboblock EXCEPT ![2].data = "" ] \*Relocation of valid user data to destination jumboblock

Next ==

\/ \E s,d \in JB : Relocate(s,d)

Thanks again Andrew, Hillel, and Stephan.

More power to TLA+ and to tlaplus group,

zitro

On Thursday, December 7, 2023 at 4:01:20 AM UTC-8 Stephan Merz wrote:

Please note that the operators :> and @@ construct functions, do not use function brackets with those operators. That is, you should write something like(0 :> [data |-> "a"]) @@ (1 :> [data |-> "erased"])StephanOn 6 Dec 2023, at 20:10, Chris Ortiz <zitro...@xxxxxxxxx> wrote: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,ZitroOn 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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/af172a90-7a84-406d-bc7f-ea01b1c8ba34n%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/cbb5a6f7-a21d-4539-9ae5-e0438e4d482en%40googlegroups.com.

**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

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

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

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