diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp index 04f31dfd6..a5ff3e325 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp @@ -5,10 +5,6 @@ #include "storm/settings/Option.h" #include "storm/settings/OptionBuilder.h" #include "storm/settings/ArgumentBuilder.h" -#include "storm/settings/Argument.h" - -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/IllegalArgumentValueException.h" namespace storm { namespace settings { @@ -21,6 +17,8 @@ namespace storm { const std::string mecReductionOption = "mecreduction"; const std::string selfloopReductionOption = "selfloopreduction"; const std::string memoryBoundOption = "memorybound"; + const std::string fscmode = "fscmode"; + std::vector fscModes = {"standard", "simple-linear", "simple-linear-inverse"}; POMDPSettings::POMDPSettings() : ModuleSettings(moduleName) { 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()); @@ -29,7 +27,7 @@ namespace storm { 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, 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()); } bool POMDPSettings::isExportToParametricSet() const { @@ -59,7 +57,10 @@ namespace storm { uint64_t POMDPSettings::getMemoryBound() const { return this->getOption(memoryBoundOption).getArgumentByName("bound").getValueAsUnsignedInteger(); } - + + std::string POMDPSettings::getFscApplicationTypeString() const { + return this->getOption(fscmode).getArgumentByName("type").getValueAsString(); + } diff --git a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h index 8aed328f7..6620ee3da 100644 --- a/src/storm-pomdp-cli/settings/modules/POMDPSettings.h +++ b/src/storm-pomdp-cli/settings/modules/POMDPSettings.h @@ -29,6 +29,7 @@ namespace storm { bool isAnalyzeUniqueObservationsSet() const; bool isMecReductionSet() const; bool isSelfloopReductionSet() const; + std::string getFscApplicationTypeString() const; uint64_t getMemoryBound() const; diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 1418781dd..ec30516d9 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -39,6 +39,7 @@ #include "storm-pomdp/transformer/PomdpMemoryUnfolder.h" #include "storm-pomdp/analysis/UniqueObservationStates.h" #include "storm-pomdp/analysis/QualitativeAnalysis.h" +#include "storm/api/storm.h" /*! * Initialize the settings manager. @@ -51,8 +52,8 @@ void initializeSettings() { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(false); - storm::settings::addModule(); - storm::settings::addModule(); +//storm::settings::addModule(); +// storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); @@ -95,6 +96,8 @@ int main(const int argc, const char** argv) { auto const& coreSettings = storm::settings::getModule(); + auto const& generalSettings = storm::settings::getModule(); + auto const& bisimulationSettings = storm::settings::getModule(); auto const& pomdpSettings = storm::settings::getModule(); // For several engines, no model building step is performed, but the verification is started right away. @@ -139,6 +142,14 @@ int main(const int argc, const char** argv) { STORM_PRINT_AND_LOG(" done." << std::endl); std::cout << "actual reduction not yet implemented..." << std::endl; } + } else if (formula->isRewardOperatorFormula()) { + if (pomdpSettings.isSelfloopReductionSet() && storm::solver::minimize(formula->asRewardOperatorFormula().getOptimalityType())) { + STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); + uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); + storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); + pomdp = selfLoopEliminator.transform(); + STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); + } } if (pomdpSettings.getMemoryBound() > 1) { STORM_PRINT_AND_LOG("Computing the unfolding for memory bound " << pomdpSettings.getMemoryBound() << "..."); @@ -165,7 +176,15 @@ int main(const int argc, const char** argv) { if (pomdpSettings.isExportToParametricSet()) { STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC..."); storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*pomdp); - auto pmc = toPMCTransformer.transform(); + std::string transformMode = pomdpSettings.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(pmc->as>(),{formula})->as>(); + + //} STORM_PRINT_AND_LOG(" done." << std::endl); pmc->printModelInformationToStream(std::cout); STORM_PRINT_AND_LOG("Exporting pMC..."); diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp index e175139e6..8f432bb2e 100644 --- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp +++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp @@ -1,9 +1,22 @@ +#include "storm/exceptions/IllegalArgumentException.h" #include "storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h" #include "storm/utility/vector.h" +#include "storm/exceptions/NotImplementedException.h" namespace storm { namespace transformer { + PomdpFscApplicationMode parsePomdpFscApplicationMode(std::string const& mode) { + if (mode == "standard") { + return PomdpFscApplicationMode::STANDARD; + } else if (mode == "simple-linear") { + return PomdpFscApplicationMode::SIMPLE_LINEAR; + } else if (mode == "simple-linear-inverse") { + return PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE; + } else { + STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Mode " << mode << " not known." ); + } + } struct RationalFunctionConstructor { RationalFunctionConstructor() : cache(std::make_shared()) { @@ -20,19 +33,29 @@ namespace storm { template - std::unordered_map> ApplyFiniteSchedulerToPomdp::getObservationChoiceWeights() const { + std::unordered_map> ApplyFiniteSchedulerToPomdp::getObservationChoiceWeights(PomdpFscApplicationMode applicationMode ) const { std::unordered_map> res; RationalFunctionConstructor ratFuncConstructor; - + for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) { auto observation = pomdp.getObservation(state); auto it = res.find(observation); if (it == res.end()) { std::vector weights; + storm::RationalFunction collected = storm::utility::one(); storm::RationalFunction lastWeight = storm::utility::one(); for (uint64_t a = 0; a < pomdp.getNumberOfChoices(state) - 1; ++a) { std::string varName = "p" + std::to_string(observation) + "_" + std::to_string(a); - weights.push_back(ratFuncConstructor.translate(carl::freshRealVariable(varName))); + storm::RationalFunction var = ratFuncConstructor.translate(carl::freshRealVariable(varName)); + if (applicationMode == PomdpFscApplicationMode::SIMPLE_LINEAR) { + weights.push_back(collected * var); + collected *= storm::utility::one() - var; + } else if (applicationMode == PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) { + weights.push_back(collected * (storm::utility::one() - var)); + collected *= var; + } else if (applicationMode == PomdpFscApplicationMode::STANDARD) { + weights.push_back(var); + } lastWeight -= weights.back(); } weights.push_back(lastWeight); @@ -46,11 +69,11 @@ namespace storm { template - std::shared_ptr> ApplyFiniteSchedulerToPomdp::transform() const { + std::shared_ptr> ApplyFiniteSchedulerToPomdp::transform(PomdpFscApplicationMode applicationMode ) const { storm::storage::sparse::ModelComponents modelComponents; uint64_t nrStates = pomdp.getNumberOfStates(); - std::unordered_map> observationChoiceWeights = getObservationChoiceWeights(); + std::unordered_map> observationChoiceWeights = getObservationChoiceWeights(applicationMode); storm::storage::SparseMatrixBuilder smb(nrStates, nrStates, 0, true); for (uint64_t state = 0; state < nrStates; ++state) { @@ -94,7 +117,7 @@ namespace storm { } } storm::models::sparse::StandardRewardModel rewardModel(std::move(stateRewards)); - modelComponents.rewardModels.emplace(pomdpRewardModel.first, std::move(rewardModel)); + modelComponents.rewardModels.emplace(pomdpRewardModel.first, std::move(rewardModel)) ; } modelComponents.stateLabeling = pomdp.getStateLabeling(); diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h index d6b4967ce..61e956102 100644 --- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h +++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h @@ -8,6 +8,14 @@ namespace storm { namespace transformer { + + enum class PomdpFscApplicationMode { + STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL + }; + + PomdpFscApplicationMode parsePomdpFscApplicationMode(std::string const& mode) ; + + template class ApplyFiniteSchedulerToPomdp { @@ -16,12 +24,12 @@ namespace storm { } - std::shared_ptr> transform() const; + std::shared_ptr> transform(PomdpFscApplicationMode applicationMode = PomdpFscApplicationMode::SIMPLE_LINEAR) const; private: - std::unordered_map> getObservationChoiceWeights() const; + std::unordered_map> getObservationChoiceWeights(PomdpFscApplicationMode applicationMode ) const; storm::models::sparse::Pomdp const& pomdp; };