## Reachability graph

The reachability graph contains all the possible states (nodes) and transitions (edges) of a CommaSuite model. It can be generated for a single interface. Values for input parameters of commands and signals, if any, have to be specified in a parameters file.

To generate a reachability graph for an interface `Camera.interface` 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: 300
            // 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 → Run As → Run generators). In the above example, the output can be found under `src-gen/reachability_graph/ReachabilityGraph_ICamera`. This folder will contain the reachability graph (`reachability_graph.json`) and a visual representation of the reachability graph (`reachability_graph.html`, double click to open).

### 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 max depth, this is to prevent an endless loop, can be configure in the .prj file.
          "max-depth": 1000,
          // The reached depth, will never be larger than the max depth
          "depth": 24,
          // The initial node (starting point)
          "initial": "S_Off_{''}_V_{{capacityLeft:2,capacityTotal:2}}"
        },
        // Nodes represent all the possible states
        "nodes": {
          // S_Off_{''}_V_{{capacityLeft:2,capacityTotal:2}} is the unique ID of this node
          "S_Off_{''}_V_{{capacityLeft:2,capacityTotal:2}}": {
            // Which place types in the Petrinet produced this node
            "place_types": [
              "parameters",
              "state",
              "variables"
            ],
            // Every node has a friendly name which is the "STATE" or "STATE_transient"
            "friendly_name": "Off"
          },
          "T_Off_0_PowerOn()_{{g:{capacityLeft:2,capacityTotal:2},l:{}}}": {
            "place_types": [
              "parameters",
              "transition"
            ],
            "friendly_name": "Off_transient"
          },
          "C_Off_0_PowerOn()_0_0_{{g:{capacityLeft:2,capacityTotal:2},l:{}}}": {
            "place_types": [
              "clause",
              "parameters"
            ],
            "friendly_name": "Off_transient"
          },
          ...
        // Edges represent all the possible transitions
        "edges": [
          {
            // Source/target refer to nodes of this transition
            "source": "S_Off_{''}_V_{{capacityLeft:2,capacityTotal:2}}",
            "target": "T_Off_0_PowerOn()_{{g:{capacityLeft:2,capacityTotal:2},l:{}}}",
            // Transition name in the Petrinet which produced this edge
            "transition": "T0_event_PowerOn",
            // Optionally and edge has an event
            "event": {
              "kind": "Command",
              "method": "PowerOn",
              "parameters": [],
              "interface": "interfaceCamera",
              "port": "interfaceCamera"
            }
          },
          {
            "source": "T_Off_0_PowerOn()_{{g:{capacityLeft:2,capacityTotal:2},l:{}}}",
            "target": "C_Off_0_PowerOn()_0_0_{{g:{capacityLeft:2,capacityTotal:2},l:{}}}",
            "transition": "T1"
          },
          ...
        ]
      }
    }

In the above example there are 3 possible states. The initial state is `S_Off_{''}_V_{{capacityLeft:2,capacityTotal:2}}`, from this we can transition to `T_Off_0_PowerOn()_{{g:{capacityLeft:2,capacityTotal:2},l:{}}}` by the command `PowerOn()`. Next we can transition to the `C_Off_0_PowerOn()_0_0{{g:{capacityLeft:2,capacityTotal:2},l:{}}}` without executing any event.