Activity 17: Generate the reachability graph
Generate the reachability graph, which is the basis for test generation, as follows:
-
Define a task for the generation of a reachability graph for IService in file VendingMachine.prj
Generate ReachabilityGraph { ReachabilityGraph_IService for interface IService { max-depth: 30 params: 'IService/IService.params' debug } }
Note that:
-
A maximum depth is specified to ensure the tasks terminates in case the full reachability graph is infinite, e.g. in case of unbounded variables. Decrease depth 30 if the generation takes too much time.
-
The location of the files with input parameters is specified.
-
The "debug" option is added to obtain insight in the generation; since it takes a significant amount of time to generate the debug information, it can be removed for the final test generation.
-
-
Execute the CommaSuite workflow on VendingMachine.prj and inspect folder src-gen/reachabilityGraph/IService. The two main files use a JSON presentation:
-
reachability_graph.json: a graph which shows all possible paths through the state machine of the interface
-
deterministic_scenarios.json: all possible deterministic scenarios based on the reachability graph
The "debug" option leads to three additional files:
-
reachability_graph.html: a graphical representation of the reachability graph
-
builder.txt: a textual representation of the steps taken by the algorithm which produces the reachability graph
-
deterministic_scenarios.txt: a textual representation of all generated scenarios; it also shows the depth reached by the algorithm
-