A | |
| acc_states [Nfa.T] |
Returns the set of accepting states
|
| acc_states' [Nfa.T] |
Returns the set of accepting states as a list
|
| accept [Nfa.T] | accept a ss returns true iff ss is accepted by a.
|
| add [Valuation.T] | |
| add_itransition [Fsm.T] | add_itransition (acts,s) m returns the FSM obtained by adding the initial transition (acts,s)
to FSM m
|
| add_itransition [Moore.T] | |
| add_itransition [Mealy.T] | add_itransition q s adds an initial transition to state q to the Mealy structure s
|
| add_itransition [Lts.T] | add_itransition (l,q) s returns the LTS obtained by adding initial transition to state q,
with label l to LTS s.
|
| add_itransition [Ltsa.T] | add_itransition (l,q) s returns the LTSA obtained by adding initial transition to state q,
with label l to LTSA s.
|
| add_itransition' [Fsm.T] | add_itransition' is a variant of add_itransition for which the initial actions are specified
using concrete syntax as a string
|
| add_state [Fsm.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_state [Moore.T] | |
| add_state [Mealy.T] | add_state q s adds state q to the Mealy structure s
|
| add_state [Nfa.T] | add_state (q,i,f) a returns the NFA obtained by adding state q to s.
|
| add_state [Lts.T] | add_state q s returns the LTS obtained by adding state q to s.
|
| add_state [Ltsa.T] | add_state (q,a) s returns the LTSA obtained by adding state q, with attribute a, to s.
|
| add_transition [Fsm.T] | add_transition t m returns the FSM obtained by adding transition t to FSM m
|
| add_transition [Moore.T] | |
| add_transition [Mealy.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
|
| add_transition [Lts.T] | add_transition (q1,l,q2) s returns the LTS obtained by adding transition from state q1
to state q2, with label l to LTS s.
|
| add_transition [Ltsa.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.
|
| add_transition' [Fsm.T] | add_transition is a variant of add_transition for which the added transition is specified
using concrete syntax as a pair of strings
|
| assoc [Valuation.T] | |
| asynchronous_product [Lts.IProduct3] | asynchronous_product s1 s2 computes the asynchronous product of the three LTS s1, s2 and s3
|
| asynchronous_product [Lts.IProduct] | asynchronous_product s1 s2 computes the asynchronous product of the two LTS s1 and s2
|
| asynchronous_product [Lts.Product3] | asynchronous_product s1 s2 computes the asynchronous product of the three LTS s1, s2 and s3
|
| asynchronous_product [Lts.Product] | asynchronous_product s1 s2 computes the asynchronous product of the two LTS s1 and s2.
|
| asynchronous_product [Ltsa.IProduct3] | asynchronous_product s1 s2 computes the asynchronous product of the three LTSA s1, s2 and s3
|
| asynchronous_product [Ltsa.IProduct] | asynchronous_product s1 s2 computes the asynchronous product of the two LTSA s1 and s2
|
| asynchronous_product [Ltsa.Product3] | asynchronous_product s1 s2 computes the asynchronous product of the three LTSA s1, s2 and s3
|
| asynchronous_product [Ltsa.Product] | asynchronous_product s1 s2 computes the asynchronous product of the two LTSA s1 and s2.
|
| attr_of [Ltsa.T] | attr_of s q returns the attribute of state q in s.
|
C | |
| check [Valuation.T] | check names vs checks whether vs is a "complete" valuation wrt.
|
| clean [Lts.T] |
Removes unreachable nodes and associated transitions
|
| clean [Ltsa.T] |
Removes unreachable nodes and associated transitions
|
| compare [Fsm.TRANSITION] | |
| compare [Mealy.TRANSITION] | |
| compare [Valuation.T] | |
| conv [Conv.ToMoore] |
Convert a Mealy automata into a Moore automata, by turning each transition
q,(i/o'),q' into a set of transitions (q,o),i,(q',o') for each possible output valuation o.
|
| conv [Conv.ToMealy] |
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'
|
| conv [Conv.ToDfa] | |
| conv [Conv.FromLts] | |
| conv [Conv.ToLts] | |
| create [Fsm.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.
|
| create [Moore.T] | mk ivs ovs ss is ts builds an Moore structure from a list of input and output variables (each being described by a name and a domain), a list ss of states, each state being assigned a valuation for outputs, an initial state is, a list of transitions ts, where each transition is given as (src_state,input_valuation,values,dst_state)
Raises Invalid_valuation when appropriate (TBD)
|
| create [Mealy.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.
|
| create [Dfa.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.
|
| create [Nfa.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_states), a list of accepting states aqs
Raises Failure if q0 does not appear in qs.
|
| create [Lts.T] | create qs q0s ts builds a LTS from a list of states identifiers, 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)
|
| create [Ltsa.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)
|
D | |
| defactorize [Conv.Fsm] | defactorize vars m returns an equivalent FSM m' obtained by removing variable listed in vars from m (all variables if vars=[]), introducing new states., the optional argument init can be used to designate the initial state of the resulting
automata (when the operation leads to several initial states), unreachable states are removed from the resulting automata unlesse the optional
argument clean is set to false
|
| dot_output [Fsm.T] | dot_output name fname s writes a .dot representation of s with name name in file fname.
|
| dot_output [Moore.T] | dot_output name fname s writes a .dot representation of s with name name in file fname.
|
| dot_output [Mealy.T] | dot_output name fname s writes a .dot representation of s with name name in file fname.
|
| dot_output [Nfa.T] | dot_output name fname s writes a .dot representation of s with name name in file fname.
|
| dot_output [Lts.T] | dot_output name s writes a .dot representation of s with name name in file.
|
| dot_output [Ltsa.T] | dot_output name s writes a .dot representation of s with name name.
|
| dot_output_execs [Lts.T] | dot_output_execs name depth s writes a .dot representation, with name name
of the execution trees obtained by calling unwind depth s.
|
| dot_output_execs [Ltsa.T] | dot_output_execs name depth s writes a .dot representation, with name name
of the execution trees obtained by calling unwind depth s.
|
| dot_output_oc [Fsm.T] | 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.
|
| dot_output_oc [Moore.T] | 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.
|
| dot_output_oc [Mealy.T] | 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.
|
| dot_output_oc [Nfa.T] | 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.
|
| dot_output_oc [Lts.T] | 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.
|
| dot_output_oc [Ltsa.T] | 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.
|
E | |
| empty [Fsm.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).
|
| empty [Moore.T] | |
| empty [Mealy.T] | empty ivs ovs builds an empty Mealy structure from a list of input and output variables.
|
| empty [Valuation.T] | |
| empty [Nfa.T] |
Creates an empty NFA (no states, no transitions) with a given symbol set.
|
| empty [Lts.T] |
The empty LTS (no state, no transition)
|
| empty [Ltsa.T] |
The empty LTSA (no state, no transition)
|
| epsilon [Nfa.SYMBOL] |
The empty symbol
|
| eval [Fsm.CONDITION] | |
| eval [Fsm_expr] | |
F | |
| fold_itransitions [Lts.T] | fold_itransitions f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the initial transitions of s
|
| fold_itransitions [Ltsa.T] | fold_itransitions f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the initial transitions of s
|
| fold_preds [Lts.T] | 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 LTS s, and l1, ..., lN the associated transitions labels
|
| fold_preds [Ltsa.T] | 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
|
| fold_states [Lts.T] | fold_states f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the states of s
|
| fold_states [Ltsa.T] | fold_states f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the states of s
|
| fold_succs [Lts.T] | 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 LTS s, and l1, ..., lN the associated transitions labels
|
| fold_succs [Ltsa.T] | 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
|
| fold_transitions [Lts.T] | fold_transitions f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the transitions of s
|
| fold_transitions [Ltsa.T] | fold_transitions f s z computes f xN ... (f x2 (f x1 z))..., where x1, ..., xN are all the transitions of s
|
| free_product [Lts.IProduct3] | free_product s1 s2 s3 computes the free product of the three LTS s1, s2 and s3
|
| free_product [Lts.IProduct] | free_product s1 s2 computes the free product of the two LTS s1 and s2
|
| free_product [Lts.Product3] | free_product s1 s2 computes the free product of the three LTS s1, s2 and s3
|
| free_product [Lts.Product] | free_product s1 s2 computes the free product of the two LTS s1 and s2.
|
| free_product [Ltsa.IProduct3] | free_product s1 s2 s3 computes the free product of the three LTSA s1, s2 and s3
|
| free_product [Ltsa.IProduct] | free_product s1 s2 computes the free product of the two LTSA s1 and s2
|
| free_product [Ltsa.Product3] | free_product s1 s2 computes the free product of the three LTSA s1, s2 and s3
|
| free_product [Ltsa.Product] | free_product s1 s2 computes the free product of the two LTSA s1 and s2.
|
I | |
| inps [Fsm.T] |
Returns the list of inputs variables, with corresponding domains
|
| inps [Moore.T] |
Returns the list of inputs variables, with corresponding domains
|
| inps [Mealy.T] |
Returns the list of inputs variables
|
| is_acc_state [Nfa.T] | |
| is_in_cycle [Nfa.T] | cycles a q tests whether state q in automata a belongs to a cycle
|
| is_init_state [Lts.T] | is_init s q returns true iff q is an initial state in s
|
| is_init_state [Ltsa.T] | is_init s q returns true iff q is an initial state in s
|
| is_reachable [Lts.T] | is_reachable s q returns true iff q is a reachable state in s, i.e.
|
| is_reachable [Ltsa.T] | is_reachable s q returns true iff q is a reachable state in s, i.e.
|
| is_state [Lts.T] | is_state s q returns true iff q is a state in s
|
| is_state [Ltsa.T] | is_state s q returns true iff q is a state in s
|
| is_transition [Lts.T] | is_transition t q returns true iff t is a transition in s
|
| is_transition [Ltsa.T] | is_transition t q returns true iff t is a transition in s
|
| istate [Fsm.T] |
Returns the initial state, when specified
|
| istate [Moore.T] |
Returns the initial state, when specified
|
| istate [Mealy.T] |
Returns the initial state, when specified
|
| istate [Nfa.T] |
Returns the initial state, when specified
|
| istates [Lts.T] |
Returns the set of initial states
|
| istates [Ltsa.T] |
Returns the set of initial states
|
| istates' [Lts.T] |
Returns the list of initial states
|
| istates' [Ltsa.T] |
Returns the set of initial states as a list
|
| iter_itransitions [Lts.T] | iter_itransitions f s applies function f to all initial transitions of s
|
| iter_itransitions [Ltsa.T] | iter_itransitions f s applies function f to all initial transitions of s
|
| iter_preds [Lts.T] | iter_preds s x f z computes f x1 l1; ... ;f xN lN, where x1, ..., xN are all the
predecessors of state x in LTS s, and l1, ..., lN the associated transitions labels
|
| iter_preds [Ltsa.T] | 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
|
| iter_states [Lts.T] | iter_states f s applies function f to all states (with associated attribute) of s
|
| iter_states [Ltsa.T] | iter_states f s applies function f to all states (with associated attribute) of s
|
| iter_succs [Lts.T] | iter_succs s x f z computes f x1 l1; ... ;f xN lN, where x1, ..., xN are all the
successors of state x in LTS s, and l1, ..., lN the associated transitions labels
|
| iter_succs [Ltsa.T] | 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
|
| iter_transitions [Lts.T] | iter_transitions f s applies function f to all transitions of s
|
| iter_transitions [Ltsa.T] | iter_transitions f s applies function f to all transitions of s
|
| itransitions [Lts.T] |
Returns the list of initial transitions
|
| itransitions [Ltsa.T] |
Returns the list of initial transitions
|
L | |
| lexer [Fsm_expr] | |
| list_of_string [Fsm.ACTION] | |
| list_of_string [Fsm.CONDITION] | |
| lookup [Fsm_expr] | |
| lts_of [Fsm.T] |
Return the underlying representation of the Moore Machine as a LTS
|
| lts_of [Moore.T] |
Return the underlying representation of the Moore Machine as a LTS
|
| lts_of [Mealy.T] |
Return the underlying representation of the Moore Machine as a LTS
|
| lts_of [Nfa.T] |
Return the underlying representation of the NFA as a LTS
|
M | |
| map [Dfa.Trans] | |
| map [Nfa.Trans] | |
| map [Lts.Trans] | |
| map [Ltsa.Trans] | |
| map_attr [Ltsa.T] | map_attr f s returns the LTSA obtained by replacing each state attribute a by f a in s.
|
| map_label [Lts.T] | map_states f s returns the LTS obtained by replacing each transition label l by f l in s.
|
| map_label [Ltsa.T] | map_label f s returns the LTSA obtained by replacing each transition label l by f l in s.
|
| map_state [Ltsa.T] | map_state f s returns the LTSA obtained by replacing each state q by f q in s.
|
| mem [Valuation.T] | |
| merge_attr [Ltsa.Merge3] | |
| merge_attr [Ltsa.Merge] | |
| merge_label [Lts.Merge3] | |
| merge_label [Lts.Merge] | |
| merge_label [Ltsa.Merge3] | |
| merge_label [Ltsa.Merge] | |
| merge_state [Lts.Merge3] | |
| merge_state [Lts.Merge] | |
| merge_state [Ltsa.Merge3] | |
| merge_state [Ltsa.Merge] | |
N | |
| nfa_of [Dfa.T] |
For internal use
|
O | |
| of_nfa [Dfa.T] |
For internal use
|
| of_repr [Lts.T] | |
| of_string [Fsm.TRANSITION] | |
| of_string [Fsm.ACTION] | |
| of_string [Fsm.CONDITION] | |
| of_string [Fsm_expr] | |
| outps [Fsm.T] |
Returns the list of outputs variables, with corresponding domains
|
| outps [Moore.T] |
Returns the list of outputs variables, with corresponding domains
|
| outps [Mealy.T] |
Returns the list of outputs variables
|
P | |
| parse [Fsm_expr] | |
| preds [Lts.T] | preds s q returns the set of immediate predecessors of state q in s, i.e.
|
| preds [Ltsa.T] | preds s q returns the set of immediate predecessors of state q in s, i.e.
|
| preds' [Lts.T] | preds' s q returns the list of immediate predecessors, with the associated transition label, of state q in s.
|
| preds' [Ltsa.T] | preds' s q returns the list of immediate predecessors, with the associated transition label, of state q in s.
|
| preds_hat [Lts.T] |
Transitive closure of
preds.
|
| preds_hat [Ltsa.T] |
Transitive closure of
preds.
|
| product [Dfa.Product] | |
| product [Nfa.Product] | |
R | |
| remove [Valuation.T] | |
| remove_state [Mealy.T] | remove_state q s removes state q from the Mealy structure s
|
| remove_state [Lts.T] | remove_state q s returns the LTS obtained by removing state q, and all attached transitions, from s.
|
| remove_state [Ltsa.T] | remove_state q s returns the LTSA obtained by removing state q, and all attached transitions, from s.
|
| repr_of [Lts.T] | |
S | |
| states [Lts.T] |
Returns the set of states
|
| states [Ltsa.T] |
Returns the set of states
|
| states' [Lts.T] |
Returns the list of states
|
| states' [Ltsa.T] |
Returns the set of states, with attached attribute as a assocation list
|
| string_of_attr [Ltsa.T] |
A synonym of
Attr.to_string
|
| string_of_label [Lts.T] |
A synonym of
Label.to_string
|
| string_of_label [Ltsa.T] |
A synonym of
Label.to_string
|
| string_of_state [Lts.T] |
A synonym of
State.to_string
|
| string_of_state [Ltsa.T] |
A synonym of
State.to_string
|
| string_of_symbol [Nfa.T] | |
| string_of_transition [Lts.T] | |
| succs [Lts.T] | succs s q returns the set of immediate successors in s, i.e.
|
| succs [Ltsa.T] | succs s q returns the set of immediate successors in s, i.e.
|
| succs' [Lts.T] | succs' s q returns the list of immediate successors, with the associated transition label, of state q in s.
|
| succs' [Ltsa.T] | succs' s q returns the list of immediate successors, with the associated transition label, of state q in s.
|
| succs_hat [Lts.T] |
Transitive closure of
succs.
|
| succs_hat [Ltsa.T] |
Transitive closure of
succs.
|
| symbols [Nfa.T] |
Returns the set of symbols
|
| symbols' [Nfa.T] |
Returns the set of symbols as a list
|
| synch_product [Lts.IProduct3] | synch_product p s1 s2 s3 computes the synchronized product of the three LTS s1, s2 and s3 using the synchronisation
predicate p.
|
| synch_product [Lts.IProduct] | synch_product p s1 s2 computes the synchronized product of the two LTS s1 and s2 using the synchronisation
predicate p.
|
| synch_product [Lts.Product3] | synch_product p s1 s2 s3 computes the synchronized product of the three LTS s1, s2 and s3 using the synchronisation
predicate p.
|
| synch_product [Lts.Product] | synch_product p s1 s2 computes the synchronized product of the two LTS s1 and s2.
|
| synch_product [Ltsa.IProduct3] | synch_product p s1 s2 s3 computes the synchronized product of the three LTSA s1, s2 and s3 using the synchronisation
predicate p.
|
| synch_product [Ltsa.IProduct] | synch_product p s1 s2 computes the synchronized product of the two LTSA s1 and s2 using the synchronisation
predicate p.
|
| synch_product [Ltsa.Product3] | synch_product p s1 s2 s3 computes the synchronized product of the three LTSA s1, s2 and s3 using the synchronisation
predicate p.
|
| synch_product [Ltsa.Product] | synch_product p s1 s2 computes the synchronized product of the two LTSA s1 and s2.
|
| synchronized_product [Lts.IProduct3] | synchronized_product sync s1 s2 computes the synchronized product of the three LTS s1, s2 and s3 using the
synchronization set sync
|
| synchronized_product [Lts.IProduct] | synchronized_product sync s1 s2 computes the synchronized product of the two LTS s1 and s2using the
synchronization set sync
|
| synchronized_product [Lts.Product3] | synchronized_product sync s1 s2 computes the synchronized product of the three LTS s1, s2 and s3 using the
synchronization set sync
|
| synchronized_product [Lts.Product] | 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.
|
| synchronized_product [Ltsa.IProduct3] | synchronized_product sync s1 s2 computes the synchronized product of the three LTSA s1, s2 and s3 using the
synchronization set sync
|
| synchronized_product [Ltsa.IProduct] | synchronized_product sync s1 s2 computes the synchronized product of the two LTSA s1 and s2using the
synchronization set sync
|
| synchronized_product [Ltsa.Product3] | synchronized_product sync s1 s2 computes the synchronized product of the three LTSA s1, s2 and s3 using the
synchronization set sync
|
| synchronized_product [Ltsa.Product] | 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.
|
| synchronous_product [Lts.IProduct3] | synchronous_product p s1 s2 computes the synchronous product of the three LTS s1, s2 and s3
|
| synchronous_product [Lts.IProduct] | synchronous_product p s1 s2 computes the synchronous product of the two LTS s1 and s2
|
| synchronous_product [Lts.Product3] | synchronous_product p s1 s2 computes the synchronous product of the three LTS s1, s2 and s3
|
| synchronous_product [Lts.Product] | synchronous_product p s1 s2 computes the synchronous product of the two LTS s1 and s2.
|
| synchronous_product [Ltsa.IProduct3] | synchronous_product p s1 s2 computes the synchronous product of the three LTSA s1, s2 and s3
|
| synchronous_product [Ltsa.IProduct] | synchronous_product p s1 s2 computes the synchronous product of the two LTSA s1 and s2
|
| synchronous_product [Ltsa.Product3] | synchronous_product p s1 s2 computes the synchronous product of the three LTSA s1, s2 and s3
|
| synchronous_product [Ltsa.Product] | synchronous_product p s1 s2 computes the synchronous product of the two LTSA s1 and s2.
|
T | |
| tex_output [Lts.T] | tex_output name fname s writes a .tex representation of s with name name.
|
| tex_output [Ltsa.T] | tex_output name fname s writes a .tex representation of s with name name.
|
| to_string [Fsm.TRANSITION] | |
| to_string [Fsm.ACTION] | |
| to_string [Fsm.CONDITION] | |
| to_string [Fsm_expr] | |
| to_string [Mealy.TRANSITION] | |
| to_string [Valuation.T] | |
| to_string [Ltsa.ATTR] | |
| totalize [Nfa.T] | totalize a q returns a "totalized" version of automaton a by adding an extra "sink" state q.
|
| trans [Moore.T] | trans a q s returns the set of states q' such that (q,s,q')
belongs to the transition relation of a
|
| trans [Mealy.T] | trans a q t returns the set of states q' such that (q,t,q')
belongs to the transition relation of a
|
| trans [Dfa.T] | trans a q s returns, it it exists, the state q' such that (q,s,q') occurs in the transition relation.
|
| trans [Nfa.T] | trans a q s returns the set of states q' such that (q,s,q')
belongs to the transition relation of a
|
| trans' [Moore.T] | trans' is like trans but returns a list
|
| trans' [Mealy.T] | trans' is like trans but returns a list
|
| trans' [Nfa.T] | trans' is like trans but returns a list
|
| trans_hat [Dfa.T] | 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
|
| trans_hat [Nfa.T] | trans_hat a q ss is the transitive generalisation of trans.
|
| trans_hat' [Nfa.T] | trans_hat' is like trans_hat but returns a list
|
| transitions [Lts.T] |
Returns the list of transitions
|
| transitions [Ltsa.T] |
Returns the list of transitions
|
U | |
| unwind [Fsm.T] | unwind depth s unwind machine s to produce an execution tree (rooted at initial state)
up to the specified depth.
|
| unwind [Moore.T] | unwind depth s unwind machine s to produce an execution tree (rooted at initial state)
up to the specified depth.
|
| unwind [Mealy.T] | unwind depth s unwind machine s to produce an execution tree (rooted at initial state)
up to the specified depth.
|
| unwind [Nfa.T] | unwind depth s unwinds LTS system s to produce an execution tree (rooted at initial state)
up to the specified depth.
|
| unwind [Ltsa.T] | unwind depth s unwinds LTSA system s to produce a list of execution trees (rooted at
initial states) up to the specified depth
|
V | |
| vars [Fsm.T] |
Returns the list of outputs variables, with corresponding domains
|