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

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)

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"])

Stephan

On 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,
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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/af172a90-7a84-406d-bc7f-ea01b1c8ba34n%40googlegroups.com.