Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::gbar::abstraction::RefinementPredicates Class Reference

#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)
 

Detailed Description

Definition at line 43 of file MenuGameRefiner.h.

Member Enumeration Documentation

◆ Source

Enumerator
WeakestPrecondition 
InitialGuard 
InitialExpression 
Guard 
Interpolation 
Manual 

Definition at line 45 of file MenuGameRefiner.h.

Constructor & Destructor Documentation

◆ RefinementPredicates() [1/2]

storm::gbar::abstraction::RefinementPredicates::RefinementPredicates ( )
default

◆ RefinementPredicates() [2/2]

storm::gbar::abstraction::RefinementPredicates::RefinementPredicates ( Source const &  source,
std::vector< storm::expressions::Expression > const &  predicates 
)

Definition at line 33 of file MenuGameRefiner.cpp.

Member Function Documentation

◆ addPredicates()

void storm::gbar::abstraction::RefinementPredicates::addPredicates ( std::vector< storm::expressions::Expression > const &  newPredicates)

Definition at line 46 of file MenuGameRefiner.cpp.

◆ getPredicates()

std::vector< storm::expressions::Expression > const & storm::gbar::abstraction::RefinementPredicates::getPredicates ( ) const

Definition at line 42 of file MenuGameRefiner.cpp.

◆ getSource()

RefinementPredicates::Source storm::gbar::abstraction::RefinementPredicates::getSource ( ) const

Definition at line 38 of file MenuGameRefiner.cpp.


The documentation for this class was generated from the following files: