An assertion that a process is deadlock free. More...
#include <deadlock_free_assertion.h>
Public Member Functions | |
DeadlockFreeAssertion (const DeadlockFreeAssertion &assertion) | |
DeadlockFreeAssertion (const std::shared_ptr< Session > &session, const std::shared_ptr< LTS::Machine > &machine, const LTS::SemanticModel model) | |
Construct a new deadlock-freedom assertion. | |
DeadlockFreeAssertion & | operator= (const DeadlockFreeAssertion &assertion) |
Friends | |
struct | AssertionFactory |
An assertion that a process is deadlock free.
FDR::Assertions::DeadlockFreeAssertion::DeadlockFreeAssertion | ( | const std::shared_ptr< Session > & | session, | |
const std::shared_ptr< LTS::Machine > & | machine, | |||
const LTS::SemanticModel | model | |||
) |
Construct a new deadlock-freedom 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. |