diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index 6aae4d493..634316e33 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -22,11 +22,15 @@ #include "storm-pomdp/analysis/UniqueObservationStates.h" #include "storm-pomdp/analysis/QualitativeAnalysis.h" #include "storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.h" +#include "storm-pomdp/analysis/FormulaInformation.h" #include "storm-pomdp/analysis/MemlessStrategySearchQualitative.h" #include "storm-pomdp/analysis/QualitativeStrategySearchNaive.h" + #include "storm/api/storm.h" +#include "storm/utility/Stopwatch.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/NotSupportedException.h" #include @@ -34,96 +38,184 @@ namespace storm { namespace pomdp { namespace cli { - - template - bool extractTargetAndSinkObservationSets(std::shared_ptr> const& pomdp, storm::logic::Formula const& subformula, std::set& 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); - } - } + /// Perform preprocessings based on the graph structure (if requested or necessary). Return true, if some preprocessing has been done + template + bool performPreprocessing(std::shared_ptr>& pomdp, storm::pomdp::analysis::FormulaInformation& formulaInfo, storm::logic::Formula const& formula) { + auto const& pomdpSettings = storm::settings::getModule(); + bool preprocessingPerformed = false; + if (pomdpSettings.isSelfloopReductionSet()) { + bool apply = formulaInfo.isNonNestedReachabilityProbability() && formulaInfo.maximize(); + apply = apply || (formulaInfo.isNonNestedExpectedRewardFormula() && formulaInfo.minimize()); + if (apply) { + 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); + preprocessingPerformed = true; } - } 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); - } + } + if (pomdpSettings.isQualitativeReductionSet() && formulaInfo.isNonNestedReachabilityProbability()) { + storm::analysis::QualitativeAnalysis qualitativeAnalysis(*pomdp); + STORM_PRINT_AND_LOG("Computing states with probability 0 ..."); + storm::storage::BitVector 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 ..."); + storm::storage::BitVector prob1States = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula()); + std::cout << prob1States << std::endl; + STORM_PRINT_AND_LOG(" done." << std::endl); + storm::pomdp::transformer::KnownProbabilityTransformer kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); + pomdp = kpt.transform(*pomdp, prob0States, prob1States); + // Update formulaInfo to changes from Preprocessing + formulaInfo.updateTargetStates(*pomdp, std::move(prob1States)); + formulaInfo.updateSinkStates(*pomdp, std::move(prob0States)); + preprocessingPerformed = true; + } else if (pomdpSettings.isGridApproximationSet()) { + // We still might need to apply the KnownProbabilityTransformer, to ensure that the grid approximation works properly + if (formulaInfo.isNonNestedReachabilityProbability()) { + if (!formulaInfo.getTargetStates().observationClosed || !formulaInfo.getSinkStates().states.empty()) { + // Make target states observation closed and/or sink states absorbing + storm::pomdp::transformer::KnownProbabilityTransformer kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); + auto prob0States = formulaInfo.getSinkStates().states; + auto prob1States = formulaInfo.getTargetStates().states; + pomdp = kpt.transform(*pomdp, prob0States, prob1States); + // Update formulaInfo to changes from Preprocessing + formulaInfo.updateTargetStates(*pomdp, std::move(prob1States)); + formulaInfo.updateSinkStates(*pomdp, std::move(prob0States)); + preprocessingPerformed = true; } + } else if (formulaInfo.isNonNestedExpectedRewardFormula()) { + STORM_LOG_THROW(formulaInfo.getTargetStates().observationClosed, storm::exceptions::NotSupportedException, "Target states of reward property are not observation closed. This case is not yet implemented."); + } + } + return preprocessingPerformed; + } + + template + bool performAnalysis(std::shared_ptr> const& pomdp, storm::pomdp::analysis::FormulaInformation const& formulaInfo) { + auto const& pomdpSettings = storm::settings::getModule(); + bool analysisPerformed = false; + if (pomdpSettings.isGridApproximationSet()) { + STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability() || formulaInfo.isNonNestedExpectedRewardFormula(), storm::exceptions::NotSupportedException, "Unsupported formula type for Grid approximation."); + STORM_LOG_THROW(!formulaInfo.getTargetStates().empty(), storm::exceptions::UnexpectedException, "The set of target states is empty."); + STORM_LOG_THROW(formulaInfo.getTargetStates().observationClosed, storm::exceptions::UnexpectedException, "Observations on target states also occur on non-target states. This is unexpected at this point."); + storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); + std::unique_ptr> result; + if (formulaInfo.isNonNestedReachabilityProbability()) { + result = checker.refineReachabilityProbability(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.minimize(), pomdpSettings.getGridResolution(), pomdpSettings.getExplorationThreshold()); + } else { + // TODO: no exploration threshold? + result = checker.computeReachabilityReward(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.minimize(), pomdpSettings.getGridResolution()); + } + ValueType overRes = result->overApproxValue; + ValueType 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) + } + analysisPerformed = true; + } + if (pomdpSettings.isMemlessSearchSet()) { + STORM_LOG_THROW(formulaInfo.isNonNestedReachabilityProbability(), storm::exceptions::NotSupportedException, "Qualitative memoryless scheduler search is not implemented for this property type."); + + // std::cout << std::endl; + // pomdp->writeDotToStream(std::cout); + // std::cout << std::endl; + // std::cout << std::endl; + storm::expressions::ExpressionManager expressionManager; + std::shared_ptr smtSolverFactory = std::make_shared(); + if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") { + storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.getTargetStates().states, formulaInfo.getSinkStates().states, smtSolverFactory); + memlessSearch.findNewStrategyForSomeState(5); + } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { + storm::pomdp::MemlessStrategySearchQualitative memlessSearch(*pomdp, formulaInfo.getTargetStates().observations, formulaInfo.getTargetStates().states, formulaInfo.getSinkStates().states, smtSolverFactory); + memlessSearch.findNewStrategyForSomeState(5); } else { - return false; + STORM_LOG_ERROR("This method is not implemented."); } - 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); - } + analysisPerformed = true; + } + return analysisPerformed; + } - } - } 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 + bool performTransformation(std::shared_ptr>& pomdp, storm::logic::Formula const& formula) { + auto const& pomdpSettings = storm::settings::getModule(); + bool transformationPerformed = false; + bool memoryUnfolded = false; + 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 memoryUnfolder(*pomdp, memory); + pomdp = memoryUnfolder.transform(); + STORM_PRINT_AND_LOG(" done." << std::endl); + pomdp->printModelInformationToStream(std::cout); + transformationPerformed = true; + memoryUnfolded = true; + } + + // 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); + 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); + transformationPerformed = true; + } + + 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); + } else { + STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP."); + pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); + } + pomdp->printModelInformationToStream(std::cout); + STORM_PRINT_AND_LOG(" done." << std::endl); + transformationPerformed = true; + } + + if (pomdpSettings.isExportToParametricSet()) { + STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC..."); + 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); + pmc->printModelInformationToStream(std::cout); + STORM_PRINT_AND_LOG("Simplifying pMC..."); + //if (generalSettings.isBisimulationSet()) { + pmc = storm::api::performBisimulationMinimization(pmc->template as>(),{formula.asSharedPointer()}, storm::storage::BisimulationType::Strong)->template as>(); + + //} + STORM_PRINT_AND_LOG(" done." << std::endl); + pmc->printModelInformationToStream(std::cout); + STORM_PRINT_AND_LOG("Exporting pMC..."); + storm::analysis::ConstraintCollector constraints(*pmc); + auto const& parameterSet = constraints.getVariables(); + std::vector parameters(parameterSet.begin(), parameterSet.end()); + std::vector 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); + transformationPerformed = true; + } + if (transformationPerformed && !memoryUnfolded) { + STORM_PRINT_AND_LOG("Implicitly assumed restriction to memoryless schedulers for at least one transformation." << std::endl); } - return validFormula; + return transformationPerformed; } template @@ -131,7 +223,11 @@ namespace storm { auto const& pomdpSettings = storm::settings::getModule(); auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib(symbolicInput, mpi); - STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp && model->isSparseModel(), storm::exceptions::WrongFormatException, "Expected a POMDP in sparse representation."); + if (!model) { + STORM_PRINT_AND_LOG("No input model given."); + return; + } + STORM_LOG_THROW(model->getType() == storm::models::ModelType::Pomdp && model->isSparseModel(), storm::exceptions::WrongFormatException, "Expected a POMDP in sparse representation."); std::shared_ptr> pomdp = model->template as>(); storm::transformer::MakePOMDPCanonic makeCanonic(*pomdp); @@ -151,207 +247,28 @@ namespace storm { } if (formula) { - if (formula->isProbabilityOperatorFormula()) { - storm::logic::ProbabilityOperatorFormula const &probFormula = formula->asProbabilityOperatorFormula(); - storm::logic::Formula const &subformula1 = probFormula.getSubformula(); - std::set 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 prob1States; - boost::optional 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 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_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 kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); - pomdp = kpt.transform(*pomdp, *prob0States, *prob1States); - } - if (pomdpSettings.isGridApproximationSet()) { - - storm::pomdp::modelchecker::ApproximatePOMDPModelchecker checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - auto overRes = storm::utility::one(); - auto underRes = storm::utility::zero(); - std::unique_ptr> 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 smtSolverFactory = std::make_shared(); - if (pomdpSettings.getMemlessSearchMethod() == "ccd16memless") { - storm::pomdp::QualitativeStrategySearchNaive memlessSearch(*pomdp, targetObservationSet, targetStates, badStates, smtSolverFactory); - memlessSearch.findNewStrategyForSomeState(5); - } else if (pomdpSettings.getMemlessSearchMethod() == "iterative") { - storm::pomdp::MemlessStrategySearchQualitative 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 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 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 checker = storm::pomdp::modelchecker::ApproximatePOMDPModelchecker(); - auto overRes = storm::utility::one(); - auto underRes = storm::utility::zero(); - std::unique_ptr> 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 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); - 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); + auto formulaInfo = storm::pomdp::analysis::getFormulaInformation(*pomdp, *formula); + STORM_LOG_THROW(!formulaInfo.isUnsupported(), storm::exceptions::InvalidPropertyException, "The formula '" << *formula << "' is not supported by storm-pomdp."); + + storm::utility::Stopwatch sw(true); + // Note that formulaInfo contains state-based information which potentially needs to be updated during preprocessing + if (performPreprocessing(pomdp, formulaInfo, *formula)) { + sw.stop(); + STORM_PRINT_AND_LOG("Time for graph-based POMDP (pre-)processing: " << sw << "s." << 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); - } else { - STORM_PRINT_AND_LOG("Transforming the POMDP to a binary POMDP."); - pomdp = storm::transformer::BinaryPomdpTransformer().transform(*pomdp, false); - } - pomdp->printModelInformationToStream(std::cout); - STORM_PRINT_AND_LOG(" done." << std::endl); + + sw.restart(); + if (performAnalysis(pomdp, formulaInfo)) { + sw.stop(); + STORM_PRINT_AND_LOG("Time for POMDP analysis: " << sw << "s." << std::endl); } - - - if (pomdpSettings.isExportToParametricSet()) { - STORM_PRINT_AND_LOG("Transforming memoryless POMDP to pMC..."); - 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); - pmc->printModelInformationToStream(std::cout); - STORM_PRINT_AND_LOG("Simplifying pMC..."); - //if (generalSettings.isBisimulationSet()) { - pmc = storm::api::performBisimulationMinimization(pmc->template as>(),{formula}, storm::storage::BisimulationType::Strong)->template as>(); - - //} - STORM_PRINT_AND_LOG(" done." << std::endl); - pmc->printModelInformationToStream(std::cout); - STORM_PRINT_AND_LOG("Exporting pMC..."); - storm::analysis::ConstraintCollector constraints(*pmc); - auto const& parameterSet = constraints.getVariables(); - std::vector parameters(parameterSet.begin(), parameterSet.end()); - std::vector 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); + + sw.restart(); + if (performTransformation(pomdp, *formula)) { + sw.stop(); + STORM_PRINT_AND_LOG("Time for POMDP transformation(s): " << sw << "s." << std::endl); } - } else { STORM_LOG_WARN("Nothing to be done. Did you forget to specify a formula?"); } @@ -360,6 +277,7 @@ namespace storm { template void processOptionsWithDdLib(storm::cli::SymbolicInput const& symbolicInput, storm::cli::ModelProcessingInformation const& mpi) { + STORM_LOG_ERROR_COND(mpi.buildValueType == mpi.verificationValueType, "Build value type differs from verification value type. Will ignore Verification value type."); switch (mpi.buildValueType) { case storm::cli::ModelProcessingInformation::ValueType::FinitePrecision: processOptionsWithValueTypeAndDdLib(symbolicInput, mpi); diff --git a/src/storm-pomdp/analysis/FormulaInformation.cpp b/src/storm-pomdp/analysis/FormulaInformation.cpp new file mode 100644 index 000000000..836abf881 --- /dev/null +++ b/src/storm-pomdp/analysis/FormulaInformation.cpp @@ -0,0 +1,177 @@ +#include "storm-pomdp/analysis/FormulaInformation.h" +#include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" +#include "storm/models/sparse/Pomdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidPropertyException.h" + +namespace storm { + namespace pomdp { + namespace analysis { + + bool FormulaInformation::StateSet::empty() const { + STORM_LOG_ASSERT(states.empty() == observations.empty(), "Inconsistent StateSet."); + return observations.empty(); + } + + FormulaInformation::FormulaInformation() : type(Type::Unsupported) { + // Intentionally left empty + } + + FormulaInformation::FormulaInformation(Type const& type, storm::solver::OptimizationDirection const& dir, boost::optional const& rewardModelName) : type(type), optimizationDirection(dir), rewardModelName(rewardModelName) { + STORM_LOG_ASSERT(!this->rewardModelName.is_initialized() || this->type == Type::NonNestedExpectedRewardFormula, "Got a reward model name for a non-reward formula."); + + } + + FormulaInformation::Type const& FormulaInformation::getType() const { + return type; + } + + bool FormulaInformation::isNonNestedReachabilityProbability() const { + return type == Type::NonNestedReachabilityProbability; + } + + bool FormulaInformation::isNonNestedExpectedRewardFormula() const { + return type == Type::NonNestedExpectedRewardFormula; + } + + bool FormulaInformation::isUnsupported() const { + return type == Type::Unsupported; + } + + typename FormulaInformation::StateSet const& FormulaInformation::getTargetStates() const { + STORM_LOG_ASSERT(this->type == Type::NonNestedExpectedRewardFormula || this->type == Type::NonNestedReachabilityProbability, "Target states requested for unexpected formula type."); + return targetStates.get(); + } + + typename FormulaInformation::StateSet const& FormulaInformation::getSinkStates() const { + STORM_LOG_ASSERT(this->type == Type::NonNestedReachabilityProbability, "Sink states requested for unexpected formula type."); + return sinkStates.get(); + } + + std::string const& FormulaInformation::getRewardModelName() const { + STORM_LOG_ASSERT(this->type == Type::NonNestedExpectedRewardFormula, "Reward model requested for unexpected formula type."); + return rewardModelName.get(); + } + + storm::solver::OptimizationDirection const& FormulaInformation::getOptimizationDirection() const { + return optimizationDirection; + } + + bool FormulaInformation::minimize() const { + return storm::solver::minimize(optimizationDirection); + } + + bool FormulaInformation::maximize() const { + return storm::solver::maximize(optimizationDirection); + } + + template + FormulaInformation::StateSet getStateSet(PomdpType const& pomdp, storm::storage::BitVector&& inputStates) { + FormulaInformation::StateSet result; + result.states = std::move(inputStates); + for (auto const& state : result.states) { + result.observations.insert(pomdp.getObservation(state)); + } + // check if this set is observation-closed, i.e., whether there is a state outside of this set with one of the observations collected above + result.observationClosed = true; + for (uint64_t state = result.states.getNextUnsetIndex(0); state < result.states.size(); state = result.states.getNextUnsetIndex(state + 1)) { + if (result.observations.count(pomdp.getObservation(state)) > 0) { + result.observationClosed = false; + break; + } + } + return result; + } + + template + void FormulaInformation::updateTargetStates(PomdpType const& pomdp, storm::storage::BitVector&& newTargetStates) { + STORM_LOG_ASSERT(this->type == Type::NonNestedExpectedRewardFormula || this->type == Type::NonNestedReachabilityProbability, "Target states updated for unexpected formula type."); + targetStates = getStateSet(pomdp, std::move(newTargetStates)); + } + + template + void FormulaInformation::updateSinkStates(PomdpType const& pomdp, storm::storage::BitVector&& newSinkStates) { + STORM_LOG_ASSERT(this->type == Type::NonNestedReachabilityProbability, "Sink states requested for unexpected formula type."); + sinkStates = getStateSet(pomdp, std::move(newSinkStates)); + } + + template + storm::storage::BitVector getStates(storm::logic::Formula const& propositionalFormula, bool formulaInverted, PomdpType const& pomdp) { + storm::modelchecker::SparsePropositionalModelChecker mc(pomdp); + auto checkResult = mc.check(propositionalFormula); + storm::storage::BitVector resultBitVector(checkResult->asExplicitQualitativeCheckResult().getTruthValuesVector()); + if (formulaInverted) { + resultBitVector.complement(); + } + return resultBitVector; + } + + template + FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::ProbabilityOperatorFormula const& formula) { + STORM_LOG_THROW(formula.hasOptimalityType(), storm::exceptions::InvalidPropertyException, "The property does not specify an optimization direction (min/max)"); + STORM_LOG_WARN_COND(!formula.hasBound(), "The probability threshold for the given property will be ignored."); + auto const& subformula = formula.getSubformula(); + std::shared_ptr targetStatesFormula, constraintsStatesFormula; + if (subformula.isEventuallyFormula()) { + targetStatesFormula = subformula.asEventuallyFormula().getSubformula().asSharedPointer(); + constraintsStatesFormula = storm::logic::Formula::getTrueFormula()->asSharedPointer(); + } else if (subformula.isUntilFormula()) { + storm::logic::UntilFormula const &untilFormula = subformula.asUntilFormula(); + targetStatesFormula = untilFormula.getRightSubformula().asSharedPointer(); + constraintsStatesFormula = untilFormula.getLeftSubformula().asSharedPointer(); + } + if (targetStatesFormula && targetStatesFormula->isInFragment(storm::logic::propositional()) && constraintsStatesFormula && constraintsStatesFormula->isInFragment(storm::logic::propositional())) { + FormulaInformation result(FormulaInformation::Type::NonNestedReachabilityProbability, formula.getOptimalityType()); + result.updateTargetStates(pomdp, getStates(*targetStatesFormula, false, pomdp)); + result.updateSinkStates(pomdp, getStates(*constraintsStatesFormula, true, pomdp)); + return result; + } + return FormulaInformation(); + } + + template + FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::RewardOperatorFormula const& formula) { + STORM_LOG_THROW(formula.hasOptimalityType(), storm::exceptions::InvalidPropertyException, "The property does not specify an optimization direction (min/max)"); + STORM_LOG_WARN_COND(formula.hasBound(), "The reward threshold for the given property will be ignored."); + std::string rewardModelName = ""; + if (formula.hasRewardModelName()) { + rewardModelName = formula.getRewardModelName(); + STORM_LOG_THROW(pomdp.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "Selected reward model with name '" << rewardModelName << "' does not exist."); + } else { + STORM_LOG_THROW(pomdp.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "Reward operator formula does not specify a reward model and the reward model is not unique."); + rewardModelName = pomdp.getUniqueRewardModelName(); + } + auto const& subformula = formula.getSubformula(); + std::shared_ptr targetStatesFormula; + if (subformula.isEventuallyFormula()) { + targetStatesFormula = subformula.asEventuallyFormula().getSubformula().asSharedPointer(); + } + if (targetStatesFormula && targetStatesFormula->isInFragment(storm::logic::propositional())) { + FormulaInformation result(FormulaInformation::Type::NonNestedReachabilityProbability, formula.getOptimalityType(), rewardModelName); + result.updateTargetStates(pomdp, getStates(*targetStatesFormula, false, pomdp)); + return result; + } + return FormulaInformation(); + } + + template + FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::Formula const& formula) { + if (formula.isProbabilityOperatorFormula()) { + return getFormulaInformation(pomdp, formula.asProbabilityOperatorFormula()); + } else if (formula.isRewardOperatorFormula()) { + return getFormulaInformation(pomdp, formula.asRewardOperatorFormula()); + } + return FormulaInformation(); + } + + template FormulaInformation getFormulaInformation>(storm::models::sparse::Pomdp const& pomdp, storm::logic::Formula const& formula); + template FormulaInformation getFormulaInformation>(storm::models::sparse::Pomdp const& pomdp, storm::logic::Formula const& formula); + + } + } +} diff --git a/src/storm-pomdp/analysis/FormulaInformation.h b/src/storm-pomdp/analysis/FormulaInformation.h new file mode 100644 index 000000000..10a92ab02 --- /dev/null +++ b/src/storm-pomdp/analysis/FormulaInformation.h @@ -0,0 +1,69 @@ +#pragma once + +#include +#include +#include + +#include "storm/storage/BitVector.h" +#include "storm/solver/OptimizationDirection.h" + +namespace storm { + + namespace logic { + class Formula; + } + + namespace pomdp { + namespace analysis { + class FormulaInformation { + public: + /// Characterizes a certain set of states + struct StateSet { + storm::storage::BitVector states; // The set of states + std::set observations; // The set of the observations that are assigned to at least one state of the set + bool observationClosed; // True iff this state set can be uniquely characterized by the observations + bool empty() const; + }; + + /// Possible supported formula types + enum class Type { + NonNestedReachabilityProbability, // e.g. 'Pmax=? [F "target"]' or 'Pmin=? [!"sink" U "target"]' + NonNestedExpectedRewardFormula, // e.g. 'Rmin=? [F x>0 ]' + Unsupported // The formula type is unsupported + }; + + FormulaInformation(); // Unsupported + FormulaInformation(Type const& type, storm::solver::OptimizationDirection const& dir, boost::optional const& rewardModelName = boost::none); + + Type const& getType() const; + bool isNonNestedReachabilityProbability() const; + bool isNonNestedExpectedRewardFormula() const; + bool isUnsupported() const; + StateSet const& getTargetStates() const; + StateSet const& getSinkStates() const; // Shall not be called for reward formulas + std::string const& getRewardModelName() const; // Shall not be called for probability formulas + storm::solver::OptimizationDirection const& getOptimizationDirection() const; + bool minimize() const; + bool maximize() const; + + template + void updateTargetStates(PomdpType const& pomdp, storm::storage::BitVector&& newTargetStates); + + template + void updateSinkStates(PomdpType const& pomdp, storm::storage::BitVector&& newSinkStates); + + private: + Type type; + storm::solver::OptimizationDirection optimizationDirection; + boost::optional targetStates; + boost::optional sinkStates; + boost::optional rewardModelName; + }; + + template + FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::Formula const& formula); + + + } + } +}