package lascar

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

Module Conv.ToMealySource

Functor for converting a Moore machine nto an equivalent Mealy one

Parameters

module MM : Moore.T

Signature

include Mealy.T with type state = MM.state
Sourcetype state = MM.state
include Ltsa.T with type label := Mealy.Transition.t and type state := state and type attr := unit
Sourcetype transition = state * Mealy.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 = Mealy.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 Attr : Ltsa.ATTR with type t = unit
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 = Mealy.Transition.t
Sourceval states : t -> States.t

Returns the set of states

Sourceval states' : t -> (state * unit) 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 : Mealy.Transition.t -> string

A synonym of State.to_string

A synonym of Label.to_string

Sourceval string_of_attr : unit -> 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 * Mealy.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 * Mealy.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 -> unit

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

Global iterators

Sourceval iter_states : (state -> unit -> unit) -> t -> unit

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

Sourceval fold_states : (state -> unit -> '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 -> Mealy.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 -> Mealy.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 -> Mealy.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 -> Mealy.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 : (unit -> unit) -> t -> t

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

Sourceval map_label : (Mealy.Transition.t -> Mealy.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:Mealy.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 = Mealy.Transition.t and type attr = unit
Sourceexception Invalid_transition of transition
Sourceval create : inps:Valuation.Bool.name list -> outps:Valuation.Bool.name list -> states:state list -> istate:state -> trans:(state * Mealy.Transition.t * state) list -> t

create ivs ovs ss is ts builds an Mealy structure from

  • a list of input and output variables
  • a list ss of states
  • an initial state is
  • a list of transitions ts, where each transition is given as (src_state,(input_valuation,output_valuation),dst_state)

Raises !Valuation.Invalid_valuation if any specified valuation/assignement is incorrect (i.e. involves identifiers not listed in ivs or ovs or incomplete (i.e. lacks a input or output identifier).

Sourceval empty : inps:Valuation.Bool.name list -> outps:Valuation.Bool.name list -> t

empty ivs ovs builds an empty Mealy structure from a list of input and output variables.

Sourceval add_state : state -> t -> t

add_state q s adds state q to the Mealy structure s

Sourceval remove_state : state -> t -> t

remove_state q s removes state q from the Mealy structure s

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

add_transition (q,(iv,os),q') s adds a transition from state q to state q', labeled with the IO valuation (iv,ov) to the Mealy structure s

Sourceval add_itransition : state -> t -> t

add_itransition q s adds an initial transition to state q to the Mealy structure s

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 -> Valuation.Bool.name list

Returns the initial state, when specified

Returns the list of inputs variables

Sourceval outps : t -> Valuation.Bool.name list

Returns the list of inputs variables

Returns the list of outputs variables

trans a q t returns the set of states q' such that (q,t,q') belongs to the transition relation of a

Sourceval trans' : t -> state -> Mealy.Transition.t -> state list

trans a q t returns the set of states q' such that (q,t,q') belongs to the transition relation of a

trans' is like trans but returns a list

Sourceval unwind : int -> t -> M.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.

Sourceval conv : MM.t -> t

Convert a Moore automata into a Mealy automata, by turning

  • turning each state (q,o) into q
  • turning each transitions ((q,o)/i/(q',o') into q,(i/o'),q'