diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index 62fe2c1dd..2aeab204f 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -57,7 +57,7 @@ namespace storm { template bool HybridQuantitativeCheckResult::isResultForAllStates() const { - return true; + return (symbolicStates || explicitStates) == reachableStates; } template @@ -169,12 +169,16 @@ namespace storm { template ValueType HybridQuantitativeCheckResult::sum() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for hybrid results"); + ValueType sum = symbolicValues.sumAbstract(symbolicValues.getContainedMetaVariables()).getValue(); + for (auto const& value : explicitValues) { + sum += value; + } + return sum; } template ValueType HybridQuantitativeCheckResult::average() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for hybrid results"); + return this->sum() / (symbolicStates || explicitStates).getNonZeroCount(); } template @@ -193,4 +197,4 @@ namespace storm { template class HybridQuantitativeCheckResult; template class HybridQuantitativeCheckResult; } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 16a802331..43b1a39a4 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -54,7 +54,6 @@ namespace storm { virtual ValueType average() const override; - virtual void oneMinus() override; private: @@ -79,4 +78,4 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */ diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 3468a13c9..da97a38da 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -8,7 +8,7 @@ namespace storm { namespace modelchecker { template - SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& truthValues) : reachableStates(reachableStates), truthValues(truthValues) { + SymbolicQualitativeCheckResult::SymbolicQualitativeCheckResult(storm::dd::Bdd const& reachableStates, storm::dd::Bdd const& truthValues) : reachableStates(reachableStates), states(reachableStates), truthValues(truthValues) { // Intentionally left empty. } @@ -19,7 +19,7 @@ namespace storm { template bool SymbolicQualitativeCheckResult::isResultForAllStates() const { - return true; + return reachableStates == states; } template @@ -48,22 +48,22 @@ namespace storm { template storm::dd::Bdd const& SymbolicQualitativeCheckResult::getTruthValuesVector() const { - return truthValues; + return this->truthValues; } template bool SymbolicQualitativeCheckResult::existsTrue() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Exists not implemented for symbolic results"); + return !this->truthValues.isZero(); } template bool SymbolicQualitativeCheckResult::forallTrue() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall not implemented for symbolic results"); + return this->truthValues == this->states; } template uint64_t SymbolicQualitativeCheckResult::count() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Count not implemented for symbolic results"); + return this->truthValues.getNonZeroCount(); } template @@ -80,9 +80,10 @@ namespace storm { void SymbolicQualitativeCheckResult::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().getTruthValuesVector(); + this->states &= filter.asSymbolicQualitativeCheckResult().getTruthValuesVector(); } template class SymbolicQualitativeCheckResult; template class SymbolicQualitativeCheckResult; } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 775b8c467..db3ee1ab5 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -45,11 +45,14 @@ namespace storm { private: // The set of all reachable states. storm::dd::Bdd reachableStates; - + + // The set of states for which this check result contains values. + storm::dd::Bdd states; + // The values of the qualitative check result. storm::dd::Bdd truthValues; }; } } -#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */ diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index bde1407a4..5bc712d2d 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -93,12 +93,12 @@ namespace storm { template ValueType SymbolicQuantitativeCheckResult::average() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for symbolic results"); + return this->sum() / this->states.getNonZeroCount(); } template ValueType SymbolicQuantitativeCheckResult::sum() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for symbolic results"); + return this->values.sumAbstract(this->values.getContainedMetaVariables()).getValue(); } template @@ -111,4 +111,4 @@ namespace storm { template class SymbolicQuantitativeCheckResult; template class SymbolicQuantitativeCheckResult; } -} \ No newline at end of file +} diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index cfe2ce9b6..edbdc5d5a 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ #include +#include namespace storm { namespace expressions { @@ -33,4 +34,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ */