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"
},
],
...
}
}