package nuscr

  1. Overview
  2. Docs
A tool to manipulate and validate Scribble-style multiparty protocols

Install 

dune-project
 Dependency

nuscr.dev Changelog Edit opam file Versions (5)

Authors

  1. F
    Francisco Ferreira
  2. F
    Fangyi Zhou
  3. S
    Simon Castellan
  4. B
    Benito Echarren

Maintainers

  1. F
    Francisco Ferreira

Sources

nuscr-2.1.1.tbz
sha256=c5a419fd1fdea78fb63b3a3c335b0e6b0f2b08d65b79870565bdcc0f997bc728
sha512=83ef593ed514eeef1b10069af54562833d617d1c338c5adaf82ee5c3ea7ec4569b3643fcbb237b3cb79ce2f579094cbd17217efa5f4e522bd20f67e1df3a7dbd

doc/nuscr.lib/Nuscrlib/Efsm/G/index.html

Module Efsm.G

EFSM graph representation

A persistent graph is a graph.

include Graph.Sig.G with type V.t = state with type E.label = action with type E.t = state * action * state

Graph structure

type t

Abstract type of graphs

module V : Graph.Sig.VERTEX with type t = state

Vertices have type V.t and are labeled with type V.label (note that an implementation may identify the vertex with its label)

type vertex = V.t
module E : Graph.Sig.EDGE with type vertex = vertex with type label = action with type t = state * action * state

Edges have type E.t and are labeled with type E.label. src (resp. dst) returns the origin (resp. the destination) of a given edge.

type edge = E.t
val is_directed : bool

Is this an implementation of directed graphs?

Size functions

val is_empty : t -> bool
val nb_vertex : t -> int
val nb_edges : t -> int

Degree of a vertex

val out_degree : t -> vertex -> int

out_degree g v returns the out-degree of v in g.

val in_degree : t -> vertex -> int

in_degree g v returns the in-degree of v in g.

Membership functions

val mem_vertex : t -> vertex -> bool
val mem_edge : t -> vertex -> vertex -> bool
val mem_edge_e : t -> edge -> bool
val find_edge : t -> vertex -> vertex -> edge

find_edge g v1 v2 returns the edge from v1 to v2 if it exists. Unspecified behaviour if g has several edges from v1 to v2.

val find_all_edges : t -> vertex -> vertex -> edge list

find_all_edges g v1 v2 returns all the edges from v1 to v2.

  • since ocamlgraph 1.8

Successors and predecessors

You should better use iterators on successors/predecessors (see Section "Vertex iterators").

val succ : t -> vertex -> vertex list

succ g v returns the successors of v in g.

val pred : t -> vertex -> vertex list

pred g v returns the predecessors of v in g.

Labeled edges going from/to a vertex

val succ_e : t -> vertex -> edge list

succ_e g v returns the edges going from v in g.

val pred_e : t -> vertex -> edge list

pred_e g v returns the edges going to v in g.

Graph iterators

val iter_vertex : (vertex -> unit) -> t -> unit

Iter on all vertices of a graph.

val fold_vertex : (vertex -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all vertices of a graph.

val iter_edges : (vertex -> vertex -> unit) -> t -> unit

Iter on all edges of a graph. Edge label is ignored.

val fold_edges : (vertex -> vertex -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all edges of a graph. Edge label is ignored.

val iter_edges_e : (edge -> unit) -> t -> unit

Iter on all edges of a graph.

val fold_edges_e : (edge -> 'a -> 'a) -> t -> 'a -> 'a

Fold on all edges of a graph.

val map_vertex : (vertex -> vertex) -> t -> t

Map on all vertices of a graph.

The current implementation requires the supplied function to be injective. Said otherwise, map_vertex cannot be used to contract a graph by mapping several vertices to the same vertex. To contract a graph, use instead create, add_vertex, and add_edge.

Vertex iterators

Each iterator iterator f v g iters f to the successors/predecessors of v in the graph g and raises Invalid_argument if v is not in g. It is the same for functions fold_* which use an additional accumulator.

<b>Time complexity for ocamlgraph implementations:</b> operations on successors are in O(1) amortized for imperative graphs and in O(ln(|V|)) for persistent graphs while operations on predecessors are in O(max(|V|,|E|)) for imperative graphs and in O(max(|V|,|E|)*ln|V|) for persistent graphs.

iter/fold on all successors/predecessors of a vertex.

val iter_succ : (vertex -> unit) -> t -> vertex -> unit
val iter_pred : (vertex -> unit) -> t -> vertex -> unit
val fold_succ : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val fold_pred : (vertex -> 'a -> 'a) -> t -> vertex -> 'a -> 'a

iter/fold on all edges going from/to a vertex.

val iter_succ_e : (edge -> unit) -> t -> vertex -> unit
val fold_succ_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val iter_pred_e : (edge -> unit) -> t -> vertex -> unit
val fold_pred_e : (edge -> 'a -> 'a) -> t -> vertex -> 'a -> 'a
val empty : t

The empty graph.

val add_vertex : t -> vertex -> t

add_vertex g v adds the vertex v to the graph g. Just return g if v is already in g.

val remove_vertex : t -> vertex -> t

remove g v removes the vertex v from the graph g (and all the edges going from v in g). Just return g if v is not in g.

<b>Time complexity for ocamlgraph implementations:</b> O(|V|*ln(|V|)) for unlabeled graphs and O(|V|*max(ln(|V|),D)) for labeled graphs. D is the maximal degree of the graph.

val add_edge : t -> vertex -> vertex -> t

add_edge g v1 v2 adds an edge from the vertex v1 to the vertex v2 in the graph g. Add also v1 (resp. v2) in g if v1 (resp. v2) is not in g. Just return g if this edge is already in g.

val add_edge_e : t -> edge -> t

add_edge_e g e adds the edge e in the graph g. Add also E.src e (resp. E.dst e) in g if E.src e (resp. E.dst e) is not in g. Just return g if e is already in g.

val remove_edge : t -> vertex -> vertex -> t

remove_edge g v1 v2 removes the edge going from v1 to v2 from the graph g. If the graph is labelled, all the edges going from v1 to v2 are removed from g. Just return g if this edge is not in g.

val remove_edge_e : t -> edge -> t

remove_edge_e g e removes the edge e from the graph g. Just return g if e is not in g.