An refinement assertion about two processes. More...
#include <refinement_assertion.h>
Public Member Functions | |
RefinementAssertion (const RefinementAssertion &assertion) | |
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. | |
std::shared_ptr< LTS::Machine > | implementation () const |
The implementation process. | |
LTS::SemanticModel | model () const |
The semantic model this check has been performed in. | |
RefinementAssertion & | operator= (const RefinementAssertion &assertion) |
std::shared_ptr< LTS::Machine > | specification () const |
The specification process. | |
Friends | |
struct | AssertionFactory |
An refinement assertion about two processes.
FDR::Assertions::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.
session | The session associated with the machines. | |
specification | The specification, or left hand, process. | |
model | The semantic model in which to perform the check. | |
implementation | The implementation, or right hand, process. |
std::shared_ptr<LTS::Machine> FDR::Assertions::RefinementAssertion::implementation | ( | ) | const |
The implementation process.
This property is only available after the assertion has been compiled, which occurs during Assertion::execute().
std::shared_ptr<LTS::Machine> FDR::Assertions::RefinementAssertion::specification | ( | ) | const |
The specification process.
This property is only available after the assertion has been compiled, which occurs during Assertion::execute().