00001 #pragma once 00002 00003 #include <fdr/assertions/property_assertion.h> 00004 00005 namespace FDR 00006 { 00007 namespace Assertions 00008 { 00010 class DivergenceFreeAssertion : public PropertyAssertion 00011 { 00012 public: 00020 DivergenceFreeAssertion(const std::shared_ptr<Session>& session, const std::shared_ptr<LTS::Machine>& machine, 00021 const LTS::SemanticModel model); 00022 ~DivergenceFreeAssertion(); 00023 00024 DivergenceFreeAssertion(const DivergenceFreeAssertion& assertion) = delete; 00025 DivergenceFreeAssertion& operator=(const DivergenceFreeAssertion& assertion) = delete; 00026 00027 private: 00028 DivergenceFreeAssertion(); 00029 00030 friend struct AssertionFactory; 00031 }; 00032 00033 } // end Assertions 00034 } // end FDR