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

(MDP-LTL) SparseMdpPrctlModelChecker: handle LTL 

Conflicts:
	src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
tempestpy_adaptions
Joachim Klein 4 years ago
committed by Stefan Pranger
parent
615b2b5399
commit
04a8bec83f
3 changed files with 174 additions and 13 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 155
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  2. 5
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  3. 27
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

155
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
View File

@ -1,5 +1,7 @@
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include <sstream>
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
@ -12,6 +14,10 @@
#include "storm/logic/FragmentSpecification.h"
#include "storm/transformer/DAProductBuilder.h"
#include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
#include "storm/automata/LTL2DeterministicAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
@ -23,12 +29,14 @@
#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
#include "storm/solver/SolveGoal.h"
#include "storm/storage/BitVector.h"
#include "storm/shields/ShieldHandling.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/DebugSettings.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidPropertyException.h"
@ -48,7 +56,7 @@ namespace storm {
template<typename SparseMdpModelType>
bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandleStatic(CheckTask<storm::logic::Formula, ValueType> const& checkTask, bool* requiresSingleInitialState) {
storm::logic::Formula const& formula = checkTask.getFormula();
if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
if (formula.isInFragment(storm::logic::prctlstar().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setTimeOperatorsAllowed(true).setReachbilityTimeFormulasAllowed(true).setRewardAccumulationAllowed(true))) {
return true;
} else if (checkTask.isOnlyInitialStatesRelevantSet()) {
auto multiObjectiveFragment = storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true).setRewardAccumulationAllowed(true);
@ -169,6 +177,149 @@ namespace storm {
return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(result);
}
template<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
std::vector<storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> extracted;
std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted);
STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula);
std::map<std::string, storm::storage::BitVector> apSets;
for (auto& p : extracted) {
STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
std::unique_ptr<CheckResult> subResultPointer = this->check(env, *p.second);
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
auto sat = subResult.getTruthValuesVector();
STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states.");
apSets[p.first] = std::move(sat);
}
bool minimize = false;
CheckTask<storm::logic::Formula, ValueType> subTask(checkTask);
if (checkTask.getOptimizationDirection() == OptimizationDirection::Minimize) {
minimize = true;
// negate
ltlFormula = std::make_shared<storm::logic::UnaryBooleanPathFormula>(storm::logic::UnaryBooleanOperatorType::Not, ltlFormula);
STORM_LOG_INFO("Computing Pmin, proceeding with negated LTL formula.");
subTask = checkTask.negate().substituteFormula(*ltlFormula);
} else {
subTask = checkTask.substituteFormula(*ltlFormula);
}
STORM_LOG_INFO("Resulting LTL path formula: " << *ltlFormula);
STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString());
std::shared_ptr<storm::automata::DeterministicAutomaton> da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula);
STORM_LOG_INFO("Deterministic automaton for LTL formula has "
<< da->getNumberOfStates() << " states, "
<< da->getAPSet().size() << " atomic propositions and "
<< *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
const SparseMdpModelType& mdp = this->getModel();
storm::solver::SolveGoal<ValueType> goal(mdp, subTask);
std::vector<ValueType> numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSets, checkTask.isQualitativeSet());
if (minimize) {
// compute 1-Pmax[!ltl]
for (auto& value : numericResult) {
value = storm::utility::one<ValueType>() - value;
}
}
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseMdpModelType>
std::vector<typename SparseMdpPrctlModelChecker<SparseMdpModelType>::ValueType> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<typename SparseMdpPrctlModelChecker<SparseMdpModelType>::ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) const {
STORM_LOG_THROW(goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP");
const storm::automata::APSet& apSet = da.getAPSet();
std::vector<storm::storage::BitVector> apLabels;
for (const std::string& ap : apSet.getAPs()) {
auto it = apSatSets.find(ap);
STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula");
apLabels.push_back(std::move(it->second));
}
const SparseMdpModelType& mdp = this->getModel();
storm::storage::BitVector statesOfInterest;
if (goal.hasRelevantValues()) {
statesOfInterest = goal.relevantValues();
} else {
// product from all model states
statesOfInterest = storm::storage::BitVector(mdp.getNumberOfStates(), true);
}
STORM_LOG_INFO("Building MDP-DA product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states...");
storm::transformer::DAProductBuilder productBuilder(da, apLabels);
auto product = productBuilder.build(mdp, statesOfInterest);
STORM_LOG_INFO("Product MDP has " << product->getProductModel().getNumberOfStates() << " states and "
<< product->getProductModel().getNumberOfTransitions() << " transitions.");
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
STORM_LOG_TRACE("Writing model to model.dot");
std::ofstream modelDot("model.dot");
mdp.writeDotToStream(modelDot);
modelDot.close();
STORM_LOG_TRACE("Writing product model to product.dot");
std::ofstream productDot("product.dot");
product->getProductModel().writeDotToStream(productDot);
productDot.close();
STORM_LOG_TRACE("Product model mapping:");
std::stringstream str;
product->printMapping(str);
STORM_LOG_TRACE(str.str());
}
STORM_LOG_INFO("Computing accepting end components...");
storm::storage::BitVector accepting = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions());
if (accepting.empty()) {
STORM_LOG_INFO("No accepting states, skipping probability computation.");
std::vector<ValueType> numericResult(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
return numericResult;
}
STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs...");
storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true);
storm::solver::SolveGoal<ValueType> solveGoalProduct(goal);
storm::storage::BitVector soiProduct(product->getStatesOfInterest());
solveGoalProduct.setRelevantValues(std::move(soiProduct));
std::vector<ValueType> prodNumericResult
= std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env,
std::move(solveGoalProduct),
product->getProductModel().getTransitionMatrix(),
product->getProductModel().getBackwardTransitions(),
bvTrue,
accepting,
qualitative,
false // no schedulers (at the moment)
).values);
std::vector<ValueType> numericResult = product->projectToOriginalModel(this->getModel(), prodNumericResult);
return numericResult;
}
template<typename SparseMdpModelType>
std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeConditionalProbabilities(Environment const& env, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) {
storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();

5
src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View File

@ -4,6 +4,8 @@
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/SolveGoal.h"
namespace storm {
@ -39,9 +41,12 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeStateFormulaProbabilities(Environment const& env, CheckTask<storm::logic::Formula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) override;
private:
std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) const;
};
} // namespace modelchecker
} // namespace storm

