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

fixed some warnings and issues and introduce cli switch to select IMCA or UnifPlus

main
dehnert 8 years ago
parent
54ab1c114e
commit
a6046ab0b3
6 changed files with 119 additions and 27 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. 69
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  2. 3
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
  3. 2
      src/storm/settings/SettingsManager.cpp
  4. 32
      src/storm/settings/modules/MarkovAutomatonSettings.cpp
  5. 38
      src/storm/settings/modules/MarkovAutomatonSettings.h
  6. 2
      src/storm/settings/modules/SylvanSettings.h

69
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -10,6 +10,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
#include "storm/settings/modules/MarkovAutomatonSettings.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
@ -134,19 +135,19 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded reachability probabilities is unsupported for this value type.");
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
void SparseMarkovAutomatonCslHelper::printTransitions(std::vector<ValueType> const& exitRateVector, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, std::vector<std::vector<ValueType>>& vd, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu){
std::ofstream logfile("U+logfile.txt", std::ios::app);
auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
auto numberOfStates = fullTransitionMatrix.getRowGroupCount();
logfile << "number of states = num of row group count " << numberOfStates << "\n";
for (int i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) {
for (uint_fast64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) {
logfile << " from node " << i << " ";
auto from = rowGroupIndices[i];
auto to = rowGroupIndices[i+1];
for (auto j = from ; j< to; j++){
for (auto j = from ; j < to; j++){
for (auto &v : fullTransitionMatrix.getRow(j)) {
if (markovianStates[i]){
logfile << v.getValue() *exitRateVector[i] << " -> "<< v.getColumn() << "\t";
@ -160,24 +161,24 @@ namespace storm {
logfile << "\n";
logfile << "vd: \n";
for (int i =0 ; i<vd.size(); i++){
for(int j=0; j<fullTransitionMatrix.getRowGroupCount(); j++){
for (uint_fast64_t i =0 ; i<vd.size(); i++){
for(uint_fast64_t j=0; j<fullTransitionMatrix.getRowGroupCount(); j++){
logfile << vd[i][j] << "\t" ;
}
logfile << "\n";
}
logfile << "\nvu:\n";
for (int i =0 ; i<vu.size(); i++){
for(int j=0; j<fullTransitionMatrix.getRowGroupCount(); j++){
for (uint_fast64_t i =0 ; i<vu.size(); i++){
for(uint_fast64_t j=0; j<fullTransitionMatrix.getRowGroupCount(); j++){
logfile << vu[i][j] << "\t" ;
}
logfile << "\n";
}
logfile << "\nwu\n";
for (int i =0 ; i<wu.size(); i++){
for(int j=0; j<fullTransitionMatrix.getRowGroupCount(); j++){
for (uint_fast64_t i =0 ; i<wu.size(); i++){
for(uint_fast64_t j=0; j<fullTransitionMatrix.getRowGroupCount(); j++){
logfile << wu[i][j] << "\t" ;
}
logfile << "\n";
@ -198,14 +199,14 @@ namespace storm {
return res;
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
void SparseMarkovAutomatonCslHelper::calculateVu(uint64_t k, uint64_t node, ValueType lambda, std::vector<std::vector<ValueType>>& vu, std::vector<std::vector<ValueType>>& wu, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){
if (vu[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation.
uint64_t N = vu.size()-1;
auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
ValueType res =0;
for (long i = k ; i < N ; i++ ){
for (uint_fast64_t i = k ; i < N ; i++ ){
if (wu[N-1-(i-k)][node]==-1){
calculateWu((N-1-(i-k)),node,lambda,wu,fullTransitionMatrix,markovianStates,psiStates);
}
@ -214,11 +215,11 @@ namespace storm {
vu[k][node]=res;
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
void SparseMarkovAutomatonCslHelper::calculateWu(uint64_t k, uint64_t node, ValueType lambda, std::vector<std::vector<ValueType>>& wu, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){
if (wu[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation.
uint64_t N = wu.size()-1;
auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
ValueType res;
if (k==N){
@ -267,7 +268,7 @@ namespace storm {
wu[k][node]=res;
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type=0>
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
void SparseMarkovAutomatonCslHelper::calculateVd(uint64_t k, uint64_t node, ValueType lambda, std::vector<std::vector<ValueType>>& vd, storm::storage::SparseMatrix<ValueType> const& fullTransitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){
std::ofstream logfile("U+logfile.txt", std::ios::app);
@ -275,7 +276,7 @@ namespace storm {
if (vd[k][node]!=-1){return;} //dynamic programming. avoiding multiple calculation.
logfile << "calculating vd for k = " << k << " node "<< node << " \t";
uint64_t N = vd.size()-1;
auto rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
auto const& rowGroupIndices = fullTransitionMatrix.getRowGroupIndices();
ValueType res;
if (k==N){
@ -337,13 +338,15 @@ namespace storm {
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseMarkovAutomatonCslHelper::unifPlus( std::pair<double, double> const& boundsPair, std::vector<ValueType> const& exitRateVector, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates){
STORM_LOG_TRACE("Using UnifPlus to compute bounded until probabilities.");
std::ofstream logfile("U+logfile.txt", std::ios::app);
ValueType maxNorm = 0;
//bitvectors to identify different kind of states
storm::storage::BitVector const &markovianNonGoalStates = markovianStates & ~psiStates;
storm::storage::BitVector const &probabilisticNonGoalStates = ~markovianStates & ~psiStates;
storm::storage::BitVector const &allStates = markovianStates | ~markovianStates;
// storm::storage::BitVector const &markovianNonGoalStates = markovianStates & ~psiStates;
// storm::storage::BitVector const &probabilisticNonGoalStates = ~markovianStates & ~psiStates;
storm::storage::BitVector allStates(markovianStates.size(), true);
//vectors to save calculation
std::vector<std::vector<ValueType>> vd,vu,wu;
@ -371,7 +374,7 @@ namespace storm {
N = ceil(lambda*T*exp(2)-log(kappa*epsilon));
// (3) uniform - just applied to markovian states
for (int i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) {
for (uint_fast64_t i = 0; i < fullTransitionMatrix.getRowGroupCount(); i++) {
if (!markovianStates[i]) {
continue;
}
@ -428,15 +431,15 @@ namespace storm {
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
return unifPlus(boundsPair, exitRateVector, transitionMatrix, markovianStates, psiStates);
/*
std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilitiesImca(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
STORM_LOG_TRACE("Using IMCA's technique to compute bounded until probabilities.");
uint64_t numberOfStates = transitionMatrix.getRowGroupCount();
// 'Unpack' the bounds to make them more easily accessible.
double lowerBound = boundsPair.first;
double upperBound = boundsPair.second;
// (1) Compute the accuracy we need to achieve the required error bound.
ValueType maxExitRate = 0;
for (auto value : exitRateVector) {
@ -489,7 +492,21 @@ namespace storm {
storm::utility::vector::setVectorValues(result, probabilisticNonGoalStates, vProbabilistic);
storm::utility::vector::setVectorValues(result, markovianNonGoalStates, vMarkovian);
return result;
}*/
}
}
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
auto const& markovAutomatonSettings = storm::settings::getModule<storm::settings::modules::MarkovAutomatonSettings>();
if (markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::Imca) {
return computeBoundedUntilProbabilitiesImca(dir, transitionMatrix, exitRateVector, markovianStates, psiStates, boundsPair, minMaxLinearEquationSolverFactory);
} else {
STORM_LOG_ASSERT(markovAutomatonSettings.getTechnique() == storm::settings::modules::MarkovAutomatonSettings::BoundedReachabilityTechnique::UnifPlus, "Unknown solution technique.");
// Why is optimization direction not passed?
return unifPlus(boundsPair, exitRateVector, transitionMatrix, markovianStates, psiStates);
}
}
template <typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type>

3
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h
View File

@ -33,6 +33,9 @@ namespace storm {
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
static std::vector<ValueType> computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
static std::vector<ValueType> computeBoundedUntilProbabilitiesImca(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
template <typename ValueType, typename std::enable_if<!storm::NumberTraits<ValueType>::SupportsExponential, int>::type = 0>
static std::vector<ValueType> computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);

2
src/storm/settings/SettingsManager.cpp
View File

@ -37,6 +37,7 @@
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/settings/modules/MultiObjectiveSettings.h"
#include "storm/settings/modules/MarkovAutomatonSettings.h"
#include "storm/utility/macros.h"
#include "storm/utility/file.h"
#include "storm/settings/Option.h"
@ -534,6 +535,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
storm::settings::addModule<storm::settings::modules::JitBuilderSettings>();
storm::settings::addModule<storm::settings::modules::MultiObjectiveSettings>();
storm::settings::addModule<storm::settings::modules::MarkovAutomatonSettings>();
}
}

32
src/storm/settings/modules/MarkovAutomatonSettings.cpp
View File

@ -0,0 +1,32 @@
#include "storm/settings/modules/MarkovAutomatonSettings.h"
#include "storm/settings/Option.h"
#include "storm/settings/OptionBuilder.h"
#include "storm/settings/ArgumentBuilder.h"
#include "storm/settings/Argument.h"
#include "storm/settings/SettingsManager.h"
namespace storm {
namespace settings {
namespace modules {
const std::string MarkovAutomatonSettings::moduleName = "ma";
const std::string MarkovAutomatonSettings::techniqueOptionName = "technique";
MarkovAutomatonSettings::MarkovAutomatonSettings() : ModuleSettings(moduleName) {
std::vector<std::string> techniques = {"imca", "unifplus"};
this->addOption(storm::settings::OptionBuilder(moduleName, techniqueOptionName, true, "The technique to use to solve bounded reachability queries.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the technique to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(techniques)).setDefaultValueString("imca").build()).build());
}
MarkovAutomatonSettings::BoundedReachabilityTechnique MarkovAutomatonSettings::getTechnique() const {
std::string techniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (techniqueAsString == "imca") {
return MarkovAutomatonSettings::BoundedReachabilityTechnique::Imca;
}
return MarkovAutomatonSettings::BoundedReachabilityTechnique::UnifPlus;
}
}
}
}

38
src/storm/settings/modules/MarkovAutomatonSettings.h
View File

@ -0,0 +1,38 @@
#pragma once
#include "storm/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for Sylvan.
*/
class MarkovAutomatonSettings : public ModuleSettings {
public:
enum class BoundedReachabilityTechnique { Imca, UnifPlus };
/*!
* Creates a new set of Markov automaton settings.
*/
MarkovAutomatonSettings();
/*!
* Retrieves the technique to use to solve bounded reachability properties.
*
* @return The selected technique.
*/
BoundedReachabilityTechnique getTechnique() const;
// The name of the module.
static const std::string moduleName;
private:
// Define the string names of the options as constants.
static const std::string techniqueOptionName;
};
}
}
}

2
src/storm/settings/modules/SylvanSettings.h
View File

@ -13,7 +13,7 @@ namespace storm {
class SylvanSettings : public ModuleSettings {
public:
/*!
* Creates a new set of CUDD settings.
* Creates a new set of Sylvan settings.
*/
SylvanSettings();

Write Preview
Loading…
Cancel
Save