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