An assertion about processes. More...
#include <assertion.h>
Public Member Functions | |
| 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... | |
Protected Attributes | |
| std::shared_ptr< Data > | data |
| friend | Session |
Friends | |
| struct | AssertionFactory |
Detailed Description
An assertion about processes.
For example, this may represent a deadlock freedom or refinement assertion.
Member Function Documentation
◆ counterexamples()
| const std::vector<std::shared_ptr<Counterexample> >& FDR::Assertions::Assertion::counterexamples | ( | ) | const |
A list of counterexamples, if the assertion failed.
May only be called after execute() has returned.
Note that if passed() is false does not necessarily imply that there are counterexamples. For example, if the assertion is negated then the inner assertion passing will not generate any counterexamples.
◆ execute()
| void FDR::Assertions::Assertion::execute | ( | Canceller * | canceller | ) |
Checks the given assertion.
This is idempotent, and may be called harmlessly multiple times.
- Parameters
-
canceller A canceller object that can be used to cancel an in-progress check. If cancellation is not required, NULL may be passed instead.
- Exceptions
-
CancelledError if the canceller was cancelled during the check. CompilationError if the assertion could not be compiled (i.e. converted into FDR's internal data structures) as a result of an error detected in the input file.
◆ passed()
| bool FDR::Assertions::Assertion::passed | ( | ) | const |
If the assertion has been executed, true iff the assertion passed.
This may only be called once execute has returned.
◆ progress()
| std::shared_ptr<Progress> FDR::Assertions::Assertion::progress | ( | ) | const |
Reports statistics about the assertion's progress.
- Returns
- an appropriate progress representation, or nullptr if no progress information is available.
◆ root_task_id()
| TaskId FDR::Assertions::Assertion::root_task_id | ( | ) | const |
Returns the identity of the task under which all tasks in this assertion will be created under.
This will be INVALID_TASK until execute() has been called.
◆ to_string()
| std::string FDR::Assertions::Assertion::to_string | ( | ) | const |
Returns a string representation of this assertion.
This will be a pretty-printed version of the assertion in the original input file.
The documentation for this class was generated from the following file:
- libfdr/include/fdr/assertions/assertion.h
