From cf772688f01eb66469d8c0779cc31651e1ba609d Mon Sep 17 00:00:00 2001 From: gereon Date: Fri, 8 Mar 2013 12:04:42 +0100 Subject: [PATCH 1/8] added setter for options in Settings class. --- src/utility/Settings.h | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/utility/Settings.h b/src/utility/Settings.h index b35e893c4..900b34673 100644 --- a/src/utility/Settings.h +++ b/src/utility/Settings.h @@ -70,6 +70,23 @@ namespace settings { inline const bool isSet(std::string const & name) const { return this->vm.count(name) > 0; } + + /*! + * @brief Set an option. + */ + inline void set(std::string const & name) { + bpo::variable_value val; + this->vm.insert( std::make_pair(name, val) ); + } + + /*! + * @brief Set value for an option. + */ + template + inline void set(std::string const & name, T const & value) { + bpo::variable_value val(value, false); + this->vm.insert( std::make_pair(name, val) ); + } /*! * @brief Register a new module. From abae3047193721e6906fbbe6cde1533ceee9c182 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Mar 2013 15:32:47 +0100 Subject: [PATCH 2/8] Included tests for model checkers in test suite. --- .../GmmxxDtmcPrctModelCheckerTest.cpp | 162 ++++++++++++ .../GmmxxMdpPrctModelCheckerTest.cpp | 248 ++++++++++++++++++ 2 files changed, 410 insertions(+) create mode 100644 test/functional/GmmxxDtmcPrctModelCheckerTest.cpp create mode 100644 test/functional/GmmxxMdpPrctModelCheckerTest.cpp diff --git a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp new file mode 100644 index 000000000..6c0fe540d --- /dev/null +++ b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp @@ -0,0 +1,162 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(GmmxxDtmcPrctModelCheckerTest, Die) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 14); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28); + + storm::modelChecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + + storm::formula::Ap* apFormula = new storm::formula::Ap("one"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("two"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("three"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get("precision")); + + delete probFormula; + delete result; + + storm::formula::Ap* done = new storm::formula::Ap("done"); + storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(done); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula); + + result = rewardFormula->check(mc); + + + ASSERT_TRUE(std::abs((*result)[1] - ((double)11/3)) < s->get("precision")); + + delete rewardFormula; + delete result; +} + +TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 8608); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 22461); + + storm::modelChecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + + storm::formula::Ap* apFormula = new storm::formula::Ap("observe0Greater1"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - 0.3328800375801578281) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("observeIGreater1"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - 0.1522173670950556501) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("observeOnlyTrueSender"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - 0.32153724292835045) < s->get("precision")); + + delete probFormula; + delete result; +} + +TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 12401); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28895); + + storm::modelChecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + + storm::formula::Ap* apFormula = new storm::formula::Ap("elected"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - 1) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + storm::formula::BoundedUntil* boundedUntilFormula = new storm::formula::BoundedUntil(new storm::formula::Ap("true"), apFormula, 20); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedUntilFormula); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - 0.9999965911265462636) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula); + + result = rewardFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[1] - 1.0448979591835938496) < s->get("precision")); + + delete rewardFormula; + delete result; +} diff --git a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp new file mode 100644 index 000000000..093afc33a --- /dev/null +++ b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp @@ -0,0 +1,248 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(GmmxxMdpPrctModelCheckerTest, Dice) { + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 169); + ASSERT_EQ(mdp->getNumberOfTransitions(), 436); + + storm::modelChecker::GmmxxMdpPrctlModelChecker mc(*mdp); + + storm::formula::Ap* apFormula = new storm::formula::Ap("two"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + std::vector* result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.0277777612209320068) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("two"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, false); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.0277777612209320068) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("three"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.0555555224418640136) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("three"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, false); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.0555555224418640136) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("four"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.083333283662796020508) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("four"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, false); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.083333283662796020508) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("done"); + storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = rewardFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::formula::Ap("done"); + reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = rewardFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + + delete rewardFormula; + delete result; + + storm::parser::AutoParser stateRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", ""); + + ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP); + + std::shared_ptr> stateRewardMdp = stateRewardParser.getModel>(); + + storm::modelChecker::GmmxxMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp); + + apFormula = new storm::formula::Ap("done"); + reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = rewardFormula->check(stateRewardModelChecker); + + ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::formula::Ap("done"); + reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = rewardFormula->check(stateRewardModelChecker); + + ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + + delete rewardFormula; + delete result; + + storm::parser::AutoParser stateAndTransitionRewardParser(STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.tra", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.lab", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.state.rew", STORM_CPP_TESTS_BASE_PATH "/functional/two_dice/two_dice.flip.trans.rew"); + + ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP); + + std::shared_ptr> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); + + storm::modelChecker::GmmxxMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp); + + apFormula = new storm::formula::Ap("done"); + reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = rewardFormula->check(stateAndTransitionRewardModelChecker); + + ASSERT_TRUE(std::abs((*result)[0] - (2 * 7.3333272933959960938)) < s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::formula::Ap("done"); + reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = rewardFormula->check(stateAndTransitionRewardModelChecker); + + ASSERT_TRUE(std::abs((*result)[0] - (2 * 7.3333272933959960938)) < s->get("precision")); + + delete rewardFormula; + delete result; +} + +TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { + storm::settings::Settings* s = storm::settings::instance(); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.tra", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/asynchronous_leader/leader4.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::MDP); + + std::shared_ptr> mdp = parser.getModel>(); + + ASSERT_EQ(mdp->getNumberOfStates(), 3172); + ASSERT_EQ(mdp->getNumberOfTransitions(), 7144); + + storm::modelChecker::GmmxxMdpPrctlModelChecker mc(*mdp); + + storm::formula::Ap* apFormula = new storm::formula::Ap("elected"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, true); + + std::vector* result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 1) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula, false); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 1) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + storm::formula::BoundedEventually* boundedEventuallyFormula = new storm::formula::BoundedEventually(apFormula, 25); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.0625) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + boundedEventuallyFormula = new storm::formula::BoundedEventually(apFormula, 25); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); + + result = probFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 0.0625) < s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, true); + + result = rewardFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 4.28568908480604982) < s->get("precision")); + + delete rewardFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula, false); + + result = rewardFormula->check(mc); + + ASSERT_TRUE(std::abs((*result)[0] - 4.2856904354441400784) < s->get("precision")); + + delete rewardFormula; + delete result; +} From c7f58ed5f5d516a6ee29901009691bfd56614200 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Mar 2013 15:33:32 +0100 Subject: [PATCH 3/8] Modified parsers such that the reward matrices are of the same size as the transition matrices. --- src/parser/DeterministicModelParser.cpp | 4 +- .../DeterministicSparseTransitionParser.cpp | 47 +++++++++++------ .../DeterministicSparseTransitionParser.h | 4 +- src/parser/NondeterministicModelParser.cpp | 4 +- ...NondeterministicSparseTransitionParser.cpp | 52 ++++++++++++------- .../NondeterministicSparseTransitionParser.h | 4 +- src/parser/Parser.h | 17 ++++++ 7 files changed, 92 insertions(+), 40 deletions(-) diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 2300ad74d..35818ffbf 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -45,7 +45,9 @@ DeterministicModelParser::DeterministicModelParser(std::string const & transitio this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { - storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, true); + RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(stateCount, stateCount, nullptr); + storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, rewardMatrixInfo); + delete rewardMatrixInfo; this->transitionRewards = trp.getMatrix(); } this->dtmc = nullptr; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 031087b88..60957a17a 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -44,12 +44,14 @@ namespace parser { * @param buf Data to scan. Is expected to be some char array. * @param maxnode Is set to highest id of all nodes. */ -uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, bool rewardFile) { +uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { + bool isRewardMatrix = rewardMatrixInformation != nullptr; + uint_fast64_t nonZeroEntryCount = 0; /* * Check file header and extract number of transitions. */ - if (!rewardFile) { + if (!isRewardMatrix) { buf = strchr(buf, '\n') + 1; // skip format hint } @@ -68,7 +70,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast row = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf); - if (!rewardFile) { + if (!isRewardMatrix) { if (lastRow != row) { if ((lastRow != -1) && (!rowHadDiagonalEntry)) { ++nonZeroEntryCount; @@ -109,7 +111,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast buf = trimWhitespaces(buf); } - if (!rowHadDiagonalEntry && !rewardFile) { + if (!rowHadDiagonalEntry && !isRewardMatrix) { ++nonZeroEntryCount; } @@ -126,13 +128,15 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast * @return a pointer to the created sparse matrix. */ -DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, bool rewardFile) +DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) : matrix(nullptr) { /* * Enforce locale where decimal point is '.'. */ setlocale(LC_NUMERIC, "C"); + bool isRewardMatrix = rewardMatrixInformation != nullptr; + /* * Open file. */ @@ -143,7 +147,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st * Perform first pass, i.e. count entries that are not zero. */ int_fast64_t maxStateId; - uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardFile); + uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardMatrixInformation); LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros."); @@ -164,10 +168,21 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st /* * Read file header, extract number of states. */ - if (!rewardFile) { + if (!isRewardMatrix) { buf = strchr(buf, '\n') + 1; // skip format hint } + // If the matrix that is being parsed is a reward matrix, it should match the size of the + // transition matrix. + if (isRewardMatrix) { + if (maxStateId + 1 > rewardMatrixInformation->rowCount || maxStateId + 1 > rewardMatrixInformation->columnCount) { + LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix."); + throw storm::exceptions::WrongFileFormatException() << "Reward matrix has more rows or columns than transition matrix."; + } else { + maxStateId = rewardMatrixInformation->rowCount - 1; + } + } + /* * Creating matrix here. * The number of non-zero elements is computed by firstPass(). @@ -201,10 +216,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st if (lastRow != row) { if ((lastRow != -1) && (!rowHadDiagonalEntry)) { - if (insertDiagonalEntriesIfMissing) { + if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); - } else if (!rewardFile) { + } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); } // No increment for lastRow @@ -212,11 +227,11 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; - if (fixDeadlocks && !rewardFile) { + if (fixDeadlocks && !isRewardMatrix) { this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne()); rowHadDiagonalEntry = true; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted."); - } else if (!rewardFile) { + } else if (!isRewardMatrix) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions."); // FIXME Why no exception at this point? This will break the App. } @@ -229,10 +244,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st rowHadDiagonalEntry = true; } else if (col > row && !rowHadDiagonalEntry) { rowHadDiagonalEntry = true; - if (insertDiagonalEntriesIfMissing && !rewardFile) { + if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { this->matrix->addNextValue(row, row, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); - } else if (!rewardFile) { + } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); } } @@ -242,15 +257,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing && !rewardFile) { + if (insertDiagonalEntriesIfMissing && !isRewardMatrix) { this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero()); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); - } else if (!rewardFile) { + } else if (!isRewardMatrix) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); } } - if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; + if (!fixDeadlocks && hadDeadlocks && !isRewardMatrix) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; /* * Finalize Matrix. diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index a023debb7..cb91901f8 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -17,7 +17,7 @@ namespace parser { */ class DeterministicSparseTransitionParser : public Parser { public: - DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, bool rewardFile = false); + DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); std::shared_ptr> getMatrix() { return this->matrix; @@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser { private: std::shared_ptr> matrix; - uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, bool rewardFile); + uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation); }; diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 303789a99..a0ce35674 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -38,7 +38,9 @@ NondeterministicModelParser::NondeterministicModelParser(std::string const & tra this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { - storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, true, tp.getRowMapping()); + RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(tp.getMatrix()->getRowCount(), tp.getMatrix()->getColumnCount(), tp.getRowMapping()); + storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, rewardMatrixInfo); + delete rewardMatrixInfo; this->transitionRewardMatrix = trp.getMatrix(); } diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 1019240c7..79bb9f3f5 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -49,11 +49,13 @@ namespace parser { * @param maxnode Is set to highest id of all nodes. * @return The number of non-zero elements. */ -uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr> const nondeterministicChoiceIndices) { +uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { + bool isRewardFile = rewardMatrixInformation != nullptr; + /* * Check file header and extract number of transitions. */ - if (!rewardFile) { + if (!isRewardFile) { buf = strchr(buf, '\n') + 1; // skip format hint } @@ -80,17 +82,17 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ maxnode = source; } - if (rewardFile) { + if (isRewardFile) { // If we have switched the source state, we possibly need to insert the rows of the last // last source state. if (source != lastsource && lastsource != -1) { - choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1); + choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. for (uint_fast64_t i = lastsource + 1; i < source; ++i) { - choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]); + choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows @@ -151,14 +153,14 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ buf = trimWhitespaces(buf); } - if (rewardFile) { + if (isRewardFile) { // If not all rows were filled for the last state, we need to insert them. - choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1); + choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1); // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. - for (uint_fast64_t i = lastsource + 1; i < nondeterministicChoiceIndices->size() - 1; ++i) { - choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]); + for (uint_fast64_t i = lastsource + 1; i < rewardMatrixInformation->nondeterministicChoiceIndices->size() - 1; ++i) { + choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]); } } @@ -175,13 +177,15 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ * @return a pointer to the created sparse matrix. */ -NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile, std::shared_ptr> const nondeterministicChoiceIndices) +NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation) : matrix(nullptr) { /* * Enforce locale where decimal point is '.'. */ setlocale(LC_NUMERIC, "C"); + bool isRewardFile = rewardMatrixInformation != nullptr; + /* * Open file. */ @@ -193,7 +197,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s */ int_fast64_t maxnode; uint_fast64_t choices; - uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardFile, nondeterministicChoiceIndices); + uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardMatrixInformation); /* * If first pass returned zero, the file format was wrong. @@ -212,10 +216,22 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s /* * Skip file header. */ - if (!rewardFile) { + if (!isRewardFile) { buf = strchr(buf, '\n') + 1; // skip format hint } + if (isRewardFile) { + if (choices > rewardMatrixInformation->rowCount || maxnode + 1 > rewardMatrixInformation->columnCount) { + LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size."); + throw storm::exceptions::WrongFileFormatException() << "Reward matrix size exceeds transition matrix size."; + } else if (choices != rewardMatrixInformation->rowCount) { + LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count."); + throw storm::exceptions::WrongFileFormatException() << "Reward matrix row count does not match transition matrix row count."; + } else { + maxnode = rewardMatrixInformation->columnCount - 1; + } + } + /* * Create and initialize matrix. * The matrix should have as many columns as we have nodes and as many rows as we have choices. @@ -253,17 +269,17 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s source = checked_strtol(buf, &buf); choice = checked_strtol(buf, &buf); - if (rewardFile) { + if (isRewardFile) { // If we have switched the source state, we possibly need to insert the rows of the last // last source state. if (source != lastsource && lastsource != -1) { - curRow += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1); + curRow += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1); } // If we skipped some states, we need to reserve empty rows for all their nondeterministic // choices. for (uint_fast64_t i = lastsource + 1; i < source; ++i) { - curRow += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]); + curRow += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows @@ -286,12 +302,12 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s */ for (int_fast64_t node = lastsource + 1; node < source; node++) { hadDeadlocks = true; - if (!rewardFile && fixDeadlocks) { + if (fixDeadlocks) { this->rowMapping->at(node) = curRow; this->matrix->addNextValue(curRow, node, 1); ++curRow; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); - } else if (!rewardFile) { + } else { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); } } @@ -323,7 +339,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s this->rowMapping->at(maxnode+1) = curRow + 1; - if (!fixDeadlocks && hadDeadlocks && !rewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; + if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; /* * Finalize matrix. diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index 79947dd93..5731017ec 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -19,7 +19,7 @@ namespace parser { */ class NondeterministicSparseTransitionParser : public Parser { public: - NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile = false, std::shared_ptr> const nondeterministicChoiceIndices = nullptr); + NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); inline std::shared_ptr> getMatrix() const { return this->matrix; @@ -33,7 +33,7 @@ class NondeterministicSparseTransitionParser : public Parser { std::shared_ptr> matrix; std::shared_ptr> rowMapping; - uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr> const nondeterministicChoiceIndices); + uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation); }; diff --git a/src/parser/Parser.h b/src/parser/Parser.h index ef6c38c84..6cb4abe65 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -14,6 +14,8 @@ #include #include #include +#include +#include #include #include "src/exceptions/FileIoException.h" @@ -30,6 +32,21 @@ namespace storm { */ namespace parser { + struct RewardMatrixInformationStruct { + RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) { + // Intentionally left empty. + } + + RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::shared_ptr> nondeterministicChoiceIndices) + : rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) { + // Intentionally left empty. + } + + uint_fast64_t rowCount; + uint_fast64_t columnCount; + std::shared_ptr> nondeterministicChoiceIndices; + }; + /*! * @brief Opens a file and maps it to memory providing a char* * containing the file content. From a6ae3d713a9eda275e3611df46a0a23841bf2bd0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Mar 2013 16:06:53 +0100 Subject: [PATCH 4/8] Fixed test for nondeterministic model parser. --- test/parser/ParseMdpTest.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp index 949c3854d..02302dc2a 100644 --- a/test/parser/ParseMdpTest.cpp +++ b/test/parser/ParseMdpTest.cpp @@ -13,9 +13,9 @@ TEST(ParseMdpTest, parseAndOutput) { storm::parser::NondeterministicModelParser* mdpParser = nullptr; - /*ASSERT_NO_THROW(*/mdpParser = new storm::parser::NondeterministicModelParser( + ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser( STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", - STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")/*)*/; + STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); std::shared_ptr> mdp = mdpParser->getMdp(); std::shared_ptr> matrix = mdp->getTransitionMatrix(); From 5e3a8a12326a6dd5cc336ab01c7bb86522e0691e Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Mar 2013 16:21:15 +0100 Subject: [PATCH 5/8] Fixed wrong check for submatrix property of reward matrices. --- src/models/Dtmc.h | 9 ++++----- src/storage/SparseMatrix.h | 16 ++++++++++++++-- 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 7f0a0bb89..eefcc2ab5 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -50,11 +50,10 @@ public: throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; } if (this->getTransitionRewardMatrix() != nullptr) { - // FIXME: This is temporarily commented out, because the checking routine does not work properly. - //if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) { - // LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); - // throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; - //} + if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) { + LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; + } } } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index bde75c354..f5c4c954f 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -865,16 +865,28 @@ public: * @param matrix Matrix to check against. * @return True iff this is a submatrix of matrix. */ - bool isSubmatrixOf(SparseMatrix const & matrix) const { - // FIXME: THIS DOES NOT IMPLEMENT WHAT IS PROMISED. + bool isSubmatrixOf(SparseMatrix const& matrix) const { if (this->getRowCount() != matrix.getRowCount()) return false; if (this->getColumnCount() != matrix.getColumnCount()) return false; + /* for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem, ++elem2) { if (columnIndications[elem] < matrix.columnIndications[elem2]) return false; } } + */ + + for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { + for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem) { + // Skip over all entries of the other matrix that are before the current entry in + // the current matrix. + while (elem2 < matrix.rowIndications[row + 1] && matrix.columnIndications[elem2] < columnIndications[elem]) { + ++elem2; + } + if (!(elem2 < matrix.rowIndications[row + 1]) || columnIndications[elem] != matrix.columnIndications[elem2]) return false; + } + } return true; } From 4bcb26ab965bcd3c75836f9b4dec8aea8dabc0d4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 8 Mar 2013 16:33:52 +0100 Subject: [PATCH 6/8] Included subset-test in bitvector. --- src/storage/BitVector.h | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 801ec2bb2..e6d0add3e 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -392,6 +392,23 @@ public: return result; } + /*! + * Checks whether all bits that are set in the current bit vector are also set in the given bit + * vector. + * @param bv A reference to the bit vector whose bits are (possibly) a superset of the bits of + * the current bit vector. + * @returns True iff all bits that are set in the current bit vector are also set in the given bit + * vector. + */ + bool isContainedIn(BitVector const& bv) const { + for (uint_fast64_t i = 0; i < this->bucketCount; ++i) { + if ((this->bucketArray[i] & bv.bucketArray[i]) != bv.bucketArray[i]) { + return false; + } + } + return true; + } + /*! * Adds all indices of bits set to one to the provided list. * @param list The list to which to append the indices. From 34b85b956ee4d5c7d9fe29cc992e323bddf0c14c Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 9 Mar 2013 00:36:39 +0100 Subject: [PATCH 7/8] Moved model checking of DTMCs to superclass. Now, each DTMC model checker only needs to implement matrix-vector multiplication and linear equation solving to be able to fully model check DTMCs. Added subset/disjoint functionality to bit vector. Changed tests for MDP and DTMC model checking a bit. --- src/modelchecker/AbstractModelChecker.h | 79 ++++ src/modelchecker/DtmcPrctlModelChecker.h | 334 ++++++++++++----- src/modelchecker/EigenDtmcPrctlModelChecker.h | 244 ++++-------- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 354 +++--------------- src/storage/BitVector.h | 17 + src/utility/ConstTemplates.h | 3 + .../EigenDtmcPrctModelCheckerTest.cpp | 164 ++++++++ .../GmmxxDtmcPrctModelCheckerTest.cpp | 20 +- .../GmmxxMdpPrctModelCheckerTest.cpp | 36 +- 9 files changed, 648 insertions(+), 603 deletions(-) create mode 100644 test/functional/EigenDtmcPrctModelCheckerTest.cpp diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 698aaa466..5517dbacd 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -71,6 +71,85 @@ public: return nullptr; } + /*! + * Checks the given state formula on the DTMC and prints the result (true/false) for all initial + * states. + * @param stateFormula The formula to be checked. + */ + void check(const storm::formula::AbstractStateFormula& stateFormula) const { + std::cout << std::endl; + LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); + std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; + storm::storage::BitVector* result = nullptr; + try { + result = stateFormula.check(*this); + LOG4CPLUS_INFO(logger, "Result for initial states:"); + std::cout << "Result for initial states:" << std::endl; + for (auto initialState : model.getLabeledStates("init")) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); + std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; + } + delete result; + } catch (std::exception& e) { + std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; + if (result != nullptr) { + delete result; + } + } + std::cout << std::endl; + storm::utility::printSeparationLine(std::cout); + } + + /*! + * Checks the given operator (with no bound) on the DTMC and prints the result + * (probability/rewards) for all initial states. + * @param noBoundFormula The formula to be checked. + */ + void check(const storm::formula::NoBoundOperator& noBoundFormula) const { + std::cout << std::endl; + LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); + std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; + std::vector* result = nullptr; + try { + result = noBoundFormula.check(*this); + LOG4CPLUS_INFO(logger, "Result for initial states:"); + std::cout << "Result for initial states:" << std::endl; + for (auto initialState : *model.getLabeledStates("init")) { + LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); + std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; + } + delete result; + } catch (std::exception& e) { + std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl; + if (result != nullptr) { + delete result; + } + } + std::cout << std::endl; + storm::utility::printSeparationLine(std::cout); + } + + /*! + * The check method for a formula with an AP node as root in its formula tree + * + * @param formula The Ap state formula to check + * @returns The set of states satisfying the formula, represented by a bit vector + */ + storm::storage::BitVector* checkAp(const storm::formula::Ap& formula) const { + if (formula.getAp().compare("true") == 0) { + return new storm::storage::BitVector(model.getNumberOfStates(), true); + } else if (formula.getAp().compare("false") == 0) { + return new storm::storage::BitVector(model.getNumberOfStates()); + } + + if (!model.hasAtomicProposition(formula.getAp())) { + LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); + throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; + } + + return new storm::storage::BitVector(*model.getLabeledStates(formula.getAp())); + } + /*! * The check method for a state formula with an And node as root in its formula tree * diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h index 0e16dca5f..d38e6f2b3 100644 --- a/src/modelchecker/DtmcPrctlModelChecker.h +++ b/src/modelchecker/DtmcPrctlModelChecker.h @@ -8,6 +8,8 @@ #ifndef STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ #define STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ +#include + #include "src/formula/Formulas.h" #include "src/utility/Vector.h" #include "src/storage/SparseMatrix.h" @@ -16,12 +18,11 @@ #include "src/storage/BitVector.h" #include "src/exceptions/InvalidPropertyException.h" #include "src/utility/Vector.h" +#include "src/utility/GraphAnalyzer.h" #include "src/modelchecker/AbstractModelChecker.h" -#include #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" - extern log4cplus::Logger logger; namespace storm { @@ -38,8 +39,7 @@ namespace modelChecker { * @attention This class is abstract. */ template -class DtmcPrctlModelChecker : - public AbstractModelChecker { +class DtmcPrctlModelChecker : public AbstractModelChecker { public: /*! @@ -47,8 +47,7 @@ public: * * @param model The dtmc model which is checked. */ - explicit DtmcPrctlModelChecker(storm::models::Dtmc& model) - : AbstractModelChecker(model) { + explicit DtmcPrctlModelChecker(storm::models::Dtmc& model) : AbstractModelChecker(model) { // Intentionally left empty. } @@ -58,6 +57,7 @@ public: * @param modelChecker The model checker that is copied. */ explicit DtmcPrctlModelChecker(const storm::modelChecker::DtmcPrctlModelChecker* modelChecker) : AbstractModelChecker(modelChecker) { + // Intentionally left empty. } /*! @@ -74,93 +74,6 @@ public: return AbstractModelChecker::template getModel>(); } - /*! - * Sets the DTMC model which is checked - * @param model - */ - void setModel(storm::models::Dtmc& model) { - AbstractModelChecker::setModel(model); - } - - /*! - * The check method for a formula with an AP node as root in its formula tree - * - * @param formula The Ap state formula to check - * @returns The set of states satisfying the formula, represented by a bit vector - */ - storm::storage::BitVector* checkAp(const storm::formula::Ap& formula) const { - if (formula.getAp().compare("true") == 0) { - return new storm::storage::BitVector(this->getModel().getNumberOfStates(), true); - } else if (formula.getAp().compare("false") == 0) { - return new storm::storage::BitVector(this->getModel().getNumberOfStates()); - } - - if (!this->getModel().hasAtomicProposition(formula.getAp())) { - LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid."); - throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; - } - - return new storm::storage::BitVector(*this->getModel().getLabeledStates(formula.getAp())); - } - - /*! - * Checks the given state formula on the DTMC and prints the result (true/false) for all initial - * states. - * @param stateFormula The formula to be checked. - */ - void check(const storm::formula::AbstractStateFormula& stateFormula) const { - std::cout << std::endl; - LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString()); - std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl; - storm::storage::BitVector* result = nullptr; - try { - result = stateFormula.check(*this); - LOG4CPLUS_INFO(logger, "Result for initial states:"); - std::cout << "Result for initial states:" << std::endl; - for (auto initialState : *this->getModel().getLabeledStates("init")) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); - std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; - } - delete result; - } catch (std::exception& e) { - std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl; - if (result != nullptr) { - delete result; - } - } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); - } - - /*! - * Checks the given operator (with no bound) on the DTMC and prints the result - * (probability/rewards) for all initial states. - * @param noBoundFormula The formula to be checked. - */ - void check(const storm::formula::NoBoundOperator& noBoundFormula) const { - std::cout << std::endl; - LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString()); - std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl; - std::vector* result = nullptr; - try { - result = noBoundFormula.check(*this); - LOG4CPLUS_INFO(logger, "Result for initial states:"); - std::cout << "Result for initial states:" << std::endl; - for (auto initialState : *this->getModel().getLabeledStates("init")) { - LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); - std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; - } - delete result; - } catch (std::exception& e) { - std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl; - if (result != nullptr) { - delete result; - } - } - std::cout << std::endl; - storm::utility::printSeparationLine(std::cout); - } - /*! * The check method for a state formula with a probabilistic operator node without bounds as root * in its formula tree @@ -182,7 +95,31 @@ public: * @param formula The Bounded Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const = 0; + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); + + // Copy the matrix before we make any changes. + storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); + + // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. + tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); + + // Delete obsolete intermediates. + delete leftStates; + delete rightStates; + + // Create the vector with which to multiply. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); + + // Perform the matrix vector multiplication as often as required by the formula bound. + this->performMatrixVectorMultiplication(tmpMatrix, &result, nullptr, formula.getBound()); + + // Return result. + return result; + } /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -190,7 +127,23 @@ public: * @param formula The Next path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const = 0; + virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const { + // First, we need to compute the states that satisfy the child formula of the next-formula. + storm::storage::BitVector* nextStates = formula.getChild().check(*this); + + // Create the vector with which to multiply and initialize it correctly. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne()); + + // Delete obsolete intermediate. + delete nextStates; + + // Perform one single matrix-vector multiplication. + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result); + + // Return result. + return result; + } /*! * The check method for a path formula with a Bounded Eventually operator node as root in its @@ -239,7 +192,68 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const = 0; + virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); + + // Then, we need to identify the states which have to be taken out of the matrix, i.e. + // all states that have probability 0 and 1 of satisfying the until-formula. + storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); + storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); + storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); + + // Delete intermediate results that are obsolete now. + delete leftStates; + delete rightStates; + + // Perform some logging. + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); + storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Create resulting vector. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + + // Only try to solve system if there are states for which the probability is unknown. + uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); + if (maybeStatesSetBitCount > 0 && !qualitative) { + // Now we can eliminate the rows and columns from the original transition probability matrix. + storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix->convertToEquationSystem(); + + // Initialize the x vector with 0.5 for each element. This is the initial guess for + // the iterative solvers. It should be safe as for all 'maybe' states we know that the + // probability is strictly larger than 0. + std::vector* x = new std::vector(maybeStatesSetBitCount, Type(0.5)); + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some 'yes' state. + std::vector b(maybeStatesSetBitCount); + this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b); + + this->solveEquationSystem(*submatrix, &x, b); + + // Delete the created submatrix. + delete submatrix; + + // Set values of resulting vector according to result. + storm::utility::setVectorValues(result, maybeStates, *x); + } else if (qualitative) { + // If we only need a qualitative result, we can safely assume that the results will only be compared to + // bounds which are either 0 or 1. Setting the value to 0.5 is thus safe. + storm::utility::setVectorValues(result, maybeStates, Type(0.5)); + } + + // Set values of resulting vector that are known exactly. + storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); + + return result; + } /*! * The check method for a path formula with an Instantaneous Reward operator node as root in its @@ -248,7 +262,22 @@ public: * @param formula The Instantaneous Reward formula to check * @returns for each state the reward that the instantaneous reward yields */ - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const = 0; + virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const { + // Only compute the result if the model has a state-based reward model. + if (!this->getModel().hasStateRewards()) { + LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); + throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; + } + + // Initialize result to state rewards of the model. + std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); + + // Perform the actual matrix-vector multiplication as long as the bound of the formula is met. + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result, nullptr, formula.getBound()); + + // Return result. + return result; + } /*! * The check method for a path formula with a Cumulative Reward operator node as root in its @@ -257,7 +286,32 @@ public: * @param formula The Cumulative Reward formula to check * @returns for each state the reward that the cumulative reward yields */ - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const = 0; + virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const { + // Only compute the result if the model has at least one reward model. + if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { + LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); + throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; + } + + // Compute the reward vector to add in each step based on the available reward models. + std::vector* totalRewardVector = nullptr; + if (this->getModel().hasTransitionRewards()) { + totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); + if (this->getModel().hasStateRewards()) { + gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector); + } + } else { + totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); + } + + std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); + + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result, totalRewardVector, formula.getBound()); + + // Delete temporary variables and return result. + delete totalRewardVector; + return result; + } /*! * The check method for a path formula with a Reachability Reward operator node as root in its @@ -266,10 +320,90 @@ public: * @param formula The Reachbility Reward formula to check * @returns for each state the reward that the reachability reward yields */ - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const = 0; + virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const { + // Only compute the result if the model has at least one reward model. + if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { + LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); + throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; + } + + // Determine the states for which the target predicate holds. + storm::storage::BitVector* targetStates = formula.getChild().check(*this); + + // Determine which states have a reward of infinity by definition. + storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); + storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); + storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates); + infinityStates.complement(); + + // Create resulting vector. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + + // Check whether there are states for which we have to compute the result. + storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; + const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); + if (maybeStatesSetBitCount > 0) { + // Now we can eliminate the rows and columns from the original transition probability matrix. + storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix->convertToEquationSystem(); + + // Initialize the x vector with 1 for each element. This is the initial guess for + // the iterative solvers. + std::vector* x = new std::vector(maybeStatesSetBitCount, storm::utility::constGetOne()); + + // Prepare the right-hand side of the equation system. + std::vector* b = new std::vector(maybeStatesSetBitCount); + if (this->getModel().hasTransitionRewards()) { + // If a transition-based reward model is available, we initialize the right-hand + // side to the vector resulting from summing the rows of the pointwise product + // of the transition probability matrix and the transition reward matrix. + std::vector* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); + storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector); + delete pointwiseProductRowSumVector; + + if (this->getModel().hasStateRewards()) { + // If a state-based reward model is also available, we need to add this vector + // as well. As the state reward vector contains entries not just for the states + // that we still consider (i.e. maybeStates), we need to extract these values + // first. + std::vector* subStateRewards = new std::vector(maybeStatesSetBitCount); + storm::utility::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); + gmm::add(*subStateRewards, *b); + delete subStateRewards; + } + } else { + // If only a state-based reward model is available, we take this vector as the + // right-hand side. As the state reward vector contains entries not just for the + // states that we still consider (i.e. maybeStates), we need to extract these values + // first. + storm::utility::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); + } + + this->solveEquationSystem(*submatrix, &x, *b); + + // Set values of resulting vector according to result. + storm::utility::setVectorValues(result, maybeStates, *x); + + // Delete temporary matrix and right-hand side. + delete submatrix; + delete b; + } + + // Set values of resulting vector that are known exactly. + storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); + + // Delete temporary storages and return result. + delete targetStates; + return result; + } private: -// storm::models::Dtmc& model; + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const = 0; + + virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector& b) const = 0; }; } //namespace modelChecker diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h index 6965b3a0c..167b02f72 100644 --- a/src/modelchecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h @@ -38,183 +38,101 @@ namespace modelChecker { template class EigenDtmcPrctlModelChecker : public DtmcPrctlModelChecker { -public: - explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { } - - virtual ~EigenDtmcPrctlModelChecker() { } - - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); - - // Copy the matrix before we make any changes. - storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionProbabilityMatrix()); - - // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing((~*leftStates | *rightStates) | *rightStates); - - // Transform the transition probability matrix to the eigen format to use its arithmetic. - Eigen::SparseMatrix* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(tmpMatrix); - - // Create the vector with which to multiply. - uint_fast64_t stateCount = this->getModel().getNumberOfStates(); - - typedef Eigen::Matrix VectorType; - typedef Eigen::Map MapType; - - std::vector* result = new std::vector(stateCount); - - storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); - - Type *p = &((*result)[0]); // get the address storing the data for result - MapType vectorMap(p, result->size()); // vectorMap shares data - +typedef Eigen::Matrix VectorType; +typedef Eigen::Map MapType; - // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - for (uint_fast64_t i = 0, bound = formula.getBound(); i < bound; ++i) { - vectorMap = (*eigenMatrix) * vectorMap; - } - - // Delete intermediate results. - delete leftStates; - delete rightStates; - delete eigenMatrix; - - return result; +public: + explicit EigenDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { + // Intentionally left empty. } - virtual std::vector* checkNext(const storm::formula::Next& formula) const { - // First, we need to compute the states that satisfy the sub-formula of the next-formula. - storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); + virtual ~EigenDtmcPrctlModelChecker() { + // Intentionally left empty. + } +private: + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector* summand, uint_fast64_t repetitions = 1) const { // Transform the transition probability matrix to the eigen format to use its arithmetic. - Eigen::SparseMatrix* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(this->getModel().getTransitionProbabilityMatrix()); - - // Create the vector with which to multiply and initialize it correctly. - std::vector x(this->getModel().getNumberOfStates()); - - storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne()); - - // Delete not needed next states bit vector. - delete nextStates; - - typedef Eigen::Matrix VectorType; - typedef Eigen::Map MapType; - - Type *px = &(x[0]); // get the address storing the data for x - MapType vectorX(px, x.size()); // vectorX shares data + Eigen::SparseMatrix* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(matrix); - // Create resulting vector. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + Type* p = &((**vector)[0]); // get the address storing the data for result + MapType vectorMap(p, (*vector)->size()); // vectorMap shares data - // Type *pr = &((*result)[0]); // get the address storing the data for result - MapType vectorResult(px, result->size()); // vectorResult shares data + p = &((*summand)[0]); + MapType summandMap(p, summand->size()); - // Perform the actual computation. - vectorResult = (*eigenMatrix) * vectorX; + // Now perform matrix-vector multiplication as long as we meet the bound. + std::vector* swap = nullptr; + std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); + for (uint_fast64_t i = 0; i < repetitions; ++i) { + vectorMap = (*eigenMatrix) * (vectorMap); - // Delete temporary matrix and return result. + // If requested, add an offset to the current result vector. + if (summand != nullptr) { + vectorMap = vectorMap + summandMap; + } + } delete eigenMatrix; - return result; } - virtual std::vector* checkUntil(const storm::formula::Until& formula) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft()); - storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight()); - - // Then, we need to identify the states which have to be taken out of the matrix, i.e. - // all states that have probability 0 and 1 of satisfying the until-formula. - storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); - storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); - storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); - - delete leftStates; - delete rightStates; - - LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); - LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - - // Create resulting vector and set values accordingly. - uint_fast64_t stateCount = this->getModel().getNumberOfStates(); - std::vector* result = new std::vector(stateCount); - - // Only try to solve system if there are states for which the probability is unknown. - if (maybeStates.getNumberOfSetBits() > 0) { - typedef Eigen::Matrix VectorType; - typedef Eigen::Map MapType; - - // Now we can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); - // Converting the matrix to the form needed for the equation system. That is, we go from - // x = A*x + b to (I-A)x = b. - submatrix->convertToEquationSystem(); - - // Transform the submatric matrix to the eigen format to use its solvers - Eigen::SparseMatrix* eigenSubMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(submatrix); - delete submatrix; - - // Initialize the x vector with 0.5 for each element. This is the initial guess for - // the iterative solvers. It should be safe as for all 'maybe' states we know that the - // probability is strictly larger than 0. - std::vector x(maybeStates.getNumberOfSetBits(), Type(0.5)); - - // Map for x - Type *px = &(x[0]); // get the address storing the data for x - MapType vectorX(px, x.size()); // vectorX shares data - - - // Prepare the right-hand side of the equation system. For entry i this corresponds to - // the accumulated probability of going from state i to some 'yes' state. - std::vector b(maybeStates.getNumberOfSetBits()); - - Type *pb = &(b[0]); // get the address storing the data for b - MapType vectorB(pb, b.size()); // vectorB shares data - - this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &x); - - Eigen::BiCGSTAB> solver; - solver.compute(*eigenSubMatrix); - if(solver.info()!= Eigen::ComputationInfo::Success) { - // decomposition failed - LOG4CPLUS_ERROR(logger, "Decomposition of Submatrix failed!"); - } - - // Now do the actual solving. - LOG4CPLUS_INFO(logger, "Starting iterative solver."); - - solver.setTolerance(0.000001); - - vectorX = solver.solveWithGuess(vectorB, vectorX); - - if(solver.info() == Eigen::ComputationInfo::InvalidInput) { - // solving failed - LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput"); - } else if(solver.info() == Eigen::ComputationInfo::NoConvergence) { - // NoConvergence - throw storm::exceptions::NoConvergenceException("Solving of Submatrix with Eigen failed", solver.iterations(), solver.maxIterations()); - } else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) { - // NumericalIssue - LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); - } else if(solver.info() == Eigen::ComputationInfo::Success) { - // solving Success - LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success"); - } - - // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); - - // Delete temporary matrix. - delete eigenSubMatrix; + /*! + * Solves the linear equation system Ax=b with the given parameters. + * + * @param A The matrix A specifying the coefficients of the linear equations. + * @param x The vector x for which to solve the equations. The initial value of the elements of + * this vector are used as the initial guess and might thus influence performance and convergence. + * @param b The vector b specifying the values on the right-hand-sides of the equations. + * @return The solution of the system of linear equations in form of the elements of the vector + * x. + */ + virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector& b) const { + // Get the settings object to customize linear solving. + storm::settings::Settings* s = storm::settings::instance(); + + // Transform the submatric matrix to the eigen format to use its solvers + Eigen::SparseMatrix* eigenMatrix = storm::adapters::EigenAdapter::toEigenSparseMatrix(matrix); + + Eigen::BiCGSTAB> solver; + solver.compute(*eigenMatrix); + if(solver.info()!= Eigen::ComputationInfo::Success) { + // decomposition failed + LOG4CPLUS_ERROR(logger, "Decomposition of matrix failed!"); + } + solver.setMaxIterations(s->get("maxiter")); + solver.setTolerance(s->get("precision")); + + std::cout << matrix.toString(nullptr) << std::endl; + std::cout << **vector << std::endl; + std::cout << b << std::endl; + + std::cout << *eigenMatrix << std::endl; + + // Map for x + Type *px = &((**vector)[0]); // get the address storing the data for x + MapType vectorX(px, (*vector)->size()); // vectorX shares data + + Type *pb = &(b[0]); // get the address storing the data for b + MapType vectorB(pb, b.size()); // vectorB shares data + + vectorX = solver.solveWithGuess(vectorB, vectorX); + + std::cout << **vector << std::endl; + + if(solver.info() == Eigen::ComputationInfo::InvalidInput) { + // solving failed + LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: InvalidInput"); + } else if(solver.info() == Eigen::ComputationInfo::NoConvergence) { + // NoConvergence + throw storm::exceptions::NoConvergenceException() << "Failed to converge within " << solver.iterations() << " out of a maximum of " << solver.maxIterations() << " iterations."; + } else if(solver.info() == Eigen::ComputationInfo::NumericalIssue) { + // NumericalIssue + LOG4CPLUS_ERROR(logger, "Solving of Submatrix failed: NumericalIssue"); + } else if(solver.info() == Eigen::ComputationInfo::Success) { + // solving Success + LOG4CPLUS_INFO(logger, "Solving of Submatrix succeeded: Success"); } - storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); - - return result; + delete eigenMatrix; } }; diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index 9213df3fa..97c41093f 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -12,7 +12,6 @@ #include "src/models/Dtmc.h" #include "src/modelchecker/DtmcPrctlModelChecker.h" -#include "src/utility/GraphAnalyzer.h" #include "src/utility/Vector.h" #include "src/utility/ConstTemplates.h" #include "src/utility/Settings.h" @@ -36,300 +35,15 @@ namespace modelChecker { * A model checking engine that makes use of the gmm++ backend. */ template -class GmmxxDtmcPrctlModelChecker - : public DtmcPrctlModelChecker { +class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker { public: - explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) - : DtmcPrctlModelChecker(dtmc) { + explicit GmmxxDtmcPrctlModelChecker(storm::models::Dtmc& dtmc) : DtmcPrctlModelChecker(dtmc) { // Intentionally left empty. } - virtual ~GmmxxDtmcPrctlModelChecker() { } + virtual ~GmmxxDtmcPrctlModelChecker() { - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = formula.getLeft().check(*this); - storm::storage::BitVector* rightStates = formula.getRight().check(*this); - - // Copy the matrix before we make any changes. - storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); - - // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates); - - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(tmpMatrix); - - // Create the vector with which to multiply. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); - - // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - std::vector* swap = nullptr; - std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); - for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *tmpResult); - swap = tmpResult; - tmpResult = result; - result = swap; - } - delete tmpResult; - - // Delete intermediate results and return result. - delete gmmxxMatrix; - delete leftStates; - delete rightStates; - return result; - } - - virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formula of the next-formula. - storm::storage::BitVector* nextStates = formula.getChild().check(*this); - - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); - - // Create the vector with which to multiply and initialize it correctly. - std::vector x(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(&x, *nextStates, storm::utility::constGetOne()); - - // Delete obsolete sub-result. - delete nextStates; - - // Create resulting vector. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - - // Perform the actual computation, namely matrix-vector multiplication. - gmm::mult(*gmmxxMatrix, x, *result); - - // Delete temporary matrix and return result. - delete gmmxxMatrix; - return result; - } - - virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = formula.getLeft().check(*this); - storm::storage::BitVector* rightStates = formula.getRight().check(*this); - - // Then, we need to identify the states which have to be taken out of the matrix, i.e. - // all states that have probability 0 and 1 of satisfying the until-formula. - storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); - storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); - storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); - - // Delete sub-results that are obsolete now. - delete leftStates; - delete rightStates; - - LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); - LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - - // Create resulting vector. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - - // Only try to solve system if there are states for which the probability is unknown. - uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - if (mayBeStatesSetBitCount > 0 && !qualitative) { - // Now we can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix->convertToEquationSystem(); - - // Transform the submatrix to the gmm++ format to use its solvers. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); - delete submatrix; - - // Initialize the x vector with 0.5 for each element. This is the initial guess for - // the iterative solvers. It should be safe as for all 'maybe' states we know that the - // probability is strictly larger than 0. - std::vector x(mayBeStatesSetBitCount, Type(0.5)); - - // Prepare the right-hand side of the equation system. For entry i this corresponds to - // the accumulated probability of going from state i to some 'yes' state. - std::vector b(mayBeStatesSetBitCount); - this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b); - - // Solve the corresponding system of linear equations. - this->solveLinearEquationSystem(*gmmxxMatrix, x, b); - - // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); - - // Delete temporary matrix. - delete gmmxxMatrix; - } else if (qualitative) { - // If we only need a qualitative result, we can safely assume that the results will only be compared to - // bounds which are either 0 or 1. Setting the value to 0.5 is thus safe. - storm::utility::setVectorValues(result, maybeStates, Type(0.5)); - } - - // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); - - return result; - } - - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const { - // Only compute the result if the model has a state-based reward model. - if (!this->getModel().hasStateRewards()) { - LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); - throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; - } - - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); - - // Initialize result to state rewards of the model. - std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); - - // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - std::vector* swap = nullptr; - std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); - for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *tmpResult); - swap = tmpResult; - tmpResult = result; - result = swap; - } - - // Delete temporary variables and return result. - delete tmpResult; - delete gmmxxMatrix; - return result; - } - - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const { - // Only compute the result if the model has at least one reward model. - if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { - LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); - throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; - } - - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); - - // Compute the reward vector to add in each step based on the available reward models. - std::vector* totalRewardVector = nullptr; - if (this->getModel().hasTransitionRewards()) { - totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - if (this->getModel().hasStateRewards()) { - gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector); - } - } else { - totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); - } - - std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); - - // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - std::vector* swap = nullptr; - std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); - for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *tmpResult); - swap = tmpResult; - tmpResult = result; - result = swap; - - // Add the reward vector to the result. - gmm::add(*totalRewardVector, *result); - } - - // Delete temporary variables and return result. - delete tmpResult; - delete gmmxxMatrix; - delete totalRewardVector; - return result; - } - - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const { - // Only compute the result if the model has at least one reward model. - if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { - LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); - throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; - } - - // Determine the states for which the target predicate holds. - storm::storage::BitVector* targetStates = formula.getChild().check(*this); - - // Determine which states have a reward of infinity by definition. - storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); - storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates); - infinityStates.complement(); - - // Create resulting vector. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - - // Check whether there are states for which we have to compute the result. - storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; - const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - if (maybeStatesSetBitCount > 0) { - // Now we can eliminate the rows and columns from the original transition probability matrix. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates); - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix->convertToEquationSystem(); - - // Transform the submatrix to the gmm++ format to use its solvers. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); - delete submatrix; - - // Initialize the x vector with 1 for each element. This is the initial guess for - // the iterative solvers. - std::vector x(maybeStatesSetBitCount, storm::utility::constGetOne()); - - // Prepare the right-hand side of the equation system. - std::vector* b = new std::vector(maybeStatesSetBitCount); - if (this->getModel().hasTransitionRewards()) { - // If a transition-based reward model is available, we initialize the right-hand - // side to the vector resulting from summing the rows of the pointwise product - // of the transition probability matrix and the transition reward matrix. - std::vector* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector); - delete pointwiseProductRowSumVector; - - if (this->getModel().hasStateRewards()) { - // If a state-based reward model is also available, we need to add this vector - // as well. As the state reward vector contains entries not just for the states - // that we still consider (i.e. maybeStates), we need to extract these values - // first. - std::vector* subStateRewards = new std::vector(maybeStatesSetBitCount); - storm::utility::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); - gmm::add(*subStateRewards, *b); - delete subStateRewards; - } - } else { - // If only a state-based reward model is available, we take this vector as the - // right-hand side. As the state reward vector contains entries not just for the - // states that we still consider (i.e. maybeStates), we need to extract these values - // first. - storm::utility::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); - } - - // Solve the corresponding system of linear equations. - this->solveLinearEquationSystem(*gmmxxMatrix, x, *b); - - // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, x); - - // Delete temporary matrix and right-hand side. - delete gmmxxMatrix; - delete b; - } - - // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); - - // Delete temporary storages and return result. - delete targetStates; - return result; } /*! @@ -337,7 +51,7 @@ public: * @return The name of this module. */ static std::string getModuleName() { - return "gmm++det"; + return "gmm++"; } /*! @@ -381,6 +95,29 @@ public: } private: + + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector* summand, uint_fast64_t repetitions = 1) const { + // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + + // Now perform matrix-vector multiplication as long as we meet the bound. + std::vector* swap = nullptr; + std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); + for (uint_fast64_t i = 0; i < repetitions; ++i) { + gmm::mult(*gmmxxMatrix, **vector, *tmpResult); + swap = tmpResult; + tmpResult = *vector; + *vector = swap; + + // If requested, add an offset to the current result vector. + if (summand != nullptr) { + gmm::add(*summand, **vector); + } + } + delete tmpResult; + delete gmmxxMatrix; + } + /*! * Solves the linear equation system Ax=b with the given parameters. * @@ -391,10 +128,13 @@ private: * @return The solution of the system of linear equations in form of the elements of the vector * x. */ - void solveLinearEquationSystem(gmm::csr_matrix const& A, std::vector& x, std::vector const& b) const { + virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector& b) const { // Get the settings object to customize linear solving. storm::settings::Settings* s = storm::settings::instance(); + // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + gmm::csr_matrix* A = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + // Prepare an iteration object that determines the accuracy, maximum number of iterations // and the like. gmm::iteration iter(s->get("precision"), 0, s->get("maxiter")); @@ -415,13 +155,13 @@ private: if (s->getString("lemethod") == "bicgstab") { LOG4CPLUS_INFO(logger, "Using BiCGStab method."); if (precond == "ilu") { - gmm::bicgstab(A, x, b, gmm::ilu_precond>(A), iter); + gmm::bicgstab(*A, **vector, b, gmm::ilu_precond>(*A), iter); } else if (precond == "diagonal") { - gmm::bicgstab(A, x, b, gmm::diagonal_precond>(A), iter); + gmm::bicgstab(*A, **vector, b, gmm::diagonal_precond>(*A), iter); } else if (precond == "ildlt") { - gmm::bicgstab(A, x, b, gmm::ildlt_precond>(A), iter); + gmm::bicgstab(*A, **vector, b, gmm::ildlt_precond>(*A), iter); } else if (precond == "none") { - gmm::bicgstab(A, x, b, gmm::identity_matrix(), iter); + gmm::bicgstab(*A, **vector, b, gmm::identity_matrix(), iter); } // Check if the solver converged and issue a warning otherwise. @@ -430,28 +170,16 @@ private: } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); } - // FIXME: gmres has been disabled, because it triggers gmm++ compilation errors - /* } else if (s->getString("lemethod").compare("gmres") == 0) { - LOG4CPLUS_INFO(logger, "Using GMRES method."); - if (precond.compare("ilu")) { - gmm::gmres(A, x, b, gmm::ilu_precond>(A), s->get("restart"), iter); - } else if (precond == "diagonal") { - gmm::gmres(A, x, b, gmm::diagonal_precond>(A), s->get("restart"), iter); - } else if (precond == "ildlt") { - gmm::gmres(A, x, b, gmm::ildlt_precond>(A), s->get("restart"), iter); - } else if (precond == "none") { - gmm::gmres(A, x, b, gmm::identity_matrix(), s->get("restart"), iter); - } */ } else if (s->getString("lemethod") == "qmr") { LOG4CPLUS_INFO(logger, "Using QMR method."); if (precond == "ilu") { - gmm::qmr(A, x, b, gmm::ilu_precond>(A), iter); + gmm::qmr(*A, **vector, b, gmm::ilu_precond>(*A), iter); } else if (precond == "diagonal") { - gmm::qmr(A, x, b, gmm::diagonal_precond>(A), iter); + gmm::qmr(*A, **vector, b, gmm::diagonal_precond>(*A), iter); } else if (precond == "ildlt") { - gmm::qmr(A, x, b, gmm::ildlt_precond>(A), iter); + gmm::qmr(*A, **vector, b, gmm::ildlt_precond>(*A), iter); } else if (precond == "none") { - gmm::qmr(A, x, b, gmm::identity_matrix(), iter); + gmm::qmr(*A, **vector, b, gmm::identity_matrix(), iter); } // Check if the solver converged and issue a warning otherwise. @@ -462,8 +190,10 @@ private: } } else if (s->getString("lemethod") == "jacobi") { LOG4CPLUS_INFO(logger, "Using Jacobi method."); - solveLinearEquationSystemWithJacobi(A, x, b); + solveLinearEquationSystemWithJacobi(*A, **vector, b); } + + delete A; } /*! diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index e6d0add3e..65ace6e3c 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -409,6 +409,23 @@ public: return true; } + /*! + * Checks whether none of the bits that are set in the current bit vector are also set in the + * given bit vector. + * @param bv A reference to the bit vector whose bits are (possibly) disjoint from the bits in + * the current bit vector. + * @returns True iff none of the bits that are set in the current bit vector are also set in the + * given bit vector. + */ + bool isDisjointFrom(BitVector const& bv) const { + for (uint_fast64_t i = 0; i < this->bucketCount; ++i) { + if ((this->bucketArray[i] & bv.bucketArray[i]) != 0) { + return false; + } + } + return true; + } + /*! * Adds all indices of bits set to one to the provided list. * @param list The list to which to append the indices. diff --git a/src/utility/ConstTemplates.h b/src/utility/ConstTemplates.h index ace4c7bd9..847c38174 100644 --- a/src/utility/ConstTemplates.h +++ b/src/utility/ConstTemplates.h @@ -18,6 +18,9 @@ #include +#include "src/exceptions/InvalidArgumentException.h" +#include "src/storage/BitVector.h" + namespace storm { namespace utility { diff --git a/test/functional/EigenDtmcPrctModelCheckerTest.cpp b/test/functional/EigenDtmcPrctModelCheckerTest.cpp new file mode 100644 index 000000000..224084e5c --- /dev/null +++ b/test/functional/EigenDtmcPrctModelCheckerTest.cpp @@ -0,0 +1,164 @@ +/* +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/utility/Settings.h" +#include "src/modelchecker/EigenDtmcPrctlModelChecker.h" +#include "src/parser/AutoParser.h" + +TEST(EigenDtmcPrctModelCheckerTest, Die) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/die/die.tra", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/die/die.coin_flips.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 14); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28); + + storm::modelChecker::EigenDtmcPrctlModelChecker mc(*dtmc); + + storm::formula::Ap* apFormula = new storm::formula::Ap("one"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("two"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("three"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get("precision")); + + delete probFormula; + delete result; + + storm::formula::Ap* done = new storm::formula::Ap("done"); + storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(done); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula); + + result = rewardFormula->check(mc); + + + ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->get("precision")); + + delete rewardFormula; + delete result; +} + +TEST(EigenDtmcPrctModelCheckerTest, Crowds) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.tra", STORM_CPP_TESTS_BASE_PATH "/functional/crowds/crowds5_5.lab", "", ""); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 8608); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 22461); + + storm::modelChecker::EigenDtmcPrctlModelChecker mc(*dtmc); + + storm::formula::Ap* apFormula = new storm::formula::Ap("observe0Greater1"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("observeIGreater1"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("observeOnlyTrueSender"); + eventuallyFormula = new storm::formula::Eventually(apFormula); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->get("precision")); + + delete probFormula; + delete result; +} + +TEST(EigenDtmcPrctModelCheckerTest, SynchronousLeader) { + storm::settings::Settings* s = storm::settings::instance(); + s->set("fix-deadlocks"); + storm::parser::AutoParser parser(STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.tra", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.lab", "", STORM_CPP_TESTS_BASE_PATH "/functional/synchronous_leader/leader4_8.pick.trans.rew"); + + ASSERT_EQ(parser.getType(), storm::models::DTMC); + + std::shared_ptr> dtmc = parser.getModel>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 12401); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28895); + + storm::modelChecker::EigenDtmcPrctlModelChecker mc(*dtmc); + + storm::formula::Ap* apFormula = new storm::formula::Ap("elected"); + storm::formula::Eventually* eventuallyFormula = new storm::formula::Eventually(apFormula); + storm::formula::ProbabilisticNoBoundOperator* probFormula = new storm::formula::ProbabilisticNoBoundOperator(eventuallyFormula); + + std::vector* result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - 1), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + storm::formula::BoundedUntil* boundedUntilFormula = new storm::formula::BoundedUntil(new storm::formula::Ap("true"), apFormula, 20); + probFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedUntilFormula); + + result = probFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->get("precision")); + + delete probFormula; + delete result; + + apFormula = new storm::formula::Ap("elected"); + storm::formula::ReachabilityReward* reachabilityRewardFormula = new storm::formula::ReachabilityReward(apFormula); + storm::formula::RewardNoBoundOperator* rewardFormula = new storm::formula::RewardNoBoundOperator(reachabilityRewardFormula); + + result = rewardFormula->check(mc); + + ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->get("precision")); + + delete rewardFormula; + delete result; +} +*/ diff --git a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp index 6c0fe540d..7d4161e8e 100644 --- a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp @@ -25,7 +25,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { std::vector* result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get("precision")); delete probFormula; delete result; @@ -36,7 +36,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get("precision")); delete probFormula; delete result; @@ -47,7 +47,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - ((double)1/6)) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - ((double)1/6)), s->get("precision")); delete probFormula; delete result; @@ -59,7 +59,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) { result = rewardFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - ((double)11/3)) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - ((double)11/3)), s->get("precision")); delete rewardFormula; delete result; @@ -85,7 +85,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { std::vector* result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - 0.3328800375801578281) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - 0.3328800375801578281), s->get("precision")); delete probFormula; delete result; @@ -96,7 +96,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - 0.1522173670950556501) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - 0.1522173670950556501), s->get("precision")); delete probFormula; delete result; @@ -107,7 +107,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - 0.32153724292835045) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - 0.32153724292835045), s->get("precision")); delete probFormula; delete result; @@ -133,7 +133,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { std::vector* result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - 1) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - 1), s->get("precision")); delete probFormula; delete result; @@ -144,7 +144,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - 0.9999965911265462636) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - 0.9999965911265462636), s->get("precision")); delete probFormula; delete result; @@ -155,7 +155,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { result = rewardFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[1] - 1.0448979591835938496) < s->get("precision")); + ASSERT_LT(std::abs((*result)[1] - 1.0448979591835938496), s->get("precision")); delete rewardFormula; delete result; diff --git a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp index 093afc33a..c2f1b3cac 100644 --- a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp @@ -24,7 +24,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { std::vector* result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.0277777612209320068) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get("precision")); delete probFormula; delete result; @@ -35,7 +35,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.0277777612209320068) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.0277777612209320068), s->get("precision")); delete probFormula; delete result; @@ -46,7 +46,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.0555555224418640136) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get("precision")); delete probFormula; delete result; @@ -57,7 +57,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.0555555224418640136) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.0555555224418640136), s->get("precision")); delete probFormula; delete result; @@ -68,7 +68,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.083333283662796020508) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get("precision")); delete probFormula; delete result; @@ -79,7 +79,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.083333283662796020508) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.083333283662796020508), s->get("precision")); delete probFormula; delete result; @@ -90,7 +90,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); delete rewardFormula; delete result; @@ -101,7 +101,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); delete rewardFormula; delete result; @@ -120,7 +120,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateRewardModelChecker); - ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); delete rewardFormula; delete result; @@ -131,7 +131,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateRewardModelChecker); - ASSERT_TRUE(std::abs((*result)[0] - 7.3333272933959960938) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); delete rewardFormula; delete result; @@ -150,7 +150,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateAndTransitionRewardModelChecker); - ASSERT_TRUE(std::abs((*result)[0] - (2 * 7.3333272933959960938)) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333272933959960938)), s->get("precision")); delete rewardFormula; delete result; @@ -161,7 +161,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateAndTransitionRewardModelChecker); - ASSERT_TRUE(std::abs((*result)[0] - (2 * 7.3333272933959960938)) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333272933959960938)), s->get("precision")); delete rewardFormula; delete result; @@ -186,7 +186,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { std::vector* result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 1) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); delete probFormula; delete result; @@ -197,7 +197,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 1) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 1), s->get("precision")); delete probFormula; delete result; @@ -208,7 +208,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.0625) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); delete probFormula; delete result; @@ -219,7 +219,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { result = probFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 0.0625) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get("precision")); delete probFormula; delete result; @@ -230,7 +230,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { result = rewardFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 4.28568908480604982) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get("precision")); delete rewardFormula; delete result; @@ -241,7 +241,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) { result = rewardFormula->check(mc); - ASSERT_TRUE(std::abs((*result)[0] - 4.2856904354441400784) < s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get("precision")); delete rewardFormula; delete result; From f1c379bbe350ea71453ccab9d6f02526b165cda1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 9 Mar 2013 21:18:36 +0100 Subject: [PATCH 8/8] Moved model checking functionality for MDPs for general superclass such that specialized model checkers only need to implement certain operations. Fixed tests. --- src/modelchecker/DtmcPrctlModelChecker.h | 38 +- src/modelchecker/GmmxxDtmcPrctlModelChecker.h | 44 ++- src/modelchecker/GmmxxMdpPrctlModelChecker.h | 369 ++---------------- src/modelchecker/MdpPrctlModelChecker.h | 255 +++++++++++- .../GmmxxMdpPrctModelCheckerTest.cpp | 12 +- 5 files changed, 325 insertions(+), 393 deletions(-) diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h index d38e6f2b3..3fa4cc238 100644 --- a/src/modelchecker/DtmcPrctlModelChecker.h +++ b/src/modelchecker/DtmcPrctlModelChecker.h @@ -115,7 +115,7 @@ public: storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); // Perform the matrix vector multiplication as often as required by the formula bound. - this->performMatrixVectorMultiplication(tmpMatrix, &result, nullptr, formula.getBound()); + this->performMatrixVectorMultiplication(tmpMatrix, *result, nullptr, formula.getBound()); // Return result. return result; @@ -139,7 +139,7 @@ public: delete nextStates; // Perform one single matrix-vector multiplication. - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result); // Return result. return result; @@ -228,20 +228,20 @@ public: // Initialize the x vector with 0.5 for each element. This is the initial guess for // the iterative solvers. It should be safe as for all 'maybe' states we know that the // probability is strictly larger than 0. - std::vector* x = new std::vector(maybeStatesSetBitCount, Type(0.5)); + std::vector x(maybeStatesSetBitCount, Type(0.5)); // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. std::vector b(maybeStatesSetBitCount); this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, statesWithProbability1, &b); - this->solveEquationSystem(*submatrix, &x, b); + this->solveEquationSystem(*submatrix, x, b); // Delete the created submatrix. delete submatrix; // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, *x); + storm::utility::setVectorValues(result, maybeStates, x); } else if (qualitative) { // If we only need a qualitative result, we can safely assume that the results will only be compared to // bounds which are either 0 or 1. Setting the value to 0.5 is thus safe. @@ -273,7 +273,7 @@ public: std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); // Perform the actual matrix-vector multiplication as long as the bound of the formula is met. - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result, nullptr, formula.getBound()); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); // Return result. return result; @@ -306,7 +306,7 @@ public: std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); - this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), &result, totalRewardVector, formula.getBound()); + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound()); // Delete temporary variables and return result. delete totalRewardVector; @@ -351,16 +351,16 @@ public: // Initialize the x vector with 1 for each element. This is the initial guess for // the iterative solvers. - std::vector* x = new std::vector(maybeStatesSetBitCount, storm::utility::constGetOne()); + std::vector x(maybeStatesSetBitCount, storm::utility::constGetOne()); // Prepare the right-hand side of the equation system. - std::vector* b = new std::vector(maybeStatesSetBitCount); + std::vector b(maybeStatesSetBitCount); if (this->getModel().hasTransitionRewards()) { // If a transition-based reward model is available, we initialize the right-hand // side to the vector resulting from summing the rows of the pointwise product // of the transition probability matrix and the transition reward matrix. std::vector* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector); + storm::utility::selectVectorValues(&b, maybeStates, *pointwiseProductRowSumVector); delete pointwiseProductRowSumVector; if (this->getModel().hasStateRewards()) { @@ -368,27 +368,25 @@ public: // as well. As the state reward vector contains entries not just for the states // that we still consider (i.e. maybeStates), we need to extract these values // first. - std::vector* subStateRewards = new std::vector(maybeStatesSetBitCount); - storm::utility::selectVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); - gmm::add(*subStateRewards, *b); - delete subStateRewards; + std::vector subStateRewards(maybeStatesSetBitCount); + storm::utility::selectVectorValues(&subStateRewards, maybeStates, *this->getModel().getStateRewardVector()); + gmm::add(subStateRewards, b); } } else { // If only a state-based reward model is available, we take this vector as the // right-hand side. As the state reward vector contains entries not just for the // states that we still consider (i.e. maybeStates), we need to extract these values // first. - storm::utility::selectVectorValues(b, maybeStates, *this->getModel().getStateRewardVector()); + storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getStateRewardVector()); } - this->solveEquationSystem(*submatrix, &x, *b); + this->solveEquationSystem(*submatrix, x, b); // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, *x); + storm::utility::setVectorValues(result, maybeStates, x); // Delete temporary matrix and right-hand side. delete submatrix; - delete b; } // Set values of resulting vector that are known exactly. @@ -401,9 +399,9 @@ public: } private: - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const = 0; + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const = 0; - virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector& b) const = 0; + virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector const& b) const = 0; }; } //namespace modelChecker diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h index 97c41093f..c96fb4cac 100644 --- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h @@ -96,25 +96,33 @@ public: private: - virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector* summand, uint_fast64_t repetitions = 1) const { + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand, uint_fast64_t repetitions = 1) const { // Transform the transition probability matrix to the gmm++ format to use its arithmetic. gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); // Now perform matrix-vector multiplication as long as we meet the bound. std::vector* swap = nullptr; - std::vector* tmpResult = new std::vector(this->getModel().getNumberOfStates()); + std::vector* currentVector = &vector; + std::vector* tmpVector = new std::vector(this->getModel().getNumberOfStates()); for (uint_fast64_t i = 0; i < repetitions; ++i) { - gmm::mult(*gmmxxMatrix, **vector, *tmpResult); - swap = tmpResult; - tmpResult = *vector; - *vector = swap; + gmm::mult(*gmmxxMatrix, *currentVector, *tmpVector); + swap = tmpVector; + tmpVector = currentVector; + currentVector = swap; // If requested, add an offset to the current result vector. if (summand != nullptr) { - gmm::add(*summand, **vector); + gmm::add(*summand, *currentVector); } } - delete tmpResult; + + if (repetitions % 2 == 1) { + std::swap(vector, *currentVector); + delete currentVector; + } else { + delete tmpVector; + } + delete gmmxxMatrix; } @@ -128,7 +136,7 @@ private: * @return The solution of the system of linear equations in form of the elements of the vector * x. */ - virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector** vector, std::vector& b) const { + virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector const& b) const { // Get the settings object to customize linear solving. storm::settings::Settings* s = storm::settings::instance(); @@ -155,13 +163,13 @@ private: if (s->getString("lemethod") == "bicgstab") { LOG4CPLUS_INFO(logger, "Using BiCGStab method."); if (precond == "ilu") { - gmm::bicgstab(*A, **vector, b, gmm::ilu_precond>(*A), iter); + gmm::bicgstab(*A, vector, b, gmm::ilu_precond>(*A), iter); } else if (precond == "diagonal") { - gmm::bicgstab(*A, **vector, b, gmm::diagonal_precond>(*A), iter); + gmm::bicgstab(*A, vector, b, gmm::diagonal_precond>(*A), iter); } else if (precond == "ildlt") { - gmm::bicgstab(*A, **vector, b, gmm::ildlt_precond>(*A), iter); + gmm::bicgstab(*A, vector, b, gmm::ildlt_precond>(*A), iter); } else if (precond == "none") { - gmm::bicgstab(*A, **vector, b, gmm::identity_matrix(), iter); + gmm::bicgstab(*A, vector, b, gmm::identity_matrix(), iter); } // Check if the solver converged and issue a warning otherwise. @@ -173,13 +181,13 @@ private: } else if (s->getString("lemethod") == "qmr") { LOG4CPLUS_INFO(logger, "Using QMR method."); if (precond == "ilu") { - gmm::qmr(*A, **vector, b, gmm::ilu_precond>(*A), iter); + gmm::qmr(*A, vector, b, gmm::ilu_precond>(*A), iter); } else if (precond == "diagonal") { - gmm::qmr(*A, **vector, b, gmm::diagonal_precond>(*A), iter); + gmm::qmr(*A, vector, b, gmm::diagonal_precond>(*A), iter); } else if (precond == "ildlt") { - gmm::qmr(*A, **vector, b, gmm::ildlt_precond>(*A), iter); + gmm::qmr(*A, vector, b, gmm::ildlt_precond>(*A), iter); } else if (precond == "none") { - gmm::qmr(*A, **vector, b, gmm::identity_matrix(), iter); + gmm::qmr(*A, vector, b, gmm::identity_matrix(), iter); } // Check if the solver converged and issue a warning otherwise. @@ -190,7 +198,7 @@ private: } } else if (s->getString("lemethod") == "jacobi") { LOG4CPLUS_INFO(logger, "Using Jacobi method."); - solveLinearEquationSystemWithJacobi(*A, **vector, b); + solveLinearEquationSystemWithJacobi(*A, vector, b); } delete A; diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/GmmxxMdpPrctlModelChecker.h index a329fc303..d27b26b21 100644 --- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h +++ b/src/modelchecker/GmmxxMdpPrctlModelChecker.h @@ -43,339 +43,33 @@ public: virtual ~GmmxxMdpPrctlModelChecker() { } - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = formula.getLeft().check(*this); - storm::storage::BitVector* rightStates = formula.getRight().check(*this); - - // Copy the matrix before we make any changes. - storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); - +private: + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const { // Get the starting row indices for the non-deterministic choices to reduce the resulting // vector properly. std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. - tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *nondeterministicChoiceIndices); - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(tmpMatrix); - - // Create the vector with which to multiply. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); // Create vector for result of multiplication, which is reduced to the result vector after // each multiplication. - std::vector* multiplyResult = new std::vector(this->getModel().getTransitionMatrix()->getRowCount(), 0); + std::vector multiplyResult(matrix.getRowCount()); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *multiplyResult); + for (uint_fast64_t i = 0; i < repetitions; ++i) { + gmm::mult(*gmmxxMatrix, vector, multiplyResult); if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices); + storm::utility::reduceVectorMin(multiplyResult, &vector, *nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(*multiplyResult, result, *nondeterministicChoiceIndices); + storm::utility::reduceVectorMax(multiplyResult, &vector, *nondeterministicChoiceIndices); } } - delete multiplyResult; // Delete intermediate results and return result. delete gmmxxMatrix; - delete leftStates; - delete rightStates; - return result; - } - - virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formula of the next-formula. - storm::storage::BitVector* nextStates = formula.getChild().check(*this); - - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); - - // Create the vector with which to multiply and initialize it correctly. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne()); - - // Delete obsolete sub-result. - delete nextStates; - - // Create resulting vector. - std::vector* temporaryResult = new std::vector(this->getModel().getTransitionMatrix()->getRowCount()); - - // Perform the actual computation, namely matrix-vector multiplication. - gmm::mult(*gmmxxMatrix, *result, *temporaryResult); - - // Get the starting row indices for the non-deterministic choices to reduce the resulting - // vector properly. - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - - if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(*temporaryResult, result, *nondeterministicChoiceIndices); - } else { - storm::utility::reduceVectorMax(*temporaryResult, result, *nondeterministicChoiceIndices); - } - - // Delete temporary matrix plus temporary result and return result. - delete gmmxxMatrix; - delete temporaryResult; - return result; - } - - virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const { - // First, we need to compute the states that satisfy the sub-formulas of the until-formula. - storm::storage::BitVector* leftStates = formula.getLeft().check(*this); - storm::storage::BitVector* rightStates = formula.getRight().check(*this); - - // Then, we need to identify the states which have to be taken out of the matrix, i.e. - // all states that have probability 0 and 1 of satisfying the until-formula. - storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); - storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); - if (this->minimumOperatorStack.top()) { - storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); - } else { - storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); - } - - // Delete sub-results that are obsolete now. - delete leftStates; - delete rightStates; - - LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); - LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); - storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); - LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - - // Create resulting vector. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - - // Only try to solve system if there are states for which the probability is unknown. - uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - if (maybeStatesSetBitCount > 0) { - // First, we can eliminate the rows and columns from the original transition probability matrix for states - // whose probabilities are already known. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); - - // Get the "new" nondeterministic choice indices for the submatrix. - std::shared_ptr> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - - // Transform the submatrix to the gmm++ format to use its capabilities. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); - - // Create vector for results for maybe states. - std::vector* x = new std::vector(maybeStatesSetBitCount); - - // Prepare the right-hand side of the equation system. For entry i this corresponds to - // the accumulated probability of going from state i to some 'yes' state. - std::vector b(submatrix->getRowCount()); - this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b); - delete submatrix; - - // Solve the corresponding system of equations. - this->solveEquationSystem(*gmmxxMatrix, x, b, *subNondeterministicChoiceIndices); - - // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, *x); - - // Delete temporary matrix and vector. - delete gmmxxMatrix; - delete x; - } - - // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); - - return result; - } - - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const { - // Only compute the result if the model has a state-based reward model. - if (!this->getModel().hasStateRewards()) { - LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); - throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; - } - - // Get the starting row indices for the non-deterministic choices to reduce the resulting - // vector properly. - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); - - // Initialize result to state rewards of the model. - std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); - - // Create vector for result of multiplication, which is reduced to the result vector after - // each multiplication. - std::vector* multiplyResult = new std::vector(this->getModel().getTransitionMatrix()->getRowCount(), 0); - - // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *multiplyResult); - if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices); - } else { - storm::utility::reduceVectorMax(*multiplyResult, result, *nondeterministicChoiceIndices); - } - } - delete multiplyResult; - - // Delete temporary variables and return result. - delete gmmxxMatrix; - return result; - } - - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const { - // Only compute the result if the model has at least one reward model. - if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { - LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); - throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; - } - - // Get the starting row indices for the non-deterministic choices to reduce the resulting - // vector properly. - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*this->getModel().getTransitionMatrix()); - - // Compute the reward vector to add in each step based on the available reward models. - std::vector* totalRewardVector = nullptr; - if (this->getModel().hasTransitionRewards()) { - totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - if (this->getModel().hasStateRewards()) { - gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector); - } - } else { - totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); - } - - std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); - - // Create vector for result of multiplication, which is reduced to the result vector after - // each multiplication. - std::vector* multiplyResult = new std::vector(this->getModel().getTransitionMatrix()->getRowCount(), 0); - - // Now perform matrix-vector multiplication as long as we meet the bound of the formula. - for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { - gmm::mult(*gmmxxMatrix, *result, *multiplyResult); - if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(*multiplyResult, result, *nondeterministicChoiceIndices); - } else { - storm::utility::reduceVectorMax(*multiplyResult, result, *nondeterministicChoiceIndices); - } - - // Add the reward vector to the result. - gmm::add(*totalRewardVector, *result); - } - delete multiplyResult; - - // Delete temporary variables and return result. - delete gmmxxMatrix; - delete totalRewardVector; - return result; } - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const { - // Only compute the result if the model has at least one reward model. - if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { - LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); - throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; - } - - // Determine the states for which the target predicate holds. - storm::storage::BitVector* targetStates = formula.getChild().check(*this); - - // Determine which states have a reward of infinity by definition. - storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); - storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); - if (this->minimumOperatorStack.top()) { - storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates, &infinityStates); - } else { - storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates, &infinityStates); - } - infinityStates.complement(); - - LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); - LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states."); - storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; - LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); - - // Create resulting vector. - std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - - // Get the starting row indices for the non-deterministic choices to reduce the resulting - // vector properly. - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - - // Check whether there are states for which we have to compute the result. - const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); - if (maybeStatesSetBitCount > 0) { - // First, we can eliminate the rows and columns from the original transition probability matrix for states - // whose probabilities are already known. - storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); - - // Get the "new" nondeterministic choice indices for the submatrix. - std::shared_ptr> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); - - // Transform the submatrix to the gmm++ format to use its capabilities. - gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*submatrix); - - // Create vector for results for maybe states. - std::vector* x = new std::vector(maybeStatesSetBitCount); - - // Prepare the right-hand side of the equation system. For entry i this corresponds to - // the accumulated probability of going from state i to some 'yes' state. - std::vector b(submatrix->getRowCount()); - delete submatrix; - - if (this->getModel().hasTransitionRewards()) { - // If a transition-based reward model is available, we initialize the right-hand - // side to the vector resulting from summing the rows of the pointwise product - // of the transition probability matrix and the transition reward matrix. - std::vector* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); - storm::utility::selectVectorValues(&b, maybeStates, *nondeterministicChoiceIndices, *pointwiseProductRowSumVector); - delete pointwiseProductRowSumVector; - - if (this->getModel().hasStateRewards()) { - // If a state-based reward model is also available, we need to add this vector - // as well. As the state reward vector contains entries not just for the states - // that we still consider (i.e. maybeStates), we need to extract these values - // first. - std::vector* subStateRewards = new std::vector(b.size()); - storm::utility::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *nondeterministicChoiceIndices, *this->getModel().getStateRewardVector()); - gmm::add(*subStateRewards, b); - delete subStateRewards; - } - } else { - // If only a state-based reward model is available, we take this vector as the - // right-hand side. As the state reward vector contains entries not just for the - // states that we still consider (i.e. maybeStates), we need to extract these values - // first. - storm::utility::selectVectorValuesRepeatedly(&b, maybeStates, *nondeterministicChoiceIndices, *this->getModel().getStateRewardVector()); - } - - // Solve the corresponding system of equations. - this->solveEquationSystem(*gmmxxMatrix, x, b, *subNondeterministicChoiceIndices); - - // Set values of resulting vector according to result. - storm::utility::setVectorValues(result, maybeStates, *x); - delete x; - delete gmmxxMatrix; - } - - // Set values of resulting vector that are known exactly. - storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero()); - storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); - - // Delete temporary storages and return result. - delete targetStates; - return result; - } - -private: /*! * Solves the given equation system under the given parameters using the power method. * @@ -386,7 +80,7 @@ private: * @return The solution of the system of linear equations in form of the elements of the vector * x. */ - void solveEquationSystem(gmm::csr_matrix const& A, std::vector* x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { + void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& x, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const { // Get the settings object to customize solving. storm::settings::Settings* s = storm::settings::instance(); @@ -395,43 +89,48 @@ private: unsigned maxIterations = s->get("maxiter"); bool relative = s->get("relative"); + // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + gmm::csr_matrix* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(matrix); + // Set up the environment for the power method. - std::vector* temporaryResult = new std::vector(b.size()); - std::vector* newX = new std::vector(x->size()); + std::vector multiplyResult(matrix.getRowCount()); + std::vector* currentX = &x; + std::vector* newX = new std::vector(x.size()); std::vector* swap = nullptr; - bool converged = false; uint_fast64_t iterations = 0; + bool converged = false; // Proceed with the iterations as long as the method did not converge or reach the // user-specified maximum number of iterations. while (!converged && iterations < maxIterations) { // Compute x' = A*x + b. - gmm::mult(A, *x, *temporaryResult); - gmm::add(b, *temporaryResult); + gmm::mult(*gmmxxMatrix, *currentX, multiplyResult); + gmm::add(b, multiplyResult); // Reduce the vector x' by applying min/max for all non-deterministic choices. if (this->minimumOperatorStack.top()) { - storm::utility::reduceVectorMin(*temporaryResult, newX, nondeterministicChoiceIndices); + storm::utility::reduceVectorMin(multiplyResult, newX, nondeterministicChoiceIndices); } else { - storm::utility::reduceVectorMax(*temporaryResult, newX, nondeterministicChoiceIndices); + storm::utility::reduceVectorMax(multiplyResult, newX, nondeterministicChoiceIndices); } // Determine whether the method converged. - converged = storm::utility::equalModuloPrecision(*x, *newX, precision, relative); + converged = storm::utility::equalModuloPrecision(*currentX, *newX, precision, relative); // Update environment variables. - swap = x; - x = newX; + swap = currentX; + currentX = newX; newX = swap; ++iterations; } if (iterations % 2 == 1) { - delete x; + std::swap(x, *currentX); + delete currentX; } else { delete newX; } - delete temporaryResult; + delete gmmxxMatrix; // Check if the solver converged and issue a warning otherwise. if (converged) { @@ -440,22 +139,6 @@ private: LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); } } - - std::shared_ptr> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector constraint) const { - std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); - std::shared_ptr> subNondeterministicChoiceIndices(new std::vector(constraint.getNumberOfSetBits() + 1)); - uint_fast64_t currentRowCount = 0; - uint_fast64_t currentIndexCount = 1; - (*subNondeterministicChoiceIndices)[0] = 0; - for (auto index : constraint) { - (*subNondeterministicChoiceIndices)[currentIndexCount] = currentRowCount + (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; - currentRowCount += (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; - ++currentIndexCount; - } - (*subNondeterministicChoiceIndices)[constraint.getNumberOfSetBits()] = currentRowCount; - - return subNondeterministicChoiceIndices; - } }; } //namespace modelChecker diff --git a/src/modelchecker/MdpPrctlModelChecker.h b/src/modelchecker/MdpPrctlModelChecker.h index b71d1d934..0f50dfae9 100644 --- a/src/modelchecker/MdpPrctlModelChecker.h +++ b/src/modelchecker/MdpPrctlModelChecker.h @@ -189,7 +189,28 @@ public: * @param formula The Bounded Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const = 0; + virtual std::vector* checkBoundedUntil(const storm::formula::BoundedUntil& formula, bool qualitative) const { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); + + // Copy the matrix before we make any changes. + storm::storage::SparseMatrix tmpMatrix(*this->getModel().getTransitionMatrix()); + + // Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula. + tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates, *this->getModel().getNondeterministicChoiceIndices()); + + // Create the vector with which to multiply. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + storm::utility::setVectorValues(result, *rightStates, storm::utility::constGetOne()); + + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); + + // Delete intermediate results and return result. + delete leftStates; + delete rightStates; + return result; + } /*! * The check method for a path formula with a Next operator node as root in its formula tree @@ -197,7 +218,22 @@ public: * @param formula The Next path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const = 0; + virtual std::vector* checkNext(const storm::formula::Next& formula, bool qualitative) const { + // First, we need to compute the states that satisfy the sub-formula of the next-formula. + storm::storage::BitVector* nextStates = formula.getChild().check(*this); + + // Create the vector with which to multiply and initialize it correctly. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + storm::utility::setVectorValues(result, *nextStates, storm::utility::constGetOne()); + + // Delete obsolete sub-result. + delete nextStates; + + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result); + + // Return result. + return result; + } /*! * The check method for a path formula with a Bounded Eventually operator node as root in its @@ -246,7 +282,67 @@ public: * @param formula The Until path formula to check * @returns for each state the probability that the path formula holds. */ - virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const = 0; + virtual std::vector* checkUntil(const storm::formula::Until& formula, bool qualitative) const { + // First, we need to compute the states that satisfy the sub-formulas of the until-formula. + storm::storage::BitVector* leftStates = formula.getLeft().check(*this); + storm::storage::BitVector* rightStates = formula.getRight().check(*this); + + // Then, we need to identify the states which have to be taken out of the matrix, i.e. + // all states that have probability 0 and 1 of satisfying the until-formula. + storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates()); + storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates()); + if (this->minimumOperatorStack.top()) { + storm::utility::GraphAnalyzer::performProb01Min(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); + } else { + storm::utility::GraphAnalyzer::performProb01Max(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1); + } + + // Delete sub-results that are obsolete now. + delete leftStates; + delete rightStates; + + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states."); + LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states."); + storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1); + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Create resulting vector. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + + // Only try to solve system if there are states for which the probability is unknown. + uint_fast64_t maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); + if (maybeStatesSetBitCount > 0) { + // First, we can eliminate the rows and columns from the original transition probability matrix for states + // whose probabilities are already known. + storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); + + // Get the "new" nondeterministic choice indices for the submatrix. + std::shared_ptr> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); + + // Create vector for results for maybe states. + std::vector x(maybeStatesSetBitCount); + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some 'yes' state. + std::vector b(submatrix->getRowCount()); + this->getModel().getTransitionMatrix()->getConstrainedRowSumVector(maybeStates, *this->getModel().getNondeterministicChoiceIndices(), statesWithProbability1, &b); + + // Solve the corresponding system of equations. + this->solveEquationSystem(*submatrix, x, b, *subNondeterministicChoiceIndices); + + // Set values of resulting vector according to result. + storm::utility::setVectorValues(result, maybeStates, x); + + // Delete temporary matrix. + delete submatrix; + } + + // Set values of resulting vector that are known exactly. + storm::utility::setVectorValues(result, statesWithProbability0, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, statesWithProbability1, storm::utility::constGetOne()); + + return result; + } /*! * The check method for a path formula with an Instantaneous Reward operator node as root in its @@ -255,7 +351,21 @@ public: * @param formula The Instantaneous Reward formula to check * @returns for each state the reward that the instantaneous reward yields */ - virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const = 0; + virtual std::vector* checkInstantaneousReward(const storm::formula::InstantaneousReward& formula, bool qualitative) const { + // Only compute the result if the model has a state-based reward model. + if (!this->getModel().hasStateRewards()) { + LOG4CPLUS_ERROR(logger, "Missing (state-based) reward model for formula."); + throw storm::exceptions::InvalidPropertyException() << "Missing (state-based) reward model for formula."; + } + + // Initialize result to state rewards of the model. + std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); + + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, nullptr, formula.getBound()); + + // Return result. + return result; + } /*! * The check method for a path formula with a Cumulative Reward operator node as root in its @@ -264,7 +374,32 @@ public: * @param formula The Cumulative Reward formula to check * @returns for each state the reward that the cumulative reward yields */ - virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const = 0; + virtual std::vector* checkCumulativeReward(const storm::formula::CumulativeReward& formula, bool qualitative) const { + // Only compute the result if the model has at least one reward model. + if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { + LOG4CPLUS_ERROR(logger, "Missing reward model for formula."); + throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; + } + + // Compute the reward vector to add in each step based on the available reward models. + std::vector* totalRewardVector = nullptr; + if (this->getModel().hasTransitionRewards()) { + totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); + if (this->getModel().hasStateRewards()) { + gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector); + } + } else { + totalRewardVector = new std::vector(*this->getModel().getStateRewardVector()); + } + + std::vector* result = new std::vector(*this->getModel().getStateRewardVector()); + + this->performMatrixVectorMultiplication(*this->getModel().getTransitionMatrix(), *result, totalRewardVector, formula.getBound()); + + // Delete temporary variables and return result. + delete totalRewardVector; + return result; + } /*! * The check method for a path formula with a Reachability Reward operator node as root in its @@ -273,10 +408,118 @@ public: * @param formula The Reachbility Reward formula to check * @returns for each state the reward that the reachability reward yields */ - virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const = 0; + virtual std::vector* checkReachabilityReward(const storm::formula::ReachabilityReward& formula, bool qualitative) const { + // Only compute the result if the model has at least one reward model. + if (!this->getModel().hasStateRewards() && !this->getModel().hasTransitionRewards()) { + LOG4CPLUS_ERROR(logger, "Missing reward model for formula. Skipping formula"); + throw storm::exceptions::InvalidPropertyException() << "Missing reward model for formula."; + } + + // Determine the states for which the target predicate holds. + storm::storage::BitVector* targetStates = formula.getChild().check(*this); + + // Determine which states have a reward of infinity by definition. + storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates()); + storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true); + if (this->minimumOperatorStack.top()) { + storm::utility::GraphAnalyzer::performProb1A(this->getModel(), trueStates, *targetStates, &infinityStates); + } else { + storm::utility::GraphAnalyzer::performProb1E(this->getModel(), trueStates, *targetStates, &infinityStates); + } + infinityStates.complement(); + + LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states."); + LOG4CPLUS_INFO(logger, "Found " << targetStates->getNumberOfSetBits() << " 'target' states."); + storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; + LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states."); + + // Create resulting vector. + std::vector* result = new std::vector(this->getModel().getNumberOfStates()); + + // Check whether there are states for which we have to compute the result. + const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); + if (maybeStatesSetBitCount > 0) { + // First, we can eliminate the rows and columns from the original transition probability matrix for states + // whose probabilities are already known. + storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates, *this->getModel().getNondeterministicChoiceIndices()); + + // Get the "new" nondeterministic choice indices for the submatrix. + std::shared_ptr> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates); + + // Create vector for results for maybe states. + std::vector x(maybeStatesSetBitCount); + + // Prepare the right-hand side of the equation system. For entry i this corresponds to + // the accumulated probability of going from state i to some 'yes' state. + std::vector b(submatrix->getRowCount()); + + if (this->getModel().hasTransitionRewards()) { + // If a transition-based reward model is available, we initialize the right-hand + // side to the vector resulting from summing the rows of the pointwise product + // of the transition probability matrix and the transition reward matrix. + std::vector* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix()); + storm::utility::selectVectorValues(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *pointwiseProductRowSumVector); + delete pointwiseProductRowSumVector; + + if (this->getModel().hasStateRewards()) { + // If a state-based reward model is also available, we need to add this vector + // as well. As the state reward vector contains entries not just for the states + // that we still consider (i.e. maybeStates), we need to extract these values + // first. + std::vector* subStateRewards = new std::vector(b.size()); + storm::utility::selectVectorValuesRepeatedly(subStateRewards, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector()); + gmm::add(*subStateRewards, b); + delete subStateRewards; + } + } else { + // If only a state-based reward model is available, we take this vector as the + // right-hand side. As the state reward vector contains entries not just for the + // states that we still consider (i.e. maybeStates), we need to extract these values + // first. + storm::utility::selectVectorValuesRepeatedly(&b, maybeStates, *this->getModel().getNondeterministicChoiceIndices(), *this->getModel().getStateRewardVector()); + } + + // Solve the corresponding system of equations. + this->solveEquationSystem(*submatrix, x, b, *subNondeterministicChoiceIndices); + + // Set values of resulting vector according to result. + storm::utility::setVectorValues(result, maybeStates, x); + delete submatrix; + } + + // Set values of resulting vector that are known exactly. + storm::utility::setVectorValues(result, *targetStates, storm::utility::constGetZero()); + storm::utility::setVectorValues(result, infinityStates, storm::utility::constGetInfinity()); + + // Delete temporary storages and return result. + delete targetStates; + return result; + } protected: mutable std::stack minimumOperatorStack; + +private: + virtual void performMatrixVectorMultiplication(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector* summand = nullptr, uint_fast64_t repetitions = 1) const = 0; + + virtual void solveEquationSystem(storm::storage::SparseMatrix const& matrix, std::vector& vector, std::vector const& b, std::vector const& nondeterministicChoiceIndices) const = 0; + + + std::shared_ptr> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector constraint) const { + std::shared_ptr> nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices(); + std::shared_ptr> subNondeterministicChoiceIndices(new std::vector(constraint.getNumberOfSetBits() + 1)); + uint_fast64_t currentRowCount = 0; + uint_fast64_t currentIndexCount = 1; + (*subNondeterministicChoiceIndices)[0] = 0; + for (auto index : constraint) { + (*subNondeterministicChoiceIndices)[currentIndexCount] = currentRowCount + (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; + currentRowCount += (*nondeterministicChoiceIndices)[index + 1] - (*nondeterministicChoiceIndices)[index]; + ++currentIndexCount; + } + (*subNondeterministicChoiceIndices)[constraint.getNumberOfSetBits()] = currentRowCount; + + return subNondeterministicChoiceIndices; + } }; } //namespace modelChecker diff --git a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp index c2f1b3cac..1fee30acd 100644 --- a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp +++ b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp @@ -90,7 +90,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(mc); - ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); delete rewardFormula; delete result; @@ -101,7 +101,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(mc); - ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); delete rewardFormula; delete result; @@ -120,7 +120,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateRewardModelChecker); - ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); delete rewardFormula; delete result; @@ -131,7 +131,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateRewardModelChecker); - ASSERT_LT(std::abs((*result)[0] - 7.3333272933959960938), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - 7.3333294987678527832), s->get("precision")); delete rewardFormula; delete result; @@ -150,7 +150,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateAndTransitionRewardModelChecker); - ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333272933959960938)), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get("precision")); delete rewardFormula; delete result; @@ -161,7 +161,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) { result = rewardFormula->check(stateAndTransitionRewardModelChecker); - ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333272933959960938)), s->get("precision")); + ASSERT_LT(std::abs((*result)[0] - (2 * 7.3333294987678527832)), s->get("precision")); delete rewardFormula; delete result;