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