FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
An assertion that a process has a certain trace. More...
#include <has_trace_assertion.h>
Public Member Functions | |
HasTraceAssertion (const HasTraceAssertion &assertion)=delete | |
HasTraceAssertion (const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model, const std::vector< LTS::CompiledEvent > &trace) | |
Construct a new has trace assertion. More... | |
HasTraceAssertion & | operator= (const HasTraceAssertion &assertion)=delete |
![]() | |
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 that a process has a certain trace.
FDR::Assertions::HasTraceAssertion::HasTraceAssertion | ( | const std::shared_ptr< Session > & | session, |
const std::shared_ptr< LTS::Machine > & | machine, | ||
const LTS::SemanticModel | model, | ||
const std::vector< LTS::CompiledEvent > & | trace | ||
) |
Construct a new has trace assertion.
session | The session associated with machine |
machine | The machine to check. |
model | The 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. |
trace | The trace to check can be performed by the machine. |