diff --git a/src/storm-pomdp-cli/settings/PomdpSettings.cpp b/src/storm-pomdp-cli/settings/PomdpSettings.cpp
index 241c5fd99..f529d8073 100644
--- a/src/storm-pomdp-cli/settings/PomdpSettings.cpp
+++ b/src/storm-pomdp-cli/settings/PomdpSettings.cpp
@@ -34,6 +34,7 @@
#include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
#include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h"
#include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h"
+#include "storm-pomdp-cli/settings/modules/ToParametricSettings.h"
namespace storm {
@@ -50,6 +51,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::POMDPSettings>();
storm::settings::addModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
storm::settings::addModule<storm::settings::modules::BeliefExplorationSettings>();
+ storm::settings::addModule<storm::settings::modules::ToParametricSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
index c009ba36d..d6c17224f 100644
--- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
+++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
@@ -19,15 +19,10 @@ namespace storm {
std::vector<std::string> beliefExplorationModes = {"both", "discretize", "unfold"};
const std::string qualitativeReductionOption = "qualitativereduction";
const std::string analyzeUniqueObservationsOption = "uniqueobservations";
- const std::string mecReductionOption = "mecreduction";
const std::string selfloopReductionOption = "selfloopreduction";
const std::string memoryBoundOption = "memorybound";
const std::string memoryPatternOption = "memorypattern";
std::vector<std::string> memoryPatterns = {"trivial", "fixedcounter", "selectivecounter", "ring", "fixedring", "settablebits", "full"};
- const std::string fscmode = "fscmode";
- std::vector<std::string> fscModes = {"standard", "simple-linear", "simple-linear-inverse"};
- const std::string transformBinaryOption = "transformbinary";
- const std::string transformSimpleOption = "transformsimple";
const std::string checkFullyObservableOption = "check-fully-observable";
const std::string isQualitativeOption = "qualitative-analysis";
@@ -36,13 +31,9 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, exportAsParametricModelOption, false, "Export the parametric file.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which to write the model.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, qualitativeReductionOption, false, "Reduces the model size by performing qualitative analysis (E.g. merge states with prob. 1.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, analyzeUniqueObservationsOption, false, "Computes the states with a unique observation").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, mecReductionOption, false, "Reduces the model size by analyzing maximal end components").build());
this->addOption(storm::settings::OptionBuilder(moduleName, selfloopReductionOption, false, "Reduces the model size by removing self loop actions").build());
this->addOption(storm::settings::OptionBuilder(moduleName, memoryBoundOption, false, "Sets the maximal number of allowed memory states (1 means memoryless schedulers).").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("bound", "The maximal number of memory states.").setDefaultValueUnsignedInteger(1).addValidatorUnsignedInteger(storm::settings::ArgumentValidatorFactory::createUnsignedGreaterValidator(0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, memoryPatternOption, false, "Sets the pattern of the considered memory structure").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "Pattern name.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(memoryPatterns)).setDefaultValueString("full").build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, fscmode, false, "Sets the way the pMC is obtained").addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "type name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(fscModes)).setDefaultValueString("standard").build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build());
- this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, beliefExplorationOption, false,"Analyze the POMDP by exploring the belief state-space.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "Sets whether lower, upper, or interval result bounds are computed.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(beliefExplorationModes)).setDefaultValueString("both").makeOptional().build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, checkFullyObservableOption, false, "Performs standard model checking on the underlying MDP").build());
this->addOption(storm::settings::OptionBuilder(moduleName, isQualitativeOption, false, "Sets the option qualitative analysis").build());
@@ -68,10 +59,6 @@ namespace storm {
return this->getOption(analyzeUniqueObservationsOption).getHasOptionBeenSet();
}
- bool POMDPSettings::isMecReductionSet() const {
- return this->getOption(mecReductionOption).getHasOptionBeenSet();
- }
-
bool POMDPSettings::isSelfloopReductionSet() const {
return this->getOption(selfloopReductionOption).getHasOptionBeenSet();
}
@@ -123,18 +110,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The name of the memory pattern is unknown.");
}
- std::string POMDPSettings::getFscApplicationTypeString() const {
- return this->getOption(fscmode).getArgumentByName("type").getValueAsString();
- }
-
- bool POMDPSettings::isTransformBinarySet() const {
- return this->getOption(transformBinaryOption).getHasOptionBeenSet();
- }
- bool POMDPSettings::isTransformSimpleSet() const {
- return this->getOption(transformSimpleOption).getHasOptionBeenSet();
- }
-
void POMDPSettings::finalize() {
}
diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h
index 30b0adc53..2d9b8c59b 100644
--- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h
+++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h
@@ -31,13 +31,9 @@ namespace storm {
bool isBeliefExplorationDiscretizeSet() const;
bool isBeliefExplorationUnfoldSet() const;
bool isAnalyzeUniqueObservationsSet() const;
- bool isMecReductionSet() const;
bool isSelfloopReductionSet() const;
- bool isTransformSimpleSet() const;
- bool isTransformBinarySet() const;
bool isCheckFullyObservableSet() const;
bool isQualitativeAnalysisSet() const;
- std::string getFscApplicationTypeString() const;
uint64_t getMemoryBound() const;
storm::storage::PomdpMemoryPattern getMemoryPattern() const;
diff --git a/src/storm-pomdp-cli/settings/modules/ToParametricSettings.cpp b/src/storm-pomdp-cli/settings/modules/ToParametricSettings.cpp
new file mode 100644
index 000000000..66abc3ee7
--- /dev/null
+++ b/src/storm-pomdp-cli/settings/modules/ToParametricSettings.cpp
@@ -0,0 +1,56 @@
+#include "storm-pomdp-cli/settings/modules/ToParametricSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ const std::string ToParametricSettings::moduleName = "toparametric";
+ const std::string mecReductionOption = "mecreduction";
+ const std::string selfloopReductionOption = "selfloopreduction";
+ const std::string fscmode = "fscmode";
+ std::vector<std::string> fscModes = {"standard", "simple-linear", "simple-linear-inverse"};
+ const std::string transformBinaryOption = "transformbinary";
+ const std::string transformSimpleOption = "transformsimple";
+
+ ToParametricSettings::ToParametricSettings() : ModuleSettings(moduleName) {
+ this->addOption(storm::settings::OptionBuilder(moduleName, mecReductionOption, false, "Reduces the model size by analyzing maximal end components").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, fscmode, false, "Sets the way the pMC is obtained").addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "type name").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(fscModes)).setDefaultValueString("standard").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, transformBinaryOption, false, "Transforms the pomdp to a binary pomdp.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, transformSimpleOption, false, "Transforms the pomdp to a binary and simple pomdp.").build());
+ }
+
+
+ bool ToParametricSettings::isMecReductionSet() const {
+ return this->getOption(mecReductionOption).getHasOptionBeenSet();
+ }
+
+ std::string ToParametricSettings::getFscApplicationTypeString() const {
+ return this->getOption(fscmode).getArgumentByName("type").getValueAsString();
+ }
+
+ bool ToParametricSettings::isTransformBinarySet() const {
+ return this->getOption(transformBinaryOption).getHasOptionBeenSet();
+ }
+
+ bool ToParametricSettings::isTransformSimpleSet() const {
+ return this->getOption(transformSimpleOption).getHasOptionBeenSet();
+ }
+
+ void ToParametricSettings::finalize() {
+ }
+
+ bool ToParametricSettings::check() const {
+ return true;
+ }
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
diff --git a/src/storm-pomdp-cli/settings/modules/ToParametricSettings.h b/src/storm-pomdp-cli/settings/modules/ToParametricSettings.h
new file mode 100644
index 000000000..e29586709
--- /dev/null
+++ b/src/storm-pomdp-cli/settings/modules/ToParametricSettings.h
@@ -0,0 +1,49 @@
+#pragma once
+
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+#include "storm-pomdp/storage/PomdpMemory.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ /*!
+ * This class represents the settings for POMDP model checking.
+ */
+ class ToParametricSettings : public ModuleSettings {
+ public:
+
+ /*!
+ * Creates a new set of POMDP settings.
+ */
+ ToParametricSettings();
+
+ virtual ~ToParametricSettings() = default;
+
+ bool isExportToParametricSet() const;
+ std::string getExportToParametricFilename() const;
+
+ bool isQualitativeReductionSet() const;
+
+ bool isMecReductionSet() const;
+ bool isTransformSimpleSet() const;
+ bool isTransformBinarySet() const;
+ std::string getFscApplicationTypeString() const;
+
+ bool check() const override;
+ void finalize() override;
+
+ // The name of the module.
+ static const std::string moduleName;
+
+ private:
+
+
+ };
+
+ } // namespace modules
+ } // namespace settings
+} // namespace storm
diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index d42ac48e6..979f76474 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -5,6 +5,7 @@
#include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
#include "storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h"
#include "storm-pomdp-cli/settings/modules/BeliefExplorationSettings.h"
+#include "storm-pomdp-cli/settings/modules/ToParametricSettings.h"
#include "storm-pomdp-cli/settings/PomdpSettings.h"
#include "storm/analysis/GraphConditions.h"
@@ -268,6 +269,8 @@ namespace storm {
template<typename ValueType, storm::dd::DdType DdType>
bool performTransformation(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>>& pomdp, storm::logic::Formula const& formula) {
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
+ auto const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+ auto const& transformSettings = storm::settings::getModule<storm::settings::modules::ToParametricSettings>();
bool transformationPerformed = false;
bool memoryUnfolded = false;
if (pomdpSettings.getMemoryBound() > 1) {
@@ -284,7 +287,7 @@ namespace storm {
// From now on the pomdp is considered memoryless
- if (pomdpSettings.isMecReductionSet()) {
+ if (transformSettings.isMecReductionSet()) {
STORM_PRINT_AND_LOG("Eliminating mec choices ...");
// Note: Elimination of mec choices only preserves memoryless schedulers.
uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
@@ -296,8 +299,8 @@ namespace storm {
transformationPerformed = true;
}
- if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) {
- if (pomdpSettings.isTransformSimpleSet()) {
+ if (transformSettings.isTransformBinarySet() || transformSettings.isTransformSimpleSet()) {
+ if (transformSettings.isTransformSimpleSet()) {
STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP.");
pomdp = storm::transformer::BinaryPomdpTransformer<ValueType>().transform(*pomdp, true);
} else {
@@ -312,17 +315,16 @@ namespace storm {
if (pomdpSettings.isExportToParametricSet()) {
STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC...");
storm::transformer::ApplyFiniteSchedulerToPomdp<ValueType> toPMCTransformer(*pomdp);
- std::string transformMode = pomdpSettings.getFscApplicationTypeString();
+ std::string transformMode = transformSettings.getFscApplicationTypeString();
auto pmc = toPMCTransformer.transform(storm::transformer::parsePomdpFscApplicationMode(transformMode));
STORM_PRINT_AND_LOG(" done." << std::endl);
pmc->printModelInformationToStream(std::cout);
- STORM_PRINT_AND_LOG("Simplifying pMC...");
- //if (generalSettings.isBisimulationSet()) {
- pmc = storm::api::performBisimulationMinimization<storm::RationalFunction>(pmc->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(),{formula.asSharedPointer()}, storm::storage::BisimulationType::Strong)->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
-
+ //if (transformSettings.isSimplificationSet()) {
+ STORM_PRINT_AND_LOG("Simplifying pMC...");
+ pmc = storm::api::performBisimulationMinimization<storm::RationalFunction>(pmc->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(),{formula.asSharedPointer()}, storm::storage::BisimulationType::Strong)->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+ STORM_PRINT_AND_LOG(" done." << std::endl);
+ pmc->printModelInformationToStream(std::cout);
//}
- STORM_PRINT_AND_LOG(" done." << std::endl);
- pmc->printModelInformationToStream(std::cout);
STORM_PRINT_AND_LOG("Exporting pMC...");
storm::analysis::ConstraintCollector<storm::RationalFunction> constraints(*pmc);
auto const& parameterSet = constraints.getVariables();