package lascar

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

Module Fsm.MakeSource

Parameters

module S : Ltsa.STATE

Signature

Sourcetype state = S.t
Sourcetype var_name = Valuation.Int.name
Sourcetype var_domain = int list
Sourcetype var_desc = var_name * var_domain
include Ltsa.T with type state := state and type label := Transition.t and type attr := Valuation.Int.t
Sourcetype transition = state * Transition.t * 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

Sourcetype itransition = Transition.t * 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

Sourcetype t

The type of Labeled Transition Systems with state attributes

Sourcemodule State : Ltsa.STATE with type t = state
Sourcemodule Label : Ltsa.LABEL with type t = Transition.t
Sourcemodule Attr : Ltsa.ATTR with type t = Valuation.Int.t
Sourcemodule States : Utils.SetExt.S with type elt = state
Sourcemodule Attrs : Map.S with type key = state
Sourcemodule Tree : Utils.Tree.S with type node = state and type edge = Transition.t
Sourceval states : t -> States.t

Returns the set of states

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

Returns the set of states

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

Sourceval istates : t -> States.t

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

Returns the set of initial states

Sourceval istates' : t -> state list

Returns the set of initial states

Returns the set of initial states as a list

Sourceval transitions : t -> transition list

Returns the set of initial states as a list

Returns the list of transitions

Sourceval itransitions : t -> itransition list

Returns the list of transitions

Returns the list of initial transitions

Sourceval string_of_state : state -> string

A synonym of State.to_string

Sourceval string_of_label : Transition.t -> string

A synonym of State.to_string

A synonym of Label.to_string

Sourceval string_of_attr : Valuation.Int.t -> string

A synonym of Label.to_string

A synonym of Attr.to_string

Inspectors

Sourceval is_state : t -> state -> bool

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

Sourceval 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

Sourceval 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.

Sourceval 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

Sourceval 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.

Sourceval succs' : t -> state -> (state * Transition.t) 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.

Sourceval 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.

Sourceval preds' : t -> state -> (state * Transition.t) 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.

Sourceval 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

Sourceval 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

Sourceval attr_of : t -> state -> Valuation.Int.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

Sourceexception Invalid_state of state
Sourceval 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

Sourceval iter_states : (state -> Valuation.Int.t -> unit) -> t -> unit

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

Sourceval fold_states : (state -> Valuation.Int.t -> '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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval 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

Sourceval iter_succs : t -> state -> (state -> Transition.t -> 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

Sourceval fold_preds : t -> state -> (state -> Transition.t -> '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

Sourceval iter_preds : t -> state -> (state -> Transition.t -> 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

Sourceval 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.

Sourceval map_attr : (Valuation.Int.t -> Valuation.Int.t) -> t -> t

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

Sourceval 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.

Sourceval clean : t -> t

Removes unreachable nodes and associated transitions

Output functions

Sourceval 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.

Sourceval 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.

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

mk 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 output and local variables
  • 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.

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

mk 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.

Sourceval add_state : (state * Valuation.Int.t) -> t -> t

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

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

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

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

Sourceval add_transition' : (state * (string * string) * state) -> t -> t

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

add_transition is a variant of add_transition for which the added transition is specified using concrete syntax as a pair of strings

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

add_transition is a variant of add_transition for which the added transition is specified using concrete syntax as a pair of strings

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

Sourceval add_itransition' : (string * state) -> t -> t

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

add_itransition' is a variant of add_itransition for which the initial actions are specified using concrete syntax as a string

Sourceval lts_of : t -> M.t

Return the underlying representation of the Moore Machine as a LTS

Sourceval istate : t -> state option

Returns the initial state, when specified

Sourceval inps : t -> var_desc list

Returns the initial state, when specified

Returns the list of inputs variables, with corresponding domains

Sourceval outps : t -> var_desc list

Returns the list of inputs variables, with corresponding domains

Returns the list of outputs variables, with corresponding domains

Sourceval vars : t -> var_desc list

Returns the list of outputs variables, with corresponding domains

Returns the list of outputs variables, with corresponding domains

Sourceval 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.

Sourceval 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.

Sourceval 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.