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

Cleaning up the POMDP CLI code a bit. Now supports switching to exact arithmetic with the --exact switch.

main
Tim Quatmann 6 years ago
parent
0d58ea5291
commit
5c748254a6
3 changed files with 435 additions and 384 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 67
      src/storm-pomdp-cli/settings/PomdpSettings.cpp
  2. 13
      src/storm-pomdp-cli/settings/PomdpSettings.h
  3. 737
      src/storm-pomdp-cli/storm-pomdp.cpp

67
src/storm-pomdp-cli/settings/PomdpSettings.cpp
View File

@ -0,0 +1,67 @@
#include "storm-pomdp-cli/settings/PomdpSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/CuddSettings.h"
#include "storm/settings/modules/SylvanSettings.h"
#include "storm/settings/modules/EigenEquationSolverSettings.h"
#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
#include "storm/settings/modules/NativeEquationSolverSettings.h"
#include "storm/settings/modules/EliminationSettings.h"
#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
#include "storm/settings/modules/GameSolverSettings.h"
#include "storm/settings/modules/BisimulationSettings.h"
#include "storm/settings/modules/GlpkSettings.h"
#include "storm/settings/modules/GurobiSettings.h"
#include "storm/settings/modules/Smt2SmtSolverSettings.h"
#include "storm/settings/modules/ExplorationSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/settings/modules/BuildSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/settings/modules/TopologicalEquationSolverSettings.h"
#include "storm/settings/modules/ModelCheckerSettings.h"
#include "storm/settings/modules/MultiplierSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/settings/modules/MultiObjectiveSettings.h"
#include "storm/settings/modules/HintSettings.h"
#include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
namespace storm {
namespace settings {
void initializePomdpSettings(std::string const& name, std::string const& executableName) {
storm::settings::mutableManager().setName(name, executableName);
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::IOSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::BuildSettings>();
storm::settings::addModule<storm::settings::modules::POMDPSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EliminationSettings>();
storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::GameSolverSettings>();
storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
storm::settings::addModule<storm::settings::modules::GlpkSettings>();
storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
storm::settings::addModule<storm::settings::modules::ResourceSettings>();
storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
storm::settings::addModule<storm::settings::modules::TopologicalEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
storm::settings::addModule<storm::settings::modules::HintSettings>();
}
}
}

13
src/storm-pomdp-cli/settings/PomdpSettings.h
View File

@ -0,0 +1,13 @@
#pragma once
#include <string>
namespace storm {
namespace settings {
/*!
* Initialize the settings manager.
*/
void initializePomdpSettings(std::string const& name, std::string const& executableName);
}
}

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

