FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
An assertion that the given machine is deterministic. More...
#include <deterministic_assertion.h>
Public Member Functions | |
DeterministicAssertion (const DeterministicAssertion &assertion)=delete | |
DeterministicAssertion (const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model) | |
Construct a new determinism assertion. More... | |
DeterministicAssertion & | operator= (const DeterministicAssertion &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 the given machine is deterministic.
FDR::Assertions::DeterministicAssertion::DeterministicAssertion | ( | const std::shared_ptr< Session > & | session, |
const std::shared_ptr< LTS::Machine > & | machine, | ||
const LTS::SemanticModel | model | ||
) |
Construct a new determinism 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. |