FDR::Assertions::RefinementAssertion Class Reference

An refinement assertion about two processes. More...

#include <refinement_assertion.h>

Inheritance diagram for FDR::Assertions::RefinementAssertion:
Inheritance graph
[legend]
Collaboration diagram for FDR::Assertions::RefinementAssertion:
Collaboration graph
[legend]

List of all members.

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::Machineimplementation () const
 The implementation process.
LTS::SemanticModel model () const
 The semantic model this check has been performed in.
RefinementAssertionoperator= (const RefinementAssertion &assertion)
std::shared_ptr< LTS::Machinespecification () const
 The specification process.

Friends

struct AssertionFactory

Detailed Description

An refinement assertion about two processes.


Constructor & Destructor Documentation

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.

Parameters:
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.

Member Function Documentation

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().


The documentation for this class was generated from the following file:
 All Classes Functions

Generated on 27 Oct 2017 for FDR by  doxygen 1.6.1