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

compute 1-Pmax[in order to compute Pmin for MDPs

tempestpy_adaptions
hannah 4 years ago
committed by Stefan Pranger
parent
fc0ae2ea4b
commit
93d9b586ed
3 changed files with 20 additions and 38 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. 32
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  2. 2
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
  3. 24
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

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

@ -227,7 +227,7 @@ namespace storm {
storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true);
storm::storage::BitVector soiProduct(product->getStatesOfInterest());
// Create goal for computeUntilProbabilities, compute maximizing probabilties for DA product with MDP
// Create goal for computeUntilProbabilities, compute maximizing probabilities 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));
@ -263,17 +263,23 @@ namespace storm {
return numericResult;
}
//todo remove goal?
template<typename ValueType, bool Nondeterministic>
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?
std::vector <ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets) {
std::shared_ptr<storm::logic::Formula const> ltlFormula;
STORM_LOG_THROW((!Nondeterministic) || this->isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
if (Nondeterministic && this->getOptimizationDirection() == OptimizationDirection::Minimize) {
// negate formula in order to compute 1-Pmax[!formula]
ltlFormula = std::make_shared<storm::logic::UnaryBooleanPathFormula>(storm::logic::UnaryBooleanOperatorType::Not, formula.asSharedPointer());
STORM_LOG_INFO("Computing Pmin, proceeding with negated LTL formula.");
} else {
ltlFormula = formula.asSharedPointer();
}
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("Resulting LTL path formula: " << ltlFormula->toString());
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, "
@ -281,18 +287,16 @@ namespace storm {
<< *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
//todo remove goal here? send dir instead?
// compute Pmax for MDP
std::vector<ValueType> numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet());
// 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]
// compute 1-Pmax[!fomula]
for (auto& value : numericResult) {
value = storm::utility::one<ValueType>() - value;
}
}
*/
return numericResult;
}

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

@ -45,7 +45,7 @@ namespace storm {
* Computes the ltl probabilities ...todo
* @return a value for each state
*/
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 ..?
std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets); //todo was brauchen wir hier aps und ..?
private:

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

@ -202,22 +202,7 @@ namespace storm {
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);
}
const SparseMdpModelType& mdp = this->getModel();
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()) {
@ -228,16 +213,9 @@ namespace storm {
}
storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(mdp.getTransitionMatrix(), this->getModel().getNumberOfStates());
storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, subTask, mdp);
storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, mdp);
std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
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)));
}

Write Preview
Loading…
Cancel
Save