package lascar

  1. Overview
  2. Docs
package lascar
Legend:
Library
Module
Module type
Parameter
Class
Class type

Functor for computing the external product, in different flavors, of two LTSA

Parameters

module S1 : T
module S2 : T

Signature

include T with type state = S1.state * S2.state and type label = S1.label option * S2.label option and type attr = S1.attr * S2.attr
type state = S1.state * S2.state

The type of state identifiers

type label = S1.label option * S2.label option

The type of state identifiers

The type of transition labels

type attr = S1.attr * S2.attr

The type of transition labels

The type of state attributes

type transition = state * label * state

The type for transition. A transition is a triplet (s1,l,s2), where s1 is the source state, s2 the destination state and l the transition label

type itransition = label * state

The type for transition. A transition is a triplet (s1,l,s2), where s1 is the source state, s2 the destination state and l the transition label

The type for initial transition. An initial transition is a pair (l,s), where s is the destination state and l the transition label

type t

The type of Labeled Transition Systems with state attributes

module State : STATE with type t = state
module Label : LABEL with type t = label
module Attr : ATTR with type t = attr
module States : Utils.SetExt.S with type elt = state
module Attrs : Map.S with type key = state
module Tree : Utils.Tree.S with type node = state and type edge = label
val states : t -> States.t

Returns the set of states

val states' : t -> (state * attr) list

Returns the set of states

Returns the set of states, with attached attribute as a assocation list

val istates : t -> States.t

Returns the set of states, with attached attribute as a assocation list

Returns the set of initial states

val istates' : t -> state list

Returns the set of initial states

Returns the set of initial states as a list

val transitions : t -> transition list

Returns the set of initial states as a list

Returns the list of transitions

val itransitions : t -> itransition list

Returns the list of transitions

Returns the list of initial transitions

val string_of_state : state -> string

A synonym of State.to_string

val string_of_label : label -> string

A synonym of State.to_string

A synonym of Label.to_string

val string_of_attr : attr -> string

A synonym of Label.to_string

A synonym of Attr.to_string

Inspectors

val is_state : t -> state -> bool

is_state s q returns true iff q is a state in s

val is_init_state : t -> state -> bool

is_state s q returns true iff q is a state in s

is_init s q returns true iff q is an initial state in s

val is_reachable : t -> state -> bool

is_init s q returns true iff q is an initial state in s

is_reachable s q returns true iff q is a reachable state in s, i.e. if it can be reached from an initial state using the transitio relation.

val is_transition : t -> transition -> bool

is_reachable s q returns true iff q is a reachable state in s, i.e. if it can be reached from an initial state using the transitio relation.

is_transition t q returns true iff t is a transition in s

val succs : t -> state -> States.t

succs s q returns the set of immediate successors in s, i.e. the set of state q' such that there exists a transition (q,l,q') in R. Raise Invalid_argument if q is not in s.

val succs' : t -> state -> (state * label) list

succs s q returns the set of immediate successors in s, i.e. the set of state q' such that there exists a transition (q,l,q') in R. Raise Invalid_argument if q is not in s.

succs' s q returns the list of immediate successors, with the associated transition label, of state q in s. Raise Invalid_argument if q is not in s.

val preds : t -> state -> States.t

preds s q returns the set of immediate predecessors of state q in s, i.e. the set of state q' such that there exists a transition (q',l,q) in R. Raise Invalid_argument if q is not in s.

val preds' : t -> state -> (state * label) list

preds s q returns the set of immediate predecessors of state q in s, i.e. the set of state q' such that there exists a transition (q',l,q) in R. Raise Invalid_argument if q is not in s.

preds' s q returns the list of immediate predecessors, with the associated transition label, of state q in s. Raise Invalid_argument if q is not in s.

val succs_hat : t -> state -> States.t

preds' s q returns the list of immediate predecessors, with the associated transition label, of state q in s. Raise Invalid_argument if q is not in s.

Transitive closure of succs. succs_hat s q returns all the successors (immediate or not) of q in s

val preds_hat : t -> state -> States.t

Transitive closure of succs. succs_hat s q returns all the successors (immediate or not) of q in s

Transitive closure of preds. preds_hat s q returns all the predecessors (immediate or not) of q in s

