# Model quality checks

The model quality checker checks an interface for various properties like deadlocks and race conditions. Under de hood, the CommaSuite model is converted into a Petri Net. Using this Petri Net, a reachability graph is generated where the checks are executed on. For interfaces with input parameters, a parameters file is required.

To enable the model quality checker, add a generator task for ModelQualityChecks to the `.prj` file, e.g. using content assist (`CTRL` + `SPACE`). An example:

    import "Camera.interface"

    Project Camera {

    	Generate ModelQualityChecks {
    		ModelQualityChecks_Camera for interface Camera {
    		    params: 'Camera.params'
    		    reachability-graph : {
    		    	max-depth: 100
    		    }
    		    verification-report : {
    		    	home-states: { Off }
    		    }
    		}
    	}
    }

Next run the `.prj` (right click on the `.prj` file > Run As > Run generators). The results can be found under the `src-gen` directory.

This generator task has the following options:

- `params` (only needed when the interface has input parameters): path to the parameters file.

- `reachability-graph` (optional): outputs the used reachability graph to `reachability_graph.json` and `reachability_graph.html` in the `src-gen` directory. To allow movement of nodes in the graph, open the html file in a separate browser. For instance, to use Edge: right-click on html file > Open With > Other > External Programs > Microsoft Edge HTML Document.

  - Optionally set the `max-depth` of the reachability graph (defaults to 30). The `max-depth` limits the depth when generating the reachabilty graph from the Petri Net; each step in the Petri Net increases the depth by one. Whether the max depth was reached can be found in the verification report, see Statistics > Reachability graph coverage:

    - full indicates that the max depth was not reached;

    - partial indicates that the max depth was reached. Note that constructions like counters may create an infinite state space; then the reachability graph coverage will always be partial. In this case, no checks are performed, so it might be useful to (temporarily) make the state space finite, e.g., by adding guards.

- `verification-report` (optional): create a verification report containing the results; the report can be found in the `src-gen` directory as `verification_report.html`.

  - Optionally the `home-states` for the livelock check can be set, see livelock state below for a further explanation of home states. To specify multiple home states the following syntax can be used: `home-states: { idle } { on }`. To specify multiple home states for an interface containing multiple state machines the following sytnax can be used: `home-states: { idle off } { on off }`.

  - Note that the verification checks use the reachability graph. When no `reachability-graph` is present in the task, one will be generated with a default `max-depth` of 30.

  - In case the reachablility graph coverage is partial, no checks are executed. Then the Statistics column of the reprt will be empty.

- `petri-net-model` (optional): outputs the Petri Net to `net.py` in the `src-gen` directory. The Petri Net is constructed with the SNAKES Python library.

- `picture` (optional): visualizes the Petri Net to `net.png` in the `src-gen` directory. It contains a message when the Petri Net is too big to be shown.

## Properties

The following properties can be found in the verification report:

- Unreachable state: a state that is not reachable from the initial state.

- Deadlock state: a reachable state from where no transitions can be taken.

- Sink state: a reachable state which cannot be left anymore after entering it, but - unlike a deadlock state - it should have self-transitions that can be executed.

- Livelock state: a reachable state from where none of the home states can be reached by at least one step. When the interface contains multiple parallel state machines, a home state is a set of states containing a state of each machine in the interface. For instance, if the interface has two state machines, a home state will contain two states where one comes from the first machine and one from the second machine. If no home states are provided, the home states will default to one home state containing the initial state of each machine.

- Choice state: a reachable state from which both a non-triggered and triggered transition can be executed.

- Client/server race conditions: a race happens when the client and server take different transitions ending up in a state from which they cannot handle events from the other party. For this check it is assumed that the client is a mirror of the server. There are 2 categories of races:

  - Error: either the server or client ended up in a state where it cannot handle an event from the other party. If the client cannot handle the reply or notification from the server the race is considered a client side race. If the server cannot handle the command or signals from the client the race is considered a server side race.

  - Warning: there are 2 possible types of warnings:

    - Different state: the server and client end up in different states after handling events from each other. This race will show up on both the client and server side.

    - Parameters: the client sends a command to the server where the server can handle the command but not with the specified parameters. In this case the parameters should be added to the `.params` file. This race always shows up on the client side.

- Simple confusion: a simple confusion happens when from a state the same event could lead to different states or events. Example; given we are in state A with 2 possible transitions:

  - state A → Notification1 → Notification2 → state B

  - state A → Notification1 → state C

  - Two problems can be found here:

    1. When the server sends Notification1, the client cannot determine whether to also expect a Notification2.

    2. When the server sends Notification1 and Notification2, the client could transition to state C while the server transitions to state B.

- Generalized confusion: a generalized confusion reports problems that can occur due to messages arriving out-of-order, usually due to lack of guarantees by underlying middleware, for e.g. when using UDP transport. Such problems lead to client and server ending up in different states and as a consequence, may not be able to handle messages from each other. Each such detected scenario is presented as a sequence diagram.