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

Merge branch 'master' into multi-objective

main
TimQu 8 years ago
parent
5073d243ea f02ffd9d5b
commit
4e8f05dd0b
35 changed files with 435 additions and 205 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. 20
      resources/examples/testfiles/ma/jobscheduler.ma
  2. 4
      resources/examples/testfiles/mdp/multiobj_team3.nm
  3. 60
      src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
  4. 16
      src/storm-dft/modelchecker/dft/DFTModelChecker.h
  5. 7
      src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
  6. 4
      src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h
  7. 9
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  8. 6
      src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h
  9. 21
      src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
  10. 2
      src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h
  11. 74
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  12. 14
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h
  13. 2
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
  14. 15
      src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
  15. 4
      src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
  16. 9
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  17. 1
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  18. 21
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
  19. 5
      src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h
  20. 10
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  21. 6
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
  22. 35
      src/storm/models/sparse/StandardRewardModel.cpp
  23. 6
      src/storm/models/sparse/StandardRewardModel.h
  24. 8
      src/storm/models/symbolic/StandardRewardModel.cpp
  25. 6
      src/storm/models/symbolic/StandardRewardModel.h
  26. 51
      src/storm/parser/FormulaParserGrammar.cpp
  27. 9
      src/storm/storage/dd/Add.cpp
  28. 12
      src/storm/storage/dd/cudd/InternalCuddAdd.cpp
  29. 13
      src/storm/storage/dd/cudd/InternalCuddBdd.cpp
  30. 12
      src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
  31. 12
      src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp
  32. 7
      src/storm/storm.cpp
  33. 121
      src/storm/utility/Stopwatch.h
  34. 26
      src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp
  35. 12
      src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp

20
resources/examples/testfiles/ma/jobscheduler.ma
View File