val attr_of : t -> state -> attr

attr_of s q returns the attribute of state q in s. Raise Not_found if there is no state q in s

Building functions

val empty : t

The empty LTSA (no state, no transition)

val create : states:(state * attr) list -> itrans:(label * state) list -> trans:(state * label * state) list -> t

create qs q0s ts builds a LTSA from

  • a list of states identifiers, each with an attached attribute
  • a list of initial transitions, where each transition is given as (label,dst_state)
  • a list of transitions ts, where each transition is given as (src_state,label,dst_state)
val add_state : (state * attr) -> t -> t

add_state (q,a) s returns the LTSA obtained by adding state q, with attribute a, to s. Returns s is q is already a state in s

exception Invalid_state of state
val add_transition : (state * label * state) -> t -> t

add_transition (q1,l,q2) s returns the LTSA obtained by adding transition from state q1 to state q2, with label l to LTSA s. Raises Invalid_state if q1 or q2 are not states of s

val add_itransition : (label * state) -> t -> t

add_itransition (l,q) s returns the LTSA obtained by adding initial transition to state q, with label l to LTSA s. Raises Invalid_state if q are is not a state of s

val remove_state : state -> t -> t

remove_state q s returns the LTSA obtained by removing state q, and all attached transitions, from s. Raises Invalid_state is q is not a state in s

Global iterators

val iter_states : (state -> attr -> unit) -> t -> unit

iter_states f s applies function f to all states (with associated attribute) of s

val fold_states : (state -> attr -> 'a -> 'a) -> t -> 'a -> 'a

iter_states f s applies function f to all states (with associated attribute) of s

fold_states f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the states of s

val iter_transitions : (transition -> unit) -> t -> unit

fold_states f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the states of s

iter_transitions f s applies function f to all transitions of s

val fold_transitions : (transition -> 'a -> 'a) -> t -> 'a -> 'a

iter_transitions f s applies function f to all transitions of s

fold_transitions f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the transitions of s

val iter_itransitions : (itransition -> unit) -> t -> unit

fold_transitions f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the transitions of s

iter_itransitions f s applies function f to all initial transitions of s

val fold_itransitions : (itransition -> 'a -> 'a) -> t -> 'a -> 'a

iter_itransitions f s applies function f to all initial transitions of s

fold_itransitions f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the initial transitions of s

State iterators

val fold_succs : t -> state -> (state -> label -> 'a -> 'a) -> 'a -> 'a

fold_succs s x f z computes f xN lN ... (f x2 (f x1 l1 z) l2)..., where x1, ..., xN are all the successors of state x in LTSA s, and l1, ..., lN the associated transitions labels

val iter_succs : t -> state -> (state -> label -> unit) -> unit

fold_succs s x f z computes f xN lN ... (f x2 (f x1 l1 z) l2)..., where x1, ..., xN are all the successors of state x in LTSA s, and l1, ..., lN the associated transitions labels

iter_succs s x f z computes f x1 l1; ... ;f xN lN, where x1, ..., xN are all the successors of state x in LTSA s, and l1, ..., lN the associated transitions labels

val fold_preds : t -> state -> (state -> label -> 'a -> 'a) -> 'a -> 'a

iter_succs s x f z computes f x1 l1; ... ;f xN lN, where x1, ..., xN are all the successors of state x in LTSA s, and l1, ..., lN the associated transitions labels

fold_preds s x f z computes f xN lN ... (f x2 (f x1 l1 z) l2)..., where x1, ..., xN are all the predecessors of state x in LTSA s, and l1, ..., lN the associated transitions labels

val iter_preds : t -> state -> (state -> label -> unit) -> unit

fold_preds s x f z computes f xN lN ... (f x2 (f x1 l1 z) l2)..., where x1, ..., xN are all the predecessors of state x in LTSA s, and l1, ..., lN the associated transitions labels

iter_preds s x f z computes f x1 l1; ... ;f xN lN, where x1, ..., xN are all the predecessors of state x in LTSA s, and l1, ..., lN the associated transitions labels

Global transformations

val map_state : (state -> state) -> t -> t

map_state f s returns the LTSA obtained by replacing each state q by f q in s. Result is undefined if f is not injective.

