diff --git a/resources/examples/testfiles/ma/jobscheduler.ma b/resources/examples/testfiles/ma/jobscheduler.ma index d83a199f5..68f60fb55 100644 --- a/resources/examples/testfiles/ma/jobscheduler.ma +++ b/resources/examples/testfiles/ma/jobscheduler.ma @@ -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 \ No newline at end of file +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 diff --git a/resources/examples/testfiles/mdp/multiobj_team3.nm b/resources/examples/testfiles/mdp/multiobj_team3.nm index 3c075c204..58a7108b1 100644 --- a/resources/examples/testfiles/mdp/multiobj_team3.nm +++ b/resources/examples/testfiles/mdp/multiobj_team3.nm @@ -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; diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 2de46e599..caa78060c 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -20,13 +20,8 @@ namespace storm { template void DFTModelChecker::check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { // Initialize - this->explorationTime = std::chrono::duration::zero(); - this->buildingTime = std::chrono::duration::zero(); - this->bisimulationTime = std::chrono::duration::zero(); - this->modelCheckingTime = std::chrono::duration::zero(); - this->totalTime = std::chrono::duration::zero(); this->approximationError = approximationError; - totalStart = std::chrono::high_resolution_clock::now(); + totalTimer.start(); // Optimizing DFT storm::storage::DFT dft = origDft.optimize(); @@ -44,7 +39,7 @@ namespace storm { checkResult = result->asExplicitQuantitativeCheckResult().getValueMap().begin()->second; } - this->totalTime = std::chrono::high_resolution_clock::now() - totalStart; + totalTimer.stop(); } template @@ -191,7 +186,7 @@ namespace storm { std::shared_ptr> 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>> 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> ctmc = model->template as>(); @@ -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>(composedModel, {formula}, storm::storage::BisimulationType::Weak)->template as>(); 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>> 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>(); @@ -276,7 +271,7 @@ namespace storm { template typename DFTModelChecker::dft_result DFTModelChecker::checkDFT(storm::storage::DFT const& dft, std::shared_ptr 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>> 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 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(approxResult.first) && !storm::utility::isInfinity(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 result = checkModel(model, formula); @@ -377,22 +375,22 @@ namespace storm { template std::unique_ptr DFTModelChecker::checkModel(std::shared_ptr>& model, std::shared_ptr 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().isBisimulationSet()) { STORM_LOG_INFO("Bisimulation..."); model = storm::performDeterministicSparseBisimulationMinimization>(model->template as>(), {formula}, storm::storage::BisimulationType::Weak)->template as>(); 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 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 void DFTModelChecker::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 diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.h b/src/storm-dft/modelchecker/dft/DFTModelChecker.h index 7cee7b0e4..c714999a8 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.h @@ -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 - namespace storm { namespace modelchecker { @@ -57,12 +56,11 @@ namespace storm { private: // Timing values - std::chrono::duration buildingTime = std::chrono::duration::zero(); - std::chrono::duration explorationTime = std::chrono::duration::zero(); - std::chrono::duration bisimulationTime = std::chrono::duration::zero(); - std::chrono::duration modelCheckingTime = std::chrono::duration::zero(); - std::chrono::duration totalTime = std::chrono::duration::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 { }; } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 8585bc92a..fc221147b 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -29,7 +29,7 @@ namespace storm { template bool HybridCtmcCslModelChecker::canHandle(CheckTask 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 @@ -110,6 +110,11 @@ namespace storm { return storm::modelchecker::helper::HybridCtmcCslHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector(), subResult.getTruthValuesVector(), *linearEquationSolverFactory); } + template + std::unique_ptr HybridCtmcCslModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + return storm::modelchecker::helper::HybridCtmcCslHelper::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>; template class HybridCtmcCslModelChecker>; diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h index 24dbde9d2..202456f5b 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.h @@ -24,10 +24,12 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: // An object that is used for solving linear equations and performing matrix-vector multiplication. diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index cfca43d1f..c528d4e12 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -42,7 +42,7 @@ namespace storm { template::SupportsExponential, int>::type> bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask 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 @@ -133,6 +133,13 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + storm::storage::SparseMatrix probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()); + std::vector 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(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index 830bfe135..f5ca5d6d3 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -26,11 +26,13 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: template::SupportsExponential, int>::type = 0> diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index e3e301f68..0f6fb9a4b 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -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 result = rewardModel.getStateRewardVector().toVector(odd); @@ -267,7 +267,7 @@ namespace storm { storm::storage::SparseMatrix explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd); // Then compute the state reward vector to use in the computation. - storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector); + storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false); std::vector explicitTotalRewardVector = totalRewardVector.toVector(odd); // Finally, compute the transient probabilities. @@ -290,6 +290,23 @@ namespace storm { return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); } + template + std::unique_ptr HybridCtmcCslHelper::computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + storm::dd::Add probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + + // Create ODD for the translation. + storm::dd::Odd odd = model.getReachableStates().createOdd(); + + storm::storage::SparseMatrix explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd); + std::vector explicitExitRateVector = exitRateVector.toVector(odd); + + std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, model.getColumnVariables(), exitRateVector, true).toVector(odd), &explicitExitRateVector, linearEquationSolverFactory); + + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + } + template storm::dd::Add HybridCtmcCslHelper::computeUniformizedMatrix(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& transitionMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& maybeStates, ValueType uniformizationRate) { STORM_LOG_DEBUG("Computing uniformized matrix using uniformization rate " << uniformizationRate << "."); diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h index 70f8a5c1d..62eef6264 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.h @@ -32,6 +32,8 @@ namespace storm { static std::unique_ptr computeNextProbabilities(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& nextStates); + static std::unique_ptr computeLongRunAverageRewards(storm::models::symbolic::Ctmc const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + /*! * Converts the given rate-matrix into a time-abstract probability matrix. * diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index b8f0f527a..15cbe2c64 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -208,7 +208,7 @@ namespace storm { template ::SupportsExponential, int>::type> std::vector SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory 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 ::SupportsExponential, int>::type> std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory 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 uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector); // Compute the total state reward vector. - std::vector totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector); + std::vector totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector, false); // Finally, compute the transient probabilities. return computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory); @@ -331,6 +331,7 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory 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(numberOfStates, storm::utility::one()); } - // Start by decomposing the DTMC into its BSCCs. + ValueType zero = storm::utility::zero(); + ValueType one = storm::utility::one(); + + return computeLongRunAverages(probabilityMatrix, + [&zero, &one, &psiStates] (storm::storage::sparse::state_type const& state) -> ValueType { + if (psiStates.get(state)) { + return one; + } + return zero; + }, + exitRateVector, + linearEquationSolverFactory); + } + + template + std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, RewardModelType const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory 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 + std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return computeLongRunAverages(probabilityMatrix, + [&stateRewardVector] (storm::storage::sparse::state_type const& state) -> ValueType { + return stateRewardVector[state]; + }, + exitRateVector, + linearEquationSolverFactory); + } + + template + std::vector SparseCtmcCslHelper::computeLongRunAverages(storm::storage::SparseMatrix const& probabilityMatrix, std::function const& valueGetter, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory){ + uint_fast64_t numberOfStates = probabilityMatrix.getRowCount(); + + // Start by decomposing the CTMC into its BSCCs. storm::storage::StronglyConnectedComponentDecomposition 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 tmp(probabilityMatrix.getRowCount(), storm::utility::zero()); +// 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 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(); - } + bsccLra[bsccIndex] = valueGetter(*bscc.begin()); } for (uint_fast64_t bsccIndex = 0; bsccIndex < bsccDecomposition.size(); ++bsccIndex) { @@ -700,6 +744,8 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); @@ -728,6 +774,12 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); template std::vector SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index 80aa68130..be0f8255c 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -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 static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - + + template + static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, RewardModelType const& rewardModel, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + template + static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + template static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); @@ -96,6 +104,10 @@ namespace storm { */ template static storm::storage::SparseMatrix computeGeneratorMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates); + + private: + template + static std::vector computeLongRunAverages(storm::storage::SparseMatrix const& probabilityMatrix, std::function const& valueGetter, std::vector const* exitRateVector, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); }; } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 60ac261fb..125e12a1e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -314,7 +314,7 @@ namespace storm { template void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional 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(formula.getBound()); diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp index f018458f0..1936e60bd 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp @@ -38,7 +38,7 @@ namespace storm { template bool HybridDtmcPrctlModelChecker::canHandle(CheckTask 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 @@ -108,13 +108,12 @@ namespace storm { std::unique_ptr subResultPointer = this->check(stateFormula); SymbolicQualitativeCheckResult const& subResult = subResultPointer->asSymbolicQualitativeCheckResult(); - // Create ODD for the translation. - storm::dd::Odd odd = this->getModel().getReachableStates().createOdd(); - - storm::storage::SparseMatrix explicitProbabilityMatrix = this->getModel().getTransitionMatrix().toMatrix(odd, odd); - - std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), *this->linearEquationSolverFactory); - return std::unique_ptr(new HybridQuantitativeCheckResult(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().template getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result))); + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeLongRunAverageProbabilities(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory); + } + + template + std::unique_ptr HybridDtmcPrctlModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + return storm::modelchecker::helper::HybridDtmcPrctlHelper::computeLongRunAverageRewards(this->getModel(), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), *this->linearEquationSolverFactory); } template class HybridDtmcPrctlModelChecker>; diff --git a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h index 748bf422f..b54ed38ea 100644 --- a/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h @@ -25,10 +25,12 @@ namespace storm { virtual std::unique_ptr computeNextProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; virtual std::unique_ptr computeGloballyProbabilities(CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; + + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; - virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index daaee411e..5bbf6cf23 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -36,7 +36,7 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask 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 @@ -116,6 +116,13 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeLongRunAverageRewards(this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), nullptr, *linearEquationSolverFactory); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + + } + template std::unique_ptr SparseDtmcPrctlModelChecker::computeConditionalProbabilities(CheckTask const& checkTask) { storm::logic::ConditionalFormula const& conditionalFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index 2a6269a71..3b40cad37 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -31,6 +31,7 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeLongRunAverageRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: // An object that is used for retrieving linear equation solvers. diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp index d5e21fa67..8870456cd 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp @@ -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 + std::unique_ptr HybridDtmcPrctlHelper::computeLongRunAverageProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + // Create ODD for the translation. + storm::dd::Odd odd = model.getReachableStates().createOdd(); + storm::storage::SparseMatrix explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd); + + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageProbabilities(explicitProbabilityMatrix, targetStates.toVector(odd), linearEquationSolverFactory); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + } + + template + std::unique_ptr HybridDtmcPrctlHelper::computeLongRunAverageRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + // Create ODD for the translation. + storm::dd::Odd odd = model.getReachableStates().createOdd(); + storm::storage::SparseMatrix explicitProbabilityMatrix = model.getTransitionMatrix().toMatrix(odd, odd); + + std::vector result = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeLongRunAverageRewards(explicitProbabilityMatrix, rewardModel.getTotalRewardVector(model.getTransitionMatrix(), model.getColumnVariables()).toVector(odd), linearEquationSolverFactory); + return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); + } + template class HybridDtmcPrctlHelper; template class HybridDtmcPrctlHelper; } diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h index 5bec52909..e254c5912 100644 --- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.h @@ -33,6 +33,11 @@ namespace storm { static std::unique_ptr computeInstantaneousRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::unique_ptr computeReachabilityRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::dd::Bdd const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeLongRunAverageProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& targetStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::unique_ptr computeLongRunAverageRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + }; } diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 5ba60dec3..4db5e15a9 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -236,6 +236,16 @@ namespace storm { return SparseCtmcCslHelper::computeLongRunAverageProbabilities(transitionMatrix, psiStates, nullptr, linearEquationSolverFactory); } + template + std::vector SparseDtmcPrctlHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverageRewards(transitionMatrix, rewardModel, nullptr, linearEquationSolverFactory); + } + + template + std::vector SparseDtmcPrctlHelper::computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + return SparseCtmcCslHelper::computeLongRunAverageRewards(transitionMatrix, stateRewards, nullptr, linearEquationSolverFactory); + } + template typename SparseDtmcPrctlHelper::BaierTransformedModel SparseDtmcPrctlHelper::computeBaierTransformation(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, boost::optional> const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index 0709aba11..3c3b6974b 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -39,7 +39,11 @@ namespace storm { static std::vector computeReachabilityRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory, boost::optional> resultHint = boost::none); static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& psiStates, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - + + static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + + static std::vector computeLongRunAverageRewards(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewards, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); + static std::vector computeConditionalProbabilities(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); static std::vector computeConditionalRewards(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& conditionStates, bool qualitative, storm::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index 8b7e8c349..1866be5d2 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -165,6 +165,11 @@ namespace storm { template template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const { + if (this->hasStateActionRewards()) { + for (auto const& e : this->getStateActionRewardVector()) { + std::cout << "e " << e << std::endl; + } + } std::vector result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(transitionMatrix.getRowCount())); if (this->hasStateActionRewards() && this->hasTransitionRewards()) { storm::utility::vector::addVectors(result, this->getStateActionRewardVector(), result); @@ -177,16 +182,16 @@ namespace storm { template template - std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const { - std::vector result = this->hasTransitionRewards() ? transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()) : (this->hasStateActionRewards() ? this->getStateActionRewardVector() : std::vector(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(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return resultElement + weight * rewardElement; } ); + std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const { + std::vector result; + if (this->hasTransitionRewards()) { + result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); + storm::utility::vector::applyPointwise(weights, this->getStateActionRewardVector(), result, [] (MatrixValueType const& weight, ValueType const& rewardElement, ValueType const& resultElement) { return weight * (resultElement + rewardElement); } ); + } else { + result = std::vector(transitionMatrix.getRowCount()); + if (this->hasStateActionRewards()) { + storm::utility::vector::applyPointwise(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 StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -328,7 +333,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, float const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, float const & newValue); @@ -338,7 +343,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); @@ -347,7 +352,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue); @@ -356,7 +361,7 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index 8fcfa48ef..85d6b5382 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -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 - std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; + std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and diff --git a/src/storm/models/symbolic/StandardRewardModel.cpp b/src/storm/models/symbolic/StandardRewardModel.cpp index e42fc4b70..0a3e37e79 100644 --- a/src/storm/models/symbolic/StandardRewardModel.cpp +++ b/src/storm/models/symbolic/StandardRewardModel.cpp @@ -113,7 +113,7 @@ namespace storm { } template - storm::dd::Add StandardRewardModel::getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights) const { + storm::dd::Add StandardRewardModel::getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights, bool scaleTransAndActions) const { storm::dd::Add result = transitionMatrix.getDdManager().template getAddZero(); 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; } diff --git a/src/storm/models/symbolic/StandardRewardModel.h b/src/storm/models/symbolic/StandardRewardModel.h index d44a96868..a4e9fb573 100644 --- a/src/storm/models/symbolic/StandardRewardModel.h +++ b/src/storm/models/symbolic/StandardRewardModel.h @@ -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 getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights) const; + storm::dd::Add getTotalRewardVector(storm::dd::Add const& transitionMatrix, std::set const& columnVariables, storm::dd::Add const& weights, bool scaleTransAndActions) const; /*! * Multiplies all components of the reward model with the given DD. diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 450d68fc8..86b34f19f 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -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(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index 2e72e8329..93039e480 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -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().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; diff --git a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp index 58d8b5bf3..4cf197970 100644 --- a/src/storm/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddAdd.cpp @@ -386,13 +386,17 @@ namespace storm { thenOffset = 1; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(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 elseNode = createOddRec(dd, manager, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(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 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(elseNode, totalElseOffset, thenNode, totalThenOffset); + auto oddNode = std::make_shared(elseNode, totalElseOffset, thenNode, totalThenOffset); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } } } diff --git a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp index 5ad9b5846..8cea861b6 100644 --- a/src/storm/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storm/storage/dd/cudd/InternalCuddBdd.cpp @@ -355,14 +355,19 @@ namespace storm { thenOffset = 1 - thenOffset; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(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 elseNode = createOddRec(dd, manager, currentLevel + 1, complement, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); - return std::make_shared(elseNode, totalOffset, thenNode, totalOffset); + + auto oddNode = std::make_shared(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 elseNode = createOddRec(Cudd_Regular(elseDdNode), manager, currentLevel + 1, elseComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = createOddRec(Cudd_Regular(thenDdNode), manager, currentLevel + 1, thenComplemented, maxLevel, ddVariableIndices, uniqueTableForLevels); - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp index eecfe55bb..5e5043246 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -570,13 +570,17 @@ namespace storm { thenOffset = 1; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(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 elseNode = createOddRec(dd, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(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 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(elseNode, totalElseOffset, thenNode, totalThenOffset); + auto oddNode = std::make_shared(elseNode, totalElseOffset, thenNode, totalThenOffset); + uniqueTableForLevels[currentLevel].emplace(dd, oddNode); + return oddNode; } } } diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index e6a51eb23..7097ac999 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -337,14 +337,18 @@ namespace storm { thenOffset = 1 - thenOffset; } - return std::make_shared(nullptr, elseOffset, nullptr, thenOffset); + auto oddNode = std::make_shared(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 elseNode = createOddRec(dd, complement, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = elseNode; uint_fast64_t totalOffset = elseNode->getElseOffset() + elseNode->getThenOffset(); - return std::make_shared(elseNode, totalOffset, thenNode, totalOffset); + auto oddNode = std::make_shared(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 elseNode = createOddRec(bdd_regular(elseDdNode), elseComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); std::shared_ptr thenNode = createOddRec(bdd_regular(thenDdNode), thenComplemented, currentLevel + 1, maxLevel, ddVariableIndices, uniqueTableForLevels); - return std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + auto oddNode = std::make_shared(elseNode, elseNode->getElseOffset() + elseNode->getThenOffset(), thenNode, thenNode->getElseOffset() + thenNode->getThenOffset()); + uniqueTableForLevels[currentLevel].emplace(std::make_pair(dd, complement), oddNode); + return oddNode; } } } diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp index 60576c3c0..7ce7611dc 100644 --- a/src/storm/storm.cpp +++ b/src/storm/storm.cpp @@ -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().isPrintTimeAndMemorySet()) { - storm::cli::showTimeAndMemoryStatistics(std::chrono::duration_cast(end - start).count()); + storm::cli::showTimeAndMemoryStatistics(totalTimer.getTimeMilliseconds()); } return 0; } catch (storm::exceptions::BaseException const& exception) { diff --git a/src/storm/utility/Stopwatch.h b/src/storm/utility/Stopwatch.h index c0b937c24..a30b40683 100644 --- a/src/storm/utility/Stopwatch.h +++ b/src/storm/utility/Stopwatch.h @@ -2,69 +2,116 @@ #define STORM_UTILITY_STOPWATCH_H_ #include -#include #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(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(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(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; - }; } } diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp index f1025bd6f..5f92999c1 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp @@ -26,7 +26,7 @@ TEST(SparseMaPcaaModelCheckerTest, serverRationalNumbers) { // programm, model, formula storm::prism::Program program = storm::parseProgram(programFile); program.checkValidity(); - std::vector> formulas = storm::parseFormulasForProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(parseFormulasForProgram(formulasAsString, program)); storm::generator::NextStateGeneratorOptions options(formulas); std::shared_ptr> ma = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); @@ -55,7 +55,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); - std::vector> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); @@ -74,17 +74,17 @@ TEST(SparseMaPcaaModelCheckerTest, server) { EXPECT_TRUE(expectedAchievableValues->minkowskiSum(bloatingBox)->contains(result->asParetoCurveCheckResult().getUnderApproximation()->convertNumberRepresentation())); EXPECT_TRUE(result->asParetoCurveCheckResult().getOverApproximation()->convertNumberRepresentation()->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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr 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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); 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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); 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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); diff --git a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp index c25872e9c..1116997c9 100644 --- a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp @@ -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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); 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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); 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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); 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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); 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> formulas = storm::parseFormulasForPrismProgram(formulasAsString, program); + std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();