A | |
| Action [Fsm] | |
| Attr [Ltsa.T] | |
| Attrs [Ltsa.T] | |
B | |
| BVal [Moore] | |
| Bool [Builtins] | |
| Bool [Valuation] | |
| Builtins |
Pre-defined modules to be used as functor arguments
|
C | |
| Condition [Fsm] | |
| Conv |
Functors for converting various kinds of Labeled Transition Systems
|
D | |
| Dfa |
Deterministic Finite Automata (DFA)
|
F | |
| FromLts [Conv] | |
| Fsm [Conv] |
Functor for transforming FSMs
|
| Fsm |
Finite State Machines.
|
| Fsm_expr |
Simple (int) expressions for FSMs
|
I | |
| IProduct [Lts] |
Functor for computing the internal product, in different flavors, of two LTS
|
| IProduct [Ltsa] |
Functor for computing the internal product, in different flavors, of two LTSA
|
| IProduct3 [Lts] |
Functor for computing the "internal" product, in different flavors, of three LTS
|
| IProduct3 [Ltsa] |
Functor for computing the "internal" product, in different flavors, of three LTSA
|
| Int [Builtins] | |
| Int [Valuation] | |
L | |
| LTSA [Nfa.T] | |
| Label [Lts.T] | |
| Label [Ltsa.T] | |
| Lts |
Labeled Transition Systems
|
| Ltsa |
Labeled Transition Systems with State Attributes
|
M | |
| M [Fsm.T] | |
| M [Moore.T] | |
| M [Mealy.T] | |
| Make [Fsm] | |
| Make [Moore] | |
| Make [Mealy] | |
| Make [Valuation] |
Functor building an implementation of the Valuation structure given an implementation of values
|
| Make [Dfa] |
Functor building an implementation of the DFA structure given an implementation of
state identifiers and symbols
|
| Make [Nfa] |
Functor building an implementation of the NFA structure given an implementation of
state identifiers and symbols
|
| Make [Lts] |
Functor building an implementation of the LTS structure given an implementation of
state identifiers, transition labels
|
| Make [Ltsa] |
Functor building an implementation of the LTSA structure given an implementation of
state identifiers, transition labels and state attributes
|
| Mealy |
Mealy machines.
|
| Moore |
Moore machines.
|
N | |
| NFA [Dfa.T] | |
| Nfa |
Non-deterministic Finite Automata (NFA)
|
P | |
| Product [Dfa] |
Functor for computing the products of two NFAs sharing the same symbol set
|
| Product [Nfa] |
Functor for computing the products of two NFAs sharing the same symbol set
|
| Product [Lts] |
Functor for computing the external product, in different flavors, of two LTS
|
| Product [Ltsa] |
Functor for computing the external product, in different flavors, of two LTSA
|
| Product3 [Lts] |
Functor for computing the external product, in different flavors, of three LTS
|
| Product3 [Ltsa] |
Functor for computing the external product, in different flavors, of three LTSA
|
R | |
| Repr [Lts.T] |
The underlying representation : a LTS(A) for which state attributes have type
unit.
|
S | |
| State [Lts.T] | |
| State [Ltsa.T] | |
| States [Lts.T] | |
| States [Ltsa.T] | |
| String [Builtins] | |
| Symbol [Nfa.T] | |
| Symbols [Nfa.T] | |
T | |
| ToDfa [Conv] | |
| ToLts [Conv] | |
| ToMealy [Conv] | |
| ToMoore [Conv] | |
| Trans [Dfa] |
Functor for converting a DFA, with a given implementation of state identifiers and symbols
into another one with different respective implementations
|
| Trans [Nfa] |
Functor for converting a NFA, with a given implementation of state identifiers and symbols
into another one with different respective implementations
|
| Trans [Lts] |
Functor for converting a LTS, with a given implementation of state identifiers and transition labels
into another one with different respective implementations
|
| Trans [Ltsa] |
Functor for converting a LTSA, with a given implementation of state identifiers, transition labels and state attributes
into another one with different respective implementations
|
| Transition [Fsm] | |
| Transition [Mealy] | |
| Tree [Ltsa.T] | |
V | |
| Valuation |
A
valuation is a collection of (name,value) associations
|