val map_attr : (attr -> attr) -> t -> t

map_attr f s returns the LTSA obtained by replacing each state attribute a by f a in s.

val map_label : (label -> label) -> t -> t

map_label f s returns the LTSA obtained by replacing each transition label l by f l in s.

val clean : t -> t

Removes unreachable nodes and associated transitions

val unwind : int -> t -> Tree.t list

unwind depth s unwinds LTSA system s to produce a list of execution trees (rooted at initial states) up to the specified depth

Output functions

val dot_output : string -> ?fname:string -> ?options:Utils.Dot.graph_style list -> ?marked_states:(state * Utils.Dot.node_style) list -> ?extra_nodes:(string * Utils.Dot.node_style) list -> ?implicit_transitions:transition list -> t -> unit

dot_output name s writes a .dot representation of s with name name. The name of the output file is name.dot or specified with the fname optional argument. States listed with the optional argument marked_states will be drawn with the specified style. Extra nodes, to be added to the generated graph, can be specified with the extra_nodes optional argument. Transitions listed in the implicit_transitions optional argument will not be drawn.

val dot_output_oc : string -> out_channel -> ?options:Utils.Dot.graph_style list -> ?marked_states:(state * Utils.Dot.node_style) list -> ?extra_nodes:(string * Utils.Dot.node_style) list -> ?implicit_transitions:transition list -> t -> unit

dot_output_coc name oc s is a variant of dot_output in which the description of s is written to the (previously opened) output channel oc.

val dot_output_execs : string -> ?fname:string -> ?options:Utils.Dot.graph_style list -> int -> t -> unit

dot_output_execs name depth s writes a .dot representation, with name name of the execution trees obtained by calling unwind depth s. The name of the file is name.dot or specified with the fname optional argument. Drawing options can be specified with the options optional argument.

val tex_output : string -> ?fname:string -> ?listed_transitions:label list option -> t -> unit

tex_output name fname s writes a .tex representation of s with name name. The name of the output file is name.dot or specified with the fname optional argument. When the optional argument listed_transitions is Some l, only transitions listed in l are written, otherwise all transitions of s are written.

val free_product : S1.t -> S2.t -> t

free_product s1 s2 computes the free product of the two LTSA s1 and s2. If s1=<Q1,L1,A1,a1,I1,R1> and s2=<Q2,L2,A2,a2,I2,R2>, then the free_product s1 s2 is <Q,L,A,a,I,R> where

  • Q = Q1xQ2
  • L = L1 U L2 U L1xL2
  • A = A1xA2
  • a(q1,q2) = a1(q1),a2(q2)
  • I = I1xI2
  • R, subset of QxLxQ, is {((q1,q2),l1,(q1',q2)) | (q1,l1,q1') in R1, q2 in Q2} U {((q1,q2),l2,(q1,q2')) | q1 in Q1, (q2,l2,q2') in R2} U {((q1,q2),(l2,l2),(q1',q2')) | (q1,l1,q1') in R1, (q2,l2,q2') in R2}

. In the result, transition labels

  • l1 are encoded as (Some l1, None)
  • l2 as (None, Some l2)
  • (l1,l2) as (Some l1, Some l2)

.

val synch_product : ((S1.label option * S2.label option) -> bool) -> S1.t -> S2.t -> t

synch_product p s1 s2 computes the synchronized product of the two LTSA s1 and s2. The restricted product is the obtained by first computing the free product of s1 and s2 and then keeping only transitions (q,l,q') for which the transition label l satisfies the predicate p.

val synchronized_product : (S1.label option * S2.label option) list -> S1.t -> S2.t -> t

synchronized_product sync s1 s2 is a variant of synch_product in which the synchronisation function is given in extension as a list of allowed transitions.

val asynchronous_product : S1.t -> S2.t -> t

asynchronous_product s1 s2 computes the asynchronous product of the two LTSA s1 and s2. This is a synchronized_product in which the synchronisation list contains only labels (Some l1,None) or (None,Some l2)).

val synchronous_product : S1.t -> S2.t -> t

synchronous_product p s1 s2 computes the synchronous product of the two LTSA s1 and s2. This is a synchronized_product in which the synchronisation list contains only labels (Some l1,Some l2).

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet 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