FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
An refinement assertion about two processes. More...
#include <refinement_assertion.h>
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::Machine > | implementation () const |
The implementation process. More... | |
LTS::SemanticModel | model () const |
The semantic model this check has been performed in. | |
RefinementAssertion & | operator= (const RefinementAssertion &assertion)=delete |
std::shared_ptr< LTS::Machine > | specification () const |
The specification process. More... | |
![]() | |
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... | |
Assertion & | operator= (const Assertion &assertion)=delete |
bool | passed () const |
If the assertion has been executed, true iff the assertion passed. More... | |
std::shared_ptr< Progress > | progress () 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 | |
![]() | |
std::shared_ptr< Data > | data |
friend | Session |
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().