package lascar

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

Module Dfa.ProductSource

Functor for computing the products of two NFAs sharing the same symbol set

Parameters

module S1 : T
module S2 : T with type symbol = S1.symbol and type Symbols.t = S1.Symbols.t and type NFA.Symbols.t = S1.NFA.Symbols.t

Signature

include T with type state = S1.state * S2.state and type symbol = S1.symbol
include Nfa.T with type state = S1.state * S2.state with type symbol = S1.symbol
Sourcetype symbol = S1.symbol
Sourcetype state = S1.state * S2.state
include Ltsa.T with type label := symbol and type state := state and type attr := bool
Sourcetype transition = state * symbol * 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 = symbol * 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 = symbol
Sourcemodule Attr : Ltsa.ATTR with type t = bool
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 = symbol
Sourceval states : t -> States.t

Returns the set of states

Sourceval states' : t -> (state * bool) 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 : symbol -> string

A synonym of State.to_string

A synonym of Label.to_string

Sourceval string_of_attr : bool -> 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 * symbol) 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 * symbol) 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 -> bool

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 add_transition : (state * symbol * 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

Sourceval add_itransition : (symbol * 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

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 -> bool -> unit) -> t -> unit

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

Sourceval fold_states : (state -> bool -> '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 -> symbol -> '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 -> symbol -> 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 -> symbol -> '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 -> symbol -> 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 : (bool -> bool) -> t -> t

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

Sourceval map_label : (symbol -> symbol) -> 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:symbol 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 LTSA : Ltsa.T with type state = state and type label = symbol and type attr = bool
Sourcemodule Symbol : Nfa.SYMBOL with type t = symbol
Sourcemodule Symbols : Set.S with type elt = symbol
Sourceval lts_of : t -> LTSA.t

Return the underlying representation of the NFA as a LTS

Sourceval empty : symbol list -> t

Creates an empty NFA (no states, no transitions) with a given symbol set.

Sourceval add_state : (state * bool * bool) -> t -> t

add_state (q,i,f) a returns the NFA obtained by adding state q to s. i and f resp. indicates whether q is an initial and/or an accepting state. Raises !Ltsa.Invalid_state if i is true and there's already an accepting state in a. Returns a is q is already a state in a

Sourceval symbols : t -> Symbols.t

Returns the set of symbols

Sourceval symbols' : t -> symbol list

Returns the set of symbols

Returns the set of symbols as a list

Sourceval acc_states : t -> States.t

Returns the set of symbols as a list

Returns the set of accepting states

Sourceval acc_states' : t -> state list

Returns the set of accepting states

Returns the set of accepting states as a list

Sourceval istate : t -> state option

Returns the set of accepting states as a list

Returns the initial state, when specified

Sourceval string_of_symbol : symbol -> string
Sourceval is_acc_state : t -> state -> bool

TODO : union and star operations

Sourceval trans' : t -> state -> symbol -> state list

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

trans' is like trans but returns a list

Sourceval trans_hat' : t -> state -> symbol list -> state list

trans_hat a q ss is the transitive generalisation of trans. It returns the set of states which can reached when a sequence of symbols ss is given to a, starting at state q

trans_hat' is like trans_hat but returns a list

Sourceval accept : t -> symbol list -> bool

accept a ss returns true iff ss is accepted by a. I.e., if trans_hat a q ss contains at least one accepting state. Raises Failure is no initial state has been specified in a.

Sourceval is_in_cycle : t -> state -> bool

cycles a q tests whether state q in automata a belongs to a cycle

Sourceval totalize : t -> state -> t

totalize a q returns a "totalized" version of automaton a by adding an extra "sink" state q. Raises Invalid_arg if q is already a state of a.

Sourceval unwind : int -> t -> LTSA.Tree.t

unwind depth s unwinds LTS system 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.

Sourcemodule NFA : Nfa.T with type state = state and type symbol = symbol
Sourceexception Non_deterministic
Sourceval create : states:state list -> symbols:symbol list -> istate:state -> trans:(state * symbol * state) list -> astates:state list -> t

create qs ss q0 rel aqs builds a NFA from

  • a list of states qs
  • a list of symbols (alphabet) ss
  • an initial state q0
  • a transition relation rel given as a list of triplets (src_state,symbol,dst_state)
  • a list of accepting states aqs

Raises Failure if q0 does not appear in qs.

Sourceexception Stuck of state * symbol list
Sourceval trans : t -> state -> symbol -> state

trans a q s returns, it it exists, the state q' such that (q,s,q') occurs in the transition relation. Raises Stuck otherwise.

Sourceval trans_hat : t -> state -> symbol list -> state

trans_hat a q ss is the transitive generalisation of trans : it returns the state which is reached when a sequence of symbols ss is given to a, starting at state q, or raises Stuck

Sourceval nfa_of : t -> NFA.t

For internal use

Sourceval of_nfa : NFA.t -> t

For internal use

For internal use

Sourceval product : S1.t -> S2.t -> t
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