00001 #pragma once 00002 00003 #include <fdr/assertions/counterexample/refinement_counterexample.h> 00004 00005 namespace FDR 00006 { 00007 namespace Assertions 00008 { 00014 class TraceCounterexample : public RefinementCounterexample 00015 { 00016 public: 00017 TraceCounterexample(const std::shared_ptr<Behaviour>& specification, 00018 const std::shared_ptr<Behaviour>& implementation); 00019 00021 LTS::CompiledEvent error_event() const; 00022 }; 00023 00024 } // end Assertions 00025 } // end FDR