Storm
A Modern Probabilistic Model Checker
|
#include <MenuGameRefiner.h>
Public Types | |
enum class | Source { WeakestPrecondition , InitialGuard , InitialExpression , Guard , Interpolation , Manual } |
Public Member Functions | |
RefinementPredicates ()=default | |
RefinementPredicates (Source const &source, std::vector< storm::expressions::Expression > const &predicates) | |
Source | getSource () const |
std::vector< storm::expressions::Expression > const & | getPredicates () const |
void | addPredicates (std::vector< storm::expressions::Expression > const &newPredicates) |
Definition at line 43 of file MenuGameRefiner.h.
|
strong |
Enumerator | |
---|---|
WeakestPrecondition | |
InitialGuard | |
InitialExpression | |
Guard | |
Interpolation | |
Manual |
Definition at line 45 of file MenuGameRefiner.h.
|
default |
storm::gbar::abstraction::RefinementPredicates::RefinementPredicates | ( | Source const & | source, |
std::vector< storm::expressions::Expression > const & | predicates | ||
) |
Definition at line 33 of file MenuGameRefiner.cpp.
void storm::gbar::abstraction::RefinementPredicates::addPredicates | ( | std::vector< storm::expressions::Expression > const & | newPredicates | ) |
Definition at line 46 of file MenuGameRefiner.cpp.
std::vector< storm::expressions::Expression > const & storm::gbar::abstraction::RefinementPredicates::getPredicates | ( | ) | const |
Definition at line 42 of file MenuGameRefiner.cpp.
RefinementPredicates::Source storm::gbar::abstraction::RefinementPredicates::getSource | ( | ) | const |
Definition at line 38 of file MenuGameRefiner.cpp.