@ -5,34 +5,28 @@
// Please cite Quatmann et al: Multi-objective Model Checking of Markov Automata
ma
const int x_j1 = 1;
const int x_j2 = 2;
const int x_j3 = 3;
const double x_j1 = 1.0;
const double x_j2 = 2.0;
const double x_j3 = 3.0;
formula is_running = r_j1 + r_j2 + r_j3 > 0;
formula num_finished = f_j1 + f_j2 + f_j3;
module main
r_j1 : [0..1];
r_j2 : [0..1];
r_j3 : [0..1];
f_j1 : [0..1];
f_j2 : [0..1];
f_j3 : [0..1];
<> (r_j1 = 1) -> x_j1 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j1' = 1);
<> (r_j2 = 1) -> x_j2 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j2' = 1);
<> (r_j3 = 1) -> x_j3 : (r_j1' = 0) & (r_j2' = 0) & (r_j3' = 0) & (f_j3' = 1);
[] (!is_running) & (num_finished = 2) & (f_j1 = 0) -> 1: (r_j1' = 1);
[] (!is_running) & (num_finished = 2) & (f_j2 = 0) -> 1: (r_j2' = 1);
[] (!is_running) & (num_finished = 2) & (f_j3 = 0) -> 1: (r_j3' = 1);
[] (!is_running) & (num_finished <= 1) & (f_j1 = 0) & (f_j2 = 0) -> 1: (r_j1' = 1) & (r_j2' = 1);
[] (!is_running) & (num_finished <= 1) & (f_j1 = 0) & (f_j3 = 0) -> 1: (r_j1' = 1) & (r_j3' = 1);
[] (!is_running) & (num_finished <= 1) & (f_j2 = 0) & (f_j3 = 0) -> 1: (r_j2' = 1) & (r_j3' = 1);
endmodule
init
r_j1 = 0 &
r_j2 = 0 &
@ -40,4 +34,10 @@ init
f_j1 = 0 &
f_j2 = 0 &
f_j3 = 0
endinit
endinit
label "all_jobs_finished" = num_finished=3;
label "half_of_jobs_finished" = num_finished=2;
label "slowest_before_fastest" = f_j1=1 & f_j3=0;
rewards "avg_waiting_time"
true : (3-num_finished)/3;
endrewards

4
resources/examples/testfiles/mdp/multiobj_team3.nm
View File

@ -271,6 +271,10 @@ formula agent3_joins_successful_team_of_1 = (task1_completed & m3_t1=1 & team_si
formula agent3_joins_successful_team_of_2 = (task1_completed & m3_t1=1 & team_size_t1=2) | (task2_completed & m3_t2=1 & team_size_t2=2);
formula agent3_joins_successful_team_of_3 = (task1_completed & m3_t1=1 & team_size_t1=3) | (task2_completed & m3_t2=1 & team_size_t2=3);
label "task1_compl" = task1_completed;
label "task2_compl" = task2_completed;
// rewards
rewards "w_1_total"
[] agent1_joins_successful_team : 1;

60
src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
View File

@ -20,13 +20,8 @@ namespace storm {
template<typename ValueType>
void DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) {
// Initialize
this->explorationTime = std::chrono::duration<double>::zero();
this->buildingTime = std::chrono::duration<double>::zero();
this->bisimulationTime = std::chrono::duration<double>::zero();
this->modelCheckingTime = std::chrono::duration<double>::zero();
this->totalTime = std::chrono::duration<double>::zero();
this->approximationError = approximationError;
totalStart = std::chrono::high_resolution_clock::now();
totalTimer.start();
// Optimizing DFT
storm::storage::DFT<ValueType> dft = origDft.optimize();
@ -44,7 +39,7 @@ namespace storm {
checkResult = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
}
this->totalTime = std::chrono::high_resolution_clock::now() - totalStart;
totalTimer.stop();
}
template<typename ValueType>
@ -191,7 +186,7 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> composedModel;
for (auto const ft : dfts) {
STORM_LOG_INFO("Building Model via parallel composition...");
std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
explorationTimer.start();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@ -212,7 +207,7 @@ namespace storm {
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
explorationTimer.stop();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
@ -227,10 +222,10 @@ namespace storm {
}
// Apply bisimulation
std::chrono::high_resolution_clock::time_point bisimulationStart = std::chrono::high_resolution_clock::now();
bisimulationTimer.start();
composedModel = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now();
bisimulationTime += bisimulationEnd - bisimulationStart;
bisimulationTimer.stop();
STORM_LOG_INFO("No. states (Composed): " << composedModel->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Composed): " << composedModel->getNumberOfTransitions());
@ -247,7 +242,7 @@ namespace storm {
// If we are here, no composition was possible
STORM_LOG_ASSERT(!modularisationPossible, "Modularisation should not be possible.");
std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
explorationTimer.start();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
storm::storage::DFTIndependentSymmetries symmetries(emptySymmetry);
@ -268,7 +263,7 @@ namespace storm {
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
explorationTimer.stop();
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc), storm::exceptions::NotSupportedException, "Parallel composition only applicable for CTMCs");
return model->template as<storm::models::sparse::Ctmc<ValueType>>();
@ -276,7 +271,7 @@ namespace storm {
template<typename ValueType>
typename DFTModelChecker<ValueType>::dft_result DFTModelChecker<ValueType>::checkDFT(storm::storage::DFT<ValueType> const& dft, std::shared_ptr<const storm::logic::Formula> const& formula, bool symred, bool enableDC, double approximationError) {
std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now();
explorationTimer.start();
// Find symmetries
std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
@ -302,12 +297,14 @@ namespace storm {
size_t iteration = 0;
do {
// Iteratively build finer models
std::chrono::high_resolution_clock::time_point explorationStart = std::chrono::high_resolution_clock::now();
if (iteration > 0) {
explorationTimer.start();
}
STORM_LOG_INFO("Building model...");
// TODO Matthias refine model using existing model and MC results
builder.buildModel(labeloptions, iteration, approximationError);
std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now();
explorationTime += explorationEnd - explorationStart;
explorationTimer.stop();
buildingTimer.start();
// TODO Matthias: possible to do bisimulation on approximated model and not on concrete one?
@ -317,7 +314,7 @@ namespace storm {
// We only output the info from the lower bound as the info for the upper bound is the same
STORM_LOG_INFO("No. states: " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions());
buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd;
buildingTimer.stop();
// Check lower bound
std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
@ -328,9 +325,9 @@ namespace storm {
// Build model for upper bound
STORM_LOG_INFO("Getting model for upper bound...");
explorationEnd = std::chrono::high_resolution_clock::now();
buildingTimer.start();
model = builder.getModelApproximation(probabilityFormula ? true : false);
buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd;
buildingTimer.stop();
// Check upper bound
result = checkModel(model, formula);
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
@ -340,8 +337,9 @@ namespace storm {
++iteration;
STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")");
totalTime = std::chrono::high_resolution_clock::now() - totalStart;
totalTimer.stop();
printTimings();
totalTimer.start();
STORM_LOG_THROW(!storm::utility::isInfinity<ValueType>(approxResult.first) && !storm::utility::isInfinity<ValueType>(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity.");
} while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula));
@ -365,7 +363,7 @@ namespace storm {
//model->printModelInformationToStream(std::cout);
STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions());
explorationTime += std::chrono::high_resolution_clock::now() - checkingStart;
explorationTimer.stop();
// Model checking
std::unique_ptr<storm::modelchecker::CheckResult> result = checkModel(model, formula);
@ -377,22 +375,22 @@ namespace storm {
template<typename ValueType>
std::unique_ptr<storm::modelchecker::CheckResult> DFTModelChecker<ValueType>::checkModel(std::shared_ptr<storm::models::sparse::Model<ValueType>>& model, std::shared_ptr<const storm::logic::Formula> const& formula) {
// Bisimulation
std::chrono::high_resolution_clock::time_point bisimulationStart = std::chrono::high_resolution_clock::now();
bisimulationTimer.start();
if (model->isOfType(storm::models::ModelType::Ctmc) && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
STORM_LOG_INFO("Bisimulation...");
model = storm::performDeterministicSparseBisimulationMinimization<storm::models::sparse::Ctmc<ValueType>>(model->template as<storm::models::sparse::Ctmc<ValueType>>(), {formula}, storm::storage::BisimulationType::Weak)->template as<storm::models::sparse::Ctmc<ValueType>>();
STORM_LOG_INFO("No. states (Bisimulation): " << model->getNumberOfStates());
STORM_LOG_INFO("No. transitions (Bisimulation): " << model->getNumberOfTransitions());
}
std::chrono::high_resolution_clock::time_point bisimulationEnd = std::chrono::high_resolution_clock::now();
bisimulationTime += bisimulationEnd - bisimulationStart;
bisimulationTimer.stop();
modelCheckingTimer.start();
// Check the model
STORM_LOG_INFO("Model checking...");
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula));
STORM_LOG_INFO("Model checking done.");
STORM_LOG_ASSERT(result, "Result does not exist.");
modelCheckingTime += std::chrono::high_resolution_clock::now() - bisimulationEnd;
modelCheckingTimer.stop();
return result;
}
@ -414,11 +412,11 @@ namespace storm {
template<typename ValueType>
void DFTModelChecker<ValueType>::printTimings(std::ostream& os) {
os << "Times:" << std::endl;
os << "Exploration:\t" << explorationTime.count() << std::endl;
os << "Building:\t" << buildingTime.count() << std::endl;
os << "Bisimulation:\t" << bisimulationTime.count() << std::endl;
os << "Modelchecking:\t" << modelCheckingTime.count() << std::endl;
os << "Total:\t\t" << totalTime.count() << std::endl;
os << "Exploration:\t" << explorationTimer.getTimeSeconds() << "s" << std::endl;
os << "Building:\t" << buildingTimer.getTimeSeconds() << "s" << std::endl;
os << "Bisimulation:\t" << bisimulationTimer.getTimeSeconds() << "s" << std::endl;
os << "Modelchecking:\t" << modelCheckingTimer.getTimeSeconds() << "s" << std::endl;
os << "Total:\t\t" << totalTimer.getTimeSeconds() << "s" << std::endl;
}
template<typename ValueType>

16
src/storm-dft/modelchecker/dft/DFTModelChecker.h
View File

@ -3,11 +3,10 @@
#include "storm/logic/Formula.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/utility/storm.h" // TODO this should not be included here.
#include "storm/utility/Stopwatch.h"
#include "storm-dft/storage/dft/DFT.h"
#include <chrono>
namespace storm {
namespace modelchecker {
@ -57,12 +56,11 @@ namespace storm {
private:
// Timing values
std::chrono::duration<double> buildingTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> explorationTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> bisimulationTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> modelCheckingTime = std::chrono::duration<double>::zero();
std::chrono::duration<double> totalTime = std::chrono::duration<double>::zero();
std::chrono::high_resolution_clock::time_point totalStart;
storm::utility::Stopwatch buildingTimer;
storm::utility::Stopwatch explorationTimer;
storm::utility::Stopwatch bisimulationTimer;
storm::utility::Stopwatch modelCheckingTimer;
storm::utility::Stopwatch totalTimer;
// Model checking result
dft_result checkResult;
@ -137,4 +135,4 @@ namespace storm {
};
}
}
}

7
src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp
View File

@ -29,7 +29,7 @@ namespace storm {
template<typename ModelType>
bool HybridCtmcCslModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true));
return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true));
}
template<typename ModelType>
@ -110,6 +110,11 @@ namespace storm {
return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory);
}
template<typename ModelType>
std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<ModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
return storm::modelchecker::helper::HybridCtmcCslHelper<DdType, ValueType>::computeLongRunAverageRewards(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), *linearEquationSolverFactory);
}
// Explicitly instantiate the model checker.
template class HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD, double>>;
template class HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<storm::dd::DdType::Sylvan, double>>;

4
src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h
View File

@ -24,10 +24,12 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
private:
// An object that is used for solving linear equations and performing matrix-vector multiplication.

9
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -42,7 +42,7 @@ namespace storm {
template<typename CValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type>
bool SparseCtmcCslModelChecker<SparseCtmcModelType>::canHandleImplementation(CheckTask<storm::logic::Formula, CValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true));
return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true));
}
template <typename SparseCtmcModelType>
@ -133,6 +133,13 @@ namespace storm {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
storm::storage::SparseMatrix<ValueType> probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector());
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(probabilityMatrix, checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), &this->getModel().getExitRateVector(), *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template <typename SparseCtmcModelType>
std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) {
storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();

6
src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h
View File

@ -26,11 +26,13 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(CheckTask<storm::logic::BoundedUntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
private:
template<typename CValueType = ValueType, typename std::enable_if<storm::NumberTraits<CValueType>::SupportsExponential, int>::type = 0>

21
src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp
View File

@ -224,7 +224,7 @@ namespace storm {
STORM_LOG_THROW(rewardModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Create ODD for the translation.
storm::dd::Odd odd =model.getReachableStates().createOdd();
storm::dd::Odd odd = model.getReachableStates().createOdd();
// Initialize result to state rewards of the model.
std::vector<ValueType> result = rewardModel.getStateRewardVector().toVector(odd);
@ -267,7 +267,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
// Then compute the state reward vector to use in the computation.
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector);
storm::dd::Add<DdType, ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false);
std::vector<ValueType> explicitTotalRewardVector = totalRewardVector.toVector(odd);
// Finally, compute the transient probabilities.
@ -290,6 +290,23 @@ namespace storm {
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}
template<storm::dd::DdType DdType, class ValueType>
std::unique_ptr<CheckResult> HybridCtmcCslHelper<DdType, ValueType>::computeLongRunAverageRewards(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
storm::dd::Add<DdType, ValueType> probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector);
// Create ODD for the translation.
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd);
std::vector<ValueType> explicitExitRateVector = exitRateVector.toVector(odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector, linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}
template<storm::dd::DdType DdType, class ValueType>
storm::dd::Add<DdType, ValueType> HybridCtmcCslHelper<DdType, ValueType>::computeUniformizedMatrix(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, storm::dd::Bdd<DdType> const& maybeStates, ValueType uniformizationRate) {
STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << ".");

2
src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h
View File

@ -32,6 +32,8 @@ namespace storm {
static std::unique_ptr<CheckResult> computeNextProbabilities(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, storm::dd::Bdd<DdType> const& nextStates);
static std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::models::symbolic::Ctmc<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& rateMatrix, storm::dd::Add<DdType, ValueType> const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
/*!
* Converts the given rate-matrix into a time-abstract probability matrix.
*

74
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -208,7 +208,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has a state-based reward this->getModel().
// Only compute the result if the model has a state-based reward model.
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
uint_fast64_t numberOfStates = rateMatrix.getRowCount();
@ -239,7 +239,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
std::vector<ValueType> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has a state-based reward this->getModel().
// Only compute the result if the model has a state-based reward model.
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
uint_fast64_t numberOfStates = rateMatrix.getRowCount();
@ -262,7 +262,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector);
// Compute the total state reward vector.
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector);
std::vector<ValueType> totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector, false);
// Finally, compute the transient probabilities.
return computeTransientProbabilities<ValueType, true>(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory);
@ -331,6 +331,7 @@ namespace storm {
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// If there are no goal states, we avoid the computation and directly return zero.
uint_fast64_t numberOfStates = probabilityMatrix.getRowCount();
if (psiStates.empty()) {
@ -342,7 +343,43 @@ namespace storm {
return std::vector<ValueType>(numberOfStates, storm::utility::one<ValueType>());
}
// Start by decomposing the DTMC into its BSCCs.
ValueType zero = storm::utility::zero<ValueType>();
ValueType one = storm::utility::one<ValueType>();
return computeLongRunAverages<ValueType>(probabilityMatrix,
[&zero, &one, &psiStates] (storm::storage::sparse::state_type const& state) -> ValueType {
if (psiStates.get(state)) {
return one;
}
return zero;
},
exitRateVector,
linearEquationSolverFactory);
}
template <typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, RewardModelType const& rewardModel, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has a state-based reward model.
STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
return computeLongRunAverageRewards(probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector, true), exitRateVector, linearEquationSolverFactory);
}
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, std::vector<ValueType> const& stateRewardVector, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return computeLongRunAverages<ValueType>(probabilityMatrix,
[&stateRewardVector] (storm::storage::sparse::state_type const& state) -> ValueType {
return stateRewardVector[state];
},
exitRateVector,
linearEquationSolverFactory);
}
template <typename ValueType>
std::vector<ValueType> SparseCtmcCslHelper::computeLongRunAverages(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, std::function<ValueType (storm::storage::sparse::state_type const& state)> const& valueGetter, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory){
uint_fast64_t numberOfStates = probabilityMatrix.getRowCount();
// Start by decomposing the CTMC into its BSCCs.
storm::storage::StronglyConnectedComponentDecomposition<ValueType> bsccDecomposition(probabilityMatrix, storm::storage::BitVector(probabilityMatrix.getRowCount(), true), false, true);
STORM_LOG_DEBUG("Found " << bsccDecomposition.size() << " BSCCs.");
@ -448,7 +485,7 @@ namespace storm {
storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[bsccIndex];
for (auto const& state : bscc) {
bsccEquationSystemSolution[indexInStatesInBsccs[state]] = one / bscc.size();
bsccEquationSystemSolution[indexInStatesInBsccs[state]] = one / bscc.size();
}
}
@ -459,6 +496,12 @@ namespace storm {
solver->solveEquations(bsccEquationSystemSolution, bsccEquationSystemRightSide);
}
// std::vector<ValueType> tmp(probabilityMatrix.getRowCount(), storm::utility::zero<ValueType>());
// probabilityMatrix.multiplyVectorWithMatrix(bsccEquationSystemSolution, tmp);
// for (uint64_t i = 0; i < tmp.size(); ++i) {
// std::cout << tmp[i] << " vs. " << bsccEquationSystemSolution[i] << std::endl;
// }
// If exit rates were given, we need to 'fix' the results to also account for the timing behaviour.
if (exitRateVector != nullptr) {
std::vector<ValueType> bsccTotalValue(bsccDecomposition.size(), zero);
@ -470,14 +513,17 @@ namespace storm {
bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] = (bsccEquationSystemSolution[indexInStatesInBsccs[*stateIter]] * (one / (*exitRateVector)[*stateIter])) / bsccTotalValue[stateToBsccIndexMap[indexInStatesInBsccs[*stateIter]]];
}
}
// for (auto const& val : bsccEquationSystemSolution) {
// std::cout << "val: " << val << std::endl;
// }
// Calculate LRA Value for each BSCC from steady state distribution in BSCCs.
for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) {
storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[bsccIndex];
for (auto const& state : bscc) {
if (psiStates.get(state)) {
bsccLra[stateToBsccIndexMap[indexInStatesInBsccs[state]]] += bsccEquationSystemSolution[indexInStatesInBsccs[state]];
}
bsccLra[stateToBsccIndexMap[indexInStatesInBsccs[state]]] += valueGetter(state) * bsccEquationSystemSolution[indexInStatesInBsccs[state]];
}
}
@ -490,9 +536,7 @@ namespace storm {
// At this point, all BSCCs are known to contain exactly one state, which is why we can set all values
// directly (based on whether or not the contained state is a psi state).
if (psiStates.get(*bscc.begin())) {
bsccLra[bsccIndex] = storm::utility::one<ValueType>();
}
bsccLra[bsccIndex] = valueGetter(*bscc.begin());
}
for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) {
@ -700,6 +744,8 @@ namespace storm {
template std::vector<double> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<double> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<double> const* exitRateVector, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<double> const& probabilityMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, std::vector<double> const* exitRateVector, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<double> const& probabilityMatrix, std::vector<double> const& stateRewardVector, std::vector<double> const* exitRateVector, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
@ -728,6 +774,12 @@ namespace storm {
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::models::sparse::StandardRewardModel<RationalNumber> const& rewardModel, std::vector<storm::RationalNumber> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::models::sparse::StandardRewardModel<RationalFunction> const& rewardModel, std::vector<storm::RationalFunction> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, std::vector<storm::RationalNumber> const& stateRewardVector, std::vector<storm::RationalNumber> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, std::vector<storm::RationalFunction> const& stateRewardVector, std::vector<storm::RationalFunction> const* exitRateVector, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);

14
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h
View File

@ -7,6 +7,8 @@
#include "storm/utility/NumberTraits.h"
#include "storm/storage/sparse/StateType.h"
namespace storm {
namespace modelchecker {
namespace helper {
@ -44,7 +46,13 @@ namespace storm {
template <typename ValueType>
static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
template <typename ValueType, typename RewardModelType>
static std::vector<ValueType> computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, RewardModelType const& rewardModel, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
template <typename ValueType>
static std::vector<ValueType> computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, std::vector<ValueType> const& stateRewardVector, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
template <typename ValueType>
static std::vector<ValueType> computeReachabilityTimes(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
@ -96,6 +104,10 @@ namespace storm {
*/
template <typename ValueType>
static storm::storage::SparseMatrix<ValueType> computeGeneratorMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRates);
private:
template <typename ValueType>
static std::vector<ValueType> computeLongRunAverages(storm::storage::SparseMatrix<ValueType> const& probabilityMatrix, std::function<ValueType (storm::storage::sparse::state_type const& state)> const& valueGetter, std::vector<ValueType> const* exitRateVector, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
};
}
}

