FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
Public Member Functions | Friends | List of all members
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]

Public Member Functions

 RefinementAssertion (const RefinementAssertion &assertion)=delete
 
 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. More...
 
std::shared_ptr< LTS::Machineimplementation () const
 The implementation process. More...
 
LTS::SemanticModel model () const
 The semantic model this check has been performed in.
 
RefinementAssertionoperator= (const RefinementAssertion &assertion)=delete
 
std::shared_ptr< LTS::Machinespecification () const
 The specification process. More...
 
- Public Member Functions inherited from FDR::Assertions::Assertion
 Assertion (const Assertion &assertion)=delete
 
const std::vector< std::shared_ptr< Counterexample > > & counterexamples () const
 A list of counterexamples, if the assertion failed. More...
 
void execute (Canceller *canceller)
 Checks the given assertion. More...
 
Assertionoperator= (const Assertion &assertion)=delete
 
bool passed () const
 If the assertion has been executed, true iff the assertion passed. More...
 
std::shared_ptr< Progressprogress () const
 Reports statistics about the assertion's progress. More...
 
TaskId root_task_id () const
 Returns the identity of the task under which all tasks in this assertion will be created under. More...
 
std::string to_string () const
 Returns a string representation of this assertion. More...
 

Friends

struct AssertionFactory
 

Additional Inherited Members

- Protected Attributes inherited from FDR::Assertions::Assertion
std::shared_ptr< Data > data
 
friend Session
 

Detailed Description

An refinement assertion about two processes.

Constructor & Destructor Documentation

◆ RefinementAssertion()

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
sessionThe session associated with the machines.
specificationThe specification, or left hand, process.
modelThe semantic model in which to perform the check.
implementationThe implementation, or right hand, process.

Member Function Documentation

◆ implementation()

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

◆ specification()

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: