|
| OFSMTable (const std::vector< std::shared_ptr< FsmNode >> &nodes, const int maxInput, const int maxOutput, const std::shared_ptr< FsmPresentationLayer > presentationLayer) |
|
| OFSMTable (const int numStates, const int maxInput, const int maxOutput, const std::vector< std::shared_ptr< OFSMTableRow >> &rows, const std::shared_ptr< FsmPresentationLayer > presentationLayer) |
|
int | getId () |
|
S2CMap | getS2C () |
|
void | setS2C (const S2CMap &ps2c) |
|
int | get (const int id, const int x, const int y) |
|
int | maxClassId () const |
|
std::shared_ptr< OFSMTable > | next () |
|
std::string | getMembers (const int c) const |
|
Fsm | toFsm (const std::string &name) const |
|
Table representation for observable FSMs
The table structure is as follows.
- One row for each FSM state, the FSM state number in 0..nodes.length-1 is the table index.
- Each row r has the following matrix structure. (a) The matrix is indexed over inputs i in 0..maxInput and outputs o in 0..maxOutput (b) If FSM state r has no transition labelled with i/o, then the matrix contains value -1 at position [i][o] (c) If FSM state r transits with i/o to post-state r', then the matrix contains value r' at position [i][o]
- Note
- This representation is well-defined if and only if the FSM is observable.
Additionally, each OFSMTable contains an S2CMap which maps FSM states to their equivalence class associated with the current OFSMTable