|
Storm 1.14.0.1
A Modern Probabilistic Model Checker
|
#include <map>#include "storm/logic/Formula.h"#include "storm/models/ModelBase.h"#include "storm/models/sparse/Dtmc.h"#include "storm/models/sparse/Mdp.h"#include "storm/solver/Z3SmtSolver.h"#include "storm/storage/SparseMatrix.h"#include "storm/storage/expressions/ExpressionManager.h"#include "storm/storage/expressions/RationalFunctionToExpression.h"#include "storm/utility/constants.h"#include "storm-pars/api/region.h"#include "storm-pars/modelchecker/region/monotonicity/Assumption.h"#include "storm-pars/modelchecker/region/monotonicity/AssumptionMaker.h"#include "storm-pars/modelchecker/region/monotonicity/LocalMonotonicityResult.h"#include "storm-pars/modelchecker/region/monotonicity/MonotonicityResult.h"#include "storm-pars/modelchecker/region/monotonicity/Order.h"#include "storm-pars/modelchecker/region/monotonicity/OrderExtender.h"

Go to the source code of this file.
Classes | |
| class | storm::analysis::MonotonicityHelper< ValueType, ConstantType > |
| struct | storm::analysis::MonotonicityHelper< ValueType, ConstantType >::ExpectedMonotonicityResult |
| The result of the order-based monotonicity analysis for one reachability order: the order itself, the monotonicity result computed from it, and the assumptions the order was built on. More... | |
Namespaces | |
| namespace | storm |
| namespace | storm::analysis |