From 0c2080f2208328623209987974dce431d277d7e6 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 26 Feb 2015 18:59:30 +0100 Subject: [PATCH 1/2] Added tests for sparse Prob0/1 to functional tests Former-commit-id: ef8f9ffb599f3dfcd627f88115563bac14fdf5d7 --- test/functional/utility/GraphTest.cpp | 53 ++++++++++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 9a17e4207..68c62182a 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -6,6 +6,7 @@ #include "src/models/symbolic/Dtmc.h" #include "src/models/symbolic/Mdp.h" #include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" #include "src/builder/DdPrismModelBuilder.h" #include "src/builder/ExplicitPrismModelBuilder.h" #include "src/utility/graph.h" @@ -73,7 +74,6 @@ TEST(GraphTest, SymbolicProb01MinMax) { ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); - statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff")); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); EXPECT_EQ(993, statesWithProbability01.first.getNonZeroCount()); EXPECT_EQ(16, statesWithProbability01.second.getNonZeroCount()); @@ -102,4 +102,55 @@ TEST(GraphTest, ExplicitProb01) { ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeOnlyTrueSender"))); EXPECT_EQ(5829, statesWithProbability01.first.getNumberOfSetBits()); EXPECT_EQ(1032, statesWithProbability01.second.getNumberOfSetBits()); +} + +TEST(GraphTest, ExplicitProb01MinMax) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + std::pair statesWithProbability01; + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected"))); + EXPECT_EQ(0, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(364, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected"))); + EXPECT_EQ(0, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(364, statesWithProbability01.second.getNumberOfSetBits()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0"))); + EXPECT_EQ(77, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(149, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0"))); + EXPECT_EQ(74, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(198, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(94, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(33, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1"))); + EXPECT_EQ(83, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(35, statesWithProbability01.second.getNumberOfSetBits()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + + ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(16, statesWithProbability01.second.getNumberOfSetBits()); + + ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); + EXPECT_EQ(993, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(16, statesWithProbability01.second.getNumberOfSetBits()); } \ No newline at end of file From 3fd62bc697582c42758fe891955307d9147dc100 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 16 Mar 2015 17:38:57 +0100 Subject: [PATCH 2/2] More work on MTBDD-based mc. Former-commit-id: 52081fc741694d60b2fa2389f43188e452fb3509 --- src/logic/Formula.h | 1 + src/modelchecker/AbstractModelChecker.cpp | 19 +++-- src/modelchecker/results/CheckResult.cpp | 73 ++++++++++++------- src/modelchecker/results/CheckResult.h | 45 ++++++++---- .../ExplicitQualitativeCheckResult.cpp | 65 +++++++---------- .../results/ExplicitQualitativeCheckResult.h | 9 ++- .../ExplicitQuantitativeCheckResult.cpp | 49 ++++++------- .../results/ExplicitQuantitativeCheckResult.h | 7 +- .../results/QualitativeCheckResult.cpp | 15 ++++ .../results/QualitativeCheckResult.h | 4 + .../results/QuantitativeCheckResult.cpp | 13 ++-- .../results/QuantitativeCheckResult.h | 3 +- .../SymbolicQualitativeCheckResult.cpp | 55 ++++++++++++++ .../results/SymbolicQualitativeCheckResult.h | 45 ++++++++++++ .../SymbolicQuantitativeCheckResult.cpp | 0 .../results/SymbolicQuantitativeCheckResult.h | 43 +++++++++++ 16 files changed, 315 insertions(+), 131 deletions(-) create mode 100644 src/modelchecker/results/SymbolicQualitativeCheckResult.cpp create mode 100644 src/modelchecker/results/SymbolicQualitativeCheckResult.h create mode 100644 src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp create mode 100644 src/modelchecker/results/SymbolicQuantitativeCheckResult.h diff --git a/src/logic/Formula.h b/src/logic/Formula.h index bb2e74a7c..42aafcada 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -2,6 +2,7 @@ #define STORM_LOGIC_FORMULA_H_ #include +#include #include #include "src/modelchecker/results/CheckResult.h" diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index eb9d539a9..7004245a2 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -1,5 +1,7 @@ #include "src/modelchecker/AbstractModelChecker.h" +#include "src/modelchecker/results/QualitativeCheckResult.h" +#include "src/modelchecker/results/QuantitativeCheckResult.h" #include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" @@ -131,10 +133,12 @@ namespace storm { std::unique_ptr leftResult = this->check(stateFormula.getLeftSubformula().asStateFormula()); std::unique_ptr rightResult = this->check(stateFormula.getRightSubformula().asStateFormula()); + STORM_LOG_THROW(leftResult->isQualitative() && rightResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative results."); + if (stateFormula.isAnd()) { - *leftResult &= *rightResult; + leftResult->asQualitativeCheckResult() &= rightResult->asQualitativeCheckResult(); } else if (stateFormula.isOr()) { - *leftResult |= *rightResult; + leftResult->asQualitativeCheckResult() |= rightResult->asQualitativeCheckResult(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } @@ -166,7 +170,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { return result; } @@ -192,7 +196,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { return result; } @@ -218,7 +222,7 @@ namespace storm { if (stateFormula.hasBound()) { STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result."); - return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { return result; } @@ -235,7 +239,7 @@ namespace storm { std::unique_ptr result; if (stateFormula.hasBound()) { - return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); + return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound()); } else { return result; } @@ -243,8 +247,9 @@ namespace storm { std::unique_ptr AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) { std::unique_ptr subResult = this->check(stateFormula.getSubformula()); + STORM_LOG_THROW(subResult->isQualitative(), storm::exceptions::InternalTypeErrorException, "Expected qualitative result."); if (stateFormula.isNot()) { - subResult->complement(); + subResult->asQualitativeCheckResult().complement(); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); } diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp index 22bb96ee9..5f79e0d1e 100644 --- a/src/modelchecker/results/CheckResult.cpp +++ b/src/modelchecker/results/CheckResult.cpp @@ -3,31 +3,22 @@ #include "storm-config.h" #include "src/adapters/CarlAdapter.h" +#include "src/storage/dd/CuddDd.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" +#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" namespace storm { - namespace modelchecker { - CheckResult& CheckResult::operator&=(CheckResult const& other) { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'and' on the two check results."); - } - - CheckResult& CheckResult::operator|=(CheckResult const& other) { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'or' on the two check results."); - } - - void CheckResult::complement() { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result."); - } - - std::unique_ptr CheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result."); + namespace modelchecker { + bool CheckResult::isExplicit() const { + return false; } - bool CheckResult::isExplicit() const { + bool CheckResult::isSymbolic() const { return false; } @@ -55,7 +46,15 @@ namespace storm { bool CheckResult::isExplicitQuantitativeCheckResult() const { return false; } - + + bool CheckResult::isSymbolicQualitativeCheckResult() const { + return false; + } + + bool CheckResult::isSymbolicQuantitativeCheckResult() const { + return false; + } + ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() { return dynamic_cast(*this); } @@ -74,25 +73,43 @@ namespace storm { return dynamic_cast const&>(*this); } - template - QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() { - return dynamic_cast&>(*this); + QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() { + return dynamic_cast(*this); } - template - QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const { - return dynamic_cast const&>(*this); + QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const { + return dynamic_cast(*this); + } + + template + SymbolicQualitativeCheckResult& CheckResult::asSymbolicQualitativeCheckResult() { + return dynamic_cast&>(*this); + } + + template + SymbolicQualitativeCheckResult const& CheckResult::asSymbolicQualitativeCheckResult() const { + return dynamic_cast const&>(*this); + } + + template + SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult() { + return dynamic_cast&>(*this); + } + + template + SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const { + return dynamic_cast const&>(*this); } // Explicitly instantiate the template functions. - template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); - template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; - + template SymbolicQualitativeCheckResult& CheckResult::asSymbolicQualitativeCheckResult(); + template SymbolicQualitativeCheckResult const& CheckResult::asSymbolicQualitativeCheckResult() const; + template SymbolicQuantitativeCheckResult& CheckResult::asSymbolicQuantitativeCheckResult(); + template SymbolicQuantitativeCheckResult const& CheckResult::asSymbolicQuantitativeCheckResult() const; + #ifdef STORM_HAVE_CARL - template QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult(); - template QuantitativeCheckResult const& CheckResult::asQuantitativeCheckResult() const; template ExplicitQuantitativeCheckResult& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult const& CheckResult::asExplicitQuantitativeCheckResult() const; #endif diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h index a4c4847db..05aefd984 100644 --- a/src/modelchecker/results/CheckResult.h +++ b/src/modelchecker/results/CheckResult.h @@ -4,40 +4,46 @@ #include #include -#include "src/storage/BitVector.h" +#include "src/storage/dd/DdType.h" #include "src/logic/ComparisonType.h" namespace storm { namespace modelchecker { // Forward-declare the existing subclasses. class QualitativeCheckResult; - template class QuantitativeCheckResult; + class QuantitativeCheckResult; class ExplicitQualitativeCheckResult; template class ExplicitQuantitativeCheckResult; + template class SymbolicQualitativeCheckResult; + template class SymbolicQuantitativeCheckResult; // The base class of all check results. class CheckResult { public: - virtual CheckResult& operator&=(CheckResult const& other); - virtual CheckResult& operator|=(CheckResult const& other); - virtual void complement(); - virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const; - + /*! + * Filters the current result wrt. to the filter, i.e. only keeps the entries that are selected by the filter. + * This means that the filter must be a qualitative result of proper type (symbolic/explicit). + * + * @param filter A qualitative result that serves as a filter. + */ + virtual void filter(QualitativeCheckResult const& filter) = 0; + + // Methods to retrieve the actual type of the check result. virtual bool isExplicit() const; + virtual bool isSymbolic() const; virtual bool isQuantitative() const; virtual bool isQualitative() const; - virtual bool isResultForAllStates() const; - virtual bool isExplicitQualitativeCheckResult() const; virtual bool isExplicitQuantitativeCheckResult() const; + virtual bool isSymbolicQualitativeCheckResult() const; + virtual bool isSymbolicQuantitativeCheckResult() const; + virtual bool isResultForAllStates() const; QualitativeCheckResult& asQualitativeCheckResult(); QualitativeCheckResult const& asQualitativeCheckResult() const; - template - QuantitativeCheckResult& asQuantitativeCheckResult(); - template - QuantitativeCheckResult const& asQuantitativeCheckResult() const; + QuantitativeCheckResult& asQuantitativeCheckResult(); + QuantitativeCheckResult const& asQuantitativeCheckResult() const; ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const; @@ -48,8 +54,19 @@ namespace storm { template ExplicitQuantitativeCheckResult const& asExplicitQuantitativeCheckResult() const; + template + SymbolicQualitativeCheckResult& asSymbolicQualitativeCheckResult(); + + template + SymbolicQualitativeCheckResult const& asSymbolicQualitativeCheckResult() const; + + template + SymbolicQuantitativeCheckResult& asSymbolicQuantitativeCheckResult(); + + template + SymbolicQuantitativeCheckResult const& asSymbolicQuantitativeCheckResult() const; + virtual std::ostream& writeToStream(std::ostream& out) const = 0; - virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const = 0; }; std::ostream& operator<<(std::ostream& out, CheckResult& checkResult); diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp index 167837a19..5606819db 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -29,7 +29,7 @@ namespace storm { // Intentionally left empty. } - void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, CheckResult const& second, std::function const& function) { + void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, std::function const& function) { STORM_LOG_THROW(typeid(second) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); STORM_LOG_THROW(first.isResultForAllStates() == second.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type."); ExplicitQualitativeCheckResult const& secondCheckResult = static_cast(second); @@ -52,12 +52,12 @@ namespace storm { } } - CheckResult& ExplicitQualitativeCheckResult::operator&=(CheckResult const& other) { + QualitativeCheckResult& ExplicitQualitativeCheckResult::operator&=(QualitativeCheckResult const& other) { performLogicalOperation(*this, other, [] (bool a, bool b) { return a && b; }); return *this; } - CheckResult& ExplicitQualitativeCheckResult::operator|=(CheckResult const& other) { + QualitativeCheckResult& ExplicitQualitativeCheckResult::operator|=(QualitativeCheckResult const& other) { performLogicalOperation(*this, other, [] (bool a, bool b) { return a || b; }); return *this; } @@ -109,19 +109,19 @@ namespace storm { } else { std::ios::fmtflags oldflags(std::cout.flags()); out << std::boolalpha; - + map_type const& map = boost::get(truthValues); - + #ifndef WINDOWS typename map_type::const_iterator it = map.begin(); typename map_type::const_iterator itPlusOne = map.begin(); ++itPlusOne; typename map_type::const_iterator ite = map.end(); #else - map_type::const_iterator it = map.begin(); - map_type::const_iterator itPlusOne = map.begin(); - ++itPlusOne; - map_type::const_iterator ite = map.end(); + map_type::const_iterator it = map.begin(); + map_type::const_iterator itPlusOne = map.begin(); + ++itPlusOne; + map_type::const_iterator ite = map.end(); #endif for (; it != ite; ++itPlusOne, ++it) { @@ -135,43 +135,32 @@ namespace storm { return out; } - std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const { - std::ios::fmtflags oldflags(std::cout.flags()); - - out << "["; - storm::storage::BitVector::const_iterator it = filter.begin(); - storm::storage::BitVector::const_iterator itPlusOne = filter.begin(); - ++itPlusOne; - storm::storage::BitVector::const_iterator ite = filter.end(); + void ExplicitQualitativeCheckResult::filter(QualitativeCheckResult const& filter) { + STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter."); + STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter."); + ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult(); + vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); - out << std::boolalpha; if (this->isResultForAllStates()) { - vector_type const& vector = boost::get(truthValues); - for (; it != ite; ++itPlusOne, ++it) { - out << vector[*it]; - if (itPlusOne != ite) { - out << ", "; - } + map_type newMap; + for (auto const& element : filterTruthValues) { + newMap.emplace(element, this->getTruthValuesVector().get(element)); } + this->truthValues = newMap; } else { map_type const& map = boost::get(truthValues); - bool allResultsAvailable = true; - for (; it != ite; ++itPlusOne, ++it) { - auto const& keyValuePair = map.find(*it); - if (keyValuePair != map.end()) { - out << keyValuePair->second; - if (itPlusOne != ite) { - out << ", "; - } - } else { - allResultsAvailable = false; + + map_type newMap; + for (auto const& element : map) { + if (filterTruthValues.get(element.first)) { + newMap.insert(element); } } + + STORM_LOG_THROW(newMap.size() == filterTruthValues.getNumberOfSetBits(), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter."); + + this->truthValues = newMap; } - out << "]"; - - std::cout.flags(oldflags); - return out; } } } \ No newline at end of file diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/modelchecker/results/ExplicitQualitativeCheckResult.h index 2cda892b9..8ab3e473d 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -39,18 +39,19 @@ namespace storm { virtual bool isExplicitQualitativeCheckResult() const override; - virtual CheckResult& operator&=(CheckResult const& other) override; - virtual CheckResult& operator|=(CheckResult const& other) override; + virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) override; + virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override; virtual void complement() override; vector_type const& getTruthValuesVector() const; map_type const& getTruthValuesVectorMap() const; virtual std::ostream& writeToStream(std::ostream& out) const override; - virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override; + + virtual void filter(QualitativeCheckResult const& filter) override; private: - static void performLogicalOperation(ExplicitQualitativeCheckResult& first, CheckResult const& second, std::function const& function); + static void performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, std::function const& function); // The values of the quantitative check result. boost::variant truthValues; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 31b7e5296..2f4ce34fb 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -3,6 +3,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/storage/BitVector.h" #include "src/utility/macros.h" +#include "src/utility/vector.h" #include "src/exceptions/InvalidOperationException.h" #include "src/adapters/CarlAdapter.h" @@ -49,40 +50,32 @@ namespace storm { } template - std::ostream& ExplicitQuantitativeCheckResult::writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const { - out << "["; - storm::storage::BitVector::const_iterator it = filter.begin(); - storm::storage::BitVector::const_iterator itPlusOne = filter.begin(); - ++itPlusOne; - storm::storage::BitVector::const_iterator ite = filter.end(); - + void ExplicitQuantitativeCheckResult::filter(QualitativeCheckResult const& filter) { + STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter."); + STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter."); + ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult(); + ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector(); + if (this->isResultForAllStates()) { - vector_type const& valuesAsVector = boost::get(values); - for (; it != ite; ++itPlusOne, ++it) { - out << valuesAsVector[*it]; - if (itPlusOne != ite) { - out << ", "; - } + map_type newMap; + for (auto const& element : filterTruthValues) { + newMap.emplace(element, this->getValueVector()[element]); } + this->values = newMap; } else { - map_type const& valuesAsMap = boost::get(values); - bool allResultsAvailable = true; - for (; it != ite; ++itPlusOne, ++it) { - auto const& keyValuePair = valuesAsMap.find(*it); - if (keyValuePair != valuesAsMap.end()) { - out << keyValuePair->second; - if (itPlusOne != ite) { - out << ", "; - } - } else { - allResultsAvailable = false; + map_type const& map = boost::get(values); + + map_type newMap; + for (auto const& element : map) { + if (filterTruthValues.get(element.first)) { + newMap.insert(element); } } - STORM_LOG_THROW(allResultsAvailable, storm::exceptions::InvalidOperationException, "Unable to print result for some states, because the result is not available."); + + STORM_LOG_THROW(newMap.size() == filterTruthValues.getNumberOfSetBits(), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter."); + + this->values = newMap; } - - out << "]"; - return out; } template diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 85f1218fd..07166d258 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -12,7 +12,7 @@ namespace storm { namespace modelchecker { template - class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult { + class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult { public: typedef std::vector vector_type; typedef std::map map_type; @@ -45,8 +45,9 @@ namespace storm { map_type const& getValueMap() const; virtual std::ostream& writeToStream(std::ostream& out) const override; - virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override; - + + virtual void filter(QualitativeCheckResult const& filter) override; + private: // The values of the quantitative check result. boost::variant values; diff --git a/src/modelchecker/results/QualitativeCheckResult.cpp b/src/modelchecker/results/QualitativeCheckResult.cpp index 88cc4b956..b0d1683e2 100644 --- a/src/modelchecker/results/QualitativeCheckResult.cpp +++ b/src/modelchecker/results/QualitativeCheckResult.cpp @@ -1,7 +1,22 @@ #include "src/modelchecker/results/QualitativeCheckResult.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidOperationException.h" + namespace storm { namespace modelchecker { + QualitativeCheckResult& QualitativeCheckResult::operator&=(QualitativeCheckResult const& other) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'and' on the two check results."); + } + + QualitativeCheckResult& QualitativeCheckResult::operator|=(QualitativeCheckResult const& other) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'or' on the two check results."); + } + + void QualitativeCheckResult::complement() { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform logical 'not' on the check result."); + } + bool QualitativeCheckResult::isQualitative() const { return true; } diff --git a/src/modelchecker/results/QualitativeCheckResult.h b/src/modelchecker/results/QualitativeCheckResult.h index 40675add8..5904d2b6e 100644 --- a/src/modelchecker/results/QualitativeCheckResult.h +++ b/src/modelchecker/results/QualitativeCheckResult.h @@ -7,6 +7,10 @@ namespace storm { namespace modelchecker { class QualitativeCheckResult : public CheckResult { public: + virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other); + virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other); + virtual void complement(); + virtual bool isQualitative() const override; }; } diff --git a/src/modelchecker/results/QuantitativeCheckResult.cpp b/src/modelchecker/results/QuantitativeCheckResult.cpp index 40d97d99e..6618f6231 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.cpp +++ b/src/modelchecker/results/QuantitativeCheckResult.cpp @@ -8,15 +8,12 @@ namespace storm { namespace modelchecker { - template - bool QuantitativeCheckResult::isQuantitative() const { - return true; + std::unique_ptr QuantitativeCheckResult::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform comparison against bound on the check result."); } - template class QuantitativeCheckResult; - -#ifdef STORM_HAVE_CARL - template class QuantitativeCheckResult; -#endif + bool QuantitativeCheckResult::isQuantitative() const { + return true; + } } } \ No newline at end of file diff --git a/src/modelchecker/results/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h index 9abad1652..2dc1afc39 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.h +++ b/src/modelchecker/results/QuantitativeCheckResult.h @@ -5,9 +5,10 @@ namespace storm { namespace modelchecker { - template class QuantitativeCheckResult : public CheckResult { public: + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const; + virtual bool isQuantitative() const override; }; } diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp new file mode 100644 index 000000000..f72ca929f --- /dev/null +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -0,0 +1,55 @@ +#include "src/modelcheckers/result/SymbolicQualitativeCheckResult.h" + +namespace storm { + namespace modelcheckers { + template + SymbolicQualitativeCheckResult(storm::dd::Dd const& values) { + + } + + template + bool isSymbolic() const { + + } + + template + bool isResultForAllStates() const { + + } + + template + bool isSymbolicQualitativeCheckResult() const { + + } + + template + QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) { + + } + + template + QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) { + + } + + template + void complement() { + + } + + template + storm::dd::Dd const& getTruthValuesVector() const { + + } + + template + std::ostream& writeToStream(std::ostream& out) const { + + } + + template + void filter(QualitativeCheckResult const& filter) { + + } + } +} \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h new file mode 100644 index 000000000..b13c39029 --- /dev/null +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -0,0 +1,45 @@ +#ifndef STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ +#define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ + +#include "src/storage/dd/DdType.h" +#include "src/modelchecker/results/QualitativeCheckResult.h" +#include "src/utility/OsDetection.h" + +namespace storm { + namespace modelchecker { + template + class SymbolicQualitativeCheckResult : public QualitativeCheckResult { + public: + SymbolicQualitativeCheckResult() = default; + SymbolicQualitativeCheckResult(storm::dd::Dd const& values); + + SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default; + SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default; +#ifndef WINDOWS + SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult&& other) = default; + SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult&& other) = default; +#endif + + virtual bool isSymbolic() const override; + virtual bool isResultForAllStates() const override; + + virtual bool isSymbolicQualitativeCheckResult() const override; + + virtual QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) override; + virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override; + virtual void complement() override; + + storm::dd::Dd const& getTruthValuesVector() const; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + virtual void filter(QualitativeCheckResult const& filter) override; + + private: + // The values of the qualitative check result. + storm::dd::Dd truthValues; + }; + } +} + +#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h new file mode 100644 index 000000000..bb45fe090 --- /dev/null +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -0,0 +1,43 @@ +#ifndef STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_ +#define STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_ + +#include "src/storage/dd/DdType.h" +#include "src/modelchecker/results/QuantitativeCheckResult.h" +#include "src/utility/OsDetection.h" + +namespace storm { + namespace modelchecker { + template + class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult { + public: + SymbolicQuantitativeCheckResult(); + SymbolicQuantitativeCheckResult(storm::dd::Dd const& values); + + SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default; + SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default; +#ifndef WINDOWS + SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult&& other) = default; + SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult&& other) = default; +#endif + + virtual std::unique_ptr compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override; + + virtual bool isSymbolic() const override; + virtual bool isResultForAllStates() const override; + + virtual bool isSymbolicQuantitativeCheckResult() const override; + + storm::dd::Dd const& getValueVector() const; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + virtual void filter(QualitativeCheckResult const& filter) override; + + private: + // The values of the quantitative check result. + storm::dd::Dd values; + }; + } +} + +#endif /* STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file