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

removed model from SparseLTLHelper

main
hannah 5 years ago
committed by Stefan Pranger
parent
f8d9773131
commit
ffe70ea056
7 changed files with 51 additions and 122 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. 43
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp
  2. 21
      src/storm/modelchecker/helper/ltl/SparseLTLHelper.h
  3. 4
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  4. 84
      src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  5. 11
      src/storm/transformer/DAProductBuilder.h
  6. 7
      src/storm/transformer/Product.h
  7. 3
      src/storm/transformer/ProductBuilder.h

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

@ -3,9 +3,6 @@
#include "storm/transformer/DAProductBuilder.h"
#include "storm/automata/LTL2DeterministicAutomaton.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
@ -19,13 +16,13 @@ namespace storm {
namespace modelchecker {
namespace helper {
template <typename ValueType, typename Model, bool Nondeterministic>
SparseLTLHelper<ValueType, Model, Nondeterministic>::SparseLTLHelper(Model const& model, storm::storage::SparseMatrix<ValueType> const& transitionMatrix) : _model(model), _transitionMatrix(transitionMatrix) {
template <typename ValueType, bool Nondeterministic>
SparseLTLHelper<ValueType, Nondeterministic>::SparseLTLHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::size_t numberOfStates) : _transitionMatrix(transitionMatrix), _numberOfStates(numberOfStates) {
// Intentionally left empty.
}
template<typename ValueType, typename Model, bool Nondeterministic>
std::vector<ValueType> SparseLTLHelper<ValueType, Model, 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) {
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");
@ -44,14 +41,14 @@ namespace storm {
statesOfInterest = goal.relevantValues();
} else {
// product from all model states
statesOfInterest = storm::storage::BitVector(this->_model.getNumberOfStates(), true);
statesOfInterest = storm::storage::BitVector(this->_numberOfStates, true);
}
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(this->_model, statesOfInterest);
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 "
<< product->getProductModel().getNumberOfTransitions() << " transitions.");
@ -59,7 +56,7 @@ namespace storm {
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);
// this->_model.writeDotToStream(modelDot); // TODO
modelDot.close();
STORM_LOG_TRACE("Writing product model to product.dot");
@ -82,7 +79,7 @@ namespace storm {
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->_model.getNumberOfStates(), storm::utility::zero<ValueType>());
std::vector<ValueType> numericResult(this->_numberOfStates, storm::utility::zero<ValueType>());
return numericResult;
}
@ -108,12 +105,12 @@ namespace storm {
if (acceptingBSCCs == 0) {
STORM_LOG_INFO("No accepting BSCCs, skipping probability computation.");
std::vector<ValueType> numericResult(this->_model.getNumberOfStates(), storm::utility::zero<ValueType>());
std::vector<ValueType> numericResult(this->_numberOfStates, storm::utility::zero<ValueType>());
return numericResult;
}
}
STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs...");
STORM_LOG_INFO("Computing probabilities for reaching accepting components...");
storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true);
@ -124,8 +121,7 @@ namespace storm {
std::vector<ValueType> prodNumericResult;
if (Nondeterministic) {
prodNumericResult
= std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env,
prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env,
std::move(solveGoalProduct),
product->getProductModel().getTransitionMatrix(),
product->getProductModel().getBackwardTransitions(),
@ -145,13 +141,13 @@ namespace storm {
qualitative);
}
std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_model, prodNumericResult);
std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult);
return numericResult;
}
template<typename ValueType, typename RewardModelType, bool Nondeterministic>
std::vector <ValueType> SparseLTLHelper<ValueType, RewardModelType, Nondeterministic>::computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal<ValueType>&& goal, storm::logic::Formula const& ltlFormula, std::map<std::string, storm::storage::BitVector>& apSatSets) {
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) {
STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula);
STORM_LOG_INFO(" in prefix format: " << ltlFormula.toPrefixString());
@ -165,6 +161,7 @@ namespace storm {
std::vector<ValueType> numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSatSets, this->isQualitativeSet());
// TODO
/*
if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) {
// compute 1-Pmax[!ltl]
@ -177,13 +174,13 @@ namespace storm {
return numericResult;
}
template class SparseLTLHelper<double, storm::models::sparse::Dtmc<double>, false>;
template class SparseLTLHelper<double, storm::models::sparse::Mdp<double>, true>;
template class SparseLTLHelper<double, false>;
template class SparseLTLHelper<double, true>;
#ifdef STORM_HAVE_CARL
template class SparseLTLHelper<storm::RationalNumber, storm::models::sparse::Dtmc<storm::RationalNumber>, false>;
template class SparseLTLHelper<storm::RationalNumber, storm::models::sparse::Mdp<storm::RationalNumber>, true>;
template class SparseLTLHelper<storm::RationalFunction, storm::models::sparse::Dtmc<storm::RationalFunction>, false>;
template class SparseLTLHelper<storm::RationalNumber, false>;
template class SparseLTLHelper<storm::RationalNumber, true>;
template class SparseLTLHelper<storm::RationalFunction, false>;
#endif

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

@ -1,15 +1,13 @@
#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h"
#include "storm/automata/DeterministicAutomaton.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/solver/SolveGoal.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
namespace storm {
namespace automata {
// fwd
class DeterministicAutomaton;
}
namespace modelchecker {
namespace helper {
@ -18,14 +16,21 @@ namespace storm {
* @tparam ValueType the type a value can have
* @tparam Nondeterministic true if there is nondeterminism in the Model (MDP)
*/
template<typename ValueType, typename Model, bool Nondeterministic> // todo remove Model
template<typename ValueType, bool Nondeterministic>
class SparseLTLHelper: public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
public:
/*!
* The type of the product automaton model // todo
*/
using productModelType = typename std::conditional<Nondeterministic, storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Dtmc<ValueType>>::type;
/*!
* Initializes the helper for a discrete time (i.e. DTMC, MDP)
*/
SparseLTLHelper(Model const& model, storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
SparseLTLHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::size_t numberOfSates);
/*!
@ -44,7 +49,7 @@ namespace storm {
private:
storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
Model const& _model; // todo remove ?
std::size_t _numberOfStates;
};
}

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

@ -162,7 +162,7 @@ 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 instead: std::map<std::string, storm::storage::BitVector> apSets = storm::modelchecker::helper::computeApSets(env, checkTask);
// todo apSets = computeApSets(env, checkTask);
for (auto& p : extracted) {
STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
@ -177,7 +177,7 @@ namespace storm {
const SparseDtmcModelType& dtmc = this->getModel();
storm::modelchecker::helper::SparseLTLHelper<ValueType, SparseDtmcModelType, false> helper(dtmc, dtmc.getTransitionMatrix());
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);

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

@ -219,7 +219,7 @@ namespace storm {
const SparseMdpModelType& mdp = this->getModel();
storm::solver::SolveGoal<ValueType> goal(mdp, subTask);
storm::modelchecker::helper::SparseLTLHelper<ValueType, SparseMdpModelType, true> helper(mdp, mdp.getTransitionMatrix());
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);
@ -233,88 +233,6 @@ namespace storm {
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();

11
src/storm/transformer/DAProductBuilder.h
View File

@ -18,10 +18,15 @@ namespace storm {
template <typename Model>
typename DAProduct<Model>::ptr build(const Model& originalModel, const storm::storage::BitVector& statesOfInterest) const {
typename Product<Model>::ptr product = ProductBuilder<Model>::buildProduct(originalModel, *this, statesOfInterest);
return build<Model>(originalModel.getTransitionMatrix(), statesOfInterest);
}
template <typename Model>
typename DAProduct<Model>::ptr build(const storm::storage::SparseMatrix<typename Model::ValueType>& originalMatrix, const storm::storage::BitVector& statesOfInterest) const { //todo transition matrix
typename Product<Model>::ptr product = ProductBuilder<Model>::buildProduct(originalMatrix, *this, statesOfInterest);
storm::automata::AcceptanceCondition::ptr prodAcceptance
= da.getAcceptance()->lift(product->getProductModel().getNumberOfStates(),
[&product](std::size_t prodState) {return product->getAutomatonState(prodState);});
= da.getAcceptance()->lift(product->getProductModel().getNumberOfStates(),
[&product](std::size_t prodState) {return product->getAutomatonState(prodState);});
return typename DAProduct<Model>::ptr(new DAProduct<Model>(std::move(*product), prodAcceptance));
}

7
src/storm/transformer/Product.h
View File

@ -60,7 +60,12 @@ namespace storm {
template <typename ValueType>
std::vector<ValueType> projectToOriginalModel(const Model& originalModel, const std::vector<ValueType>& prodValues) {
std::vector<ValueType> origValues(originalModel.getNumberOfStates());
return projectToOriginalModel(originalModel.getNumberOfStates(), prodValues);
}
template <typename ValueType>
std::vector<ValueType> projectToOriginalModel(std::size_t numberOfStates, const std::vector<ValueType>& prodValues) {
std::vector<ValueType> origValues(numberOfStates);
for (state_type productState : productModel.getStateLabeling().getStates(productStateOfInterestLabel)) {
state_type originalState = getModelState(productState);
origValues.at(originalState) = prodValues.at(productState);

3
src/storm/transformer/ProductBuilder.h
View File

@ -17,8 +17,7 @@ namespace storm {
typedef storm::storage::SparseMatrix<typename Model::ValueType> matrix_type;
template <typename ProductOperator>
static typename Product<Model>::ptr buildProduct(const Model& originalModel, ProductOperator& prodOp, const storm::storage::BitVector& statesOfInterest) {
const matrix_type& originalMatrix = originalModel.getTransitionMatrix();
static typename Product<Model>::ptr buildProduct(const matrix_type& originalMatrix , ProductOperator& prodOp, const storm::storage::BitVector& statesOfInterest) {
bool deterministic = originalMatrix.hasTrivialRowGrouping();
typedef storm::storage::sparse::state_type state_type;

Write Preview
Loading…
Cancel
Save