2
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp
View File

@ -314,7 +314,7 @@ namespace storm {
template<typename SparseModelType>
void SparsePcaaPreprocessor<SparseModelType>::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective<ValueType>& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type.");
STORM_LOG_THROW(!formula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << ".");
STORM_LOG_THROW(formula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << ".");
// FIXME: really convert to value type?
currentObjective.upperTimeBound = storm::utility::convertNumber<ValueType>(formula.getBound<uint64_t>());

15
src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
View File

@ -38,7 +38,7 @@ namespace storm {
template<typename ModelType>
bool HybridDtmcPrctlModelChecker<ModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true));
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true));
}
template<typename ModelType>
@ -108,13 +108,12 @@ namespace storm {
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
// Create ODD for the translation.
storm::dd::Odd odd = this->getModel().getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), *this->linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero<ValueType>(), this->getModel().getReachableStates(), std::move(odd), std::move(result)));
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory);
}
template<typename ModelType>
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<ModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
return storm::modelchecker::helper::HybridDtmcPrctlHelper<DdType, ValueType>::computeLongRunAverageRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), *this->linearEquationSolverFactory);
}
template class HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD, double>>;

4
src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h
View File

@ -25,10 +25,12 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeNextProbabilities(CheckTask<storm::logic::NextFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) override;
private:
// An object that is used for retrieving linear equation solvers.

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

@ -36,7 +36,7 @@ namespace storm {
template<typename SparseDtmcModelType>
bool SparseDtmcPrctlModelChecker<SparseDtmcModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true));
}
template<typename SparseDtmcModelType>
@ -116,6 +116,13 @@ namespace storm {
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) {
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards<ValueType>(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), nullptr, *linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
}
template<typename SparseDtmcModelType>
std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeConditionalProbabilities(CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) {
storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula();

1
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
View File

@ -31,6 +31,7 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask) override;
virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask) override;
private:
// An object that is used for retrieving linear equation solvers.

21
src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
View File

@ -1,5 +1,6 @@
#include "storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
#include "storm/solver/LinearEquationSolver.h"
@ -247,6 +248,26 @@ namespace storm {
}
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeLongRunAverageProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& targetStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Create ODD for the translation.
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageProbabilities(explicitProbabilityMatrix, targetStates.toVector(odd), linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeLongRunAverageRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Create ODD for the translation.
storm::dd::Odd odd = model.getReachableStates().createOdd();
storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd);
std::vector<ValueType> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory);
return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero<ValueType>(), model.getReachableStates(), std::move(odd), std::move(result)));
}
template class HybridDtmcPrctlHelper<storm::dd::DdType::CUDD, double>;
template class HybridDtmcPrctlHelper<storm::dd::DdType::Sylvan, double>;
}

