Hi
I am trying to learn TLA+. I have few questions:
Q. I remember reading that everything is a set in TLA+. What about records ?
I am asking to understand how should i think about records while writing TLA spec.
Q. How can i write TypeOK invariant to assert that a variable to be a set that always contains 4 elements ?
I tried, HEAD, LEN but those functions are on sequences. I can't find way to iterate over elements on a set, while maintaining a variable.
Q. How can i write TypeOK invariant for a variable to be in a set of record with start and end fields, where start <= end ?
I wrote:
WriteExtent \in [ { "start", "end" } -> 0..MaxLSN ]
but i can't understand how to add `start <= end` condition ?
Q. How can i write TypeOK invariant to assert that a variable to be in a set of sequence of records with start and end fields ?
Q. Is there something like null or Option in TLA+ to specify that a variable can be a record or null ?
Q. Currently to write my state machine in TLA+ spec, i have 2 additional variables : PrevState and NextState.
In every action, i set PrevState and NextState for telling TLA+ which next Actions are valid.
Is this the standard practice or there is a better way ?
Q. How can i version control the changes in model checker ? I only
see <X>.tla file and a <X>_toolbox folder which is very
large.
I am skipping <X>_toolbox folder in .gitignore.
So, how can i version control the changes like adding `Invariants` other
settings that i make in Model Checker page.
Q. Is there a strategy for understanding/finding "What" of a system, so that we can write spec for it ?
In the die hard lecture video, Leslie mentioned that if we write a sequence of valid events, writing spec becomes easier.
So, when i watched Transaction Commit lecture video, i wrote a spec, after watching first few minutes of video which lists the sequence of steps in marriage process.
However, after completely watching the video, i realized that what i was doing is "How" of system. And this video is focusing on "What" of system.
So, for a spec concerning "How" of system, i can list sequence of steps to understand how to write spec.
Is there a similar strategy for understanding "What" of a system, so that we can write spec for it ?
Q. When i was writing two_phase commit spec, i realized the difference in my spec vs video's spec is that i was not using messages.
So my spec missed checking for cases involving duplicate messages.So, i realized that missing modelling a part of real system can make spec weaker.
However, writing spec also involves abstracting and leaving some details of the system.
My question is if there is any pattern that helped people understand what to include or leave when modelling a system ?
Thanks for reading
Ashish Negi