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

removed SolveGoal in function computeLTLproabilities of SparseLTLHelper

tempestpy_adaptions
hannah 4 years ago
committed by Stefan Pranger
parent
1fe30f7d78
commit
fc0ae2ea4b
6 changed files with 222 additions and 189 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. 245
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  2. 21
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
  3. 11
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  4. 12
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  5. 111
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  6. 11
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

245
src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
View File

@ -7,6 +7,7 @@
#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/DebugSettings.h"
@ -21,11 +22,143 @@ namespace storm {
// Intentionally left empty.
}
template<typename ValueType, bool Nondeterministic>
std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) {
STORM_LOG_THROW((!Nondeterministic) || goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP");
// todo only for MDP and change name!
template <typename ValueType, bool Nondeterministic>
storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::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());
if (acceptance.getAcceptanceExpression()->isTRUE()) {
STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)");
return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
} else if (acceptance.getAcceptanceExpression()->isFALSE()) {
STORM_LOG_INFO(" FALSE -> all states rejecting");
return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false);
}
std::vector<std::vector<automata::AcceptanceCondition::acceptance_expr::ptr>> dnf = acceptance.extractFromDNF();
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);
for (auto const& literal : conjunction) {
STORM_LOG_INFO(" " << *literal);
if (literal->isTRUE()) {
// skip
} else if (literal->isFALSE()) {
allowed.clear();
break;
} else if (literal->isAtom()) {
const cpphoafparser::AtomAcceptance& atom = literal->getAtom();
if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) {
// only deal with FIN, ignore INF here
const storm::storage::BitVector& accSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet());
if (atom.isNegated()) {
// allowed = allowed \ ~accSet = allowed & accSet
allowed &= accSet;
} else {
// allowed = allowed \ accSet = allowed & ~accSet
allowed &= ~accSet;
}
}
}
}
if (allowed.empty()) {
// skip
continue;
}
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_DEBUG("Inspect MEC: " << mec);
bool accepting = true;
for (auto const& literal : conjunction) {
if (literal->isTRUE()) {
// skip
} else if (literal->isFALSE()) {
accepting = false;
break;
} else if (literal->isAtom()) {
const cpphoafparser::AtomAcceptance& atom = literal->getAtom();
const storm::storage::BitVector& accSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet());
if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_INF) {
if (atom.isNegated()) {
STORM_LOG_DEBUG("Checking against " << ~accSet);
if (!mec.containsAnyState(~accSet)) {
STORM_LOG_DEBUG(" -> not satisfied");
accepting = false;
break;
}
} else {
STORM_LOG_DEBUG("Checking against " << accSet);
if (!mec.containsAnyState(accSet)) {
STORM_LOG_DEBUG(" -> not satisfied");
accepting = false;
break;
}
}
} else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) {
// do only sanity checks here
STORM_LOG_ASSERT(atom.isNegated() ? !mec.containsAnyState(~accSet) : !mec.containsAnyState(accSet), "MEC contains Fin-states, which should have been removed");
}
}
}
if (accepting) {
accMECs++;
STORM_LOG_DEBUG("MEC is accepting");
for (auto const& stateChoicePair : mec) {
acceptingStates.set(stateChoicePair.first);
}
}
}
}
STORM_LOG_DEBUG("Accepting states: " << acceptingStates);
STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs).");
return acceptingStates;
}
// todo only for dtmc and change name!
template <typename ValueType, bool Nondeterministic>
storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix) {
storm::storage::StronglyConnectedComponentDecomposition<ValueType> bottomSccs(transitionMatrix, storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs());
//storm::storage::BitVector acceptingStates = storm::storage::BitVector(product->getProductModel().getNumberOfStates());
storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false);
std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0;
for (auto& scc : bottomSccs) {
checkedBSCCs++;
if (acceptance.isAccepting(scc)) {
acceptingBSCCs++;
for (auto& state : scc) {
acceptingStates.set(state);
acceptingBSCCStates++;
}
}
}
STORM_LOG_INFO("BSCC analysis: " << acceptingBSCCs << " of " << checkedBSCCs << " BSCCs were acceptingStates (" << acceptingBSCCStates << " states in acceptingStates BSCCs).");
return acceptingStates;
}
template<typename ValueType, bool Nondeterministic>
std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) {
const storm::automata::APSet& apSet = da.getAPSet();
std::vector<storm::storage::BitVector> apLabels;
@ -37,28 +170,25 @@ namespace storm {
}
storm::storage::BitVector statesOfInterest;
if (goal.hasRelevantValues()) {
statesOfInterest = goal.relevantValues();
if (this->hasRelevantStates()) {
statesOfInterest = this->getRelevantStates();
} else {
// product from all model states
statesOfInterest = storm::storage::BitVector(this->_numberOfStates, true);
}
// todo change text
STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states...");
storm::transformer::DAProductBuilder productBuilder(da, apLabels);
auto product = productBuilder.build<productModelType>(this->_transitionMatrix, statesOfInterest);
STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC")) +" has " << product->getProductModel().getNumberOfStates() << " states and "
STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +" 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");
// this->_model.writeDotToStream(modelDot); // TODO
modelDot.close();
STORM_LOG_TRACE("Writing product model to product.dot");
std::ofstream productDot("product.dot");
product->getProductModel().writeDotToStream(productDot);
@ -70,75 +200,63 @@ namespace storm {
STORM_LOG_TRACE(str.str());
}
// DTMC: BCC
// MDP: computeSurelyAcceptingPmaxStates
storm::storage::BitVector accepting;
storm::storage::BitVector acceptingStates;
if (Nondeterministic) {
STORM_LOG_INFO("Computing accepting end components...");
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->_numberOfStates, storm::utility::zero<ValueType>());
return numericResult;
}
// todo compute accepting states, same as below
acceptingStates = computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions());
} else {
STORM_LOG_INFO("Computing BSCCs and checking for acceptance...");
// todo compute accepting states, (no btm)
acceptingStates = computeAcceptingComponentStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix());
storm::storage::StronglyConnectedComponentDecomposition<ValueType> bottomSccs(product->getProductModel().getTransitionMatrix(),
storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs());
accepting = storm::storage::BitVector(product->getProductModel().getNumberOfStates());
std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0;
for (auto& scc : bottomSccs) {
checkedBSCCs++;
if (product->getAcceptance()->isAccepting(scc)) {
acceptingBSCCs++;
for (auto& state : scc) {
accepting.set(state);
acceptingBSCCStates++;
}
}
}
STORM_LOG_INFO("BSCC analysis: " << acceptingBSCCs << " of " << checkedBSCCs << " BSCCs were accepting (" << acceptingBSCCStates << " states in accepting BSCCs).");
}
if (acceptingBSCCs == 0) {
STORM_LOG_INFO("No accepting BSCCs, skipping probability computation.");
std::vector<ValueType> numericResult(this->_numberOfStates, storm::utility::zero<ValueType>());
return numericResult;
}
if (acceptingStates.empty()) {
STORM_LOG_INFO("No acceptingStates states, skipping probability computation.");
std::vector<ValueType> numericResult(this->_numberOfStates, storm::utility::zero<ValueType>());
return numericResult;
}
STORM_LOG_INFO("Computing probabilities for reaching accepting components...");
STORM_LOG_INFO("Computing probabilities for reaching acceptingStates components...");
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));
// Create goal for computeUntilProbabilities, compute maximizing probabilties for DA product with MDP
storm::solver::SolveGoal<ValueType> solveGoalProduct;
if (this->isValueThresholdSet()) {
solveGoalProduct = storm::solver::SolveGoal<ValueType>(OptimizationDirection::Maximize, this->getValueThresholdComparisonType(), this->getValueThresholdValue(), std::move(soiProduct));
} else {
solveGoalProduct = storm::solver::SolveGoal<ValueType>(OptimizationDirection::Maximize);
solveGoalProduct.setRelevantValues(std::move(soiProduct));
}
std::vector<ValueType> prodNumericResult;
if (Nondeterministic) {
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)
std::move(solveGoalProduct),
product->getProductModel().getTransitionMatrix(),
product->getProductModel().getBackwardTransitions(),
bvTrue,
acceptingStates,
qualitative,
false // no schedulers (at the moment)
).values);
} else {
prodNumericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(env,
std::move(solveGoalProduct),
product->getProductModel().getTransitionMatrix(),
product->getProductModel().getBackwardTransitions(),
bvTrue,
accepting,
qualitative);
std::move(solveGoalProduct),
product->getProductModel().getTransitionMatrix(),
product->getProductModel().getBackwardTransitions(),
bvTrue,
acceptingStates,
qualitative);
}
std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult);
@ -146,8 +264,12 @@ namespace storm {
}
//todo remove goal?
template<typename ValueType, bool Nondeterministic>
std::vector <ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal<ValueType>&& goal, storm::logic::Formula const& ltlFormula, std::map<std::string, storm::storage::BitVector>& apSatSets) {
std::vector <ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& ltlFormula, std::map<std::string, storm::storage::BitVector>& apSatSets) {
// TODO optDir: helper.getOptimizationDirection for MDP
// negate formula etc ~ap?
STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula);
STORM_LOG_INFO(" in prefix format: " << ltlFormula.toPrefixString());
@ -159,10 +281,11 @@ namespace storm {
<< *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
std::vector<ValueType> numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSatSets, this->isQualitativeSet());
//todo remove goal here? send dir instead?
std::vector<ValueType> numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet());
// TODO
/*
// TODO optDir: helper.getOptimizationDirection for MDP
/* //for any path formula ψ: pmin(s, ψ) = 1- pmax(s, ¬ψ)
if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) {
// compute 1-Pmax[!ltl]
for (auto& value : numericResult) {

21
src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
View File

@ -35,19 +35,36 @@ namespace storm {
/*!
* todo
* Computes maximizing(!) probabilties for DA product with MDP
* @return
*/
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);
std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative);
/*!
* Computes the ltl probabilities ...todo
* @return a value for each state
*/
std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal<ValueType>&& goal, storm::logic::Formula const& f, std::map<std::string, storm::storage::BitVector>& apSatSets); //todo was brauchen wir hier aps und ..?
std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::logic::Formula const& f, std::map<std::string, storm::storage::BitVector>& apSatSets); //todo was brauchen wir hier aps und ..?
private:
/*! todo only relevant for MDP - enable_if_t ?
* Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance conditon.
* More precisely, let
* accEC be the set of states that are contained in end components that satisfy the acceptance condition
* and let
* P1acc be the set of states that satisfy Pmax=1[ F accEC ].
* This function then computes a set that contains accEC and is contained by P1acc.
* However, if the acceptance condition consists of 'true', the whole state space can be returned.
*/
static storm::storage::BitVector computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
//todo only for dtmc, different to mdp: no backward tm
static storm::storage::BitVector computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
std::size_t _numberOfStates;

