Module `Fixpoint_graph.Make`

Parameters

module G : Graph

Signature

module ControlLocation : sig ... end

Control locations are also vertices in the graph. We provide to_int that uniquely identifies each node, as they will be used as keys in PatriciaTree.

include Fixpoint_wto.Graph
  with module ControlLocation := ControlLocation
   and type transition = G.transition

type transition = G.transition

val preds_with_transition : 
  ControlLocation.t ->
  (ControlLocation.t * transition) list

val succs : ControlLocation.t -> ControlLocation.t list

The list of successors from each node.

val make : 
  G.Vertex.t ->
  (G.Vertex.t -> (transition * G.Vertex.t) list) ->
  ControlLocation.t * ControlLocation.t * int

make init succs traverses the exiting graph to creates a new graph suitable for wto iteration. It returns a triple input_node,first_node,count where

first_node corresponds to init in the original graph;
input_node is a (pseudo-)node before first_node, which should not be part of the fixpoint computation, as it is used to hold the initial value for the fixpoint graph
count is the number of nodes in the graph.

Module Fixpoint_graph.Make

Parameters

Signature

Module `Fixpoint_graph.Make`