00001 #pragma once 00002 00003 #include <memory> 00004 #include <vector> 00005 00006 #include <fdr/assertions/behaviour/behaviour.h> 00007 #include <fdr/tasks/canceller.h> 00008 #include <fdr/tasks/progress_reporter.h> 00009 00010 namespace FDR 00011 { 00012 namespace Assertions 00013 { 00014 class PropertyCounterexample; 00015 class RefinementCounterexample; 00016 00026 class DebugContext 00027 { 00028 public: 00041 DebugContext(const Assertions::RefinementCounterexample& counterexample, bool elide_uninteresting_behaviours); 00042 00055 DebugContext(const Assertions::PropertyCounterexample& counterexample, bool elide_uninteresting_behaviours); 00056 00057 virtual ~DebugContext(); 00058 00059 DebugContext(DebugContext&) = delete; 00060 DebugContext& operator=(DebugContext&) = delete; 00061 00068 void initialise(Canceller* canceller); 00069 00073 TaskId root_task_id() const; 00074 00082 std::vector<std::shared_ptr<Behaviour>> root_behaviours() const; 00083 00088 std::vector<std::shared_ptr<Behaviour>> behaviour_children(const Behaviour& behaviour) const; 00089 00094 std::vector<LTS::CompiledEvent> full_alphabet() const; 00095 00107 std::shared_ptr<Behaviour> reveal_tau(const Behaviour& behaviour, unsigned int index) const; 00108 00117 std::vector<LTS::CompiledEvent> reveal_taus_in_trace(const Behaviour& behaviour) const; 00118 private: 00119 struct Data; 00120 00121 std::unique_ptr<Data> data; 00122 }; 00123 00124 } // end Assertions 00125 } // end FDR