## Reachability graph

The reachability graph contains all the possible states (nodes) and transitions (edges) of a CommaSuite model. To generate a reachability graph add the following to the `.prj` file, e.g. using content assist (ctrl + space):

    import "Camera.interface"

    Project Camera {
      Generate ReachabilityGraph {
        // ReachabilityGraph_ICamera is the name of the job (can be anything).
        ReachabilityGraph_ICamera for interface ICamera
        {
            // The traversal of the generator is limited by "max-depth"
            max-depth: 30
            // In case any of the triggers in the interface has parameters,
            // values for these variables have to be defined in the ".params" file.
            // Consult the Parameters section below for more information.
            // This file is not required when none of the triggers have parameters.
            params: "Camera.params"
        }
    	}
    }

To generate the reachability graph, run the `.prj` (right click on the `.prj` file → Execute CommaSuite Workflow). In the above example, the output can be found under `src-gen/reachabilityGraph.ICamera`. This folder will contain the reachability graph (`reachability_graph.json`).

### Reachability graph JSON

The `reachability_graph.json` represents a graph and follows the json-graph-specification. An example:

    {
      "graph": {
        // Contains some metadata of this reachability graph
        "metadata": {
          // The initial node (starting point)
          "initial": "Off_2_2",
          // The reached depth, will never be larger than the max depth
          "depth": 16,
          // The max depth, this is to prevent an endless loop, can be configure in the .prj file.
          "max-depth": 30,
          // The total amount of states in the CommaSuite model (interface/component)
          "total-states": 3,
          // The amount of states that have been covered by this reachability graph
          "covered-states": 3,
          // The total amount of clauses in the CommaSuite model (interface/component)
          "total-clauses": 9,
          // The amount of clauses that have been covered by this reachability graph
          "covered-clauses": 9
        },
        // Nodes represent all the possible states
        "nodes": {
          // 'Off_2_2' is the unique ID of this node
          "Off_2_2": {
            // The state of this node (matches the states found in the CommaSuite model)
            "state": "Off"
          },
          "PoweredOn_2_2": {
            "state": "PoweredOn"
          },
          "Off_2_2_Triggered_PowerOn": {
            "state": "Off",
            // Intermediate nodes have a trigger (in this case the command PowerOn())
            "trigger": "PowerOn"
          },
          ...
        },
        // Edges represent all the possible transitions
        "edges": [
          {
            // Source/target refer to nodes of this transition
            "source": "Off_2_2",
            "target": "Off_2_2_Triggered_PowerOn",
            // Entries is a list of events that are required to reach the next state (target).
            // To reach the Off_2_2_Triggered_PowerOn state the command PowerOn() has to be executed.
            "entries": [
              {
                "method": "PowerOn",
                "type": "void",
                // Arguments of this command
                "arguments": [
                    {"direction": "in", "type": "int", "value": 5},
                    {"direction": "out", "type": "int", "value": 0},
                ],
                "kind": "Command"
              }
            ]
          },
          {
            "source": "Off_2_2_Triggered_PowerOn",
            "target": "PoweredOn_2_2",
            "entries": [
              {
                "method": "PowerOn",
                "order": 0,
                "arguments": [
                    {"direction": "out", "type": "int", "value": 20}
                ],
                "kind": "Reply",
                "return_value": {"type": "int", "value": 6}
              }
            ]
          },
          ...
        ]
      }
    }

In the above example there are 3 possible states. The initial state is `Off_2_2`, from this we can transition to `Off_2_2_Triggered_PowerOn` by the command `PowerOn(5)`. Next we can transition to the `PoweredOn_2_2` state by the reply to the `PowerOn()` command with the output parameter being `20` and the return value being `6`.

### Parameters

