Sebastian Junges
5 years ago
6 changed files with 343 additions and 55 deletions
-
1src/storm-pomdp-cli/settings/PomdpSettings.cpp
-
6src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.cpp
-
1src/storm-pomdp-cli/settings/modules/QualitativePOMDPAnalysisSettings.h
-
128src/storm-pomdp-cli/storm-pomdp.cpp
-
235src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.cpp
-
27src/storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h
@ -0,0 +1,235 @@ |
|||||
|
#include "storm-pomdp/analysis/JaniBeliefSupportMdpGenerator.h"
|
||||
|
#include "storm/storage/jani/Model.h"
|
||||
|
#include "storm/storage/expressions/ExpressionManager.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-parsers/api/model_descriptions.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, jani::BooleanVariable> stateVariables; |
||||
|
jani::BoundedIntegerVariable obsVar = model.addVariable(jani::BoundedIntegerVariable("obs", exprManager.declareIntegerVariable("obs"), exprManager.integer(initialObs), exprManager.integer(0), exprManager.integer(pomdp.getNrObservations()))); |
||||
|
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(stateVariables.at(i), exprManager.boolean(false))); |
||||
|
} else { |
||||
|
edgedest.addAssignment( |
||||
|
jani::Assignment(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(obsVar, exprManager.integer(obsAndPredStates.first)), true); |
||||
|
tedgedest.addAssignment(jani::Assignment(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(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(); |
||||
|
std::ofstream ostr; |
||||
|
|
||||
|
storm::utility::openFile("beliefsupport-mdp.jani", ostr); |
||||
|
ostr << model; |
||||
|
model = storm::api::parseJaniModel("beliefsupport-mdp.jani").first; |
||||
|
storm::utility::closeFile(ostr); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void JaniBeliefSupportMdpGenerator<ValueType>::verifySymbolic(bool onlyInitial) { |
||||
|
storage::SymbolicModelDescription symdesc(model); |
||||
|
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()}); |
||||
|
mdp->printModelInformationToStream(std::cout); |
||||
|
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) { |
||||
|
std::cout << "count: " << result->asQualitativeCheckResult().count() << std::endl; |
||||
|
} 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>; |
||||
|
|
||||
|
|
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,27 @@ |
|||||
|
#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; |
||||
|
}; |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue