From f6d9a6ac021ca55004aaf5627b699445a5e9f19a Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 11 Oct 2019 11:02:35 +0200 Subject: [PATCH] Changed datatype used in POMDP analysis from RationalNumber to double for better comparision of approximation speeds with PRISM --- src/storm-pomdp-cli/storm-pomdp.cpp | 56 +++++++++++-------- .../analysis/QualitativeAnalysis.cpp | 4 +- .../analysis/UniqueObservationStates.cpp | 4 +- .../ApplyFiniteSchedulerToPomdp.cpp | 3 + .../transformer/BinaryPomdpTransformer.cpp | 2 + .../GlobalPOMDPSelfLoopEliminator.cpp | 3 + .../GlobalPomdpMecChoiceEliminator.cpp | 3 + .../transformer/PomdpMemoryUnfolder.cpp | 3 + 8 files changed, 54 insertions(+), 24 deletions(-) diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 18f446d20..e6be182a3 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -111,9 +111,9 @@ int main(const int argc, const char** argv) { storm::cli::SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); // We should not export here if we are going to do some processing first. - auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, engine); + auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, engine); STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP."); - std::shared_ptr> pomdp = model->template as>(); + std::shared_ptr> pomdp = model->template as>(); std::shared_ptr formula; if (!symbolicInput.properties.empty()) { @@ -121,24 +121,24 @@ int main(const int argc, const char** argv) { 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 uniqueAnalysis(*pomdp); + storm::analysis::UniqueObservationStates uniqueAnalysis(*pomdp); std::cout << uniqueAnalysis.analyse() << std::endl; } - + if (formula) { if (formula->isProbabilityOperatorFormula()) { 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 selfLoopEliminator(*pomdp); + 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.isQualitativeReductionSet()) { - storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); + storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); std::cout << qualitativeAnalysis.analyseProb0(formula->asProbabilityOperatorFormula()) << std::endl; STORM_PRINT_AND_LOG(" done." << std::endl); @@ -167,19 +167,31 @@ int main(const int argc, const char** argv) { 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::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - storm::RationalNumber overRes = storm::utility::one(); - storm::RationalNumber underRes = storm::utility::zero(); - std::unique_ptr> result; + storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); + double overRes = storm::utility::one(); + double underRes = storm::utility::zero(); + std::unique_ptr> result; result = checker.computeReachabilityProbability(*pomdp, targetObservationSet, probFormula.getOptimalityType() == storm::OptimizationDirection::Minimize, - pomdpSettings.getGridResolution() + gridIncrease); + pomdpSettings.getGridResolution()); overRes = result->OverapproximationValue; underRes = result->UnderapproximationValue; } @@ -187,7 +199,7 @@ int main(const int argc, const char** argv) { 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); + storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); pomdp = selfLoopEliminator.transform(); STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl); } @@ -196,43 +208,43 @@ int main(const int argc, const char** argv) { 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 memoryUnfolder(*pomdp, memory); + storm::transformer::PomdpMemoryUnfolder 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 mecChoiceEliminator(*pomdp); + storm::transformer::GlobalPomdpMecChoiceEliminator 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().transform(*pomdp, true); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, true); } else { STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP."); - pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); + pomdp = storm::transformer::BinaryPomdpTransformer().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 toPMCTransformer(*pomdp); + storm::transformer::ApplyFiniteSchedulerToPomdp toPMCTransformer(*pomdp); std::string transformMode = pomdpSettings.getFscApplicationTypeString(); auto pmc = toPMCTransformer.transform(storm::transformer::parsePomdpFscApplicationMode(transformMode)); STORM_PRINT_AND_LOG(" done." << std::endl); diff --git a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp index 09e2cf496..9bcec71a5 100644 --- a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp +++ b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp @@ -160,6 +160,8 @@ namespace storm { template class QualitativeAnalysis; - + + template + class QualitativeAnalysis; } } \ No newline at end of file diff --git a/src/storm-pomdp/analysis/UniqueObservationStates.cpp b/src/storm-pomdp/analysis/UniqueObservationStates.cpp index 5fc8e1426..e71ef162d 100644 --- a/src/storm-pomdp/analysis/UniqueObservationStates.cpp +++ b/src/storm-pomdp/analysis/UniqueObservationStates.cpp @@ -30,6 +30,8 @@ namespace storm { } template class UniqueObservationStates; - + + template + class UniqueObservationStates; } } \ No newline at end of file diff --git a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp index 8f432bb2e..8f276c1fb 100644 --- a/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp +++ b/src/storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.cpp @@ -127,5 +127,8 @@ namespace storm { } template class ApplyFiniteSchedulerToPomdp; + + template + class ApplyFiniteSchedulerToPomdp; } } \ No newline at end of file diff --git a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp index 170f6e863..b076ca36d 100644 --- a/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp +++ b/src/storm-pomdp/transformer/BinaryPomdpTransformer.cpp @@ -162,5 +162,7 @@ namespace storm { template class BinaryPomdpTransformer; + template + class BinaryPomdpTransformer; } } \ No newline at end of file diff --git a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp index c61ce5b0f..54ad9631c 100644 --- a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp +++ b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp @@ -77,5 +77,8 @@ namespace storm { } template class GlobalPOMDPSelfLoopEliminator; + + template + class GlobalPOMDPSelfLoopEliminator; } } diff --git a/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp b/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp index d01342a7c..853b70952 100644 --- a/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp +++ b/src/storm-pomdp/transformer/GlobalPomdpMecChoiceEliminator.cpp @@ -225,5 +225,8 @@ namespace storm { template class GlobalPomdpMecChoiceEliminator; + + template + class GlobalPomdpMecChoiceEliminator; } } \ No newline at end of file diff --git a/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp b/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp index 827493efc..c23c828ab 100644 --- a/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp +++ b/src/storm-pomdp/transformer/PomdpMemoryUnfolder.cpp @@ -185,5 +185,8 @@ namespace storm { } template class PomdpMemoryUnfolder; + + template + class PomdpMemoryUnfolder; } } \ No newline at end of file