The fsm package
Finite state machine abstraction of a network.
By Shaker Sarwary, Tom Shiple, Rajeev Ranjan, Kavita Ravi, In-Ho Moon
A finite state machine contains a pointer to a network, so it
inherits all the information that is contained in the network, such as node
names and MDD ids. An FSM has a partition associated with it; the output
and next state functions are derived from the partition. This partition
does not necessarily have to be the default partition associated with the
network.
The FSM maintains information relating to state reachability
(initial states, reachable states, underapprox or not, and the
partition of reachable states into "onion rings"), and fairness
information (fair states, fairness constraints, and generic
debugging information). Also, the FSM stores the MDD ids of present
state, next state, and input variables, in a convenient format.
Last updated on 20050519 00h50