5
src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h
View File

@ -33,6 +33,11 @@ namespace storm {
static std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeReachabilityRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd<DdType> const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& targetStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::unique_ptr<CheckResult> computeLongRunAverageRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
};
}

10
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -236,6 +236,16 @@ namespace storm {
return SparseCtmcCslHelper::computeLongRunAverageProbabilities<ValueType>(transitionMatrix, psiStates, nullptr, linearEquationSolverFactory);
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return SparseCtmcCslHelper::computeLongRunAverageRewards<ValueType, RewardModelType>(transitionMatrix, rewardModel, nullptr, linearEquationSolverFactory);
}
template<typename ValueType, typename RewardModelType>
std::vector<ValueType> SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& stateRewards, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
return SparseCtmcCslHelper::computeLongRunAverageRewards<ValueType>(transitionMatrix, stateRewards, nullptr, linearEquationSolverFactory);
}
template<typename ValueType, typename RewardModelType>
typename SparseDtmcPrctlHelper<ValueType, RewardModelType>::BaierTransformedModel SparseDtmcPrctlHelper<ValueType, RewardModelType>::computeBaierTransformation(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional<std::vector<ValueType>> const& stateRewards, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {

6
src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h
View File

@ -39,7 +39,11 @@ namespace storm {
static std::vector<ValueType> computeReachabilityRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, std::vector<ValueType> const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory, boost::optional<std::vector<ValueType>> resultHint = boost::none);
static std::vector<ValueType> computeLongRunAverageProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeLongRunAverageRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& stateRewards, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeConditionalProbabilities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
static std::vector<ValueType> computeConditionalRewards(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);

35
src/storm/models/sparse/StandardRewardModel.cpp
View File

@ -165,6 +165,11 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix) const {
if (this->hasStateActionRewards()) {
for (auto const& e : this->getStateActionRewardVector()) {
std::cout << "e " << e << std::endl;
}
}
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result);
@ -177,16 +182,16 @@ namespace storm {
template<typename ValueType>
template<typename MatrixValueType>
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const {
std::vector<ValueType> result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector<ValueType>(transitionMatrix.getRowCount()));
if (!this->hasTransitionRewards() && this->hasStateActionRewards()) {
// If we initialized the result with the state-action rewards we can scale the result in place.
storm::utility::vector::multiplyVectorsPointwise(result, weights, result);
}
if (this->hasStateActionRewards() && this->hasTransitionRewards()) {
// If we initialized the result with the transition rewards and still have state-action rewards,
// we need to add the scaled vector directly.
storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return resultElement + weight * rewardElement; } );
std::vector<ValueType> StandardRewardModel<ValueType>::getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights, bool scaleTransAndActions) const {
std::vector<ValueType> result;
if (this->hasTransitionRewards()) {
result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix());
storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return weight * (resultElement + rewardElement); } );
} else {
result = std::vector<ValueType>(transitionMatrix.getRowCount());
if (this->hasStateActionRewards()) {
storm::utility::vector::applyPointwise<MatrixValueType, ValueType, ValueType>(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return weight * rewardElement; } );
}
}
if (this->hasStateRewards()) {
storm::utility::vector::addVectorToGroupedVector(result, this->getStateRewardVector(), transitionMatrix.getRowGroupIndices());
@ -319,7 +324,7 @@ namespace storm {
// Explicitly instantiate the class.
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights, bool scaleTransAndActions) const;
template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<double>::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue);
template void StandardRewardModel<double>::setStateReward(uint_fast64_t state, double const & newValue);
@ -328,7 +333,7 @@ namespace storm {
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<float> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& weights) const;
template std::vector<float> StandardRewardModel<float>::getTotalRewardVector(storm::storage::SparseMatrix<float> const& transitionMatrix, std::vector<float> const& weights, bool scaleTransAndActions) const;
template void StandardRewardModel<float>::reduceToStateBasedRewards(storm::storage::SparseMatrix<float> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<float>::setStateActionReward(uint_fast64_t choiceIndex, float const & newValue);
template void StandardRewardModel<float>::setStateReward(uint_fast64_t state, float const & newValue);
@ -338,7 +343,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights) const;
template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights, bool scaleTransAndActions) const;
template void StandardRewardModel<storm::RationalNumber>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<storm::RationalNumber>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue);
template void StandardRewardModel<storm::RationalNumber>::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue);
@ -347,7 +352,7 @@ namespace storm {
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights) const;
template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::vector<storm::RationalFunction> const& weights, bool scaleTransAndActions) const;
template void StandardRewardModel<storm::RationalFunction>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards);
template void StandardRewardModel<storm::RationalFunction>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue);
template void StandardRewardModel<storm::RationalFunction>::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue);
@ -356,7 +361,7 @@ namespace storm {
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights) const;
template std::vector<storm::Interval> StandardRewardModel<storm::Interval>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<double> const& weights, bool scaleTransAndActions) const;
template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue);
template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue);
template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, double const & newValue);

