The Mathematical Model Module

The Mathematical Model Module explores reachable states in the model and calculates the transition rates between any two tangible states. When a state is generated, the generator must determine if it was previously explored, or if it is a new state. TANGRAM-II uses a hashing function to uniquely map states into identifiers, in order to save storage. The technique used identifies a lexicographic order for the state vectors and the state space is divided into sets according to this ordering. Then, a table that stores the number of states in each set is built. From this table, one can uniquely map the state vectors into identifiers with little effort.

The user specifies an initial state for each object. The state transition matrix generator finds a list of all events that can fire from that state. One event is then chosen to fire, and all messages that can be sent after an action is executed for that event, are found. All states with pending messages (yet to be delivered) are vanishing, and are not part of the final state space of the model. The algorithm recursively finds all states (vanishing or tangible) reachable from the current state, and the new tangible states found are inserted in the list of non-explored states (depth-first search).

The data structures generated for the class of non-Markovian models that can be solved by the tool are more complex than those needed for Markovian models, since many chains must be identified and generated as required by the solution method. Roughly, the generator first finds all tangible states assuming that all transitions in the model are exponential. Then, for non-exponential events defined by user, the generator finds one or more Markov chains associated with them. For details of the solution technique see [#!embed95!#].