sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

options how to transform fsc

tempestpy_adaptions
Sebastian Junges 7 years ago
parent
94a7cd1048
commit
fda3445746
5 changed files with 69 additions and 17 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 13
      src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
  2. 1
      src/storm-pomdp-cli/settings/modules/POMDPSettings.h
  3. 25
      src/storm-pomdp-cli/storm-pomdp.cpp
  4. 35
      src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp
  5. 12
      src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h

13
src/storm-pomdp-cli/settings/modules/POMDPSettings.cpp
View File

@ -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<std::string> 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();
}

1
src/storm-pomdp-cli/settings/modules/POMDPSettings.h
View File

@ -29,6 +29,7 @@ namespace storm {
bool isAnalyzeUniqueObservationsSet() const;
bool isMecReductionSet() const;
bool isSelfloopReductionSet() const;
std::string getFscApplicationTypeString() const;
uint64_t getMemoryBound() const;

25
src/storm-pomdp-cli/storm-pomdp.cpp
View File

@ -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::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>(false);
storm::settings::addModule<storm::settings::modules::CuddSettings>();
storm::settings::addModule<storm::settings::modules::SylvanSettings>();
//storm::settings::addModule<storm::settings::modules::CuddSettings>();
// storm::settings::addModule<storm::settings::modules::SylvanSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
@ -95,6 +96,8 @@ int main(const int argc, const char** argv) {
auto const& coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto const& bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
// 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<storm::RationalNumber> 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<storm::RationalNumber> 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<storm::RationalFunction>(pmc->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(),{formula})->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
//}
STORM_PRINT_AND_LOG(" done." << std::endl);
pmc->printModelInformationToStream(std::cout);
STORM_PRINT_AND_LOG("Exporting pMC...");

35
src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp
View File

@ -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<RawPolynomialCache>()) {
@ -20,19 +33,29 @@ namespace storm {
template<typename ValueType>
std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> ApplyFiniteSchedulerToPomdp<ValueType>::getObservationChoiceWeights() const {
std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> ApplyFiniteSchedulerToPomdp<ValueType>::getObservationChoiceWeights(PomdpFscApplicationMode applicationMode ) const {
std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> 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<storm::RationalFunction> weights;
storm::RationalFunction collected = storm::utility::one<storm::RationalFunction>();
storm::RationalFunction lastWeight = storm::utility::one<storm::RationalFunction>();
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<storm::RationalFunction>() - var;
} else if (applicationMode == PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) {
weights.push_back(collected * (storm::utility::one<storm::RationalFunction>() - 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<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> ApplyFiniteSchedulerToPomdp<ValueType>::transform() const {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> ApplyFiniteSchedulerToPomdp<ValueType>::transform(PomdpFscApplicationMode applicationMode ) const {
storm::storage::sparse::ModelComponents<storm::RationalFunction> modelComponents;
uint64_t nrStates = pomdp.getNumberOfStates();
std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> observationChoiceWeights = getObservationChoiceWeights();
std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> observationChoiceWeights = getObservationChoiceWeights(applicationMode);
storm::storage::SparseMatrixBuilder<storm::RationalFunction> smb(nrStates, nrStates, 0, true);
for (uint64_t state = 0; state < nrStates; ++state) {
@ -94,7 +117,7 @@ namespace storm {
}
}
storm::models::sparse::StandardRewardModel<storm::RationalFunction> rewardModel(std::move(stateRewards));
modelComponents.rewardModels.emplace(pomdpRewardModel.first, std::move(rewardModel));
modelComponents.rewardModels.emplace(pomdpRewardModel.first, std::move(rewardModel)) ;
}
modelComponents.stateLabeling = pomdp.getStateLabeling();

12
src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h
View File

@ -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<typename ValueType>
class ApplyFiniteSchedulerToPomdp {
@ -16,12 +24,12 @@ namespace storm {
}
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> transform() const;
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> transform(PomdpFscApplicationMode applicationMode = PomdpFscApplicationMode::SIMPLE_LINEAR) const;
private:
std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> getObservationChoiceWeights() const;
std::unordered_map<uint32_t, std::vector<storm::RationalFunction>> getObservationChoiceWeights(PomdpFscApplicationMode applicationMode ) const;
storm::models::sparse::Pomdp<ValueType> const& pomdp;
};

Write Preview
Loading…
Cancel
Save