11
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -162,7 +162,6 @@ namespace storm {
STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula);
std::map<std::string, storm::storage::BitVector> apSets;
// todo apSets = computeApSets(env, checkTask);
for (auto& p : extracted) {
STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
@ -177,9 +176,17 @@ namespace storm {
const SparseDtmcModelType& dtmc = this->getModel();
// TODO
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
STORM_LOG_TRACE("Writing model to model.dot");
std::ofstream modelDot("model.dot");
this->getModel().writeDotToStream(modelDot);
modelDot.close();
}
storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates());
storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc);
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), *ltlFormula, apSets);
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}

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

@ -217,11 +217,19 @@ namespace storm {
}
const SparseMdpModelType& mdp = this->getModel();
storm::solver::SolveGoal<ValueType> goal(mdp, subTask);
storm::solver::SolveGoal<ValueType> goal(mdp, subTask); //todo remove, infos now in helper, see below
// TODO
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
STORM_LOG_TRACE("Writing model to model.dot");
std::ofstream modelDot("model.dot");
this->getModel().writeDotToStream(modelDot);
modelDot.close();
}
storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(mdp.getTransitionMatrix(), this->getModel().getNumberOfStates());
storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, subTask, mdp);
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), subTask), *ltlFormula, apSets);
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
if(minimize) {
// compute 1-Pmax[!ltl]

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

@ -745,117 +745,6 @@ namespace storm {
return result;
}
}
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());
if (acceptance.getAcceptanceExpression()->isTRUE()) {
STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)");
return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true);
} else if (acceptance.getAcceptanceExpression()->isFALSE()) {
STORM_LOG_INFO(" FALSE -> all states rejecting");
return storm::storage::BitVector(transitionMatrix.getRowGroupCount(), false);
}
std::vector<std::vector<automata::AcceptanceCondition::acceptance_expr::ptr>> dnf = acceptance.extractFromDNF();
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_DEBUG("Handle conjunction " << i);
for (auto const& literal : conjunction) {
STORM_LOG_DEBUG(" " << *literal);
if (literal->isTRUE()) {
// skip
} else if (literal->isFALSE()) {
allowed.clear();
break;
} else if (literal->isAtom()) {
const cpphoafparser::AtomAcceptance& atom = literal->getAtom();
if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) {
// only deal with FIN, ignore INF here
const storm::storage::BitVector& accSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet());
if (atom.isNegated()) {
// allowed = allowed \ ~accSet = allowed & accSet
allowed &= accSet;
} else {
// allowed = allowed \ accSet = allowed & ~accSet
allowed &= ~accSet;
}
}
}
}
if (allowed.empty()) {
// skip
continue;
}
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_DEBUG("Inspect MEC: " << mec);
bool accepting = true;
for (auto const& literal : conjunction) {
if (literal->isTRUE()) {
// skip
} else if (literal->isFALSE()) {
accepting = false;
break;
} else if (literal->isAtom()) {
const cpphoafparser::AtomAcceptance& atom = literal->getAtom();
const storm::storage::BitVector& accSet = acceptance.getAcceptanceSet(atom.getAcceptanceSet());
if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_INF) {
if (atom.isNegated()) {
STORM_LOG_DEBUG("Checking against " << ~accSet);
if (!mec.containsAnyState(~accSet)) {
STORM_LOG_DEBUG(" -> not satisfied");
accepting = false;
break;
}
} else {
STORM_LOG_DEBUG("Checking against " << accSet);
if (!mec.containsAnyState(accSet)) {
STORM_LOG_DEBUG(" -> not satisfied");
accepting = false;
break;
}
}
} else if (atom.getType() == cpphoafparser::AtomAcceptance::TEMPORAL_FIN) {
// do only sanity checks here
STORM_LOG_ASSERT(atom.isNegated() ? !mec.containsAnyState(~accSet) : !mec.containsAnyState(accSet), "MEC contains Fin-states, which should have been removed");
}
}
}
if (accepting) {
accMECs++;
STORM_LOG_DEBUG("MEC is accepting");
for (auto const& stateChoicePair : mec) {
acceptingStates.set(stateChoicePair.first);
}
}
}
}
STORM_LOG_DEBUG("Accepting states: " << acceptingStates);
STORM_LOG_INFO("Found " << acceptingStates.getNumberOfSetBits() << " states in " << accMECs << " accepting MECs (considered " << allMECs << " MECs).");
return acceptingStates;
}
template<typename ValueType>
template<typename RewardModelType>

11
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
View File

@ -48,17 +48,6 @@ namespace storm {
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint());
static MDPSparseModelCheckingHelperReturnType<ValueType> computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, bool useMecBasedTechnique = false);
/*!
* Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance conditon.
* More precisely, let
* accEC be the set of states that are contained in end components that satisfy the acceptance condition
* and let
* P1acc be the set of states that satisfy Pmax=1[ F accEC ].
* This function then computes a set that contains accEC and is contained by P1acc.
* However, if the acceptance condition consists of 'true', the whole state space can be returned.
*/
static storm::storage::BitVector computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
template<typename RewardModelType>
static std::vector<ValueType> computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount);

Write Preview
Loading…
Cancel
Save