diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
new file mode 100644
index 000000000..137c292b5
--- /dev/null
+++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
@@ -0,0 +1,54 @@
+#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
+
+#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Mdp.h"
+
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+ namespace modelchecker {
+ template<storm::dd::DdType Type>
+ SymbolicPropositionalModelChecker<Type>::SymbolicPropositionalModelChecker(storm::models::symbolic::Model<Type> const& model) : model(model) {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType Type>
+ bool SymbolicPropositionalModelChecker<Type>::canHandle(storm::logic::Formula const& formula) const {
+ return formula.isPropositionalFormula();
+ }
+
+ template<storm::dd::DdType Type>
+ std::unique_ptr<CheckResult> SymbolicPropositionalModelChecker<Type>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
+ if (stateFormula.isTrueFormula()) {
+ return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getReachableStates()));
+ } else {
+ return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getManager().getZero()));
+ }
+ }
+
+ template<storm::dd::DdType Type>
+ std::unique_ptr<CheckResult> SymbolicPropositionalModelChecker<Type>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
+ STORM_LOG_THROW(model.hasLabel(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
+ return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getStates(stateFormula.getLabel())));
+ }
+
+ template<storm::dd::DdType Type>
+ storm::models::symbolic::Model<Type> const& SymbolicPropositionalModelChecker<Type>::getModel() const {
+ return model;
+ }
+
+ template<storm::dd::DdType Type>
+ template<typename ModelType>
+ ModelType const& SymbolicPropositionalModelChecker<Type>::getModelAs() const {
+ return dynamic_cast<ModelType const&>(model);
+ }
+
+ // Explicitly instantiate the template class.
+ template storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD> const& SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD>::getModelAs() const;
+ template storm::models::symbolic::Mdp<storm::dd::DdType::CUDD> const& SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD>::getModelAs() const;
+ template class SymbolicPropositionalModelChecker<storm::dd::DdType::CUDD>;
+ }
+}
\ No newline at end of file
diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
new file mode 100644
index 000000000..9865d74b3
--- /dev/null
+++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
@@ -0,0 +1,44 @@
+#ifndef STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
+#define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
+
+#include "src/modelchecker/AbstractModelChecker.h"
+
+#include "src/models/symbolic/Model.h"
+
+namespace storm {
+ namespace modelchecker {
+
+ template<storm::dd::DdType Type>
+ class SymbolicPropositionalModelChecker : public AbstractModelChecker {
+ public:
+ explicit SymbolicPropositionalModelChecker(storm::models::symbolic::Model<Type> const& model);
+
+ // The implemented methods of the AbstractModelChecker interface.
+ virtual bool canHandle(storm::logic::Formula const& formula) const override;
+ virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
+ virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
+
+ protected:
+ /*!
+ * Retrieves the model associated with this model checker instance.
+ *
+ * @return The model associated with this model checker instance.
+ */
+ virtual storm::models::symbolic::Model<Type> const& getModel() const;
+
+ /*!
+ * Retrieves the model associated with this model checker instance as the given template parameter type.
+ *
+ * @return The model associated with this model checker instance.
+ */
+ template<typename ModelType>
+ ModelType const& getModelAs() const;
+
+ private:
+ // The model that is to be analyzed by the model checker.
+ storm::models::symbolic::Model<Type> const& model;
+ };
+ }
+}
+
+#endif /* STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp
index 5f79e0d1e..b518b0667 100644
--- a/src/modelchecker/results/CheckResult.cpp
+++ b/src/modelchecker/results/CheckResult.cpp
@@ -73,6 +73,14 @@ namespace storm {
return dynamic_cast<ExplicitQuantitativeCheckResult<ValueType> const&>(*this);
}
+ QualitativeCheckResult& CheckResult::asQualitativeCheckResult() {
+ return dynamic_cast<QualitativeCheckResult&>(*this);
+ }
+
+ QualitativeCheckResult const& CheckResult::asQualitativeCheckResult() const {
+ return dynamic_cast<QualitativeCheckResult const&>(*this);
+ }
+
QuantitativeCheckResult& CheckResult::asQuantitativeCheckResult() {
return dynamic_cast<QuantitativeCheckResult&>(*this);
}
diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
index 5606819db..79bb34885 100644
--- a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp
@@ -30,7 +30,7 @@ namespace storm {
}
void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, QualitativeCheckResult const& second, std::function<bool (bool, bool)> 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(second.isExplicitQualitativeCheckResult(), 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<ExplicitQualitativeCheckResult const&>(second);
if (first.isResultForAllStates()) {
@@ -104,6 +104,7 @@ namespace storm {
}
std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const {
+ out << "[";
if (this->isResultForAllStates()) {
out << boost::get<vector_type>(truthValues);
} else {
@@ -111,27 +112,18 @@ namespace storm {
out << std::boolalpha;
map_type const& map = boost::get<map_type>(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();
-#endif
-
- for (; it != ite; ++itPlusOne, ++it) {
- out << it->second;
- if (itPlusOne != ite) {
+ bool first = true;
+ for (auto const& element : map) {
+ if (!first) {
out << ", ";
+ } else {
+ first = false;
}
+ out << element.second;
}
std::cout.flags(oldflags);
}
+ out << "]";
return out;
}
diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index 2f4ce34fb..6c5b4520f 100644
--- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -83,29 +83,25 @@ namespace storm {
out << "[";
if (this->isResultForAllStates()) {
vector_type const& valuesAsVector = boost::get<vector_type>(values);
- typename vector_type::const_iterator it = valuesAsVector.begin();
- typename vector_type::const_iterator itPlusOne = valuesAsVector.begin();
- ++itPlusOne;
- typename vector_type::const_iterator ite = valuesAsVector.end();
-
- for (; it != ite; ++itPlusOne, ++it) {
- out << *it;
- if (itPlusOne != ite) {
+ bool first = true;
+ for (auto const& element : valuesAsVector) {
+ if (!first) {
out << ", ";
+ } else {
+ first = false;
}
+ out << element;
}
} else {
map_type const& valuesAsMap = boost::get<map_type>(values);
- typename map_type::const_iterator it = valuesAsMap.begin();
- typename map_type::const_iterator itPlusOne = valuesAsMap.begin();
- ++itPlusOne;
- typename map_type::const_iterator ite = valuesAsMap.end();
-
- for (; it != ite; ++itPlusOne, ++it) {
- out << it->second;
- if (itPlusOne != ite) {
+ bool first = true;
+ for (auto const& element : valuesAsMap) {
+ if (!first) {
out << ", ";
+ } else {
+ first = false;
}
+ out << element.second;
}
}
out << "]";
diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp
index f72ca929f..290da6884 100644
--- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp
+++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp
@@ -1,55 +1,66 @@
-#include "src/modelcheckers/result/SymbolicQualitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/storage/dd/CuddDd.h"
+#include "src/exceptions/InvalidOperationException.h"
namespace storm {
- namespace modelcheckers {
+ namespace modelchecker {
template <storm::dd::DdType Type>
- SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& values) {
-
+ SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& truthValues) : allStates(allStates), truthValues(truthValues) {
+ // Intentionally left empty.
}
template <storm::dd::DdType Type>
- bool isSymbolic() const {
-
+ bool SymbolicQualitativeCheckResult<Type>::isSymbolic() const {
+ return true;
}
template <storm::dd::DdType Type>
- bool isResultForAllStates() const {
-
+ bool SymbolicQualitativeCheckResult<Type>::isResultForAllStates() const {
+ return true;
}
template <storm::dd::DdType Type>
- bool isSymbolicQualitativeCheckResult() const {
-
+ bool SymbolicQualitativeCheckResult<Type>::isSymbolicQualitativeCheckResult() const {
+ return true;
}
template <storm::dd::DdType Type>
- QualitativeCheckResult& operator&=(QualitativeCheckResult const& other) {
-
+ QualitativeCheckResult& SymbolicQualitativeCheckResult<Type>::operator&=(QualitativeCheckResult const& other) {
+ STORM_LOG_THROW(other.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
+ this->truthValues &= other.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
}
template <storm::dd::DdType Type>
- QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) {
-
+ QualitativeCheckResult& SymbolicQualitativeCheckResult<Type>::operator|=(QualitativeCheckResult const& other) {
+ STORM_LOG_THROW(other.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
+ this->truthValues |= other.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
}
template <storm::dd::DdType Type>
- void complement() {
-
+ void SymbolicQualitativeCheckResult<Type>::complement() {
+ this->truthValues = !this->truthValues && allStates;
}
template <storm::dd::DdType Type>
- storm::dd::Dd<Type> const& getTruthValuesVector() const {
-
+ storm::dd::Dd<Type> const& SymbolicQualitativeCheckResult<Type>::getTruthValuesVector() const {
+ return truthValues;
}
template <storm::dd::DdType Type>
- std::ostream& writeToStream(std::ostream& out) const {
-
+ std::ostream& SymbolicQualitativeCheckResult<Type>::writeToStream(std::ostream& out) const {
+ if (this->truthValues.isZero()) {
+ out << "[false]" << std::endl;
+ } else {
+ out << "[true]" << std::endl;
+ }
+ return out;
}
template <storm::dd::DdType Type>
- void filter(QualitativeCheckResult const& filter) {
-
+ void SymbolicQualitativeCheckResult<Type>::filter(QualitativeCheckResult const& filter) {
+ STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter.");
+ this->truthValues &= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector();
}
}
}
\ No newline at end of file
diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h
index b13c39029..83c49ab98 100644
--- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h
+++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h
@@ -2,6 +2,7 @@
#define STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_
#include "src/storage/dd/DdType.h"
+#include "src/storage/dd/Dd.h"
#include "src/modelchecker/results/QualitativeCheckResult.h"
#include "src/utility/OsDetection.h"
@@ -11,7 +12,7 @@ namespace storm {
class SymbolicQualitativeCheckResult : public QualitativeCheckResult {
public:
SymbolicQualitativeCheckResult() = default;
- SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& values);
+ SymbolicQualitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& truthValues);
SymbolicQualitativeCheckResult(SymbolicQualitativeCheckResult const& other) = default;
SymbolicQualitativeCheckResult& operator=(SymbolicQualitativeCheckResult const& other) = default;
@@ -36,6 +37,9 @@ namespace storm {
virtual void filter(QualitativeCheckResult const& filter) override;
private:
+ // The set of all states.
+ storm::dd::Dd<Type> allStates;
+
// The values of the qualitative check result.
storm::dd::Dd<Type> truthValues;
};
diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
index e69de29bb..b78df481d 100644
--- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp
@@ -0,0 +1,70 @@
+#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+
+#include "src/storage/dd/CuddDd.h"
+#include "src/exceptions/InvalidOperationException.h"
+
+namespace storm {
+ namespace modelchecker {
+ template<storm::dd::DdType Type>
+ SymbolicQuantitativeCheckResult<Type>::SymbolicQuantitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& values) : allStates(allStates), values(values) {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType Type>
+ std::unique_ptr<CheckResult> SymbolicQuantitativeCheckResult<Type>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
+ std::unique_ptr<SymbolicQualitativeCheckResult<Type>> result;
+ if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::GreaterEqual) {
+ result = std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(allStates, values.greaterOrEqual(bound)));
+ } else {
+ result = std::unique_ptr<SymbolicQualitativeCheckResult<Type>>(new SymbolicQualitativeCheckResult<Type>(allStates, values.greater(bound)));
+ }
+ if (comparisonType == storm::logic::ComparisonType::Less || comparisonType == storm::logic::ComparisonType::LessEqual) {
+ result->complement();
+ }
+ return result;
+ }
+
+ template<storm::dd::DdType Type>
+ bool SymbolicQuantitativeCheckResult<Type>::isSymbolic() const {
+ return true;
+ }
+
+ template<storm::dd::DdType Type>
+ bool SymbolicQuantitativeCheckResult<Type>::isResultForAllStates() const {
+ return true;
+ }
+
+ template<storm::dd::DdType Type>
+ bool SymbolicQuantitativeCheckResult<Type>::isSymbolicQuantitativeCheckResult() const {
+ return true;
+ }
+
+ template<storm::dd::DdType Type>
+ storm::dd::Dd<Type> const& SymbolicQuantitativeCheckResult<Type>::getValueVector() const {
+ return values;
+ }
+
+ template<storm::dd::DdType Type>
+ std::ostream& SymbolicQuantitativeCheckResult<Type>::writeToStream(std::ostream& out) const {
+ out << "[";
+ bool first = true;
+ for (auto valuationValuePair : this->values) {
+ if (!first) {
+ out << ", ";
+ } else {
+ first = false;
+ }
+ out << valuationValuePair.second;
+ }
+ out << "]";
+ return out;
+ }
+
+ template<storm::dd::DdType Type>
+ void SymbolicQuantitativeCheckResult<Type>::filter(QualitativeCheckResult const& filter) {
+ STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter.");
+ this->truthValues *= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector().toMtbdd();
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h
index bb45fe090..0b1e331f4 100644
--- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h
+++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h
@@ -2,6 +2,7 @@
#define STORM_MODELCHECKER_SYMBOLICQUANTITATIVECHECKRESULT_H_
#include "src/storage/dd/DdType.h"
+#include "src/storage/dd/Dd.h"
#include "src/modelchecker/results/QuantitativeCheckResult.h"
#include "src/utility/OsDetection.h"
@@ -10,8 +11,8 @@ namespace storm {
template<storm::dd::DdType Type>
class SymbolicQuantitativeCheckResult : public QuantitativeCheckResult {
public:
- SymbolicQuantitativeCheckResult();
- SymbolicQuantitativeCheckResult(storm::dd::Dd<Type> const& values);
+ SymbolicQuantitativeCheckResult() = default;
+ SymbolicQuantitativeCheckResult(storm::dd::Dd<Type> const& allStates, storm::dd::Dd<Type> const& values);
SymbolicQuantitativeCheckResult(SymbolicQuantitativeCheckResult const& other) = default;
SymbolicQuantitativeCheckResult& operator=(SymbolicQuantitativeCheckResult const& other) = default;
@@ -34,6 +35,9 @@ namespace storm {
virtual void filter(QualitativeCheckResult const& filter) override;
private:
+ // The set of all states.
+ storm::dd::Dd<Type> allStates;
+
// The values of the quantitative check result.
storm::dd::Dd<Type> values;
};
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 21622ac24..b24e57934 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -440,8 +440,8 @@ namespace storm {
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
- result->writeToStream(std::cout, sparseModel->getInitialStates());
- std::cout << std::endl << std::endl;
+ result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+ std::cout << *result << std::endl;
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}
@@ -470,8 +470,8 @@ namespace storm {
if (result) {
std::cout << " done." << std::endl;
std::cout << "Result (initial states): ";
- result->writeToStream(std::cout, model->getInitialStates());
- std::cout << std::endl << std::endl;
+ result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(dtmc->getInitialStates()));
+ std::cout << *result << std::endl;
} else {
std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
}