FDR::Assertions::DebugContext Class Reference

Allows counterexamples to be divided into behaviours of component processes. More...

#include <debug_context.h>

List of all members.

Public Member Functions

 DebugContext (DebugContext &)
 DebugContext (const Assertions::PropertyCounterexample &counterexample, bool elide_uninteresting_behaviours)
 Creates a new debug context from a property check.
 DebugContext (const Assertions::RefinementCounterexample &counterexample, bool elide_uninteresting_behaviours)
 Creates a new debug context from a refinement check.
std::vector< std::shared_ptr
< Behaviour > > 
behaviour_children (const Behaviour &behaviour) const
 Returns the children of the given behaviour.
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.
DebugContextoperator= (DebugContext &)
std::shared_ptr< Behaviourreveal_tau (const Behaviour &behaviour, unsigned int index) const
 Assuming that behaviour.trace()[index] == TAU, returns the behaviour that performs the event, if any.
std::vector< LTS::CompiledEvent > reveal_taus_in_trace (const Behaviour &behaviour) const
 Reveals all taus in the given trace.
std::vector< std::shared_ptr
< Behaviour > > 
root_behaviours () const
 The top-level behaviours.
TaskId root_task_id () const
 Returns the identity of the task under which all tasks in this assertion will be created under.

Detailed Description

Allows counterexamples to be divided into behaviours of component processes.

Given a counterexample, FDR allows it to be divided into sub-behaviours of components, thus allowing a form of debugging to occur. A DebugContext is what performs this division. It is also responsible for fully aligning any counterexamples that are found (i.e. it ensures that the traces of all behaviours are the same length, so that if two different behaviours both have an event not equal to LTS::INVALID_EVENT at index i, they must synchronise).


Constructor & Destructor Documentation

FDR::Assertions::DebugContext::DebugContext ( const Assertions::RefinementCounterexample counterexample,
bool  elide_uninteresting_behaviours 
)

Creates a new debug context from a refinement check.

This must be initialised using initialise before any other methods are called.

Parameters:
counterexample The counterexample that is going to be divided.
elide_uninteresting_behaviours If true, FDR will elide any 'uninteresting' behaviours from the debug tree. An uninteresting behaviour is defined as any behaviour that results from an uninteresting compression. The FDR user interface elides uninteresting defaults.
FDR::Assertions::DebugContext::DebugContext ( const Assertions::PropertyCounterexample counterexample,
bool  elide_uninteresting_behaviours 
)

Creates a new debug context from a property check.

This must be initialised using initialise before any other methods are called.

Parameters:
counterexample The counterexample that is going to be divided.
elide_uninteresting_behaviours If true, FDR will elide any 'uninteresting' behaviours from the debug tree. An uninteresting behaviour is defined as any behaviour that results from an uninteresting compression. The FDR user interface elides uninteresting defaults.

Member Function Documentation

std::vector<std::shared_ptr<Behaviour> > FDR::Assertions::DebugContext::behaviour_children ( const Behaviour behaviour  )  const

Returns the children of the given behaviour.

Parameters:
behaviour The behaviour to return the children of. Must be a behaviour that has been returned by a method of this class.
std::vector<LTS::CompiledEvent> FDR::Assertions::DebugContext::full_alphabet (  )  const

The union of the alphabets of all the machines in this debug tree.

In some sense, this is the set of events that it makes sense to interpret this over.

void FDR::Assertions::DebugContext::initialise ( Canceller canceller  ) 

Initialises the behaviour debug context.

This must be called before any other methods are.

Exceptions:
CancelledException if the canceller was cancelled before this returns.
std::shared_ptr<Behaviour> FDR::Assertions::DebugContext::reveal_tau ( const Behaviour behaviour,
unsigned int  index 
) const

Assuming that behaviour.trace()[index] == TAU, returns the behaviour that performs the event, if any.

For example, if the tau is a tau resulting from hiding, this will return the behaviour in the tree who actually performed the non-hidden event. If the tau results from non-determinism, then this will return nullptr.

Parameters:
behaviour The behaviour in which to reveal the tau. Must be a behaviour that has been returned by a method of this class.
index The index of the tau in the behaviour trace to reveal.
std::vector<LTS::CompiledEvent> FDR::Assertions::DebugContext::reveal_taus_in_trace ( const Behaviour behaviour  )  const

Reveals all taus in the given trace.

This looks at the trace of the specified behaviour, and for any indicies such that behaviour.trace()[index] == TAU and such that the tau resulted from hiding, computes the event that was hidden. This is equivalent to calling reveal_tau on each index.

Parameters:
behaviour The behaviour in which to reveal the tau. Must be a behaviour that has been returned by a method of this class.
std::vector<std::shared_ptr<Behaviour> > FDR::Assertions::DebugContext::root_behaviours (  )  const

The top-level behaviours.

If this was created using a RefinementCounterexample, this will have two behaviours, the first of which is for the specification machine and the second is for the implementation. If this was created using a PropertyCounterexample, this will have a single behaviour of the machine.

TaskId FDR::Assertions::DebugContext::root_task_id (  )  const

Returns the identity of the task under which all tasks in this assertion will be created under.

This will be a valid TaskId as soon as the DebugContext has been created.


The documentation for this class was generated from the following file:
 All Classes Functions

Generated on 27 Oct 2017 for FDR by  doxygen 1.6.1