@ -3,35 +3,10 @@
#include "storm/utility/initialize.h" #include "storm/utility/initialize.h"
#include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/DebugSettings.h"
#include "storm/settings/modules/CuddSettings.h"
#include "storm/settings/modules/SylvanSettings.h"
#include "storm/settings/modules/EigenEquationSolverSettings.h"
#include "storm/settings/modules/GmmxxEquationSolverSettings.h"
#include "storm/settings/modules/NativeEquationSolverSettings.h"
#include "storm/settings/modules/EliminationSettings.h"
#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
#include "storm/settings/modules/GameSolverSettings.h"
#include "storm/settings/modules/BisimulationSettings.h"
#include "storm/settings/modules/GlpkSettings.h"
#include "storm/settings/modules/GurobiSettings.h"
#include "storm/settings/modules/Smt2SmtSolverSettings.h"
#include "storm/settings/modules/ExplorationSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/AbstractionSettings.h"
#include "storm/settings/modules/BuildSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/settings/modules/TopologicalEquationSolverSettings.h"
#include "storm/settings/modules/ModelCheckerSettings.h"
#include "storm/settings/modules/MultiplierSettings.h"
#include "storm/settings/modules/TransformationSettings.h"
#include "storm/settings/modules/MultiObjectiveSettings.h"
#include "storm/settings/modules/HintSettings.h"
#include "storm-pomdp-cli/settings/modules/POMDPSettings.h" #include "storm-pomdp-cli/settings/modules/POMDPSettings.h"
#include "storm-pomdp-cli/settings/PomdpSettings.h"
#include "storm/analysis/GraphConditions.h" #include "storm/analysis/GraphConditions.h"
#include "storm-cli-utilities/cli.h" #include "storm-cli-utilities/cli.h"
@ -51,129 +26,370 @@
#include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" #include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h"
#include "storm/api/storm.h" #include "storm/api/storm.h"
#include "storm/exceptions/UnexpectedException.h"
#include <typeinfo> #include <typeinfo>
/*!
* Initialize the settings manager.
*/
void initializeSettings() {
storm::settings::mutableManager().setName("Storm-POMDP", "storm-pomdp");
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
storm::settings::addModule<storm::settings::modules::IOSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
storm::settings::addModule<storm::settings::modules::BuildSettings>();
storm::settings::addModule<storm::settings::modules::POMDPSettings>();
storm::settings::addModule<storm::settings::modules::TransformationSettings>();
storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EigenEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EliminationSettings>();
storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::GameSolverSettings>();
storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
storm::settings::addModule<storm::settings::modules::GlpkSettings>();
storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
storm::settings::addModule<storm::settings::modules::ResourceSettings>();
storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
storm::settings::addModule<storm::settings::modules::TopologicalEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::ModelCheckerSettings>();
storm::settings::addModule<storm::settings::modules::MultiplierSettings>();
storm::settings::addModule<storm::settings::modules::HintSettings>();
}
namespace storm {
namespace pomdp {
namespace cli {
template<typename ValueType>
bool extractTargetAndSinkObservationSets(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& pomdp, storm::logic::Formula const& subformula, std::set<uint32_t>& targetObservationSet, storm::storage::BitVector& targetStates, storm::storage::BitVector& badStates) {
//TODO refactor (use model checker to determine the states, then transform into observations).
//TODO rename into appropriate function name.
bool validFormula = false;
if (subformula.isEventuallyFormula()) {
storm::logic::EventuallyFormula const &eventuallyFormula = subformula.asEventuallyFormula();
storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula();
if (subformula2.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
validFormula = true;
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
}
}
} else if (subformula2.isAtomicExpressionFormula()) {
validFormula = true;
std::stringstream stream;
stream << subformula2.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
}
}
}
} else if (subformula.isUntilFormula()) {
storm::logic::UntilFormula const &untilFormula = subformula.asUntilFormula();
storm::logic::Formula const &subformula1 = untilFormula.getLeftSubformula();
if (subformula1.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula1.asAtomicLabelFormula();
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (!labeling.getStateHasLabel(targetLabel, state)) {
badStates.set(state);
}
}
} else if (subformula1.isAtomicExpressionFormula()) {
std::stringstream stream;
stream << subformula1.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (!labeling.getStateHasLabel(targetLabel, state)) {
badStates.set(state);
}
}
} else {
return false;
}
storm::logic::Formula const &subformula2 = untilFormula.getRightSubformula();
if (subformula2.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
validFormula = true;
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
}
template<typename ValueType>
bool extractTargetAndSinkObservationSets(std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> const& pomdp, storm::logic::Formula const& subformula, std::set<uint32_t>& targetObservationSet, storm::storage::BitVector& targetStates, storm::storage::BitVector& badStates) {
//TODO refactor (use model checker to determine the states, then transform into observations).
//TODO rename into appropriate function name.
bool validFormula = false;
if (subformula.isEventuallyFormula()) {
storm::logic::EventuallyFormula const &eventuallyFormula = subformula.asEventuallyFormula();
storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula();
if (subformula2.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
validFormula = true;
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
}
}
} else if (subformula2.isAtomicExpressionFormula()) {
validFormula = true;
std::stringstream stream;
stream << subformula2.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
}
} else if (subformula2.isAtomicExpressionFormula()) {
validFormula = true;
std::stringstream stream;
stream << subformula2.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
}
}
}
} }
return validFormula;
} }
}
} else if (subformula.isUntilFormula()) {
storm::logic::UntilFormula const &untilFormula = subformula.asUntilFormula();
storm::logic::Formula const &subformula1 = untilFormula.getLeftSubformula();
if (subformula1.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula1.asAtomicLabelFormula();
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (!labeling.getStateHasLabel(targetLabel, state)) {
badStates.set(state);
template<typename ValueType, storm::dd::DdType DdType>
void processOptionsWithValueTypeAndDdLib(storm::cli::SymbolicInput const& symbolicInput, storm::cli::ModelProcessingInformation const& mpi) {
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<DdType, ValueType>(symbolicInput, mpi);
STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp && model->isSparseModel(), storm::exceptions::WrongFormatException, "Expected a POMDP in sparse representation.");
std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> pomdp = model->template as<storm::models::sparse::Pomdp<ValueType>>();
storm::transformer::MakePOMDPCanonic<ValueType> makeCanonic(*pomdp);
pomdp = makeCanonic.transform();
std::shared_ptr<storm::logic::Formula const> formula;
if (!symbolicInput.properties.empty()) {
formula = symbolicInput.properties.front().getRawFormula();
STORM_PRINT_AND_LOG("Analyzing property '" << *formula << "'" << std::endl);
STORM_LOG_WARN_COND(symbolicInput.properties.size() == 1, "There is currently no support for multiple properties. All other properties will be ignored.");
} }
}
} else if (subformula1.isAtomicExpressionFormula()) {
std::stringstream stream;
stream << subformula1.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (!labeling.getStateHasLabel(targetLabel, state)) {
badStates.set(state);
if (pomdpSettings.isAnalyzeUniqueObservationsSet()) {
STORM_PRINT_AND_LOG("Analyzing states with unique observation ..." << std::endl);
storm::analysis::UniqueObservationStates<ValueType> uniqueAnalysis(*pomdp);
std::cout << uniqueAnalysis.analyse() << std::endl;
} }
}
} else {
return false;
}
storm::logic::Formula const &subformula2 = untilFormula.getRightSubformula();
if (subformula2.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
validFormula = true;
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
if (formula) {
if (formula->isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula();
storm::logic::Formula const &subformula1 = probFormula.getSubformula();
std::set<uint32_t> targetObservationSet;
storm::storage::BitVector targetStates(pomdp->getNumberOfStates());
storm::storage::BitVector badStates(pomdp->getNumberOfStates());
bool validFormula = extractTargetAndSinkObservationSets(pomdp, subformula1, targetObservationSet, targetStates, badStates);
STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException,
"The formula is not supported by the grid approximation");
STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!");
boost::optional<storm::storage::BitVector> prob1States;
boost::optional<storm::storage::BitVector> prob0States;
if (pomdpSettings.isSelfloopReductionSet() && !storm::solver::minimize(formula->asProbabilityOperatorFormula().getOptimalityType())) {
STORM_PRINT_AND_LOG("Eliminating self-loop choices ...");
uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
storm::transformer::GlobalPOMDPSelfLoopEliminator<ValueType> selfLoopEliminator(*pomdp);
pomdp = selfLoopEliminator.transform();
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl);
}
if (pomdpSettings.isQualitativeReductionSet()) {
storm::analysis::QualitativeAnalysis<ValueType> qualitativeAnalysis(*pomdp);
STORM_PRINT_AND_LOG("Computing states with probability 0 ...");
prob0States = qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula());
std::cout << *prob0States << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG("Computing states with probability 1 ...");
prob1States = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
std::cout << *prob1States << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
//std::cout << "actual reduction not yet implemented..." << std::endl;
storm::pomdp::transformer::KnownProbabilityTransformer<ValueType> kpt = storm::pomdp::transformer::KnownProbabilityTransformer<ValueType>();
pomdp = kpt.transform(*pomdp, *prob0States, *prob1States);
}
if (pomdpSettings.isGridApproximationSet()) {
storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType>();
auto overRes = storm::utility::one<ValueType>();
auto underRes = storm::utility::zero<ValueType>();
std::unique_ptr<storm::pomdp::modelchecker::POMDPCheckResult<ValueType>> result;
result = checker.refineReachabilityProbability(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize,
pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold());
//result = checker.computeReachabilityProbabilityOTF(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold());
overRes = result->overApproxValue;
underRes = result->underApproxValue;
if (overRes != underRes) {
STORM_PRINT("Overapproximation Result: " << overRes << std::endl)
STORM_PRINT("Underapproximation Result: " << underRes << std::endl)
} else {
STORM_PRINT("Result: " << overRes << std::endl)
}
}
if (pomdpSettings.isMemlessSearchSet()) {
// std::cout << std::endl;
// pomdp->writeDotToStream(std::cout);
// std::cout << std::endl;
// std::cout << std::endl;
storm::expressions::ExpressionManager expressionManager;
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") {
storm::pomdp::QualitativeStrategySearchNaive<ValueType> memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory);
memlessSearch.findNewStrategyForSomeState(5);
} else if (pomdpSettings.getMemlessSearchMethod() == "iterative") {
storm::pomdp::MemlessStrategySearchQualitative<ValueType> memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory);
memlessSearch.findNewStrategyForSomeState(5);
} else {
STORM_LOG_ERROR("This method is not implemented.");
}
}
} 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<ValueType> selfLoopEliminator(*pomdp);
pomdp = selfLoopEliminator.transform();
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl);
}
if (pomdpSettings.isGridApproximationSet()) {
std::string rewardModelName;
storm::logic::RewardOperatorFormula const &rewFormula = formula->asRewardOperatorFormula();
if (rewFormula.hasRewardModelName()) {
rewardModelName = rewFormula.getRewardModelName();
}
storm::logic::Formula const &subformula1 = rewFormula.getSubformula();
std::set<uint32_t> targetObservationSet;
//TODO refactor
bool validFormula = false;
if (subformula1.isEventuallyFormula()) {
storm::logic::EventuallyFormula const &eventuallyFormula = subformula1.asEventuallyFormula();
storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula();
if (subformula2.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
validFormula = true;
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
}
}
} else if (subformula2.isAtomicExpressionFormula()) {
validFormula = true;
std::stringstream stream;
stream << subformula2.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
}
}
}
}
STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException,
"The formula is not supported by the grid approximation");
STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!");
storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<ValueType>();
auto overRes = storm::utility::one<ValueType>();
auto underRes = storm::utility::zero<ValueType>();
std::unique_ptr<storm::pomdp::modelchecker::POMDPCheckResult<ValueType>> result;
result = checker.computeReachabilityReward(*pomdp, targetObservationSet,
rewFormula.getOptimalityType() ==
storm::OptimizationDirection::Minimize,
pomdpSettings.getGridResolution());
overRes = result->overApproxValue;
underRes = result->underApproxValue;
}
}
if (pomdpSettings.getMemoryBound() > 1) {
STORM_PRINT_AND_LOG("Computing the unfolding for memory bound " << pomdpSettings.getMemoryBound() << " and memory pattern '" << storm::storage::toString(pomdpSettings.getMemoryPattern()) << "' ...");
storm::storage::PomdpMemory memory = storm::storage::PomdpMemoryBuilder().build(pomdpSettings.getMemoryPattern(), pomdpSettings.getMemoryBound());
std::cout << memory.toString() << std::endl;
storm::transformer::PomdpMemoryUnfolder<ValueType> memoryUnfolder(*pomdp, memory);
pomdp = memoryUnfolder.transform();
STORM_PRINT_AND_LOG(" done." << std::endl);
pomdp->printModelInformationToStream(std::cout);
} else {
STORM_PRINT_AND_LOG("Assumming memoryless schedulers." << std::endl;)
}
// From now on the pomdp is considered memoryless
if (pomdpSettings.isMecReductionSet()) {
STORM_PRINT_AND_LOG("Eliminating mec choices ...");
// Note: Elimination of mec choices only preserves memoryless schedulers.
uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
storm::transformer::GlobalPomdpMecChoiceEliminator<ValueType> mecChoiceEliminator(*pomdp);
pomdp = mecChoiceEliminator.transform(*formula);
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl);
pomdp->printModelInformationToStream(std::cout);
}
if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) {
if (pomdpSettings.isTransformSimpleSet()) {
STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP.");
pomdp = storm::transformer::BinaryPomdpTransformer<ValueType>().transform(*pomdp, true);
} else {
STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP.");
pomdp = storm::transformer::BinaryPomdpTransformer<ValueType>().transform(*pomdp, false);
}
pomdp->printModelInformationToStream(std::cout);
STORM_PRINT_AND_LOG(" done." << std::endl);
}
if (pomdpSettings.isExportToParametricSet()) {
STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC...");
storm::transformer::ApplyFiniteSchedulerToPomdp<ValueType> toPMCTransformer(*pomdp);
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->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>(),{formula}, 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("Exporting pMC...");
storm::analysis::ConstraintCollector<storm::RationalFunction> constraints(*pmc);
auto const& parameterSet = constraints.getVariables();
std::vector<storm::RationalFunctionVariable> parameters(parameterSet.begin(), parameterSet.end());
std::vector<std::string> parameterNames;
for (auto const& parameter : parameters) {
parameterNames.push_back(parameter.name());
}
storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames);
STORM_PRINT_AND_LOG(" done." << std::endl);
}
} else {
STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?");
} }
} }
} else if (subformula2.isAtomicExpressionFormula()) {
validFormula = true;
std::stringstream stream;
stream << subformula2.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
targetStates.set(state);
template <storm::dd::DdType DdType>
void processOptionsWithDdLib(storm::cli::SymbolicInput const& symbolicInput, storm::cli::ModelProcessingInformation const& mpi) {
switch (mpi.buildValueType) {
case storm::cli::ModelProcessingInformation::ValueType::FinitePrecision:
processOptionsWithValueTypeAndDdLib<double, DdType>(symbolicInput, mpi);
break;
case storm::cli::ModelProcessingInformation::ValueType::Exact:
STORM_LOG_THROW(DdType == storm::dd::DdType::Sylvan, storm::exceptions::UnexpectedException, "Exact arithmetic is only supported with Dd library Sylvan.");
processOptionsWithValueTypeAndDdLib<storm::RationalNumber, storm::dd::DdType::Sylvan>(symbolicInput, mpi);
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected ValueType for model building.");
} }
}
void processOptions() {
auto symbolicInput = storm::cli::parseSymbolicInput();
storm::cli::ModelProcessingInformation mpi;
std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput);
switch (mpi.ddType) {
case storm::dd::DdType::CUDD:
processOptionsWithDdLib<storm::dd::DdType::CUDD>(symbolicInput, mpi);
break;
case storm::dd::DdType::Sylvan:
processOptionsWithDdLib<storm::dd::DdType::Sylvan>(symbolicInput, mpi);
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Dd Type.");
}
} }
} }
} }
return validFormula;
} }
/*! /*!
@ -187,7 +403,7 @@ int main(const int argc, const char** argv) {
//try { //try {
storm::utility::setUp(); storm::utility::setUp();
storm::cli::printHeader("Storm-pomdp", argc, argv); storm::cli::printHeader("Storm-pomdp", argc, argv);
initializeSettings();
storm::settings::initializePomdpSettings("Storm-POMDP", "storm-pomdp");
bool optionsCorrect = storm::cli::parseOptions(argc, argv); bool optionsCorrect = storm::cli::parseOptions(argc, argv);
if (!optionsCorrect) { if (!optionsCorrect) {
@ -195,253 +411,8 @@ int main(const int argc, const char** argv) {
} }
storm::cli::setUrgentOptions(); storm::cli::setUrgentOptions();
typedef double VT;
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
auto const &general = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto const &debug = storm::settings::getModule<storm::settings::modules::DebugSettings>();
if (general.isVerboseSet()) {
storm::utility::setLogLevel(l3pp::LogLevel::INFO);
}
if (debug.isDebugSet()) {
storm::utility::setLogLevel(l3pp::LogLevel::DEBUG);
}
if (debug.isTraceSet()) {
storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
}
auto symbolicInput = storm::cli::parseSymbolicInput();
storm::cli::ModelProcessingInformation mpi;
std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput);
// We should not export here if we are going to do some processing first.
auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, VT>(symbolicInput, mpi);
STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP.");
std::shared_ptr<storm::models::sparse::Pomdp<VT>> pomdp = model->template as<storm::models::sparse::Pomdp<VT>>();
storm::transformer::MakePOMDPCanonic<VT> makeCanonic(*pomdp);
pomdp = makeCanonic.transform();
std::shared_ptr<storm::logic::Formula const> formula;
if (!symbolicInput.properties.empty()) {
formula = symbolicInput.properties.front().getRawFormula();
STORM_PRINT_AND_LOG("Analyzing property '" << *formula << "'" << std::endl);
STORM_LOG_WARN_COND(symbolicInput.properties.size() == 1, "There is currently no support for multiple properties. All other properties will be ignored.");
}
if (pomdpSettings.isAnalyzeUniqueObservationsSet()) {
STORM_PRINT_AND_LOG("Analyzing states with unique observation ..." << std::endl);
storm::analysis::UniqueObservationStates<VT> uniqueAnalysis(*pomdp);
std::cout << uniqueAnalysis.analyse() << std::endl;
}
if (formula) {
if (formula->isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula();
storm::logic::Formula const &subformula1 = probFormula.getSubformula();
std::set<uint32_t> targetObservationSet;
storm::storage::BitVector targetStates(pomdp->getNumberOfStates());
storm::storage::BitVector badStates(pomdp->getNumberOfStates());
bool validFormula = extractTargetAndSinkObservationSets(pomdp, subformula1, targetObservationSet, targetStates, badStates);
STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException,
"The formula is not supported by the grid approximation");
STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!");
boost::optional<storm::storage::BitVector> prob1States;
boost::optional<storm::storage::BitVector> prob0States;
if (pomdpSettings.isSelfloopReductionSet() && !storm::solver::minimize(formula->asProbabilityOperatorFormula().getOptimalityType())) {
STORM_PRINT_AND_LOG("Eliminating self-loop choices ...");
uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
storm::transformer::GlobalPOMDPSelfLoopEliminator<VT> selfLoopEliminator(*pomdp);
pomdp = selfLoopEliminator.transform();
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl);
}
if (pomdpSettings.isQualitativeReductionSet()) {
storm::analysis::QualitativeAnalysis<VT> qualitativeAnalysis(*pomdp);
STORM_PRINT_AND_LOG("Computing states with probability 0 ...");
prob0States = qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula());
std::cout << *prob0States << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG("Computing states with probability 1 ...");
prob1States = qualitativeAnalysis.analyseProb1(formula->asProbabilityOperatorFormula());
std::cout << *prob1States << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
//std::cout << "actual reduction not yet implemented..." << std::endl;
storm::pomdp::transformer::KnownProbabilityTransformer<VT> kpt = storm::pomdp::transformer::KnownProbabilityTransformer<double>();
pomdp = kpt.transform(*pomdp, *prob0States, *prob1States);
}
if (pomdpSettings.isGridApproximationSet()) {
storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<VT> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<double>();
auto overRes = storm::utility::one<VT>();
auto underRes = storm::utility::zero<VT>();
std::unique_ptr<storm::pomdp::modelchecker::POMDPCheckResult<VT>> result;
result = checker.refineReachabilityProbability(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize,
pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold());
//result = checker.computeReachabilityProbabilityOTF(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold());
overRes = result->overApproxValue;
underRes = result->underApproxValue;
if (overRes != underRes) {
STORM_PRINT("Overapproximation Result: " << overRes << std::endl)
STORM_PRINT("Underapproximation Result: " << underRes << std::endl)
} else {
STORM_PRINT("Result: " << overRes << std::endl)
}
}
if (pomdpSettings.isMemlessSearchSet()) {
// std::cout << std::endl;
// pomdp->writeDotToStream(std::cout);
// std::cout << std::endl;
// std::cout << std::endl;
storm::expressions::ExpressionManager expressionManager;
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") {
storm::pomdp::QualitativeStrategySearchNaive<VT> memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory);
memlessSearch.findNewStrategyForSomeState(5);
} else if (pomdpSettings.getMemlessSearchMethod() == "iterative") {
storm::pomdp::MemlessStrategySearchQualitative<VT> memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory);
memlessSearch.findNewStrategyForSomeState(5);
} else {
STORM_LOG_ERROR("This method is not implemented.");
}
}
} 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<VT> selfLoopEliminator(*pomdp);
pomdp = selfLoopEliminator.transform();
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl);
}
if (pomdpSettings.isGridApproximationSet()) {
std::string rewardModelName;
storm::logic::RewardOperatorFormula const &rewFormula = formula->asRewardOperatorFormula();
if (rewFormula.hasRewardModelName()) {
rewardModelName = rewFormula.getRewardModelName();
}
storm::logic::Formula const &subformula1 = rewFormula.getSubformula();
std::set<uint32_t> targetObservationSet;
//TODO refactor
bool validFormula = false;
if (subformula1.isEventuallyFormula()) {
storm::logic::EventuallyFormula const &eventuallyFormula = subformula1.asEventuallyFormula();
storm::logic::Formula const &subformula2 = eventuallyFormula.getSubformula();
if (subformula2.isAtomicLabelFormula()) {
storm::logic::AtomicLabelFormula const &alFormula = subformula2.asAtomicLabelFormula();
validFormula = true;
std::string targetLabel = alFormula.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
}
}
} else if (subformula2.isAtomicExpressionFormula()) {
validFormula = true;
std::stringstream stream;
stream << subformula2.asAtomicExpressionFormula().getExpression();
storm::logic::AtomicLabelFormula formula3 = storm::logic::AtomicLabelFormula(stream.str());
std::string targetLabel = formula3.getLabel();
auto labeling = pomdp->getStateLabeling();
for (size_t state = 0; state < pomdp->getNumberOfStates(); ++state) {
if (labeling.getStateHasLabel(targetLabel, state)) {
targetObservationSet.insert(pomdp->getObservation(state));
}
}
}
}
STORM_LOG_THROW(validFormula, storm::exceptions::InvalidPropertyException,
"The formula is not supported by the grid approximation");
STORM_LOG_ASSERT(!targetObservationSet.empty(), "The set of target observations is empty!");
storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<VT> checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker<double>();
auto overRes = storm::utility::one<VT>();
auto underRes = storm::utility::zero<VT>();
std::unique_ptr<storm::pomdp::modelchecker::POMDPCheckResult<VT>> result;
result = checker.computeReachabilityReward(*pomdp, targetObservationSet,
rewFormula.getOptimalityType() ==
storm::OptimizationDirection::Minimize,
pomdpSettings.getGridResolution());
overRes = result->overApproxValue;
underRes = result->underApproxValue;
}
}
if (pomdpSettings.getMemoryBound() > 1) {
STORM_PRINT_AND_LOG("Computing the unfolding for memory bound " << pomdpSettings.getMemoryBound() << " and memory pattern '" << storm::storage::toString(pomdpSettings.getMemoryPattern()) << "' ...");
storm::storage::PomdpMemory memory = storm::storage::PomdpMemoryBuilder().build(pomdpSettings.getMemoryPattern(), pomdpSettings.getMemoryBound());
std::cout << memory.toString() << std::endl;
storm::transformer::PomdpMemoryUnfolder<VT> memoryUnfolder(*pomdp, memory);
pomdp = memoryUnfolder.transform();
STORM_PRINT_AND_LOG(" done." << std::endl);
pomdp->printModelInformationToStream(std::cout);
} else {
STORM_PRINT_AND_LOG("Assumming memoryless schedulers." << std::endl;)
}
// From now on the pomdp is considered memoryless
if (pomdpSettings.isMecReductionSet()) {
STORM_PRINT_AND_LOG("Eliminating mec choices ...");
// Note: Elimination of mec choices only preserves memoryless schedulers.
uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
storm::transformer::GlobalPomdpMecChoiceEliminator<VT> mecChoiceEliminator(*pomdp);
pomdp = mecChoiceEliminator.transform(*formula);
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through MEC choice elimination." << std::endl);
pomdp->printModelInformationToStream(std::cout);
}
if (pomdpSettings.isTransformBinarySet() || pomdpSettings.isTransformSimpleSet()) {
if (pomdpSettings.isTransformSimpleSet()) {
STORM_PRINT_AND_LOG("Transforming the POMDP to a simple POMDP.");
pomdp = storm::transformer::BinaryPomdpTransformer<VT>().transform(*pomdp, true);
} else {
STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP.");
pomdp = storm::transformer::BinaryPomdpTransformer<VT>().transform(*pomdp, false);
}
pomdp->printModelInformationToStream(std::cout);
STORM_PRINT_AND_LOG(" done." << std::endl);
}
if (pomdpSettings.isExportToParametricSet()) {
STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC...");
storm::transformer::ApplyFiniteSchedulerToPomdp<VT> toPMCTransformer(*pomdp);
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}, storm::storage::BisimulationType::Strong)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
//}
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();
std::vector<storm::RationalFunctionVariable> parameters(parameterSet.begin(), parameterSet.end());
std::vector<std::string> parameterNames;
for (auto const& parameter : parameters) {
parameterNames.push_back(parameter.name());
}
storm::api::exportSparseModelAsDrn(pmc, pomdpSettings.getExportToParametricFilename(), parameterNames);
STORM_PRINT_AND_LOG(" done." << std::endl);
}
} else {
STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?");
}
// Invoke storm-pomdp with obtained settings
storm::pomdp::cli::processOptions();
// All operations have now been performed, so we clean up everything and terminate. // All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp(); storm::utility::cleanUp();

Write Preview
Loading…
Cancel
Save