Overview
- Such that an actor's actions can be narrowed down to a definitive sequence. This may help verify a model in a smaller scope.
- Can be used to define an external actor that
- triggers certain events to the system (killing an existing actor)
- simulate incoming traffic
At the moment, an actor tries to do whatever it is allowed to at any given
time. The implementation of each actor is responsible for ensuring the actor's
state remains valid, e.g. when the ResourceManager already aborted the
transaction, any request to commit the transaction should not change its state.
This may add unnecessary complexity to some verification or simulation if we
only want to explore the state space from the interleaving of some predefined
sequences, e.g. each actor taking several actions (in predefined order) concurrently.
Overview
At the moment, an actor tries to do whatever it is allowed to at any given
time. The implementation of each actor is responsible for ensuring the actor's
state remains valid, e.g. when the ResourceManager already aborted the
transaction, any request to commit the transaction should not change its state.
This may add unnecessary complexity to some verification or simulation if we
only want to explore the state space from the interleaving of some predefined
sequences, e.g. each actor taking several actions (in predefined order) concurrently.