package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Weak topological orderings (WTOs) are a hierarchical decomposition of the a graph where each layer is topologically ordered and strongly connected components are aggregated and ordered recursively. This is a very convenient representation to describe an evaluation order to reach a fixpoint.

type 'n component =
  1. | Component of 'n * 'n partition
    (*

    A strongly connected component, described by its head node and the remaining sub-components topologically ordered

    *)
  2. | Node of 'n
    (*

    A single node without self loop

    *)

Each component of the graph is either an individual node of the graph (without) self loop, or a strongly connected component where a node is designed as the head of the component and the remaining nodes are given by a list of components topologically ordered.

and 'n partition = 'n component list

A list of strongly connected components, sorted topologically

val head : 'n partition -> 'n option

Return the first node of a partition or None if the partition is empty

val flatten : 'n partition -> 'n list

Transform the partition into a list

val fold_heads : ('a -> 'n -> 'a) -> 'a -> 'n partition -> 'a
module Make (Node : sig ... end) : sig ... end

This functor provides the partitioning algorithm constructing a WTO.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct