=================
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"];