diff --git a/resources/examples/testfiles/pomdp/maze2.prism b/resources/examples/testfiles/pomdp/maze2.prism
index e1f60ae07..19771c972 100644
--- a/resources/examples/testfiles/pomdp/maze2.prism
+++ b/resources/examples/testfiles/pomdp/maze2.prism
@@ -135,5 +135,5 @@ endrewards
// target observation
label "goal" = o=7;
-
+label "bad" = o=6;
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 5aa2d6af9..76f553091 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -501,7 +501,7 @@ namespace storm {
verifyPropertiesAtSamplePoints<storm::modelchecker::SparseDtmcInstantiationModelChecker, storm::models::sparse::Dtmc<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Dtmc<ValueType>>(), input, samples);
} else if (model->isOfType(storm::models::ModelType::Ctmc)) {
verifyPropertiesAtSamplePoints<storm::modelchecker::SparseCtmcInstantiationModelChecker, storm::models::sparse::Ctmc<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), input, samples);
- } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
+ } else if (model->isOfType(storm::models::ModelType::Mdp)) {
verifyPropertiesAtSamplePoints<storm::modelchecker::SparseMdpInstantiationModelChecker, storm::models::sparse::Mdp<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Mdp<ValueType>>(), input, samples);
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs.");
diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
index ddeb32cb3..c8cd0498e 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
@@ -15,7 +15,7 @@ namespace storm {
namespace modelchecker {
template <typename SparseModelType, typename ConstantType>
- SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
+ SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel, bool produceScheduler) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel), produceScheduler(produceScheduler) {
//Intentionally left empty
}
@@ -40,9 +40,11 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
-
- this->currentCheckTask->setProduceSchedulers(true);
-
+
+ if (produceScheduler) {
+ this->currentCheckTask->setProduceSchedulers(true);
+ }
+
if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
}
@@ -82,16 +84,21 @@ namespace storm {
// For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
result = modelChecker.check(env, *this->currentCheckTask);
- storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
- hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));
+ if (produceScheduler) {
+ storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+ hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const &>(scheduler));
+ }
} else {
auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
- storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
- hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
+ if (produceScheduler) {
+ storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
+ hint.setSchedulerHint(
+ std::move(dynamic_cast<storm::storage::Scheduler<ConstantType> &>(scheduler)));
+ }
}
return result;
diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h
index ff6a6735e..4be0812b1 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h
+++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h
@@ -18,7 +18,7 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
class SparseMdpInstantiationModelChecker : public SparseInstantiationModelChecker<SparseModelType, ConstantType> {
public:
- SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel);
+ SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel, bool produceScheduler = true);
virtual std::unique_ptr<CheckResult> check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
@@ -29,6 +29,7 @@ namespace storm {
std::unique_ptr<CheckResult> checkBoundedUntilFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker);
storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Mdp<ConstantType>> modelInstantiator;
+ bool produceScheduler;
};
}
}
diff --git a/src/storm-pomdp-cli/settings/PomdpSettings.cpp b/src/storm-pomdp-cli/settings/PomdpSettings.cpp
index f529d8073..a8def4e9e 100644
--- a/src/storm-pomdp-cli/settings/PomdpSettings.cpp
+++ b/src/storm-pomdp-cli/settings/PomdpSettings.cpp
@@ -47,6 +47,7 @@ namespace storm {
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::SylvanSettings>();
storm::settings::addModule<storm::settings::modules::POMDPSettings>();
storm::settings::addModule<storm::settings::modules::QualitativePOMDPAnalysisSettings>();
diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp
index 1d6ff6d49..112ecff25 100644
--- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp
+++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp
@@ -23,6 +23,7 @@ namespace storm {
const std::string printWinningRegionOption = "printwinningregion";
const std::string exportWinningRegionOption = "exportwinningregion";
const std::string preventGraphPreprocessing = "nographprocessing";
+ const std::string beliefSupportMCOption = "belsupmc";
const std::string memlessSearchOption = "memlesssearch";
std::vector<std::string> memlessSearchMethods = {"one-shot", "iterative"};
@@ -33,6 +34,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, exportSATCallsOption, false, "Export the SAT calls?.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "The name of the path to which to write the models.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadHorizonOption, false, "In reachability in combination with a discrete ranking function, a lookahead is necessary.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("bound", "The lookahead. Use 0 for the number of states.").setDefaultValueUnsignedInteger(0).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, onlyDeterministicOption, false, "Search only for deterministic schedulers").setIsAdvanced().build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, beliefSupportMCOption, false, "Create a symbolic description of the belief-support MDP to use for analysis purposes").build());
this->addOption(storm::settings::OptionBuilder(moduleName, winningRegionOption, false, "Search for the winning region").build());
this->addOption(storm::settings::OptionBuilder(moduleName, lookaheadTypeOption, false, "What type to use for the ranking function").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type.").setDefaultValueString("real").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"bool", "int", "real"})).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, validationLevel, true, "Validate algorithm during runtime (for debugging)").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("level", "how regular to apply this validation. Use 0 for never, 1 for the end, and >=2 within computation steps.").setDefaultValueUnsignedInteger(0).build()).build());
@@ -66,6 +68,10 @@ namespace storm {
return this->getOption(winningRegionOption).getHasOptionBeenSet();
}
+ bool QualitativePOMDPAnalysisSettings::isComputeOnBeliefSupportSet() const {
+ return this->getOption(beliefSupportMCOption).getHasOptionBeenSet();
+ }
+
bool QualitativePOMDPAnalysisSettings::validateIntermediateSteps() const {
return this->getOption(validationLevel).getArgumentByName("level").getValueAsUnsignedInteger() >= 2;
}
diff --git a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h
index cebb356e3..51477c771 100644
--- a/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h
+++ b/src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h
@@ -29,6 +29,7 @@ namespace storm {
bool validateIntermediateSteps() const;
bool validateFinalResult() const;
bool computeExpensiveStats() const;
+ bool isComputeOnBeliefSupportSet() const;
bool isPrintWinningRegionSet() const;
bool isExportWinningRegionSet() const;
std::string exportWinningRegionPath() const;
diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index 7cc999ec9..08b64a406 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -26,6 +26,7 @@
#include "storm-pomdp/analysis/FormulaInformation.h"
#include "storm-pomdp/analysis/IterativePolicySearch.h"
#include "storm-pomdp/analysis/OneShotPolicySearch.h"
+#include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h"
#include "storm/api/storm.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@@ -154,69 +155,98 @@ namespace storm {
formula.asProbabilityOperatorFormula());
pomdp.getTransitionMatrix().makeRowGroupsAbsorbing(surelyNotAlmostSurelyReachTarget);
storm::storage::BitVector targetStates = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula());
-
- storm::expressions::ExpressionManager expressionManager;
- std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
- storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings();
- uint64_t lookahead = qualSettings.getLookahead();
- if (lookahead == 0) {
- lookahead = pomdp.getNumberOfStates();
- }
- if (qualSettings.getMemlessSearchMethod() == "one-shot") {
- storm::pomdp::OneShotPolicySearch<ValueType> memlessSearch(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory);
- if (qualSettings.isWinningRegionSet()) {
- STORM_LOG_ERROR("Computing winning regions is not supported by ccd-memless.");
- } else {
- memlessSearch.analyzeForInitialStates(lookahead);
- }
- } else if (qualSettings.getMemlessSearchMethod() == "iterative") {
- storm::pomdp::IterativePolicySearch<ValueType> search(pomdp, targetStates, surelyNotAlmostSurelyReachTarget, smtSolverFactory, options);
- if (qualSettings.isWinningRegionSet()) {
- search.computeWinningRegion(lookahead);
- } else {
- search.analyzeForInitialStates(lookahead);
+ bool computedSomething = false;
+ if (qualSettings.isMemlessSearchSet()) {
+ computedSomething = true;
+ storm::expressions::ExpressionManager expressionManager;
+ std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory = std::make_shared<storm::utility::solver::Z3SmtSolverFactory>();
+ storm::pomdp::MemlessSearchOptions options = fillMemlessSearchOptionsFromSettings();
+ uint64_t lookahead = qualSettings.getLookahead();
+ if (lookahead == 0) {
+ lookahead = pomdp.getNumberOfStates();
}
+ if (qualSettings.getMemlessSearchMethod() == "one-shot") {
+ storm::pomdp::OneShotPolicySearch<ValueType> memlessSearch(pomdp, targetStates,
+ surelyNotAlmostSurelyReachTarget,
+ smtSolverFactory);
+ if (qualSettings.isWinningRegionSet()) {
+ STORM_LOG_ERROR("Computing winning regions is not supported by the one-shot method.");
+ } else {
+ memlessSearch.analyzeForInitialStates(lookahead);
+ }
+ } else if (qualSettings.getMemlessSearchMethod() == "iterative") {
+ storm::pomdp::IterativePolicySearch<ValueType> search(pomdp, targetStates,
+ surelyNotAlmostSurelyReachTarget,
+ smtSolverFactory, options);
+ if (qualSettings.isWinningRegionSet()) {
+ search.computeWinningRegion(lookahead);
+ } else {
+ search.analyzeForInitialStates(lookahead);
+ }
- if (qualSettings.isPrintWinningRegionSet()) {
- search.getLastWinningRegion().print();
- std::cout << std::endl;
- }
- if (qualSettings.isExportWinningRegionSet()) {
- std::size_t hash = pomdp.hash();
- search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath(), "model hash: " + std::to_string(hash));
- }
+ if (qualSettings.isPrintWinningRegionSet()) {
+ search.getLastWinningRegion().print();
+ std::cout << std::endl;
+ }
+ if (qualSettings.isExportWinningRegionSet()) {
+ std::size_t hash = pomdp.hash();
+ search.getLastWinningRegion().storeToFile(qualSettings.exportWinningRegionPath(),
+ "model hash: " + std::to_string(hash));
+ }
- search.finalizeStatistics();
- if(pomdp.getInitialStates().getNumberOfSetBits() == 1) {
- uint64_t initialState = pomdp.getInitialStates().getNextSetIndex(0);
- uint64_t initialObservation = pomdp.getObservation(initialState);
- // TODO this is inefficient.
- uint64_t offset = 0;
- for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
- if (state == initialState) {
- break;
+ search.finalizeStatistics();
+ if (pomdp.getInitialStates().getNumberOfSetBits() == 1) {
+ uint64_t initialState = pomdp.getInitialStates().getNextSetIndex(0);
+ uint64_t initialObservation = pomdp.getObservation(initialState);
+ // TODO this is inefficient.
+ uint64_t offset = 0;
+ for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
+ if (state == initialState) {
+ break;
+ }
+ if (pomdp.getObservation(state) == initialObservation) {
+ ++offset;
+ }
}
- if (pomdp.getObservation(state) == initialObservation) {
- ++offset;
+
+ if (search.getLastWinningRegion().isWinning(initialObservation,
+ offset)) {
+ STORM_PRINT_AND_LOG("Initial state is safe!"
+ << std::endl);
+ } else {
+ STORM_PRINT_AND_LOG("Initial state may not be safe."
+ << std::endl);
}
+ } else {
+ STORM_LOG_WARN("Output for multiple initial states is incomplete");
+ }
+
+ if (coreSettings.isShowStatisticsSet()) {
+ STORM_PRINT_AND_LOG("#STATS Number of belief support states: "
+ << search.getLastWinningRegion().beliefSupportStates() << std::endl);
+ if (qualSettings.computeExpensiveStats()) {
+ auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs();
+ STORM_PRINT_AND_LOG(
+ "#STATS Number of winning belief support states: [" << wbss.first << "," << wbss.second
+ << "]");
+ }
+ search.getStatistics().print();
}
- STORM_PRINT_AND_LOG("Initial state is safe: " << search.getLastWinningRegion().isWinning(initialObservation, offset));
+
} else {
- STORM_LOG_WARN("Output for multiple initial states is incomplete");
- }
- std::cout << "Number of belief support states: " << search.getLastWinningRegion().beliefSupportStates() << std::endl;
- if (coreSettings.isShowStatisticsSet() && qualSettings.computeExpensiveStats()) {
- auto wbss = search.getLastWinningRegion().computeNrWinningBeliefs();
- STORM_PRINT_AND_LOG( "Number of winning belief support states: [" << wbss.first << "," << wbss.second
- << "]");
- }
- if (coreSettings.isShowStatisticsSet()) {
- search.getStatistics().print();
+ STORM_LOG_ERROR("This method is not implemented.");
}
-
- } else {
- STORM_LOG_ERROR("This method is not implemented.");
}
+ if (qualSettings.isComputeOnBeliefSupportSet()) {
+ computedSomething = true;
+ storm::pomdp::qualitative::JaniBeliefSupportMdpGenerator<ValueType> janicreator(pomdp);
+ janicreator.generate(targetStates, surelyNotAlmostSurelyReachTarget);
+ bool initialOnly = !qualSettings.isWinningRegionSet();
+ janicreator.verifySymbolic(initialOnly);
+ STORM_PRINT_AND_LOG("Initial state is safe: " << janicreator.isInitialWinning() << "\n");
+ }
+ STORM_LOG_THROW(computedSomething, storm::exceptions::InvalidSettingsException, "Nothing to be done, did you forget to set a method?");
+
}
template<typename ValueType, storm::dd::DdType DdType>
@@ -457,12 +487,18 @@ int main(const int argc, const char** argv) {
if (!optionsCorrect) {
return -1;
}
+ storm::utility::Stopwatch totalTimer(true);
storm::cli::setUrgentOptions();
// Invoke storm-pomdp with obtained settings
storm::pomdp::cli::processOptions();
- // All operations have now been performed, so we clean up everything and terminate.
+ totalTimer.stop();
+ if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
+ storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds());
+ }
+
+ // All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
return 0;
// } catch (storm::exceptions::BaseException const &exception) {
diff --git a/src/storm-pomdp/analysis/IterativePolicySearch.cpp b/src/storm-pomdp/analysis/IterativePolicySearch.cpp
index f41550e9a..9dd1357d8 100644
--- a/src/storm-pomdp/analysis/IterativePolicySearch.cpp
+++ b/src/storm-pomdp/analysis/IterativePolicySearch.cpp
@@ -35,16 +35,16 @@ namespace storm {
template <typename ValueType>
void IterativePolicySearch<ValueType>::Statistics::print() const {
- STORM_PRINT_AND_LOG("Total time: " << totalTimer);
- STORM_PRINT_AND_LOG("SAT Calls " << satCalls);
- STORM_PRINT_AND_LOG("SAT Calls time: " << smtCheckTimer);
- STORM_PRINT_AND_LOG("Outer iterations: " << outerIterations);
- STORM_PRINT_AND_LOG("Solver initialization time: " << initializeSolverTimer);
- STORM_PRINT_AND_LOG("Obtain partial scheduler time: " << evaluateExtensionSolverTime);
- STORM_PRINT_AND_LOG("Update solver to extend partial scheduler time: " << encodeExtensionSolverTime);
- STORM_PRINT_AND_LOG("Update solver with new scheduler time: " << updateNewStrategySolverTime);
- STORM_PRINT_AND_LOG("Winning regions update time: " << winningRegionUpdatesTimer);
- STORM_PRINT_AND_LOG("Graph search time: " << graphSearchTime);
+ STORM_PRINT_AND_LOG("#STATS Total time: " << totalTimer << std::endl);
+ STORM_PRINT_AND_LOG("#STATS SAT Calls: " << satCalls << std::endl);
+ STORM_PRINT_AND_LOG("#STATS SAT Calls time: " << smtCheckTimer << std::endl);
+ STORM_PRINT_AND_LOG("#STATS Outer iterations: " << outerIterations << std::endl);
+ STORM_PRINT_AND_LOG("#STATS Solver initialization time: " << initializeSolverTimer << std::endl);
+ STORM_PRINT_AND_LOG("#STATS Obtain partial scheduler time: " << evaluateExtensionSolverTime << std::endl );
+ STORM_PRINT_AND_LOG("#STATS Update solver to extend partial scheduler time: " << encodeExtensionSolverTime << std::endl);
+ STORM_PRINT_AND_LOG("#STATS Update solver with new scheduler time: " << updateNewStrategySolverTime << std::endl);
+ STORM_PRINT_AND_LOG("#STATS Winning regions update time: " << winningRegionUpdatesTimer << std::endl);
+ STORM_PRINT_AND_LOG("#STATS Graph search time: " << graphSearchTime << std::endl);
}
template <typename ValueType>
@@ -203,8 +203,6 @@ namespace storm {
++obs;
}
-
-
// Update at least one observation.
// PAPER COMMENT: 2
smtSolver->add(storm::expressions::disjunction(observationUpdatedExpressions));
@@ -265,8 +263,6 @@ namespace storm {
}
}
-
-
rowindex = 0;
for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
// PAPER COMMENT 5
@@ -334,7 +330,6 @@ namespace storm {
actPathDisjunction.push_back(storm::expressions::disjunction(pathDisjunction) && actionSelectionVarExpressions.at(pomdp.getObservation(state)).at(action));
rowindex++;
}
- // TODO reconsider if this next add is sound
actPathDisjunction.push_back(switchVarExpressions.at(pomdp.getObservation(state)));
actPathDisjunction.push_back(followVarExpressions[pomdp.getObservation(state)]);
actPathDisjunction.push_back(!reachVarExpressions[state]);
@@ -349,7 +344,6 @@ namespace storm {
}
} else {
smtSolver->add(pathVarExpressions[state][0] == expressionManager->integer(0));
- //assert(false);
}
}
smtSolver->add(reachVars[state]);
diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp
new file mode 100644
index 000000000..4dbce89ef
--- /dev/null
+++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp
@@ -0,0 +1,219 @@
+#include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h"
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+#include "storm/io/file.h"
+#include "storm/api/verification.h"
+#include "storm/api/builder.h"
+#include "storm-parsers/api/properties.h"
+#include "storm/storage/SymbolicModelDescription.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+
+namespace storm {
+ namespace pomdp {
+ namespace qualitative {
+ namespace detail {
+ struct ObsActPair {
+ ObsActPair(uint64_t observation, uint64 action) : observation(observation), action(action) {}
+
+ uint64_t observation;
+ uint64_t action;
+ };
+
+ bool operator<(ObsActPair const& o1, ObsActPair const& o2) {
+ if (o1.observation == o2.observation) {
+ return o1.action < o2.action;
+ }
+ return o1.observation < o2.observation;
+ }
+ }
+
+ template <typename ValueType>
+ JaniBeliefSupportMdpGenerator<ValueType>::JaniBeliefSupportMdpGenerator(storm::models::sparse::Pomdp<ValueType> const& pomdp) :
+ pomdp(pomdp), model("beliefsupport", jani::ModelType::MDP) {
+ // Intentionally left empty.
+ }
+
+ template <typename ValueType>
+ void JaniBeliefSupportMdpGenerator<ValueType>::generate(storm::storage::BitVector const& targetStates, storm::storage::BitVector const& badStates) {
+ //
+ std::map<uint64_t, std::map<detail::ObsActPair, std::vector<uint64_t>>> predecessorInfo;
+ std::map<detail::ObsActPair, std::map<uint64_t, std::set<uint64_t>>> obsPredInfo;
+ std::set<detail::ObsActPair> obsactpairs;
+ // Initialize predecessorInfo for clean steps.
+ for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
+ predecessorInfo[state] = {};
+ }
+
+ // Fill predecessorInfo
+ for (uint64_t state = 0; state < pomdp.getNumberOfStates(); ++state) {
+ uint64_t curObs = pomdp.getObservation(state);
+ for (uint64_t act = 0; act < pomdp.getNumberOfChoices(state); ++act) {
+ detail::ObsActPair oap(curObs, act);
+ obsactpairs.insert(oap);
+ if (obsPredInfo.count(oap) == 0) {
+ obsPredInfo[oap] = std::map<uint64_t, std::set<uint64_t>>();
+ }
+ for (auto const& entry : pomdp.getTransitionMatrix().getRow(state, act)) {
+ if (predecessorInfo[entry.getColumn()].count(oap) == 0) {
+ predecessorInfo[entry.getColumn()][oap] = {state};
+ } else {
+ predecessorInfo[entry.getColumn()][oap].push_back(state);
+ }
+ uint64_t newObs = pomdp.getObservation(entry.getColumn());
+ if (obsPredInfo[oap].count(newObs)==0) {
+ obsPredInfo[oap][newObs] = {state};
+ } else {
+ obsPredInfo[oap][newObs].insert(state);
+ }
+ }
+ }
+ }
+ uint64_t initialObs = pomdp.getObservation(*(pomdp.getInitialStates().begin()));
+
+ expressions::ExpressionManager& exprManager = model.getManager();
+ storm::expressions::Variable posProbVar = exprManager.declareRationalVariable("posProb");
+ model.addConstant(jani::Constant("posProb", posProbVar));
+ std::map<uint64_t, const jani::BooleanVariable*> stateVariables;
+ const jani::BoundedIntegerVariable* obsVar = &model.addVariable(jani::BoundedIntegerVariable("obs", exprManager.declareIntegerVariable("obs"), exprManager.integer(initialObs), exprManager.integer(0), exprManager.integer(pomdp.getNrObservations())));
+ const jani::BoundedIntegerVariable* oldobsActVar = &model.addVariable(jani::BoundedIntegerVariable("prevact", exprManager.declareIntegerVariable("prevact"), exprManager.integer(0), exprManager.integer(0), exprManager.integer(obsactpairs.size())));
+
+ for (uint64_t i = 0; i < pomdp.getNumberOfStates(); ++i) {
+ std::string name = "s" + std::to_string(i);
+ bool isInitial = pomdp.getInitialStates().get(i);
+ stateVariables.emplace(i, &model.addVariable(jani::BooleanVariable(name, exprManager.declareBooleanVariable(name), exprManager.boolean(isInitial))));
+ }
+
+ std::map<detail::ObsActPair, uint64_t> actionIndices;
+ for (auto const& oap : obsactpairs) {
+ std::string actname = "act" + std::to_string(oap.action) + "from" + std::to_string(oap.observation);
+ uint64_t actindex = model.addAction(jani::Action(actname));
+ actionIndices[oap] = actindex;
+ }
+
+ for (uint64_t i = 0; i < pomdp.getNumberOfStates(); ++i) {
+ std::string name = "aut-s" + std::to_string(i);
+ jani::Automaton aut(name, exprManager.declareIntegerVariable(name));
+ uint64_t primeloc = aut.addLocation(jani::Location("default"));
+ aut.addInitialLocation(primeloc);
+ for (auto const& oaps : actionIndices) {
+ if (obsPredInfo[oaps.first].count(pomdp.getObservation(i)) == 0 && pomdp.getObservation(i) != oaps.first.observation) {
+ continue;
+ }
+ std::shared_ptr<jani::TemplateEdge> tedge = std::make_shared<jani::TemplateEdge>(exprManager.boolean(true));
+ jani::TemplateEdgeDestination edgedest;
+ std::vector<storm::expressions::Expression> exprVec;
+ for (auto const& pred : predecessorInfo[i][oaps.first]) {
+ exprVec.push_back(stateVariables.at(pred)->getExpressionVariable().getExpression());
+ }
+ if (exprVec.empty()) {
+ edgedest.addAssignment(jani::Assignment(storm::jani::LValue(*stateVariables.at(i)), exprManager.boolean(false)));
+ } else {
+ edgedest.addAssignment(
+ jani::Assignment(storm::jani::LValue(*stateVariables.at(i)), (exprManager.integer(pomdp.getObservation(i)) == obsVar->getExpressionVariable().getExpression()) && storm::expressions::disjunction(exprVec)));
+ }
+ tedge->addDestination(edgedest);
+ aut.addEdge(jani::Edge(primeloc, oaps.second, boost::none, tedge, {primeloc}, {exprManager.rational(1.0)}));
+ }
+ model.addAutomaton(aut);
+ }
+ jani::Automaton obsAut("obsAut", exprManager.declareIntegerVariable("obsAut"));
+ auto const& targetVar = model.addVariable(jani::BooleanVariable("target", exprManager.declareBooleanVariable("target"), exprManager.boolean(false), true));
+ std::vector<storm::expressions::Expression> notTargetExpression;
+ for (auto const& state : ~targetStates) {
+ notTargetExpression.push_back(!stateVariables.at(state)->getExpressionVariable().getExpression());
+ }
+ auto const& badVar = model.addVariable(jani::BooleanVariable("bad", exprManager.declareBooleanVariable("bad"), exprManager.boolean(false), true));
+ std::vector<storm::expressions::Expression> badExpression;
+ for (auto const& state : badStates) {
+ badExpression.push_back(stateVariables.at(state)->getExpressionVariable().getExpression());
+ }
+
+ auto primeLocation = jani::Location("primary");
+ primeLocation.addTransientAssignment(jani::Assignment(targetVar, expressions::conjunction(notTargetExpression)));
+ primeLocation.addTransientAssignment(jani::Assignment(badVar, badExpression.empty() ? exprManager.boolean(false) : expressions::disjunction(badExpression)));
+ uint64_t primeloc = obsAut.addLocation(primeLocation);
+ obsAut.addInitialLocation(primeloc);
+ uint64_t secloc = obsAut.addLocation(jani::Location("secondary"));
+ // First edges, select observation
+ for (auto const& oaps : actionIndices) {
+ std::shared_ptr<jani::TemplateEdge> tedge = std::make_shared<jani::TemplateEdge>(exprManager.integer(oaps.first.observation) == obsVar->getExpressionVariable().getExpression());
+ std::vector<uint64_t> destLocs;
+ std::vector<storm::expressions::Expression> probs;
+
+ for (auto const& obsAndPredStates : obsPredInfo[oaps.first]) {
+ jani::TemplateEdgeDestination tedgedest;
+ tedgedest.addAssignment(jani::Assignment(jani::LValue(*obsVar), exprManager.integer(obsAndPredStates.first)), true);
+ tedgedest.addAssignment(jani::Assignment(jani::LValue(*oldobsActVar), exprManager.integer(oaps.second)), true);
+
+ tedge->addDestination(tedgedest);
+
+ destLocs.push_back(secloc);
+ std::vector<storm::expressions::Expression> predExpressions;
+ for (auto predstate : obsAndPredStates.second) {
+ predExpressions.push_back(stateVariables.at(predstate)->getExpressionVariable().getExpression());
+ }
+ probs.push_back(storm::expressions::ite(storm::expressions::disjunction(predExpressions), posProbVar.getExpression(), exprManager.rational(0)));
+ }
+ jani::Edge edge(primeloc, jani::Model::SILENT_ACTION_INDEX, boost::none, tedge, destLocs, probs);
+ obsAut.addEdge(edge);
+ }
+ // Back edges
+ for (auto const& oaps : obsactpairs) {
+ std::shared_ptr<jani::TemplateEdge> tedge = std::make_shared<jani::TemplateEdge>(oldobsActVar->getExpressionVariable() == exprManager.integer(actionIndices[oaps]));
+
+ jani::TemplateEdgeDestination tedgedest;
+ tedgedest.addAssignment(jani::Assignment(jani::LValue(*oldobsActVar), exprManager.integer(0)));
+ tedge->addDestination(tedgedest);
+ jani::Edge edge(secloc, actionIndices[oaps], boost::none, tedge, {primeloc}, {exprManager.rational(1.0)});
+ obsAut.addEdge(edge);
+ }
+ model.addAutomaton(obsAut);
+ model.setStandardSystemComposition();
+ model.finalize();
+ }
+
+ template <typename ValueType>
+ void JaniBeliefSupportMdpGenerator<ValueType>::verifySymbolic(bool onlyInitial) {
+ storage::SymbolicModelDescription symdesc(model);
+ // This trick only works because we do not explictly check that the model is stochastic!
+ symdesc = symdesc.preprocess("posProb=0.1");
+ auto property = storm::api::parsePropertiesForJaniModel("Pmax>=1 [!\"bad\" U \"target\"]", model)[0];
+ auto mdp = storm::api::buildSymbolicModel<storm::dd::DdType::Sylvan, ValueType>(symdesc, {property.getRawFormula()});
+ storm::Environment env;
+ std::unique_ptr<modelchecker::CheckResult> result = storm::api::verifyWithDdEngine(env, mdp, storm::api::createTask<ValueType>(property.getRawFormula(), onlyInitial));
+ std::unique_ptr<storm::modelchecker::CheckResult> filter;
+
+ if (onlyInitial) {
+ filter = std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>(mdp->getReachableStates(), mdp->getInitialStates());
+ } else {
+ auto relstates = storm::api::parsePropertiesForJaniModel("prevact=0", model)[0];
+ filter = storm::api::verifyWithDdEngine<storm::dd::DdType::Sylvan, ValueType>(env, mdp, storm::api::createTask<ValueType>(relstates.getRawFormula(), false));
+ }
+ if (result && filter) {
+ result->filter(filter->asQualitativeCheckResult());
+ }
+
+ if(result && !onlyInitial) {
+ auto vars = result->asSymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>().getTruthValuesVector().getContainedMetaVariables();
+ // TODO Export these results.
+ } else if (result) {
+ initialIsWinning = result->asQualitativeCheckResult().existsTrue();
+ }
+ }
+
+ template <typename ValueType>
+ bool JaniBeliefSupportMdpGenerator<ValueType>::isInitialWinning() const {
+ return initialIsWinning;
+ }
+
+
+ template class JaniBeliefSupportMdpGenerator<double>;
+ template class JaniBeliefSupportMdpGenerator<storm::RationalNumber>;
+ template class JaniBeliefSupportMdpGenerator<storm::RationalFunction>;
+
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h
new file mode 100644
index 000000000..d0e7a8a5c
--- /dev/null
+++ b/src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h
@@ -0,0 +1,28 @@
+#pragma once
+#include "storm/models/sparse/Pomdp.h"
+#include "storm/storage/jani/Model.h"
+
+
+namespace storm {
+
+ namespace pomdp {
+
+ namespace qualitative {
+ template <typename ValueType>
+ class JaniBeliefSupportMdpGenerator {
+
+ public:
+ JaniBeliefSupportMdpGenerator(storm::models::sparse::Pomdp<ValueType> const& pomdp);
+ void generate(storm::storage::BitVector const& targetStates, storm::storage::BitVector const& badStates);
+ void verifySymbolic(bool onlyInitial = true);
+ bool isInitialWinning() const;
+
+ private:
+ storm::models::sparse::Pomdp<ValueType> const& pomdp;
+ jani::Model model;
+ bool initialIsWinning = false;
+ };
+
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storm-pomdp/analysis/OneShotPolicySearch.h b/src/storm-pomdp/analysis/OneShotPolicySearch.h
index fb2b4d5a7..af7203cea 100644
--- a/src/storm-pomdp/analysis/OneShotPolicySearch.h
+++ b/src/storm-pomdp/analysis/OneShotPolicySearch.h
@@ -55,9 +55,9 @@ namespace storm {
STORM_LOG_TRACE("Questionmark states: " << (~surelyReachSinkStates & ~targetStates));
bool result = analyze(k, ~surelyReachSinkStates & ~targetStates, pomdp.getInitialStates());
if (result) {
- STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target.");
+ STORM_PRINT_AND_LOG("From initial state, one can almost-surely reach the target." << std::endl);
} else {
- STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target .");
+ STORM_PRINT_AND_LOG("From initial state, one may not almost-surely reach the target ." << std::endl);
}
}
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index d97ed6c3d..22ea42fbb 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -746,7 +746,7 @@ namespace storm {
if (this->options.isExplorationChecksSet()) {
// Check that the resulting distribution is in fact a distribution.
- STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
+ STORM_LOG_THROW(!this->isDiscreteTimeModel() || (!storm::utility::isConstant(probabilitySum) || this->comparator.isOne(probabilitySum)), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
}
return choice;
@@ -768,7 +768,7 @@ namespace storm {
storm::jani::Edge const& edge = *iteratorList[i]->second;
lowestDestinationAssignmentLevel = std::min(lowestDestinationAssignmentLevel, edge.getLowestAssignmentLevel());
highestDestinationAssignmentLevel = std::max(highestDestinationAssignmentLevel, edge.getHighestAssignmentLevel());
- if (!edge.getAssignments().empty()) {
+ if (!edge.getAssignments().empty(true)) {
lowestEdgeAssignmentLevel = std::min(lowestEdgeAssignmentLevel, edge.getAssignments().getLowestLevel(true));
highestEdgeAssignmentLevel = std::max(highestEdgeAssignmentLevel, edge.getAssignments().getHighestLevel(true));
}
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index 747fbcecd..5d76ae03b 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -87,7 +87,10 @@ namespace storm {
return getLowestLevel(onlyTransient) != 0 || getHighestLevel(onlyTransient) != 0;
}
- bool OrderedAssignments::empty() const {
+ bool OrderedAssignments::empty(bool onlyTransient) const {
+ if (onlyTransient) {
+ return transientAssignments.empty();
+ }
return allAssignments.empty();
}
diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h
index de914b738..877ea845d 100644
--- a/src/storm/storage/jani/OrderedAssignments.h
+++ b/src/storm/storage/jani/OrderedAssignments.h
@@ -57,7 +57,7 @@ namespace storm {
/*!
* Retrieves whether this set of assignments is empty.
*/
- bool empty() const;
+ bool empty(bool onlyTransient = false) const;
/*!
* Removes all assignments from this set.