6
src/storm/models/sparse/StandardRewardModel.h
View File

@ -198,11 +198,13 @@ namespace storm {
* transition-based rewards in the reward model.
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @param weights A vector used for scaling the entries of the state-action rewards (if present).
* @param weights A vector used for scaling the entries of transition and/or state-action rewards (if present).
* @param scaleTransAndActions If true both transition rewards and state-action rewards are scaled by the
* weights. Otherwise, only the state-action rewards are scaled.
* @return The full state-action reward vector.
*/
template<typename MatrixValueType>
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights) const;
std::vector<ValueType> getTotalRewardVector(storm::storage::SparseMatrix<MatrixValueType> const& transitionMatrix, std::vector<MatrixValueType> const& weights, bool scaleTransAndActions) const;
/*!
* Creates a vector representing the complete reward vector based on the state-, state-action- and

8
src/storm/models/symbolic/StandardRewardModel.cpp
View File

@ -113,7 +113,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
storm::dd::Add<Type, ValueType> StandardRewardModel<Type, ValueType>::getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights) const {
storm::dd::Add<Type, ValueType> StandardRewardModel<Type, ValueType>::getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights, bool scaleTransAndActions) const {
storm::dd::Add<Type, ValueType> result = transitionMatrix.getDdManager().template getAddZero<ValueType>();
if (this->hasStateRewards()) {
result += optionalStateRewardVector.get();
@ -122,7 +122,11 @@ namespace storm {
result += optionalStateActionRewardVector.get() * weights;
}
if (this->hasTransitionRewards()) {
result += (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables);
if (scaleTransAndActions) {
result += weights * (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables);
} else {
result += (transitionMatrix * this->getTransitionRewardMatrix()).sumAbstract(columnVariables);
}
}
return result;
}

6
src/storm/models/symbolic/StandardRewardModel.h
View File

@ -167,10 +167,12 @@ namespace storm {
*
* @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix.
* @param columnVariables The column variables of the model.
* @param weights The weights used to scale the state-action reward vector.
* @param weights The weights used to scale the transition rewards and/or state-action rewards.
* @param scaleTransAndActions If true both transition rewards and state-action rewards are scaled by the
* weights. Otherwise, only the state-action rewards are scaled.
* @return The full state-action reward vector.
*/
storm::dd::Add<Type, ValueType> getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights) const;
storm::dd::Add<Type, ValueType> getTotalRewardVector(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& columnVariables, storm::dd::Add<Type, ValueType> const& weights, bool scaleTransAndActions) const;
/*!
* Multiplies all components of the reward model with the given DD.

51
src/storm/parser/FormulaParserGrammar.cpp
View File

@ -17,6 +17,7 @@ namespace storm {
for (auto variableTypePair : *constManager) {
identifiers_.add(variableTypePair.first.getName(), variableTypePair.first);
}
// Set the identifier mapping to actually generate expressions.
expressionParser.setIdentifierMapping(&identifiers_);
@ -126,32 +127,30 @@ namespace storm {
start.name("start");
// Enable the following lines to print debug output for most the rules.
/*
debug(start);
debug(constantDefinition);
debug(stateFormula);
debug(orStateFormula);
debug(andStateFormula);
debug(probabilityOperator);
debug(rewardOperator);
debug(longRunAverageOperator);
debug(timeOperator);
debug(pathFormulaWithoutUntil);
debug(pathFormula);
// debug(conditionalFormula);
debug(nextFormula);
debug(globallyFormula);
// debug(eventuallyFormula);
debug(atomicStateFormula);
debug(booleanLiteralFormula);
debug(labelFormula);
debug(expressionFormula);
debug(rewardPathFormula);
debug(cumulativeRewardFormula);
debug(totalRewardFormula);
debug(instantaneousRewardFormula);
debug(multiObjectiveFormula);
*/
// debug(start);
// debug(constantDefinition);
// debug(stateFormula);
// debug(orStateFormula);
// debug(andStateFormula);
// debug(probabilityOperator);
// debug(rewardOperator);
// debug(longRunAverageOperator);
// debug(timeOperator);
// debug(pathFormulaWithoutUntil);
// debug(pathFormula);
// debug(conditionalFormula);
// debug(nextFormula);
// debug(globallyFormula);
// debug(eventuallyFormula);
// debug(atomicStateFormula);
// debug(booleanLiteralFormula);
// debug(labelFormula);
// debug(expressionFormula);
// debug(rewardPathFormula);
// debug(cumulativeRewardFormula);
// debug(totalRewardFormula);
// debug(instantaneousRewardFormula);
// debug(multiObjectiveFormula);
// Enable error reporting.
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));

9
src/storm/storage/dd/Add.cpp
View File

@ -453,12 +453,9 @@ namespace storm {
++i;
}
// Use the toMatrix function to compute the number of elements in each row. Using the flag, we prevent
// it from actually generating the entries in the entry vector.
internalAdd.toMatrixComponents(trivialRowGroupIndices, rowIndications, columnsAndValues, rowOdd, columnOdd, ddRowVariableIndices, ddColumnVariableIndices, false);
// TODO: counting might be faster by just summing over the primed variables and then using the ODD to convert
// the resulting (DD) vector to an explicit vector.
// Count the number of elements in the rows.
rowIndications = this->notZero().template toAdd<uint_fast64_t>().sumAbstract(columnMetaVariables).toVector(rowOdd);
rowIndications.emplace_back();
// Now that we computed the number of entries in each row, compute the corresponding offsets in the entry vector.
uint_fast64_t tmp = 0;

12
src/storm/storage/dd/cudd/InternalCuddAdd.cpp
View File

@ -386,13 +386,17 @@ namespace storm {
thenOffset = 1;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
std::shared_ptr<Odd> elseNode = createOddRec(Cudd_E(dd), manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
@ -401,7 +405,9 @@ namespace storm {
uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
}
}
}

13
src/storm/storage/dd/cudd/InternalCuddBdd.cpp
View File

@ -355,14 +355,19 @@ namespace storm {
thenOffset = 1 - thenOffset;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else if (ddVariableIndices[currentLevel] < Cudd_NodeReadIndex(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
DdNode const* thenDdNode = Cudd_T_const(dd);
@ -375,7 +380,9 @@ namespace storm {
std::shared_ptr<Odd> elseNode = createOddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = createOddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels);
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
}
}
}

12
src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp
View File

