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 PropertyAssertion : public Assertion 00013 { 00014 public: 00015 PropertyAssertion(const PropertyAssertion& assertion) = delete; 00016 PropertyAssertion& operator=(const PropertyAssertion& assertion) = delete; 00017 00022 std::shared_ptr<LTS::Machine> machine() const; 00023 00025 LTS::SemanticModel semantic_model() const; 00026 00027 protected: 00028 PropertyAssertion(); 00029 00030 friend struct AssertionFactory; 00031 }; 00032 00033 } // end Assertions 00034 } // end FDR