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

An assertion about processes. More...

#include <property_assertion.h>

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

Public Member Functions

 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 about processes.

Member Function Documentation

◆ machine()

std::shared_ptr<LTS::Machine> FDR::Assertions::PropertyAssertion::machine ( ) const

The process that this assertion is about.

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: