An assertion that a process has a certain trace. More...
#include <has_trace_assertion.h>
Public Member Functions | |
HasTraceAssertion (const HasTraceAssertion &assertion) | |
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. | |
HasTraceAssertion & | operator= (const HasTraceAssertion &assertion) |
Friends | |
struct | AssertionFactory |
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. |