Re: [tlaplus] Beginner questions

I'll give some answers below and let others complete.

On 2 Nov 2020, at 23:45, Ashish Negi <thisismyidashish@xxxxxxxxx> wrote:

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!

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 ?

Again, no general answer here: your judgement is key. Checking non-properties can help: assert invariants or temporal properties that you expect your system not to satisfy, then compare the counter-example that TLC produces with what you expect. Also, discuss your specification with a colleague: explaining the choices you made may reveal fallacies in reasoning.

Happy TLAing!

Stephan

Thanks for reading

Ashish Negi

--
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/55b63138-2ad1-4ab6-a6f4-c026c2d3de3co%40googlegroups.com.