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

added an option for polic extraction to the helper, some includes 

Former-commit-id: 44b6a5d03f
main
sjunges 10 years ago
parent
2dc9eb9b83
commit
f08f66e900
8 changed files with 26 additions and 21 deletions
Unified View
  1. 2
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  2. 4
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  3. 2
      src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  4. 12
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
  5. 8
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  6. 11
      src/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
  7. 6
      src/solver/SolveGoal.cpp
  8. 2
      src/utility/solver.cpp

2
src/counterexamples/MILPMinimalLabelSetGenerator.h
View File

@ -934,7 +934,7 @@ namespace storm {
double maximalReachabilityProbability = 0; double maximalReachabilityProbability = 0;
if (checkThresholdFeasible) { if (checkThresholdFeasible) {
storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelcheckerHelper; storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelcheckerHelper;
std::vector<T> result = modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()); std::vector<T> result = std::move(modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()).result);
for (auto state : labeledMdp.getInitialStates()) { for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
} }

4
src/counterexamples/SMTMinimalCommandSetGenerator.h
View File

@ -1628,7 +1628,7 @@ namespace storm {
if (checkThresholdFeasible) { if (checkThresholdFeasible) {
storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper; storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper;
LOG4CPLUS_DEBUG(logger, "Invoking model checker."); LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
std::vector<T> result = modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()); std::vector<T> result = std::move(modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()).result);
for (auto state : labeledMdp.getInitialStates()) { for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
} }
@ -1692,7 +1692,7 @@ namespace storm {
storm::models::sparse::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::models::sparse::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet);
storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper; storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper;
LOG4CPLUS_DEBUG(logger, "Invoking model checker."); LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
std::vector<T> result = modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()); std::vector<T> result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()).result);
LOG4CPLUS_DEBUG(logger, "Computed model checking results."); LOG4CPLUS_DEBUG(logger, "Computed model checking results.");
totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock;

2
src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -184,7 +184,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { std::vector<ValueType> SparseMarkovAutomatonCslHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
return storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); return std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, false, minMaxLinearEquationSolverFactory).result);
} }
template <typename ValueType> template <typename ValueType>

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

@ -68,8 +68,8 @@ namespace storm {
std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula()); std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult))); return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.result)));
} }
template<typename SparseMdpModelType> template<typename SparseMdpModelType>
@ -81,13 +81,13 @@ namespace storm {
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
if(qualitative | !bound) { if(qualitative | !bound) {
// For qualitative checks, or if the , we use the standard approach. // For qualitative checks, or if the , we use the standard approach.
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(optimalityType.get(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult))); return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.result)));
} else { } else {
// With a given bound, we only iterate until we pass the bound. // With a given bound, we only iterate until we pass the bound.
storm::solver::BoundedGoal<ValueType> boundedGoal(optimalityType.get(), bound.get(), this->getModel().getInitialStates() ); storm::solver::BoundedGoal<ValueType> boundedGoal(optimalityType.get(), bound.get(), this->getModel().getInitialStates() );
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(boundedGoal, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, *minMaxLinearEquationSolverFactory); auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(boundedGoal, this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative, false, *minMaxLinearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult))); return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.result)));
} }
} }

8
src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -71,7 +71,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal const& 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, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(storm::solver::SolveGoal const& 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 getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
uint_fast64_t numberOfStates = transitionMatrix.getRowCount(); uint_fast64_t numberOfStates = transitionMatrix.getRowCount();
@ -126,14 +126,14 @@ namespace storm {
} }
} }
return result; return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(result));
} }
template<typename ValueType> template<typename ValueType>
std::vector<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) { MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, 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 getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
storm::solver::SolveGoal goal(dir); storm::solver::SolveGoal goal(dir);
return computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, minMaxLinearEquationSolverFactory); return std::move(computeUntilProbabilities(goal, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, getPolicy, minMaxLinearEquationSolverFactory));
} }

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

@ -4,8 +4,8 @@
#include <vector> #include <vector>
#include "src/storage/SparseMatrix.h" #include "src/storage/SparseMatrix.h"
#include "src/storage/BitVector.h"
#include "src/storage/MaximalEndComponent.h" #include "src/storage/MaximalEndComponent.h"
#include "MDPModelCheckingHelperReturnType.h"
#include "src/utility/solver.h" #include "src/utility/solver.h"
#include "src/solver/SolveGoal.h" #include "src/solver/SolveGoal.h"
@ -13,6 +13,10 @@
#include "src/adapters/CarlAdapter.h" #include "src/adapters/CarlAdapter.h"
namespace storm { namespace storm {
namespace storage {
class BitVector;
}
namespace models { namespace models {
namespace sparse { namespace sparse {
template <typename ValueType> template <typename ValueType>
@ -30,10 +34,9 @@ namespace storm {
static std::vector<ValueType> computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); static std::vector<ValueType> computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(OptimizationDirection dir, 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 getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(storm::solver::SolveGoal const& 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 getPolicy, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
static std::vector<ValueType> computeUntilProbabilities(storm::solver::SolveGoal const& 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, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
template<typename RewardModelType> template<typename RewardModelType>
static std::vector<ValueType> computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory); static std::vector<ValueType> computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount, storm::utility::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);

6
src/solver/SolveGoal.cpp
View File

@ -1,10 +1,14 @@
#include "SolveGoal.h" #include "SolveGoal.h"
#include "src/storage/SparseMatrix.h"
#include "src/utility/solver.h" #include "src/utility/solver.h"
#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h"
#include <memory>
namespace storm { namespace storm {
namespace storage {
template <typename VT> class SparseMatrix;
}
namespace solver { namespace solver {
template<typename VT> template<typename VT>

2
src/utility/solver.cpp
View File

@ -87,7 +87,6 @@ namespace storm {
{ {
prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS; prefTech = storm::solver::MinMaxTechniqueSelection::FROMSETTINGS;
setSolverType(solver); setSolverType(solver);
std::cout << toString(prefTech) << std::endl;
} }
template<typename ValueType> template<typename ValueType>
@ -108,7 +107,6 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy) const { std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> MinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix, bool trackPolicy) const {
std::cout << toString(prefTech) << std::endl;
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p1; std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> p1;
switch (solverType) { switch (solverType) {

Write Preview
|||||||
100:0
Loading…
Cancel
Save