FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
property_assertion.h
1 #pragma once
2 
3 #include <fdr/assertions/assertion.h>
4 #include <fdr/lts/machine.h>
5 #include <fdr/lts/semantic_model.h>
6 
7 namespace FDR
8 {
9 namespace Assertions
10 {
13 {
14 public:
15  PropertyAssertion(const PropertyAssertion& assertion) = delete;
16  PropertyAssertion& operator=(const PropertyAssertion& assertion) = delete;
17 
22  std::shared_ptr<LTS::Machine> machine() const;
23 
25  LTS::SemanticModel semantic_model() const;
26 
27 protected:
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::PropertyAssertion
An assertion about processes.
Definition: property_assertion.h:13
FDR::Assertions::Assertion
An assertion about processes.
Definition: assertion.h:23
FDR::Assertions::PropertyAssertion::semantic_model
LTS::SemanticModel semantic_model() const
The semantic model this check has been performed in.