FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
divergence_free_assertion.h
1 #pragma once
2 
3 #include <fdr/assertions/property_assertion.h>
4 
5 namespace FDR
6 {
7 namespace Assertions
8 {
11 {
12 public:
20  DivergenceFreeAssertion(const std::shared_ptr<Session>& session, const std::shared_ptr<LTS::Machine>& machine,
21  const LTS::SemanticModel model);
23 
24  DivergenceFreeAssertion(const DivergenceFreeAssertion& assertion) = delete;
25  DivergenceFreeAssertion& operator=(const DivergenceFreeAssertion& assertion) = delete;
26 
27 private:
29 
30  friend struct AssertionFactory;
31 };
32 
33 } // end Assertions
34 } // end FDR
FDR::Assertions::PropertyAssertion::machine
std::shared_ptr< LTS::Machine > machine() const
The process that this assertion is about.
FDR::Assertions::DivergenceFreeAssertion
An assertion that the given machine is divergence free.
Definition: divergence_free_assertion.h:11
FDR::Assertions::PropertyAssertion
An assertion about processes.
Definition: property_assertion.h:13
FDR::Assertions::DivergenceFreeAssertion::DivergenceFreeAssertion
DivergenceFreeAssertion(const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model)
Construct a new divergence-freedom assertion.