FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
debug_context.h
1 #pragma once
2 
3 #include <memory>
4 #include <vector>
5 
6 #include <fdr/assertions/behaviour/behaviour.h>
7 #include <fdr/tasks/canceller.h>
8 #include <fdr/tasks/progress_reporter.h>
9 
10 namespace FDR
11 {
12 namespace Assertions
13 {
14 class PropertyCounterexample;
15 class RefinementCounterexample;
16 
27 {
28 public:
41  DebugContext(const Assertions::RefinementCounterexample& counterexample, bool elide_uninteresting_behaviours);
42 
55  DebugContext(const Assertions::PropertyCounterexample& counterexample, bool elide_uninteresting_behaviours);
56 
57  virtual ~DebugContext();
58 
59  DebugContext(DebugContext&) = delete;
60  DebugContext& operator=(DebugContext&) = delete;
61 
68  void initialise(Canceller* canceller);
69 
73  TaskId root_task_id() const;
74 
82  std::vector<std::shared_ptr<Behaviour>> root_behaviours() const;
83 
88  std::vector<std::shared_ptr<Behaviour>> behaviour_children(const Behaviour& behaviour) const;
89 
94  std::vector<LTS::CompiledEvent> full_alphabet() const;
95 
107  std::shared_ptr<Behaviour> reveal_tau(const Behaviour& behaviour, unsigned int index) const;
108 
117  std::vector<LTS::CompiledEvent> reveal_taus_in_trace(const Behaviour& behaviour) const;
118 private:
119  struct Data;
120 
121  std::unique_ptr<Data> data;
122 };
123 
124 } // end Assertions
125 } // end FDR
FDR::Assertions::DebugContext::DebugContext
DebugContext(const Assertions::RefinementCounterexample &counterexample, bool elide_uninteresting_behaviours)
Creates a new debug context from a refinement check.
FDR::Assertions::DebugContext
Allows counterexamples to be divided into behaviours of component processes.
Definition: debug_context.h:27
FDR::Assertions::RefinementCounterexample
A counterexample to a refinement assertion.
Definition: refinement_counterexample.h:19
FDR::Assertions::DebugContext::reveal_taus_in_trace
std::vector< LTS::CompiledEvent > reveal_taus_in_trace(const Behaviour &behaviour) const
Reveals all taus in the given trace.
FDR::Assertions::DebugContext::full_alphabet
std::vector< LTS::CompiledEvent > full_alphabet() const
The union of the alphabets of all the machines in this debug tree.
FDR::Assertions::PropertyCounterexample
A counterexample to a property assertion, such as deadlock freedom.
Definition: property_counterexample.h:15
FDR::Assertions::DebugContext::initialise
void initialise(Canceller *canceller)
Initialises the behaviour debug context.
FDR::Assertions::DebugContext::root_behaviours
std::vector< std::shared_ptr< Behaviour > > root_behaviours() const
The top-level behaviours.
FDR::Assertions::DebugContext::DebugContext
DebugContext(const Assertions::PropertyCounterexample &counterexample, bool elide_uninteresting_behaviours)
Creates a new debug context from a property check.
FDR::Assertions::DebugContext::root_task_id
TaskId root_task_id() const
Returns the identity of the task under which all tasks in this assertion will be created under.
FDR::Assertions::DebugContext::reveal_tau
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,...
FDR::Assertions::DebugContext::behaviour_children
std::vector< std::shared_ptr< Behaviour > > behaviour_children(const Behaviour &behaviour) const
Returns the children of the given behaviour.
FDR::Canceller
Allows cancellation of a running task to be requested.
Definition: canceller.h:53
FDR::Assertions::Behaviour
A particular path through a Machine, often leading to an interesting state.
Definition: behaviour.h:22