DebugContext(const Assertions::RefinementCounterexample &counterexample, bool elide_uninteresting_behaviours)
Creates a new debug context from a refinement check.
Allows counterexamples to be divided into behaviours of component processes.
Definition: debug_context.h:27
std::vector< LTS::CompiledEvent > reveal_taus_in_trace(const Behaviour &behaviour) const
Reveals all taus in the given trace.
std::vector< LTS::CompiledEvent > full_alphabet() const
The union of the alphabets of all the machines in this debug tree.
void initialise(Canceller *canceller)
Initialises the behaviour debug context.
std::vector< std::shared_ptr< Behaviour > > root_behaviours() const
The top-level behaviours.
DebugContext(const Assertions::PropertyCounterexample &counterexample, bool elide_uninteresting_behaviours)
Creates a new debug context from a property check.
TaskId root_task_id() const
Returns the identity of the task under which all tasks in this assertion will be created under.
std::shared_ptr< Behaviour > reveal_tau(const Behaviour &behaviour, unsigned int index) const
Assuming that behaviour.trace()[index] == TAU, returns the behaviour that performs the event,...
std::vector< std::shared_ptr< Behaviour > > behaviour_children(const Behaviour &behaviour) const
Returns the children of the given behaviour.