If any of the triggers in the CommaSuite model require parameters, values for these parameters have to be provided through a `.params` file. Next to the `.interface` file, create a file called `INTERFACE_NAME.params`. Start the file by importing the interface (e.g. `import Camera.interface`), then open the content assist (ctrl + space) and select "Autocomplete missing triggers". Next fill in the desired parameters and the `.params` file is complete. An example of a `.params` file:

    // The interface we want to provide parameters for
    import "Camera.interface"

    // The trigger (command or signal)
    trigger: SetZoom
    // The state we are providing parameters for
    state: PoweredOn
    // The provided parameters, note that multiple parameters sets can be provided
    params: ( 3, 9 )
    params: ( 11, 5 )
    // Next to SetZoom in the PoweredOn state, we also provided parameters for SetZoom in the PoweredOff state.
    state: PoweredOff
    params: ( 21, 5 )

    trigger: GetCapacity
    state: PoweredOn
    params: ( CapacityType::Total )
    params: ( CapacityType::Remaining )

### Deterministic scenarios JSON

The `deterministic_scenarios.json` file contains all possible deterministic scenarios that can be generated from the reachability graph. This can be used for e.g. test generation. These scenarios cover all possible paths through the reachability graph and stop when a loop is detected. Example:

    {
      "scenarios": [
        [
          // Scenario 1
          {
            "method": "PowerOn",
            "type": "void",
            "arguments": [],
            "kind": "Command"
          },
          {
            "method": "PowerOn",
            "order": 0,
            "arguments": [],
            "kind": "Reply"
          },
          ...
        ],
        [
          // Scenario 2
          {
            "method": "PowerOn",
            "type": "void",
            "arguments": [],
            "kind": "Command"
          },
          {
            "method": "PowerOn",
            "order": 0,
            "arguments": [],
            "kind": "Reply"
          },
          {
            "method": "TakePicture",
            "type": "Status",
            "arguments": [],
            "kind": "Command"
          },
          ...
        ]
      ]
    }

The JSON contains a property callled `scenarios` which is a list of lists. Each list represents a scenario and each entry of the scenario represents an action. These actions have the same format as the actions in `entries` of the `reachability_graph.json`.

### Example

An example of the reachability graph generation is included in CommaSuite. It can be imported by clicking File (left-top) → New → Example → Test Generation Example → Next → Finish. The `Camera.prj` file contains the reachability graph generator.

### Debug

To get more insight in how the reachablity graph was build, the debug option can be enabled. This can be done by providing the `debug` flag. For instance:

    Generate ReachabilityGraph {
        ReachabilityGraph_ICamera for interface ICamera
        {
            max-depth: 30
            params: "Camera.params"
            debug  // <-- Add this
        }
    }

After running the generator there will be 3 more files next to the `reachability_graph.json`:

- `builder.txt`: This file shows how the CommaSuite model was traversed. An explanation can be found at the top of the file.

- `reachability_graph.html`: This file contains a visual representation of the reachability graph.

- `deterministic_scenarios.txt`: This file shows all possible deterministic scenarios (used for test generation) that can be generated from the reachability graph. These scenarios cover all possible paths through the reachability graph and stop when a loop is detected.

### Component

The reachability graph generator also supports components. Note that the reachability graph will only contain the `provided port`. All `required port` and all constraints that refer to a `required port` are skipped. Example:

    Generate ReachabilityGraph {
        // Instead of "for interace" use "for component".
        ReachabilityGraph_MyComponent for component MyComponent
        {
            max-depth: 30
            // For each interface having triggers with parameters, a .params file has to be provided.
            params: "Interface1.params" "Interface2.params"
        }
    }

The `entries` in the `reachability_graph.json` will include 2 additional attributes: `port` and `connection`. An example:

    {
        "graph": {
            "edges": [
                {
                    "entries": [{
                        "arguments": [],
                        // Connnection of this command
                        "connection": "id1",
                        "kind": "Command",
                        "method": "Start",
                        // Port of this command
                        "port": "temperaturePort",
                        "type": "void"
                    }],
                    "source": "imagePort_id1_NotImaging__temperaturePort_id1_Stopped",
                    "target": "imagePort_id1_NotImaging__temperaturePort_id1_Stopped_Triggered_Start"
                },
            ],
            ...
        }
    }