00001 #pragma once 00002 00003 #include <fdr/assertions/assertion.h> 00004 #include <fdr/lts/machine.h> 00005 #include <fdr/lts/semantic_model.h> 00006 00007 namespace FDR 00008 { 00009 namespace Assertions 00010 { 00012 class RefinementAssertion : public Assertion 00013 { 00014 public: 00021 RefinementAssertion(const std::shared_ptr<Session>& session, const std::shared_ptr<LTS::Machine>& specification, 00022 const LTS::SemanticModel model, const std::shared_ptr<LTS::Machine>& implementation); 00023 ~RefinementAssertion(); 00024 00025 RefinementAssertion(const RefinementAssertion& assertion) = delete; 00026 RefinementAssertion& operator=(const RefinementAssertion& assertion) = delete; 00027 00032 std::shared_ptr<LTS::Machine> implementation() const; 00033 00035 LTS::SemanticModel model() const; 00036 00041 std::shared_ptr<LTS::Machine> specification() const; 00042 00043 private: 00044 RefinementAssertion(); 00045 00046 friend struct AssertionFactory; 00047 }; 00048 00049 } // end Assertions 00050 } // end FDR