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

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



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 <zitroomega@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:
  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+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.

--
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/4EC0D2BE-DE1B-493D-8DFD-909FA05B2DDB%40gmail.com.