FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
An assertion about processes. More...
#include <property_assertion.h>
Public Member Functions | |
PropertyAssertion (const PropertyAssertion &assertion)=delete | |
std::shared_ptr< LTS::Machine > | machine () const |
The process that this assertion is about. More... | |
PropertyAssertion & | operator= (const PropertyAssertion &assertion)=delete |
LTS::SemanticModel | semantic_model () const |
The semantic model this check has been performed in. | |
![]() | |
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 assertion about processes.
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().