Activity 17: Generate the reachability graph

Generate the reachability graph 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: 300
            params: 'IService/IService.params'
        }
      }

    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 300 if the generation takes too much time.

    • The location of the files with input parameters is specified.

  • Execute the CommaSuite workflow on VendingMachine.prj and inspect folder src-gen/reachability_graph/ReachabilityGraph_IService. The two main files:

    • reachability_graph.json: a graph which shows all possible paths through the state machine of the interface

    • reachability_graph.html: a visual representation of the reachability graph (double click to open)