  Most model checkers provide a useful simulation mode, that allows users to
explore the set of possible behaviours by interactively picking at each state
which event to execute next. Traditionally this simulation mode cannot take
into consideration additional temporal logic constraints, such as arbitrary
fairness restrictions, substantially reducing its usability for debugging the
modelled system behaviour. Similarly, when a specification is false, even if
all its counter-examples combined also form a set of behaviours, most model
checkers only present one of them to the user, providing little or no mechanism
to explore alternatives. In this paper, we present a simple on-the-fly
verification technique to allow the user to explore the behaviours that satisfy
an arbitrary temporal logic specification, with an interactive process akin to
simulation. This technique enables a unified interface for simulating the
modelled system and exploring its counter-examples. The technique is formalised
in the framework of state/event linear temporal logic and a proof of concept
was implemented in an event-based variant of the Electrum framework.
