FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
refinement_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:
21  RefinementAssertion(const std::shared_ptr<Session>& session, const std::shared_ptr<LTS::Machine>& specification,
22  const LTS::SemanticModel model, const std::shared_ptr<LTS::Machine>& implementation);
24 
25  RefinementAssertion(const RefinementAssertion& assertion) = delete;
26  RefinementAssertion& operator=(const RefinementAssertion& assertion) = delete;
27 
32  std::shared_ptr<LTS::Machine> implementation() const;
33 
35  LTS::SemanticModel model() const;
36 
41  std::shared_ptr<LTS::Machine> specification() const;
42 
43 private:
45 
46  friend struct AssertionFactory;
47 };
48 
49 } // end Assertions
50 } // end FDR
FDR::Assertions::RefinementAssertion::implementation
std::shared_ptr< LTS::Machine > implementation() const
The implementation process.
FDR::Assertions::RefinementAssertion
An refinement assertion about two processes.
Definition: refinement_assertion.h:13
FDR::Assertions::RefinementAssertion::RefinementAssertion
RefinementAssertion(const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &specification, const LTS::SemanticModel model, const std::shared_ptr< LTS::Machine > &implementation)
Constructs a new refinement assertion about the specified machines.
FDR::Assertions::RefinementAssertion::model
LTS::SemanticModel model() const
The semantic model this check has been performed in.
FDR::Assertions::RefinementAssertion::specification
std::shared_ptr< LTS::Machine > specification() const
The specification process.
FDR::Assertions::Assertion
An assertion about processes.
Definition: assertion.h:23