I'll give some answers below and let others complete.
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.
Semantically, everything is a set but there are many values for which we do not care to know how they are represented as sets, such as numbers or functions. This is also true for records: think of them as primitive.
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.
How about Cardinality(var) = 4? But probably you also want to fix the "type" of the elements of the set. For example, if you have a set of positive integers, you could write
/\ var \in SUBSET (Nat \ {0})
/\ Cardinality(var) = 4
[The Cardinality operator is defined in the FiniteSets module, which you must extend or instantiate.]
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 ?
/\ WriteExtent \in [start : 0 .. MaxLSN, end : 0 .. MaxLSN]
/\ WriteExtent.start <= WriteExtent.end
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 ?
Do you mean that the value of the variable is always a sequence of such records? Write
var \in Seq([start : ..., end : ...])
Q. Is there something like null or Option in TLA+ to specify that a variable can be a record or null ?
Sometimes you can actually avoid null values. For example, suppose that you model bank accounts. You may have a constant ID for representing all possible account numbers, a record type Account that represents account information, and a variable
account \in [ID -> Account]
But since some IDs are not associated with accounts, you need a null value. Instead, you could have two variables
/\ usedID \in SUBSET ID \* set of IDs with open accounts
/\ account \in [usedID -> Account]
Which version works better is for you to decide: it may well be clearer to introduce null values. If you decide to do so, there are different established idioms, choose according to preference and readability of the spec.
1. Make the null value a parameter of your specification.
CONSTANT null
ASSUME null \notin ... \* the "type" to which you add the null value
When running TLC, instantiate the parameter `null' by a model value.
2. Define a null value using a CHOOSE _expression_.
null == CHOOSE x : x \notin ... \* again, the type to which the null value is added
The Toolbox will recognize such definitions, introduce a model value, and override the definition to assign that model value to `null'.
3. In conjunction with records, you can add an extra field to the record to distinguish records containing valid information from "null" records, like so:
var \in [valid : BOOLEAN, ....] \* "...." stands for the fields that your record would normally have
Then write var.valid to distinguish "valid" records from null records.
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 ?
Not sure what these variables represent. You may need a variable representing the control state (similar to how the PlusCal translator encodes the current location of the algorithm or processes) but I don't understand why you use two variables.
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.
I'll leave this one to others who know better. Essentially you only need to version control the .tla and .cfg files in the Model_X subdirectories of the .toolbox directories.
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 ?
Practice, practice, practice ... this is the hard part!