The single-thread Engine is the mostly used BIP Engine. It handles the full BIP syntax (except some of the time features of BIP that are only compatible with the real-time Engine).
The single-thread Engine is a direct implementation of the semantics of BIP. It is based on cyclic execution implemented by a single thread. Each execution cycle of the Engine is composed of computing the enabled interactions at the current state , choosing an interaction amongst the enabled ones, and executing the atoms involved in which updates the state of the system into .
The single-thread Engine provides the following useful modes for a given BIP model:
- simulation/execution mode is used for executing a single sequence of interactions of the considered BIP model. Interactions are chosen randomly when several interactions are enabled at a state.
- exploration mode is used for an exhaustive computation of the execution sequences of interactions (i.e. model-checking) of the model. It can be used for verification.
- interactive/debug mode let the user choosing at each state of the model the next interaction to be executed amongst the one that are enabled. It also allows displaying and modifying the state of the components (control location, data, etc.), which is useful for debugging BIP models.
The single-thread Engine is included in the core BIP distribution for GNU/Linux x86 platforms. You can dowload it here.