27
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -749,7 +749,6 @@ namespace storm {
template<typename ValueType>
storm::storage::BitVector SparseMdpPrctlHelper<ValueType>::computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
STORM_LOG_INFO("Computing accepting states for acceptance condition " << *acceptance.getAcceptanceExpression());
std::cout << transitionMatrix.getRowGroupCount() << std::endl;
if (acceptance.getAcceptanceExpression()->isTRUE()) {
STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)");
return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
@ -762,16 +761,18 @@ namespace storm {
storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false);
std::size_t accMECs = 0;
std::size_t allMECs = 0;
std::size_t i = 0;
for (auto const& conjunction : dnf) {
// determine the set of states of the subMDP that can satisfy the condition
// => remove all states that would violate Fins in the conjunction
storm::storage::BitVector allowed(transitionMatrix.getRowGroupCount(), true);
STORM_LOG_INFO("Handle conjunction " << i);
STORM_LOG_DEBUG("Handle conjunction " << i);
for (auto const& literal : conjunction) {
STORM_LOG_INFO(" " << *literal);
STORM_LOG_DEBUG(" " << *literal);
if (literal->isTRUE()) {
// skip
} else if (literal->isFALSE()) {
@ -798,12 +799,13 @@ namespace storm {
continue;
}
STORM_LOG_INFO(" Allowed states: " << allowed);
STORM_LOG_DEBUG(" Allowed states: " << allowed);
// compute MECs in the allowed fragment
storm::storage::MaximalEndComponentDecomposition<ValueType> mecs(transitionMatrix, backwardTransitions, allowed);
allMECs += mecs.size();
for (const auto& mec : mecs) {
STORM_LOG_INFO("Inspect MEC: " << mec);
STORM_LOG_DEBUG("Inspect MEC: " << mec);
bool accepting = true;
for (auto const& literal : conjunction) {
@ -817,16 +819,16 @@ namespace storm {
const storm::storage::BitVector& accSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet());
if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_INF) {
if (atom.isNegated()) {
STORM_LOG_INFO("Checking against " << ~accSet);
STORM_LOG_DEBUG("Checking against " << ~accSet);
if (!mec.containsAnyState(~accSet)) {
STORM_LOG_INFO(" -> not satisfied");
STORM_LOG_DEBUG(" -> not satisfied");
accepting = false;
break;
}
} else {
STORM_LOG_INFO("Checking against " << accSet);
STORM_LOG_DEBUG("Checking against " << accSet);
if (!mec.containsAnyState(accSet)) {
STORM_LOG_INFO(" -> not satisfied");
STORM_LOG_DEBUG(" -> not satisfied");
accepting = false;
break;
}
@ -839,7 +841,8 @@ namespace storm {
}
if (accepting) {
STORM_LOG_INFO("MEC is accepting");
accMECs++;
STORM_LOG_DEBUG("MEC is accepting");
for (auto const& stateChoicePair : mec) {
acceptingStates.set(stateChoicePair.first);
}
@ -848,7 +851,9 @@ namespace storm {
}
}
STORM_LOG_INFO("Accepting states: " << acceptingStates);
STORM_LOG_DEBUG("Accepting states: " << acceptingStates);
STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs).");
return acceptingStates;
}

Write Preview
Loading…
Cancel
Save