Modeling tutorial¶

In this tutorial we create a small model of the fire system. This follows the method described in [ROS2000].

Domain definition¶

First we create a list of input to test the features of our SUT.

Input	Description
login	Enter username/password, click “let me in!”
logout	Click on the logout link (top right)
clickLab	Click on the first lab
addFile	Upload one file to the first lab
rmFile	Remove one file from the first lab
submit	Click the submit button
withdraw	Click the withdraw button

State space¶

Some input are only available on certain pages. For instance, you can only login from the login page, or you can only add files on the lab page, etc. This gives us the operational mode Page = { Login, Home, Lab }

Adding and removing files (as well as submitting) are only possible if the submission is not yet submitted, so we have the operational mode LabStatus = { Open, Submitted }

Finally, to remove a file there need to be at least one file in the system, so we can add an additional mode NbFiles = { n \in N, n >= 0}. (Note that, unlike the operational modes in the paper, this one has an infinite number of possible values).

So every state in my model is a combination of a Page value, a LabStatus value and a NbFiles value. For instance, Login, Open, 2 or Lab, Submitted, 1.

Transition table¶

The transition table describes, for each possible state and each input, what is the resulting state. Invalid combination of State+input are omitted (e.g. Home, Open, 0 and login).

State before	Input	State after
`Login, Open, $n`	`login`	`Home, Open, $n`
`Login, Submitted, $n`	`login`	`Home, Submitted, $n`
`Home, Open, $n`	`logout`	`Login, Open, $n`
`Home, Submitted, $n`	`logout`	`Login, Submitted, $n`
`Lab, Open, $n`	`logout`	`Login, Open, $n`
`Lab, Submitted, $n`	`logout`	`Login, Submitted, $n`
`Home, Open, $n`	`clickLab`	`Lab, Open, $n`
`Home, Submitted, $n`	`clickLab`	`Lab, Submitted, $n`
`Lab, Open, $n`	`addFile`	`Lab, Open, $n ← n + 1`
`Lab, Open, $n>0`	`rmFile`	`Lab, Open, $n ← n - 1`
`Lab, Open, $n`	`submit`	`Lab, Submitted, $n`
`Lab, Submitted, $n`	`withdraw`	`Lab, Open, 0`

Model diagram¶

I need to choose which of my operational modes are best represented in the visible states (the bubbles) and which should be internal variables.

One possible way to do that is to represent finite values (i.e. Page and LabStatus) in the visible states and infinite mode (i.e. NbFiles) as internal variables, giving the following diagram with the internal variable $f representing the number of uploaded files, initialized to 0:

digraph model1 { "Login, Open" -> "Home, Open" [label="login"]; "Login, Submitted" -> "Home, Submitted" [label=login]; "Home, Open" -> "Login, Open" [label=logout]; "Home, Submitted" -> "Login, Submitted" [label=logout]; "Lab, Open" -> "Login, Open" [label=logout]; "Lab, Submitted" -> "Login, Submitted" [label=logout]; "Home, Open" -> "Lab, Open" [label=clickLab]; "Home, Submitted" -> "Lab, Submitted" [label=clickLab]; "Lab, Open" -> "Lab, Open" [label="addFile ; $f++\l[$f>0] rmFile ; $f--\l"]; "Lab, Open" -> "Lab, Submitted" [label=submit]; "Lab, Submitted" -> "Lab, Open" [label="withdraw ; $f ← 0"]; }

But we can see a lot of redundancy here and maybe we can get a simpler diagram by treating LabStatus as an internal variable $s initialized to Open (in addition to the $f variable as before). This creates a smaller diagram but note that we then need more guards:

digraph model1 { "Login" -> "Home" [label="login"]; "Home" -> "Login" [label=logout]; "Lab" -> "Login" [label=logout]; "Home" -> "Lab" [label=clickLab]; "Lab" -> "Lab" [label="[$s=Open] addFile ; $f++\l[$s=Open & $f>0] rmFile ; $f--\l[$s=Open] submit ; $s←Submitted\l[$s=Sumbitted] withdraw ; $s←Open, $f←0\l"]; }

We could push this to the extreme and have only internal variable and a single visible state, but this is silly. Don’t do it!

digraph model1 { "" -> "" [label="[$p=Login] login ; $p←Home\l[$p≠Login] logout ; $p←Login\l[$p=Home] clickLab ; $p←Lab\l[$p=Lab & $s=Open] addFile ; $f++\l[$p=Lab & $s=Open & $f>0] rmFile ; $f--\l[$p=Lab & $s=Open] submit ; $s←Submitted\l[$p=Lab & $s=Sumbitted] withdraw ; $s←Open, $f←0\l"]; }