Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
TransformationSettings.h
Go to the documentation of this file.
1#pragma once
2
3#include <optional>
4
5#include "storm-config.h"
8
9namespace storm {
10
11namespace utility::permutation {
12enum class OrderKind;
13}
14
15namespace settings::modules {
16
21 public:
26
32 bool isChainEliminationSet() const;
33
40
45
49 bool isToDiscreteTimeModelSet() const;
50
54 std::optional<storm::utility::permutation::OrderKind> getModelPermutation() const;
55
59 std::optional<uint64_t> getModelPermutationSeed() const;
60
61 bool check() const override;
62
63 void finalize() override;
64
65 // The name of the module.
66 static const std::string moduleName;
67
68 private:
69 // Define the string names of the options as constants.
70 static const std::string chainEliminationOptionName;
71 static const std::string labelBehaviorOptionName;
72 static const std::string toNondetOptionName;
73 static const std::string toDiscreteTimeOptionName;
74 static const std::string permuteModelOptionName;
75};
76
77} // namespace settings::modules
78} // namespace storm
This is the base class of the settings for a particular module.
This class represents the model transformer settings.
bool isToNondeterministicModelSet() const
Retrieves whether a DTMC/CTMC should be converted to an MDP/MA.
bool check() const override
Checks whether the settings are consistent.
TransformationSettings()
Creates a new set of transformer settings.
storm::transformer::EliminationLabelBehavior getLabelBehavior() const
Retrieves how the transformer should deal with labels when non-Markovian states are eliminated.
bool isChainEliminationSet() const
Retrieves whether the option to eliminate chains of non-Markovian states was set.
std::optional< storm::utility::permutation::OrderKind > getModelPermutation() const
If the returned value is not empty, the model should be permuted according to the given order.
void finalize() override
Prepares the modules for further usage, should be called at the end of the initialization,...
std::optional< uint64_t > getModelPermutationSeed() const
Retrieves a random seed to be used in case the model shall be permuted randomly.
bool isToDiscreteTimeModelSet() const
Retrieves whether a CTMC/MA should be converted to a DTMC/MDP.
EliminationLabelBehavior
Specify criteria whether a state can be eliminated and how its labels should be treated.
OrderKind
The order in which the states of a matrix are visited in a depth-first search or breadth-first search...
Definition permutation.h:21
LabParser.cpp.
Definition cli.cpp:18