FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
Public Member Functions | Friends | List of all members
FDR::Assertions::DivergenceFreeAssertion Class Reference

An assertion that the given machine is divergence free. More...

#include <divergence_free_assertion.h>

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

Public Member Functions

 DivergenceFreeAssertion (const DivergenceFreeAssertion &assertion)=delete
 
 DivergenceFreeAssertion (const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model)
 Construct a new divergence-freedom assertion. More...
 
DivergenceFreeAssertionoperator= (const DivergenceFreeAssertion &assertion)=delete
 
- Public Member Functions inherited from FDR::Assertions::PropertyAssertion
 PropertyAssertion (const PropertyAssertion &assertion)=delete
 
std::shared_ptr< LTS::Machinemachine () const
 The process that this assertion is about. More...
 
PropertyAssertionoperator= (const PropertyAssertion &assertion)=delete
 
LTS::SemanticModel semantic_model () const
 The semantic model this check has been performed in.
 
- 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 assertion that the given machine is divergence free.

Constructor & Destructor Documentation

◆ DivergenceFreeAssertion()

FDR::Assertions::DivergenceFreeAssertion::DivergenceFreeAssertion ( const std::shared_ptr< Session > &  session,
const std::shared_ptr< LTS::Machine > &  machine,
const LTS::SemanticModel  model 
)

Construct a new divergence-freedom assertion.

Parameters
sessionThe session associated with machine
machineThe machine to check.
modelThe semantic model in which to perform the check. An exception may be thrown in Assertion::execute() if this is not a valid model for this assertion.

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