From e1761fa774c68b84f91c361cc868fe8418db03b0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 8 Apr 2015 23:08:59 +0200
Subject: [PATCH] Enabled hybrid CTMC model checker in cli. Further work on
hybrid CTMC model checker (not yet working). Fixed some minor issues in
sparse CTMC model checker.
Former-commit-id: f9c0f976e187c4e39a96dacfe2291e23ddf13172
---
examples/ctmc/tandem/tandem.sm | 6 +-
.../csl/HybridCtmcCslModelChecker.cpp | 37 +--
.../csl/HybridCtmcCslModelChecker.h | 4 +-
.../csl/SparseCtmcCslModelChecker.cpp | 82 +++---
.../csl/SparseCtmcCslModelChecker.h | 2 +
.../prctl/HybridDtmcPrctlModelChecker.cpp | 4 +-
.../prctl/SparseDtmcPrctlModelChecker.cpp | 2 +-
.../SymbolicPropositionalModelChecker.cpp | 2 +
.../results/HybridQuantitativeCheckResult.cpp | 2 +-
src/storage/BitVector.h | 21 ++
src/utility/cli.h | 7 +
.../GmmxxCtmcCslModelCheckerTest.cpp | 19 +-
.../GmmxxHybridCtmcCslModelCheckerTest.cpp | 261 ++++++++++++++++++
13 files changed, 383 insertions(+), 66 deletions(-)
create mode 100644 test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
diff --git a/examples/ctmc/tandem/tandem.sm b/examples/ctmc/tandem/tandem.sm
index 439d33813..c35246e1a 100644
--- a/examples/ctmc/tandem/tandem.sm
+++ b/examples/ctmc/tandem/tandem.sm
@@ -35,4 +35,8 @@ endmodule
// reward - number of customers in network
rewards "customers"
true : sc + sm;
-endrewards
\ No newline at end of file
+endrewards
+
+label "network_full" = sc=c&sm=c&ph=2;
+label "first_queue_full" = sc=c;
+label "second_queue_full" = sm=c;
diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
index a8c088aeb..67578184e 100644
--- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
@@ -10,6 +10,7 @@
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/InvalidPropertyException.h"
@@ -33,7 +34,7 @@ namespace storm {
template<storm::dd::DdType DdType, class ValueType>
storm::dd::Add<DdType> HybridCtmcCslModelChecker<DdType, ValueType>::computeProbabilityMatrix(storm::models::symbolic::Model<DdType> const& model, storm::dd::Add<DdType> const& rateMatrix, storm::dd::Add<DdType> const& exitRateVector) {
- return rateMatrix / exitRateVector.swapVariables(model.getRowColumnMetaVariablePairs());
+ return rateMatrix / exitRateVector;
}
template<storm::dd::DdType DdType, class ValueType>
@@ -68,9 +69,10 @@ namespace storm {
// Now perform the uniformization.
uniformizedMatrix = uniformizedMatrix / model.getManager().getConstant(uniformizationRate);
- storm::dd::Add<DdType> diagonalOffset = model.getRowColumnIdentity();
- diagonalOffset -= model.getRowColumnIdentity() * (exitRateVector / model.getManager().getConstant(uniformizationRate));
- uniformizedMatrix = uniformizedMatrix + diagonalOffset;
+ storm::dd::Add<DdType> diagonal = model.getRowColumnIdentity() * maybeStates.toAdd();
+ storm::dd::Add<DdType> diagonalOffset = diagonal;
+ diagonalOffset -= diagonal * (exitRateVector / model.getManager().getConstant(uniformizationRate));
+ uniformizedMatrix += diagonalOffset;
return uniformizedMatrix;
}
@@ -82,7 +84,7 @@ namespace storm {
boost::optional<storm::dd::Add<DdType>> modifiedStateRewardVector;
if (this->getModel().hasStateRewards()) {
- modifiedStateRewardVector = this->getModel().getStateRewardVector() / this->getModel().getTransitionMatrix().sumAbstract(this->getModel().getColumnVariables());
+ modifiedStateRewardVector = this->getModel().getStateRewardVector() / this->getModel().getExitRateVector();
}
return HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewardsHelper(this->getModel(), this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector()), modifiedStateRewardVector, this->getModel().getOptionalTransitionRewardMatrix(), subResult.getTruthValuesVector(), *linearEquationSolverFactory, qualitative);
@@ -171,7 +173,7 @@ namespace storm {
std::unique_ptr<CheckResult> statesWithValuesGreaterZero = unboundedResult->asQuantitativeCheckResult().compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero<ValueType>());
// And use it to compute the set of relevant states.
- storm::dd::Bdd<DdType> relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector());
+ storm::dd::Bdd<DdType> relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix().notZero(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector());
// Filter the unbounded result such that it only contains values for the relevant states.
unboundedResult->filter(SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), relevantStates));
@@ -185,7 +187,7 @@ namespace storm {
result = std::move(explicitUnboundedResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());
} else {
STORM_LOG_THROW(unboundedResult->isSymbolicQuantitativeCheckResult(), storm::exceptions::InvalidStateException, "Expected check result of different type.");
- result = unboundedResult->asSymbolicQuantitativeCheckResult<DdType>().getValueVector().toVector(odd);
+ result = unboundedResult->asSymbolicQuantitativeCheckResult<DdType>().getValueVector().template toVector<ValueType>(odd);
}
// Determine the uniformization rate for the transient probability computation.
@@ -196,9 +198,9 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
// Compute the transient probabilities.
- std::vector<ValueType> subResult = SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, subResult, *this->linearEquationSolverFactory);
+ result = SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, result, *this->linearEquationSolverFactory);
- return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, odd, subResult));
+ return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, odd, result));
} else {
// In this case, the interval is of the form [t, t'] with t != 0 and t' != inf.
@@ -223,9 +225,9 @@ namespace storm {
storm::dd::Add<DdType> b = (statesWithProbabilityGreater0NonPsi.toAdd() * this->getModel().getTransitionMatrix() * psiStates.swapVariables(this->getModel().getRowColumnMetaVariablePairs()).toAdd()).sumAbstract(this->getModel().getColumnVariables()) / this->getModel().getManager().getConstant(uniformizationRate);
// Build an ODD for the relevant states and translate the symbolic parts to their explicit representation.
- odd(statesWithProbabilityGreater0NonPsi);
+ odd = storm::dd::Odd<DdType>(statesWithProbabilityGreater0NonPsi);
storm::storage::SparseMatrix<ValueType> explicitUniformizedMatrix = uniformizedMatrix.toMatrix(odd, odd);
- std::vector<ValueType> explicitB = b.toVector(odd);
+ std::vector<ValueType> explicitB = b.template toVector<ValueType>(odd);
// Compute the transient probabilities.
std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNonZeroCount(), storm::utility::zero<ValueType>());
@@ -234,16 +236,16 @@ namespace storm {
// Transform the explicit result to a hybrid check result, so we can easily convert it to
// a symbolic qualitative format.
HybridQuantitativeCheckResult<DdType> hybridResult(this->getModel().getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && this->getModel().getReachableStates()),
- psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, subResult);
+ psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, odd, subResult);
// Determine the set of states that achieved a strictly positive probability.
std::unique_ptr<CheckResult> statesWithValuesGreaterZero = hybridResult.compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero<ValueType>());
// And use it to compute the set of relevant states.
- storm::dd::Bdd<DdType> relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector());
+ storm::dd::Bdd<DdType> relevantStates = storm::utility::graph::performProbGreater0(this->getModel(), this->getModel().getTransitionMatrix().notZero(), phiStates, statesWithValuesGreaterZero->asSymbolicQualitativeCheckResult<DdType>().getTruthValuesVector());
// Filter the unbounded result such that it only contains values for the relevant states.
- hybridResult->filter(SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), relevantStates));
+ hybridResult.filter(SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), relevantStates));
// Build an ODD for the relevant states.
odd = storm::dd::Odd<DdType>(relevantStates);
@@ -261,7 +263,8 @@ namespace storm {
// If the lower and upper bounds coincide, we have only determined the relevant states at this
// point, but we still need to construct the starting vector.
if (lowerBound == upperBound) {
- newSubresult = psiStates.toAdd().toVector(odd); std::vector<ValueType>(relevantStates.getNonZeroCount());
+ odd = storm::dd::Odd<DdType>(relevantStates);
+ newSubresult = psiStates.toAdd().template toVector<ValueType>(odd);
}
// Finally, we compute the second set of transient probabilities.
@@ -270,11 +273,11 @@ namespace storm {
newSubresult = SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory);
- return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, newSubresult));
+ return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), !relevantStates && this->getModel().getReachableStates(), this->getModel().getManager().getAddZero(), relevantStates, odd, newSubresult));
}
}
} else {
- return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>>(this->getModel().getReachableStates(), psiStates.toAdd()));
+ return std::unique_ptr<CheckResult>(new SymbolicQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), psiStates.toAdd()));
}
}
diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h
index ffc2d2694..331e12152 100644
--- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h
+++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h
@@ -20,8 +20,8 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
- virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
- virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+// virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+// virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
protected:
diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
index 0a1a71c42..898993437 100644
--- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
@@ -138,8 +138,7 @@ namespace storm {
result = this->computeUntilProbabilitiesHelper(this->getModel().getTransitionMatrix(), backwardTransitions, phiStates, psiStates, qualitative, *this->linearEquationSolverFactory);
// Determine the set of states that must be considered further.
- storm::storage::BitVector relevantStates = storm::utility::vector::filterGreaterZero(result);
- relevantStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, relevantStates & phiStates);
+ storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & phiStates;
std::vector<ValueType> subResult(relevantStates.getNumberOfSetBits());
storm::utility::vector::selectVectorValues(subResult, relevantStates, result);
@@ -163,14 +162,11 @@ namespace storm {
// In this case, the interval is of the form [t, t'] with t != 0 and t' != inf.
// Prepare some variables that are used by the two following blocks.
- storm::storage::BitVector relevantStates;
ValueType uniformizationRate = 0;
storm::storage::SparseMatrix<ValueType> uniformizedMatrix;
std::vector<ValueType> newSubresult;
- if (lowerBound == upperBound) {
- relevantStates = statesWithProbabilityGreater0;
- } else {
+ if (lowerBound != upperBound) {
// Find the maximal rate of all 'maybe' states to take it as the uniformization rate.
uniformizationRate = 0;
for (auto const& state : statesWithProbabilityGreater0NonPsi) {
@@ -192,38 +188,51 @@ namespace storm {
std::vector<ValueType> values(statesWithProbabilityGreater0NonPsi.getNumberOfSetBits(), storm::utility::zero<ValueType>());
std::vector<ValueType> subresult = computeTransientProbabilities(uniformizedMatrix, &b, upperBound - lowerBound, uniformizationRate, values, *this->linearEquationSolverFactory);
- // Determine the set of states that must be considered further.
- relevantStates = storm::utility::vector::filterGreaterZero(subresult);
- relevantStates = storm::utility::graph::performProbGreater0(uniformizedMatrix.transpose(), phiStates % statesWithProbabilityGreater0NonPsi, relevantStates & (phiStates % statesWithProbabilityGreater0NonPsi));
-
- newSubresult = std::vector<ValueType>(relevantStates.getNumberOfSetBits());
- storm::utility::vector::selectVectorValues(newSubresult, relevantStates, subresult);
- }
-
- // Then compute the transient probabilities of being in such a state after t time units. For this,
- // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
- uniformizationRate = 0;
- for (auto const& state : relevantStates) {
- uniformizationRate = std::max(uniformizationRate, exitRates[state]);
- }
- uniformizationRate *= 1.02;
- STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
-
- // If the lower and upper bounds coincide, we have only determined the relevant states at this
- // point, but we still need to construct the starting vector.
- if (lowerBound == upperBound) {
+ storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & phiStates;
newSubresult = std::vector<ValueType>(relevantStates.getNumberOfSetBits());
+ storm::utility::vector::selectVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult);
storm::utility::vector::setVectorValues(newSubresult, psiStates % relevantStates, storm::utility::one<ValueType>());
+
+ // Then compute the transient probabilities of being in such a state after t time units. For this,
+ // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
+ uniformizationRate = 0;
+ for (auto const& state : relevantStates) {
+ uniformizationRate = std::max(uniformizationRate, exitRates[state]);
+ }
+ uniformizationRate *= 1.02;
+ STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
+
+ // Finally, we compute the second set of transient probabilities.
+ uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, uniformizationRate, exitRates);
+ newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory);
+
+ // Fill in the correct values.
+ result = std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
+ storm::utility::vector::setVectorValues(result, ~relevantStates, storm::utility::zero<ValueType>());
+ storm::utility::vector::setVectorValues(result, relevantStates, newSubresult);
+ } else {
+ newSubresult = std::vector<ValueType>(statesWithProbabilityGreater0.getNumberOfSetBits());
+ storm::utility::vector::setVectorValues(newSubresult, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>());
+
+ // Then compute the transient probabilities of being in such a state after t time units. For this,
+ // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
+ uniformizationRate = 0;
+ for (auto const& state : statesWithProbabilityGreater0) {
+ uniformizationRate = std::max(uniformizationRate, exitRates[state]);
+ }
+ uniformizationRate *= 1.02;
+ STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
+
+ // Finally, we compute the second set of transient probabilities.
+ uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0, uniformizationRate, exitRates);
+ newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory);
+
+ // Fill in the correct values.
+ result = std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
+ storm::utility::vector::setVectorValues(result, ~statesWithProbabilityGreater0, storm::utility::zero<ValueType>());
+ storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, newSubresult);
+
}
-
- // Finally, we compute the second set of transient probabilities.
- uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), relevantStates, uniformizationRate, exitRates);
- newSubresult = computeTransientProbabilities(uniformizedMatrix, nullptr, lowerBound, uniformizationRate, newSubresult, *this->linearEquationSolverFactory);
-
- // Fill in the correct values.
- result = std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
- storm::utility::vector::setVectorValues(result, ~relevantStates, storm::utility::zero<ValueType>());
- storm::utility::vector::setVectorValues(result, relevantStates, newSubresult);
}
}
}
@@ -337,7 +346,7 @@ namespace storm {
weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)];
storm::utility::vector::applyPointwise(result, values, result, addAndScale);
}
-
+
return result;
}
@@ -438,6 +447,7 @@ namespace storm {
boost::optional<std::vector<ValueType>> modifiedStateRewardVector;
if (this->getModel().hasStateRewards()) {
modifiedStateRewardVector = std::vector<ValueType>(this->getModel().getStateRewardVector());
+
typename std::vector<ValueType>::const_iterator it2 = this->getModel().getExitRateVector().begin();
for (typename std::vector<ValueType>::iterator it1 = modifiedStateRewardVector.get().begin(), ite1 = modifiedStateRewardVector.get().end(); it1 != ite1; ++it1, ++it2) {
*it1 /= *it2;
diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h
index ffa89f904..5108a183f 100644
--- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h
+++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h
@@ -16,6 +16,8 @@ namespace storm {
template<class ValueType>
class SparseCtmcCslModelChecker : public SparsePropositionalModelChecker<ValueType> {
public:
+ friend class HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, ValueType>;
+
explicit SparseCtmcCslModelChecker(storm::models::sparse::Ctmc<ValueType> const& model);
explicit SparseCtmcCslModelChecker(storm::models::sparse::Ctmc<ValueType> const& model, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<ValueType>>&& linearEquationSolverFactory);
diff --git a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
index 231c17a94..25a02adff 100644
--- a/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/HybridDtmcPrctlModelChecker.cpp
@@ -231,7 +231,7 @@ namespace storm {
std::unique_ptr<CheckResult> HybridDtmcPrctlModelChecker<DdType, ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
- return this->computeReachabilityRewardsHelper(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory, qualitative);
+ return this->computeReachabilityRewardsHelper(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getOptionalStateRewardVector(), this->getModel().getOptionalTransitionRewardMatrix(), subResult.getTruthValuesVector(), *this->linearEquationSolverFactory, qualitative);
}
template<storm::dd::DdType DdType, typename ValueType>
@@ -247,7 +247,7 @@ namespace storm {
STORM_LOG_INFO("Found " << infinityStates.getNonZeroCount() << " 'infinity' states.");
STORM_LOG_INFO("Found " << targetStates.getNonZeroCount() << " 'target' states.");
STORM_LOG_INFO("Found " << maybeStates.getNonZeroCount() << " 'maybe' states.");
-
+
// Check whether we need to compute exact rewards for some states.
if (qualitative) {
// Set the values for all maybe-states to 1 to indicate that their reward values
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index a7775139a..179e82f42 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -248,7 +248,7 @@ namespace storm {
// 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<ValueType> x(submatrix.getColumnCount(), storm::utility::one<ValueType>());
diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
index 1552235d9..4fa0dbafe 100644
--- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
@@ -1,6 +1,7 @@
#include "src/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
#include "src/models/symbolic/Dtmc.h"
+#include "src/models/symbolic/Ctmc.h"
#include "src/models/symbolic/Mdp.h"
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
@@ -48,6 +49,7 @@ namespace storm {
// 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::Ctmc<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>;
}
diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
index 7019786ad..abf56e163 100644
--- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp
@@ -150,7 +150,7 @@ namespace storm {
template<storm::dd::DdType Type>
double HybridQuantitativeCheckResult<Type>::getMax() const {
- double max = this->symbolicValues.getMin();
+ double max = this->symbolicValues.getMax();
if (!explicitStates.isZero()) {
for (auto const& element : explicitValues) {
max = std::max(max, element);
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index ec4cce693..5072d71cf 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -277,6 +277,27 @@ namespace storm {
*/
BitVector operator%(BitVector const& filter) const;
+// /*!
+// * Computes a bit vector that is as long as the number of set bits in the given filter that has bit i is set
+// * iff the i-th set bit of the current bit vector is set in the filter. Note: this functionality is exactly
+// * the same as operator%.
+// *
+// * @param filter A reference the bit vector to use as the filter.
+// * @return A bit vector that is as long as the number of set bits in the given filter that has bit i is set
+// * iff the i-th set bit of the current bit vector is set in the filter.
+// */
+// BitVector operator<<(BitVector const& filter) const;
+//
+// /*!
+// * Computes a bit vector that is as long as the number of set bits in the given filter that has bit i is set
+// * iff the i-th set bit of the current bit vector is set in the filter.
+// *
+// * @param filter A reference the bit vector to use as the filter.
+// * @return A bit vector that is as long as the number of set bits in the given filter that has bit i is set
+// * iff the i-th set bit of the current bit vector is set in the filter.
+// */
+// BitVector operator>>(BitVector const& filter) const;
+
/*!
* Performs a logical "not" on the bit vector.
*
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 780201cf3..b46867be0 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -68,6 +68,7 @@ log4cplus::Logger printer;
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
+#include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
@@ -503,6 +504,12 @@ namespace storm {
if (modelchecker.canHandle(*formula.get())) {
result = modelchecker.check(*formula.get());
}
+ } else if (model->getType() == storm::models::ModelType::Ctmc) {
+ std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
+ storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
+ if (modelchecker.canHandle(*formula.get())) {
+ result = modelchecker.check(*formula.get());
+ }
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
}
diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
index 6a814d63d..56c61da5a 100644
--- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
@@ -48,26 +48,33 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
- formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
+ formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
- EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(0.001105335651650576, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
- formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+ formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
- EXPECT_NEAR(0, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
- formula = formulaParser.parseFromString("R=? [C<=100]");
+ formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
- EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("R=? [C<=100]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
+ storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult<double>();
+ EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision());
}
TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
new file mode 100644
index 000000000..472547ba3
--- /dev/null
+++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
@@ -0,0 +1,261 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/settings/SettingMemento.h"
+#include "src/parser/PrismParser.h"
+#include "src/parser/FormulaParser.h"
+#include "src/logic/Formulas.h"
+#include "src/builder/DdPrismModelBuilder.h"
+#include "src/storage/dd/DdType.h"
+
+#include "src/utility/solver.h"
+#include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
+#include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+
+#include "src/settings/SettingsManager.h"
+
+TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
+ // Parse the model description.
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+ storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
+ std::shared_ptr<storm::logic::Formula> formula(nullptr);
+
+ // Build the model.
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+ options.buildRewards = true;
+ options.rewardModelName = "num_repairs";
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
+ std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
+
+ // Create model checker.
+ storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
+
+ // Start checking properties.
+ formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
+ std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(0, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(0, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
+
+// formula = formulaParser.parseFromString("R=? [C<=100]");
+// checkResult = modelchecker.check(*formula);
+//
+// ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+// checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+// storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+// EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
+// EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
+}
+
+TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
+ // Parse the model description.
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+ storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
+ std::shared_ptr<storm::logic::Formula> formula(nullptr);
+
+ // Build the model.
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+ options.buildRewards = true;
+ options.rewardModelName = "up";
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
+ std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
+
+ // Create model checker.
+ storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
+
+ // Start checking properties.
+ formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
+ std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
+
+// formula = formulaParser.parseFromString("R=? [C<=10000]");
+// checkResult = modelchecker.check(*formula);
+//
+// ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+// checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+// storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+// EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
+// EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
+}
+
+TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
+ // Parse the model description.
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+ storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
+ std::shared_ptr<storm::logic::Formula> formula(nullptr);
+
+ // Build the model.
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
+ ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
+ std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
+
+ // Create model checker.
+ storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
+
+ // Start checking properties.
+ formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
+ std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
+}
+
+TEST(GmmxxHybridCtmcCslModelCheckerTest, Fms) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
+ // No properties to check at this point.
+}
+
+TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
+ // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+ std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true);
+
+ // Parse the model description.
+ storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+ storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
+ std::shared_ptr<storm::logic::Formula> formula(nullptr);
+
+ // Build the model with the customers reward structure.
+ typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
+ options.buildRewards = true;
+ options.rewardModelName = "customers";
+ std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
+ ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
+ std::shared_ptr<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>> ctmc = model->as<storm::models::symbolic::Ctmc<storm::dd::DdType::CUDD>>();
+
+ // Create model checker.
+ storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
+
+ // Start checking properties.
+ formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
+ std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult1 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult2 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
+
+// formula = formulaParser.parseFromString("R=? [I=10]");
+// checkResult = modelchecker.check(*formula);
+//
+// ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+// checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+// storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult4 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+// EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
+// EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
+//
+// formula = formulaParser.parseFromString("R=? [C<=10]");
+// checkResult = modelchecker.check(*formula);
+//
+// ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+// checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+// storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+// EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
+// EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
+
+ formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
+ checkResult = modelchecker.check(*formula);
+
+ ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
+ checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
+ storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult6 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
+ EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision());
+ EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision());
+}