package lascar

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type state
module Expr : Fsm_expr.T with type value = Value.t
module Valuation : Valuation.T with type value = Value.t

for outputs and local variables

type var_name = Valuation.name
type var_domain = Value.t list
type var_desc = var_name * var_domain
include Ltsa.T with type state := state and type label := Transition.t and type attr := Valuation.t
type transition = state * Transition.t * state

The type for transitions. 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 = Transition.t * state

The type for initial transitions. 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 : Ltsa.STATE with type t = state
module Label : Ltsa.LABEL with type t = Transition.t
module Attr : Ltsa.ATTR with type t = Valuation.t
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 = Transition.t
val states : t -> States.t

Returns the set of states

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

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

val istates : t -> States.t

Returns the set of initial states

val istates' : t -> state list

Returns the set of initial states as a list

val transitions : t -> transition list

Returns the list of transitions

val itransitions : t -> itransition list

Returns the list of initial transitions

val string_of_state : state -> string

A synonym of State.to_string

val string_of_label : Transition.t -> string

A synonym of Label.to_string

val string_of_attr : Valuation.t -> 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_init s q returns true iff q is an initial state in s

val is_reachable : t -> state -> 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.

val is_transition : t -> transition -> bool

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 * Transition.t) list

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 * Transition.t) list

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

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 preds. preds_hat s q returns all the predecessors (immediate or not) of q in s

val attr_of : t -> state -> Valuation.t

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

exception Invalid_state of state
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 -> Valuation.t -> unit) -> t -> unit

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

val fold_states : (state -> Valuation.t -> 'a -> 'a) -> t -> 'a -> 'a

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

iter_transitions f s applies function f to all transitions of s

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

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

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

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

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 -> Transition.t -> '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 -> Transition.t -> unit) -> unit

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 -> Transition.t -> 'a -> 'a) -> 'a -> 'a

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 -> Transition.t -> unit) -> unit

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. State attributes are left unchanged. Result is undefined if f is not injective.

val map_attr : (Valuation.t -> Valuation.t) -> t -> t

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

val map_state_attr : ((state * Valuation.t) -> state * Valuation.t) -> t -> t

map_state_attr f s returns the LTSA obtained by replacing each pair of state and associated attributes (q,a) by f (q,a) in s. As for map_state, the result is undefined if f is not injective its first argument.

val map_label : (Transition.t -> Transition.t) -> t -> t

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

val map_transition : ((state option * Transition.t * state) -> state option * Transition.t * state) -> t -> t

map_transition f s returns the LTSA obtained by replacing each transition t by f t in s. Each non-initial transition qs,l,qd is replaced by qs',l',qd', where (Some qs',l',qd') = f (Some qs,l,qd). If present, the initial transition l,qi is replaced by l',qi' where (None,l',qi') = f (None, l, qi). Warning: updating the source and/or destination state in a transition may result in a incoherent LTS description. This function should essentially be viewed as a variant of map_label in which the transformation function f can take the source and destination state into account.

val clean : t -> t

Removes unreachable nodes and associated transitions

Output functions

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:Transition.t 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.

module M : Ltsa.T with type state = state and type label = Transition.t and type attr = Valuation.t
val create : inps:var_desc list -> outps:var_desc list -> vars:var_desc list -> states:(state * Valuation.t) list -> istate:(Transition.Action.t list * state) -> trans:(state * Transition.t * state) list -> t

create ivs ovs lvs qs q0 ts builds an FSM structure from

  • a list of input, output and local variables (each being described by a name and a domain)
  • a list of input and output identifiers
  • a list qs of states, with possible valuations of outputs
  • an initial state q0 with the list of initial actions
  • a list of transitions ts, where each transition is given as (src_state,(conditions,actions),dst_state)

Raises Not_found if any specified condition or action involves identifiers not listed in ivs, ovs or lvs.

val empty : inps:var_desc list -> outps:var_desc list -> lvars:var_desc list -> t

empty ivs ovs lvs builds an "empty" FSM structure from a list of input, output and local variables (each being described by a name and a domain). This empty structure can then be "filled" using the add_state, add_transition and add_itransition functions.

val add_state : (state * Valuation.t) -> t -> t

add_state (s,v) m returns the FSM obtained by adding state s, with a valuation of outputs v, to FSM m

val add_transition : (state * Transition.t * state) -> t -> t

add_transition t m returns the FSM obtained by adding transition t to FSM m

val add_itransition : (Transition.Action.t list * state) -> t -> t

add_itransition (acts,s) m returns the FSM obtained by adding the initial transition (acts,s) to FSM m

val lts_of : t -> M.t

Return the underlying representation of the LTS as a LTSA

val istate : t -> state option

Returns the initial state, when specified

val inps : t -> var_desc list

Returns the list of inputs variables, with corresponding domains

val outps : t -> var_desc list

Returns the list of outputs variables, with corresponding domains

val vars : t -> var_desc list

Returns the list of outputs variables, with corresponding domains

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

unwind depth s unwind machine s to produce an execution tree (rooted at initial state) up to the specified depth.

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

dot_output name fname s writes a .dot representation of s with name name in file fname. Global graph drawing options can be specified with the options optional argument.

val dot_output_oc : string -> out_channel -> ?options:Utils.Dot.graph_style list -> t -> unit

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

Helping parsers

val mk_cond : string -> Transition.Condition.t
val mk_conds : string -> Transition.Condition.t list
val mk_act : string -> Transition.Action.t
val mk_acts : string -> Transition.Action.t list
val mk_trans : string -> Transition.t