@ -570,13 +570,17 @@ namespace storm {
thenOffset = 1;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else if (mtbdd_isleaf(dd) || ddVariableIndices[currentLevel] < mtbdd_getvar(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
std::shared_ptr<Odd> elseNode = createOddRec(mtbdd_regular(mtbdd_getlow(dd)), currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
@ -585,7 +589,9 @@ namespace storm {
uint_fast64_t totalElseOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
uint_fast64_t totalThenOffset = thenNode->getElseOffset() + thenNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalElseOffset, thenNode, totalThenOffset);
uniqueTableForLevels[currentLevel].emplace(dd, oddNode);
return oddNode;
}
}
}

12
src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp
View File

@ -337,14 +337,18 @@ namespace storm {
thenOffset = 1 - thenOffset;
}
return std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
auto oddNode = std::make_shared<Odd>(nullptr, elseOffset, nullptr, thenOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else if (bdd_isterminal(dd) || ddVariableIndices[currentLevel] < sylvan_var(dd)) {
// If we skipped the level in the DD, we compute the ODD just for the else-successor and use the same
// node for the then-successor as well.
std::shared_ptr<Odd> elseNode = createOddRec(dd, complement, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = elseNode;
uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset();
return std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
auto oddNode = std::make_shared<Odd>(elseNode, totalOffset, thenNode, totalOffset);
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
} else {
// Otherwise, we compute the ODDs for both the then- and else successors.
BDD thenDdNode = sylvan_high(dd);
@ -357,7 +361,9 @@ namespace storm {
std::shared_ptr<Odd> elseNode = createOddRec(bdd_regular(elseDdNode), elseComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
std::shared_ptr<Odd> thenNode = createOddRec(bdd_regular(thenDdNode), thenComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels);
return std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
auto oddNode = std::make_shared<Odd>(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset());
uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode);
return oddNode;
}
}
}

7
src/storm/storm.cpp
View File

@ -4,6 +4,7 @@
#include "storm/utility/macros.h"
#include "storm/cli/cli.h"
#include "storm/utility/initialize.h"
#include "storm/utility/Stopwatch.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/ResourceSettings.h"
@ -14,7 +15,7 @@
int main(const int argc, const char** argv) {
try {
auto start = std::chrono::high_resolution_clock::now();
storm::utility::Stopwatch totalTimer(true);
storm::utility::setUp();
storm::cli::printHeader("Storm", argc, argv);
storm::settings::initializeAll("Storm", "storm");
@ -28,10 +29,10 @@ int main(const int argc, const char** argv) {
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
auto end = std::chrono::high_resolution_clock::now();
totalTimer.stop();
if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
storm::cli::showTimeAndMemoryStatistics(std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count());
storm::cli::showTimeAndMemoryStatistics(totalTimer.getTimeMilliseconds());
}
return 0;
} catch (storm::exceptions::BaseException const& exception) {

121
src/storm/utility/Stopwatch.h
View File

@ -2,69 +2,116 @@
#define STORM_UTILITY_STOPWATCH_H_
#include <chrono>
#include <math.h>
#include "storm/utility/macros.h"
namespace storm {
namespace utility {
// A class that provides convenience operations to display run times.
/*!
* A class that provides convenience operations to display run times.
*/
class Stopwatch {
public:
Stopwatch(double initialValueInSeconds = 0.0) : accumulatedSeconds(initialValueInSeconds), paused(false), startOfCurrentMeasurement(std::chrono::high_resolution_clock::now()) {
// Intentionally left empty
/*!
* Constructor.
*
* @param startNow If true, the stopwatch starts right away.
*/
Stopwatch(bool startNow = false) : accumulatedTime(std::chrono::nanoseconds::zero()), stopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) {
if (startNow) {
start();
}
}
/*!
* Destructor.
*/
~Stopwatch() = default;
double getAccumulatedSeconds() const {
if(paused) {
return accumulatedSeconds;
} else {
return accumulatedSeconds + std::chrono::duration<double>(std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement).count();
}
/*!
* Get measured time in seconds.
*
* @return seconds as floating point number.
*/
double getTimeSeconds() const {
return std::chrono::duration<float>(accumulatedTime).count();
}
void addToAccumulatedSeconds(double value) {
accumulatedSeconds += value;
/*!
* Get measured time in milliseconds.
*
* @return Milliseconds.
*/
unsigned long long int getTimeMilliseconds() const {
return std::chrono::duration_cast<std::chrono::milliseconds>(accumulatedTime).count();
}
void pause() {
if(paused) {
STORM_LOG_WARN("Tried to pause a stopwatch that was already paused.");
} else {
accumulatedSeconds = getAccumulatedSeconds();
paused = true;
/*!
* Get measured time in nanoseconds.
*
* @return Nanoseconds.
*/
unsigned long long int getTimeNanoseconds() const {
return accumulatedTime.count();
}
/*!
* Add given time to measured time.
*
* @param timeNanoseconds Additional time in nanoseconds.
*/
void addToTime(std::chrono::nanoseconds timeNanoseconds) {
accumulatedTime += timeNanoseconds;
}
/*!
* Stop stopwatch and add measured time to total time.
*/
void stop() {
if (stopped) {
// Assertions are only available in DEBUG build and therefore not used here.
STORM_LOG_WARN("Stopwatch is already paused.");
}
stopped = true;
accumulatedTime += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement;
}
void unpause() {
if(paused) {
startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
paused = false;
} else {
STORM_LOG_WARN("Tried to unpause a stopwatch that was not paused.");
/*!
* Start stopwatch (again) and start measuring time.
*/
void start() {
if (!stopped) {
// Assertions are only available in DEBUG build and therefore not used here.
STORM_LOG_WARN("Stopwatch is already running.");
}
stopped = false;
startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
}
// Note: Does NOT unpause if stopwatch is currently paused.
/*!
* Reset the stopwatch. Reset the measured time to zero and stop the stopwatch.
*/
void reset() {
accumulatedSeconds = 0.0;
startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
accumulatedTime = std::chrono::nanoseconds::zero();
stopped = true;
}
friend std::ostream& operator<<(std::ostream& out, Stopwatch const& sw) {
out << (round(sw.getAccumulatedSeconds()*1000)/1000);
friend std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) {
out << stopwatch.getTimeSeconds();
return out;
}
private:
double accumulatedSeconds;
bool paused;
// Total measured time
std::chrono::nanoseconds accumulatedTime;
// Flag indicating if the stopwatch is stopped right now.
bool stopped;
// Timepoint when the stopwatch was started the last time.
std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;
};
}
}

26
src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp
View File

@ -26,7 +26,7 @@ TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) {
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program.checkValidity();
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program));
storm::generator::NextStateGeneratorOptions options(formulas);
std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> ma = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>();
@ -55,7 +55,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
@ -74,17 +74,17 @@ TEST(SparseMaPcaaModelCheckerTest, server) {
EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult<double>().getUnderApproximation()->convertNumberRepresentation<storm::RationalNumber>()));
EXPECT_TRUE(result->asParetoCurveCheckResult<double>().getOverApproximation()->convertNumberRepresentation<storm::RationalNumber>()->minkowskiSum(bloatingBox)->contains(expectedAchievableValues));
}
TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi(Tmin=? [ F num_finished=3 ], Pmax=? [ F<=0.2 num_finished=2 ], Pmin=? [ F f_j1=1 & f_j3=0 ]) ";
std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) ";
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());
@ -112,12 +112,12 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) {
TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi(T<=1.31 [ F num_finished=3 ], P>=0.17 [ F<=0.2 num_finished=2 ], P<=0.31 [ F f_j1=1 & f_j3=0 ]) "; //true
formulasAsString += "; multi(T<=1.29 [ F num_finished=3 ], P>=0.18 [ F<=0.2 num_finished=2 ], P<=0.29 [ F f_j1=1 & f_j3=0 ])"; //false
std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true
formulasAsString += "; multi(T<=1.29 [ F \"all_jobs_finished\" ], P>=0.18 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.29 [ F \"slowest_before_fastest\" ])"; //false
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
uint_fast64_t const initState = *ma->getInitialStates().begin();
@ -133,12 +133,12 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) {
TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi(Tmin=? [ F num_finished=3 ], P>=0.1797900683 [ F<=0.2 num_finished=2 ], P<=0.3 [ F f_j1=1 & f_j3=0 ]) "; //quantitative
formulasAsString += "; multi(T<=1.26 [ F num_finished=3 ], P>=0.2 [ F<=0.2 num_finished=2 ], Pmin=? [ F f_j1=1 & f_j3=0 ])"; //false
std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], P>=0.1797900683 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.3 [ F \"slowest_before_fastest\" ]) "; //quantitative
formulasAsString += "; multi(T<=1.26 [ F \"all_jobs_finished\" ], P>=0.2 [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ])"; //false
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
uint_fast64_t const initState = *ma->getInitialStates().begin();
@ -155,11 +155,11 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) {
TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi( Pmax=? [ F<=0.1 num_finished=1], Pmin=? [F<=0.2 num_finished=3]) ";
std::string formulasAsString = "multi( Pmax=? [ F<=0.1 num_finished=1], Pmin=? [F<=0.2 \"all_jobs_finished\"]) ";
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::MarkovAutomaton<double>>();
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula());

12
src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp
View File

@ -22,7 +22,7 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) {
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();;
@ -48,7 +48,7 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
@ -60,12 +60,12 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) {
TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm";
std::string formulasAsString = "multi(Pmax=? [ F task1_completed ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F task2_completed ])"; // numerical
std::string formulasAsString = "multi(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
@ -82,7 +82,7 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) {
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();
@ -98,7 +98,7 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) {
// programm, model, formula
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::buildSparseModel<double>(program, formulas)->as<storm::models::sparse::Mdp<double>>();
uint_fast64_t const initState = *mdp->getInitialStates().begin();

Write Preview
Loading…
Cancel
Save