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.