diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
index e371ad8ce..498a2fc02 100644
--- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
@@ -141,7 +141,7 @@ namespace storm {
STORM_LOG_THROW(uniformizationRate > 0, storm::exceptions::InvalidStateException, "The uniformization rate must be positive.");
// Compute the uniformized matrix.
- storm::dd::Add<DdType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, statesWithProbabilityGreater0NonPsi, uniformizationRate);
+ storm::dd::Add<DdType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel(), this->getModel().getTransitionMatrix(), exitRates, statesWithProbabilityGreater0NonPsi, uniformizationRate);
// Compute the vector that is to be added as a compensation for removing the absorbing states.
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);
@@ -354,7 +354,24 @@ namespace storm {
// Finally, compute the transient probabilities.
std::vector<ValueType> result = SparseCtmcCslModelChecker<ValueType>::template computeTransientProbabilities<true>(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, *this->linearEquationSolverFactory);
- return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().getAddZero(), this->getModel().getReachableStates(), odd, result));
+ return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result)));
+ }
+
+ template<storm::dd::DdType DdType, class ValueType>
+ std::unique_ptr<CheckResult> HybridCtmcCslModelChecker<DdType, ValueType>::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+ std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
+ SymbolicQualitativeCheckResult<DdType> const& subResult = subResultPointer->asSymbolicQualitativeCheckResult<DdType>();
+
+ storm::dd::Add<DdType> probabilityMatrix = this->computeProbabilityMatrix(this->getModel(), this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector());
+
+ // Create ODD for the translation.
+ storm::dd::Odd<DdType> odd(this->getModel().getReachableStates());
+
+ storm::storage::SparseMatrix<ValueType> explicitProbabilityMatrix = probabilityMatrix.toMatrix(odd, odd);
+ std::vector<ValueType> explicitExitRateVector = this->getModel().getExitRateVector().template toVector<ValueType>(odd);
+
+ std::vector<ValueType> result = SparseCtmcCslModelChecker<ValueType>::computeLongRunAverageHelper(explicitProbabilityMatrix, subResult.getTruthValuesVector().toVector(odd), &explicitExitRateVector, qualitative, *this->linearEquationSolverFactory);
+ return std::unique_ptr<CheckResult>(new HybridQuantitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getManager().getBddZero(), this->getModel().getManager().getAddZero(), this->getModel().getReachableStates(), std::move(odd), std::move(result)));
}
// Explicitly instantiate the model checker.
diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.h b/src/modelchecker/csl/HybridCtmcCslModelChecker.h
index f0e619533..b2a94d51e 100644
--- a/src/modelchecker/csl/HybridCtmcCslModelChecker.h
+++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.h
@@ -23,7 +23,8 @@ namespace storm {
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;
-
+ virtual std::unique_ptr<CheckResult> computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+
protected:
storm::models::symbolic::Ctmc<DdType> const& getModel() const override;
diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
index dce356de7..62ca9af85 100644
--- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
@@ -479,11 +479,11 @@ namespace storm {
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
storm::storage::SparseMatrix<ValueType> probabilityMatrix = this->computeProbabilityMatrix(this->getModel().getTransitionMatrix(), this->getModel().getExitRateVector());
- return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(computeLongRunAverageHelper(this->getModel(), probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), qualitative, *linearEquationSolverFactory)));
+ return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(computeLongRunAverageHelper(probabilityMatrix, subResult.getTruthValuesVector(), &this->getModel().getExitRateVector(), qualitative, *linearEquationSolverFactory)));
}
template<typename ValueType>
- std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeLongRunAverageHelper(storm::models::sparse::DeterministicModel<ValueType> const& model, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
+ std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeLongRunAverageHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// If there are no goal states, we avoid the computation and directly return zero.
uint_fast64_t numOfStates = transitionMatrix.getRowCount();
if (psiStates.empty()) {
@@ -496,7 +496,7 @@ namespace storm {
}
// Start by decomposing the DTMC into its BSCCs.
- storm::storage::StronglyConnectedComponentDecomposition<double> bsccDecomposition(model, false, true);
+ storm::storage::StronglyConnectedComponentDecomposition<double> bsccDecomposition(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowCount(), true), false, true);
// Get some data members for convenience.
ValueType one = storm::utility::one<ValueType>();
diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h
index 42a1c9a0f..af1c9394a 100644
--- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h
+++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h
@@ -44,7 +44,7 @@ namespace storm {
static std::vector<ValueType> computeUntilProbabilitiesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
std::vector<ValueType> computeInstantaneousRewardsHelper(double timeBound) const;
std::vector<ValueType> computeCumulativeRewardsHelper(double timeBound) const;
- static std::vector<ValueType> computeLongRunAverageHelper(storm::models::sparse::DeterministicModel<ValueType> const& model, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
+ static std::vector<ValueType> computeLongRunAverageHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& psiStates, std::vector<ValueType> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory);
/*!
* Computes the matrix representing the transitions of the uniformized CTMC.
*
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index 538aa78aa..8c15f0bd8 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -308,7 +308,7 @@ namespace storm {
std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
- return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseCtmcCslModelChecker<ValueType>::computeLongRunAverageHelper(this->getModel(), this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory)));
+ return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseCtmcCslModelChecker<ValueType>::computeLongRunAverageHelper(this->getModel().getTransitionMatrix(), subResult.getTruthValuesVector(), nullptr, qualitative, *linearEquationSolverFactory)));
}
template<typename ValueType>
diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
index 4fa0dbafe..1ddd761d6 100644
--- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.cpp
@@ -36,6 +36,11 @@ namespace storm {
return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getStates(stateFormula.getLabel())));
}
+ template<storm::dd::DdType Type>
+ std::unique_ptr<CheckResult> SymbolicPropositionalModelChecker<Type>::checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) {
+ return std::unique_ptr<CheckResult>(new SymbolicQualitativeCheckResult<Type>(model.getReachableStates(), model.getStates(stateFormula.getExpression())));
+ }
+
template<storm::dd::DdType Type>
storm::models::symbolic::Model<Type> const& SymbolicPropositionalModelChecker<Type>::getModel() const {
return model;
diff --git a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
index 96dcea601..ec3433dec 100644
--- a/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
+++ b/src/modelchecker/propositional/SymbolicPropositionalModelChecker.h
@@ -16,7 +16,8 @@ namespace storm {
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;
-
+ virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula) override;
+
protected:
/*!
* Retrieves the model associated with this model checker instance.
diff --git a/src/storage/dd/CuddAdd.h b/src/storage/dd/CuddAdd.h
index 01a57b629..03c8b3a2c 100644
--- a/src/storage/dd/CuddAdd.h
+++ b/src/storage/dd/CuddAdd.h
@@ -721,7 +721,7 @@ namespace storm {
void toMatrixRec(DdNode const* dd, std::vector<uint_fast64_t>& rowIndications, std::vector<storm::storage::MatrixEntry<uint_fast64_t, double>>& columnsAndValues, std::vector<uint_fast64_t> const& rowGroupOffsets, Odd<DdType::CUDD> const& rowOdd, Odd<DdType::CUDD> const& columnOdd, uint_fast64_t currentRowLevel, uint_fast64_t currentColumnLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, uint_fast64_t currentColumnOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices, std::vector<uint_fast64_t> const& ddColumnVariableIndices, bool generateValues = true) const;
/*!
- * Helper function to convert the DD into a (sparse) vector.
+ * Helper function to convert the DD into an (explicit) vector.
*
* @param dd The DD to convert.
* @param result The vector that will hold the values upon successful completion.
@@ -772,7 +772,7 @@ namespace storm {
void addToVector(Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::vector<ValueType>& targetVector) const;
/*!
- * Performs a recursive step to perform the given function between the given DD-based vector to the given
+ * Performs a recursive step to perform the given function between the given DD-based vector and the given
* explicit vector.
*
* @param dd The DD to add to the explicit vector.
diff --git a/src/storage/dd/CuddBdd.cpp b/src/storage/dd/CuddBdd.cpp
index ca93c1742..30ed8a191 100644
--- a/src/storage/dd/CuddBdd.cpp
+++ b/src/storage/dd/CuddBdd.cpp
@@ -337,6 +337,41 @@ namespace storm {
}
}
+ storm::storage::BitVector Bdd<DdType::CUDD>::toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const {
+ std::vector<uint_fast64_t> ddVariableIndices = this->getSortedVariableIndices();
+ storm::storage::BitVector result(rowOdd.getTotalOffset());
+ this->toVectorRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices);
+ return result;
+ }
+
+ void Bdd<DdType::CUDD>::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const {
+ // If there are no more values to select, we can directly return.
+ if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) {
+ return;
+ } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) {
+ return;
+ }
+
+ // If we are at the maximal level, the value to be set is stored as a constant in the DD.
+ if (currentRowLevel == maxLevel) {
+ result.set(currentRowOffset, true);
+ } else if (ddRowVariableIndices[currentRowLevel] < dd->index) {
+ toVectorRec(dd, manager, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
+ toVectorRec(dd, manager, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
+ } else {
+ // Otherwise, we compute the ODDs for both the then- and else successors.
+ DdNode* elseDdNode = Cudd_E(dd);
+ DdNode* thenDdNode = Cudd_T(dd);
+
+ // Determine whether we have to evaluate the successors as if they were complemented.
+ bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement;
+ bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement;
+
+ toVectorRec(Cudd_Regular(elseDdNode), manager, result, rowOdd.getElseSuccessor(), elseComplemented, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices);
+ toVectorRec(Cudd_Regular(thenDdNode), manager, result, rowOdd.getThenSuccessor(), thenComplemented, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices);
+ }
+ }
+
std::ostream& operator<<(std::ostream& out, const Bdd<DdType::CUDD>& bdd) {
bdd.exportToDot();
return out;
diff --git a/src/storage/dd/CuddBdd.h b/src/storage/dd/CuddBdd.h
index 326072eb9..ad2d9aa6a 100644
--- a/src/storage/dd/CuddBdd.h
+++ b/src/storage/dd/CuddBdd.h
@@ -263,6 +263,15 @@ namespace storm {
*/
Add<DdType::CUDD> toAdd() const;
+ /*!
+ * Converts the BDD to a bit vector. The given offset-labeled DD is used to determine the correct row of
+ * each entry.
+ *
+ * @param rowOdd The ODD used for determining the correct row.
+ * @return The bit vector that is represented by this BDD.
+ */
+ storm::storage::BitVector toVector(storm::dd::Odd<DdType::CUDD> const& rowOdd) const;
+
private:
/*!
* Retrieves the CUDD BDD object associated with this DD.
@@ -315,6 +324,21 @@ namespace storm {
template<typename ValueType>
static DdNode* fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd<DdType::CUDD> const& odd, std::vector<uint_fast64_t> const& ddVariableIndices, std::function<bool (ValueType const&)> const& filter);
+ /*!
+ * Helper function to convert the DD into a bit vector.
+ *
+ * @param dd The DD to convert.
+ * @param manager The Cudd manager responsible for the DDs.
+ * @param result The vector that will hold the values upon successful completion.
+ * @param rowOdd The ODD used for the row translation.
+ * @param complement A flag indicating whether the result is to be interpreted as a complement.
+ * @param currentRowLevel The currently considered row level in the DD.
+ * @param maxLevel The number of levels that need to be considered.
+ * @param currentRowOffset The current row offset.
+ * @param ddRowVariableIndices The (sorted) indices of all DD row variables that need to be considered.
+ */
+ void toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd<DdType::CUDD> const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector<uint_fast64_t> const& ddRowVariableIndices) const;
+
// The BDD created by CUDD.
BDD cuddBdd;
};