diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index e3cea0fb6..8356620c1 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -34,7 +34,7 @@ namespace storm { template bool SparseCtmcCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setExpectedTimeAllowed(true)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(false).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); } template @@ -114,12 +114,12 @@ namespace storm { } template - std::unique_ptr SparseCtmcCslModelChecker::computeExpectedTimes(CheckTask const& checkTask) { + std::unique_ptr SparseCtmcCslModelChecker::computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) { storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula(); std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimes(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), this->getModel().getInitialStates(), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *linearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 4d838d4d8..802841dee 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -28,7 +28,7 @@ namespace storm { virtual std::unique_ptr computeInstantaneousRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(CheckTask const& checkTask) override; - virtual std::unique_ptr computeExpectedTimes(CheckTask const& checkTask) override; + virtual std::unique_ptr computeReachabilityTimes(storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: // An object that is used for solving linear equations and performing matrix-vector multiplication. diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index ff04148aa..d0f8a1b69 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -656,7 +656,7 @@ namespace storm { } template - std::vector SparseCtmcCslHelper::computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { + std::vector SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // Compute expected time on CTMC by reduction to DTMC with rewards. storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -677,7 +677,7 @@ namespace storm { template - std::vector SparseCtmcCslHelper::computeExpectedTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative) { + std::vector SparseCtmcCslHelper::computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative) { // Use "normal" function again, if RationalFunction finally is supported. // Compute expected time on CTMC by reduction to DTMC with rewards. storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); @@ -704,7 +704,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template std::vector SparseCtmcCslHelper::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); - template std::vector SparseCtmcCslHelper::computeExpectedTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); #endif } } diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h index 14a98f752..2b4dd6043 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -29,8 +29,8 @@ namespace storm { static std::vector computeLongRunAverageProbabilities(storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory); - static std::vector computeExpectedTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeExpectedTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); + static std::vector computeReachabilityTimes(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + static std::vector computeReachabilityTimesElimination(storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative); /*! * Computes the matrix representing the transitions of the uniformized CTMC. @@ -82,4 +82,4 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_SPARSE_CTMC_CSL_MODELCHECKER_HELPER_H_ */ diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 97614507a..22803d9c1 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -280,7 +280,7 @@ namespace storm { booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; booleanLiteralFormula.name("boolean literal formula"); - operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | expectedTimeOperator; + operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator; operatorFormula.name("operator formulas"); atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; @@ -355,7 +355,7 @@ namespace storm { debug(probabilityOperator); debug(rewardOperator); debug(longRunAverageOperator); - debug(expectedTimeOperator); + debug(timeOperator); debug(pathFormulaWithoutUntil); debug(pathFormula); // debug(conditionalFormula); @@ -379,7 +379,7 @@ namespace storm { qi::on_error(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(longRunAverageOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(expectedTimeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(timeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index f5aea6370..28f6bdcff 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -468,10 +468,10 @@ namespace storm { if (bitIndexInBucket < 62) { // bitIndexInBucket + 2 < 64 // If the value stops before the end of the bucket, we need to erase some lower bits. mask &= ~((1ull << (62 - (bitIndexInBucket))) - 1ull); - return (bucketVector[bucket] & mask) >> (62 - bitIndexInBucket); + return (buckets[bucket] & mask) >> (62 - bitIndexInBucket); } else { // In this case, it suffices to take the current mask. - return bucketVector[bucket] & mask; + return buckets[bucket] & mask; } } @@ -669,29 +669,29 @@ namespace storm { storm::storage::BitVector result(length, false); uint_fast64_t offset = start % 64; - uint_fast64_t bucketIndex = start / 64; - uint_fast64_t insertBucket = 0; + uint64_t* getBucket = buckets + (start / 64); + uint64_t* insertBucket = result.buckets; uint_fast64_t getValue; uint_fast64_t writeValue = 0; uint_fast64_t noBits = 0; if (offset == 0) { // Copy complete buckets - for ( ; noBits + 64 <= length; ++bucketIndex, ++insertBucket, noBits += 64) { - result.bucketVector[insertBucket] = bucketVector[bucketIndex]; + for ( ; noBits + 64 <= length; ++getBucket, ++insertBucket, noBits += 64) { + *insertBucket = *getBucket; } } else { //Get first bits up until next bucket - getValue = bucketVector[bucketIndex]; + getValue = *getBucket; writeValue = (getValue << offset); noBits += (64-offset); - ++bucketIndex; + ++getBucket; //Get complete buckets - for ( ; noBits + 64 <= length; ++bucketIndex, ++insertBucket, noBits += 64) { - getValue = bucketVector[bucketIndex]; + for ( ; noBits + 64 <= length; ++getBucket, ++insertBucket, noBits += 64) { + getValue = *getBucket; // Get bits till write bucket is full writeValue |= (getValue >> (64-offset)); - result.bucketVector[insertBucket] = writeValue; + *insertBucket = writeValue; // Get bits up until next bucket writeValue = (getValue << offset); } @@ -699,22 +699,23 @@ namespace storm { // Write last bits uint_fast64_t remainingBits = length - noBits; - assert(bucketIndex < bucketCount()); + assert(getBucket != buckets + bucketCount()); // Get remaining bits - getValue = (bucketVector[bucketIndex] >> (64-remainingBits)) << (64-remainingBits); + getValue = (*getBucket >> (64-remainingBits)) << (64-remainingBits); assert(remainingBits < 64); // Write bucket - assert(insertBucket < result.bucketCount()); + assert(insertBucket != result.buckets + result.bucketCount()); if (offset == 0) { - result.bucketVector[insertBucket]= getValue; + *insertBucket = getValue; } else { writeValue |= getValue >> (64-offset); - result.bucketVector[insertBucket] = writeValue; + *insertBucket = writeValue; if (remainingBits > offset) { // Write last bits in new value writeValue = (getValue << offset); - assert(insertBucket+1 < result.bucketCount()); - result.bucketVector[++insertBucket] = writeValue; + ++insertBucket; + assert(insertBucket != result.buckets + result.bucketCount()); + *insertBucket = writeValue; } } @@ -752,56 +753,58 @@ namespace storm { assert(start + other.bitCount <= bitCount); uint_fast64_t offset = start % 64; - uint_fast64_t bucketIndex = start / 64; - uint_fast64_t getBucket = 0; + uint64_t* insertBucket = buckets + (start / 64); + uint64_t* getBucket = other.buckets; uint_fast64_t getValue; uint_fast64_t writeValue = 0; uint_fast64_t noBits = 0; if (offset == 0) { // Copy complete buckets - for ( ; noBits + 64 <= other.bitCount; ++bucketIndex, ++getBucket, noBits += 64) { - bucketVector[bucketIndex] = other.bucketVector[getBucket]; + for ( ; noBits + 64 <= other.bitCount; ++insertBucket, ++getBucket, noBits += 64) { + *insertBucket = *getBucket; } } else { //Get first bits up until next bucket - getValue = other.bucketVector[getBucket]; - writeValue = (bucketVector[bucketIndex] >> (64-offset)) << (64-offset); + getValue = *getBucket; + writeValue = (*insertBucket >> (64-offset)) << (64-offset); writeValue |= (getValue >> offset); - bucketVector[bucketIndex] = writeValue; + *insertBucket = writeValue; noBits += (64-offset); - ++bucketIndex; + ++insertBucket; //Get complete buckets - for ( ; noBits + 64 <= other.bitCount; ++bucketIndex, noBits += 64) { + for ( ; noBits + 64 <= other.bitCount; ++insertBucket, noBits += 64) { // Get all remaining bits from other bucket writeValue = getValue << (64-offset); // Get bits from next bucket - getValue = other.bucketVector[++getBucket]; + ++getBucket; + getValue = *getBucket; writeValue |= getValue >> offset; - bucketVector[bucketIndex] = writeValue; + *insertBucket = writeValue; } } // Write last bits uint_fast64_t remainingBits = other.bitCount - noBits; assert(remainingBits < 64); - assert(bucketIndex < bucketCount()); - assert(getBucket < other.bucketCount()); + assert(insertBucket != buckets + bucketCount()); + assert(getBucket != other.buckets + other.bucketCount()); // Get remaining bits of bucket - getValue = other.bucketVector[getBucket]; + getValue = *getBucket; if (offset > 0) { getValue = getValue << (64-offset); } // Get unchanged part of bucket - writeValue = (bucketVector[bucketIndex] << remainingBits) >> remainingBits; + writeValue = (*insertBucket << remainingBits) >> remainingBits; if (remainingBits > offset && offset > 0) { // Remaining bits do not come from one bucket -> consider next bucket - assert(getBucket == other.bucketCount() - 2); - getValue |= other.bucketVector[++getBucket] >> offset; + ++getBucket; + assert(getBucket != other.buckets + other.bucketCount()); + getValue |= *getBucket >> offset; } // Write completely writeValue |= getValue; - bucketVector[bucketIndex] = writeValue; + *insertBucket = writeValue; #ifdef ASSERT_BITVECTOR // Check correctness of setter @@ -919,14 +922,14 @@ namespace storm { out << "bit vector(" << getNumberOfSetBits() << "/" << bitCount << ") "; uint_fast64_t index = 0; for ( ; index * 64 + 64 <= bitCount; ++index) { - std::bitset<64> tmp(bucketVector[index]); + std::bitset<64> tmp(buckets[index]); out << tmp << "|"; } // Print last bits if (index * 64 < bitCount) { - assert(index == bucketVector.size() - 1); - std::bitset<64> tmp(bucketVector[index]); + assert(index == bucketCount() - 1); + std::bitset<64> tmp(buckets[index]); for (size_t i = 0; i + index * 64 < bitCount; ++i) { // Bits are counted from rightmost in bitset out << tmp[63-i]; diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp index 60422dc08..2e3a4e876 100644 --- a/src/storage/FlexibleSparseMatrix.cpp +++ b/src/storage/FlexibleSparseMatrix.cpp @@ -13,8 +13,8 @@ namespace storm { } template - FlexibleSparseMatrix::FlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) : data(matrix.getRowCount()), columnCount(matrix.getColumnCount()), nonzeroEntryCount(matrix.getNonzeroEntryCount()), nontrivialRowGrouping(matrix.hasNontrivialRowGrouping()) { - if (nontrivialRowGrouping) { + FlexibleSparseMatrix::FlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne) : data(matrix.getRowCount()), columnCount(matrix.getColumnCount()), nonzeroEntryCount(matrix.getNonzeroEntryCount()), trivialRowGrouping(matrix.hasTrivialRowGrouping()) { + if (!trivialRowGrouping) { rowGroupIndices = matrix.getRowGroupIndices(); } for (index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) { @@ -130,8 +130,8 @@ namespace storm { } template - bool FlexibleSparseMatrix::hasNontrivialRowGrouping() const { - return nontrivialRowGrouping; + bool FlexibleSparseMatrix::hasTrivialRowGrouping() const { + return trivialRowGrouping; } template @@ -208,7 +208,7 @@ namespace storm { } out << std::endl; - if (matrix.hasNontrivialRowGrouping()) { + if (!matrix.hasTrivialRowGrouping()) { // Iterate over all row groups FlexibleIndex rowGroupCount = matrix.getRowGroupCount(); for (FlexibleIndex rowGroup = 0; rowGroup < rowGroupCount; ++rowGroup) { diff --git a/src/storage/FlexibleSparseMatrix.h b/src/storage/FlexibleSparseMatrix.h index 28100e0a2..d5e6c2124 100644 --- a/src/storage/FlexibleSparseMatrix.h +++ b/src/storage/FlexibleSparseMatrix.h @@ -149,11 +149,11 @@ namespace storm { bool empty() const; /*! - * Retrieves whether the matrix has a (possibly) non-trivial row grouping. + * Retrieves whether the matrix has a (possibly) trivial row grouping. * - * @return True iff the matrix has a (possibly) non-trivial row grouping. + * @return True iff the matrix has a (possibly) trivial row grouping. */ - bool hasNontrivialRowGrouping() const; + bool hasTrivialRowGrouping() const; /*! * Creates a submatrix of the current matrix in place by dropping all rows and columns whose bits are not @@ -198,9 +198,9 @@ namespace storm { // The number of entries in the matrix. index_type nonzeroEntryCount; - // A flag that indicates whether the matrix has a non-trivial row-grouping, i.e. (possibly) more than one - // row per row group. - bool nontrivialRowGrouping; + // A flag indicating whether the matrix has a trivial row grouping. Note that this may be true and yet + // there may be row group indices, because they were requested from the outside. + bool trivialRowGrouping; // A vector indicating the row groups of the matrix. std::vector rowGroupIndices; diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 69f12b696..d4028b55d 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -264,9 +264,26 @@ namespace storm { // Sort columns per row typename SparseMatrix::index_type endGroups; typename SparseMatrix::index_type endRows; - for (index_type group = 0; group < rowGroupIndices.size(); ++group) { - endGroups = group < rowGroupIndices.size()-1 ? rowGroupIndices[group+1] : rowIndications.size(); - for (index_type i = rowGroupIndices[group]; i < endGroups; ++i) { + + if (hasCustomRowGrouping) { + for (index_type group = 0; group < rowGroupIndices.get().size(); ++group) { + endGroups = group < rowGroupIndices.get().size()-1 ? rowGroupIndices.get()[group+1] : rowIndications.size(); + for (index_type i = rowGroupIndices.get()[group]; i < endGroups; ++i) { + endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); + // Sort the row + std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, + [](MatrixEntry const& a, MatrixEntry const& b) { + return a.getColumn() < b.getColumn(); + }); + // Assert no equal elements + assert(std::is_sorted(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, + [](MatrixEntry const& a, MatrixEntry const& b) { + return a.getColumn() <= b.getColumn(); + })); + } + } + } else { + for (index_type i = 0; i < rowIndications.size(); ++i) { endRows = i < rowIndications.size()-1 ? rowIndications[i+1] : columnsAndValues.size(); // Sort the row std::sort(columnsAndValues.begin() + rowIndications[i], columnsAndValues.begin() + endRows, @@ -279,47 +296,10 @@ namespace storm { return a.getColumn() <= b.getColumn(); })); } + } } - - template - bool SparseMatrixBuilder::replaceColumns(std::vector const& replacements, index_type offset) { - bool matrixChanged = false; - - // Walk through all rows. - for (index_type row = 0; row < rowIndications.size(); ++row) { - bool rowChanged = false; - index_type rowEnd = row < rowIndications.size()-1 ? rowIndications[row+1] : columnsAndValues.size(); - - for (auto it = columnsAndValues.begin() + rowIndications[row], ite = columnsAndValues.begin() + rowEnd; it != ite; ++it) { - if (it->getColumn() >= offset && it->getColumn() != replacements[it->getColumn() - offset]) { - it->setColumn(replacements[it->getColumn() - offset]); - rowChanged = true; - } - // Update highest column in a way that only works if the highest appearing index does not become - // lower during performing the replacement. - highestColumn = std::max(highestColumn, it->getColumn()); - } - - if (rowChanged) { - matrixChanged = true; - - // Sort the row. - std::sort(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd, - [](MatrixEntry const& a, MatrixEntry const& b) { - return a.getColumn() < b.getColumn(); - }); - // Assert no equal elements - STORM_LOG_ASSERT(std::is_sorted(columnsAndValues.begin() + rowIndications[row], columnsAndValues.begin() + rowEnd, - [](MatrixEntry const& a, MatrixEntry const& b) { - return a.getColumn() <= b.getColumn(); - }), "Must not have different elements with the same column in a row."); - } - } - - return matrixChanged; - } - + template SparseMatrix::rows::rows(iterator begin, index_type entryCount) : beginIterator(begin), entryCount(entryCount) { // Intentionally left empty. diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index ea0da3a14..4f6c1f7e0 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -58,7 +58,7 @@ int main(int argc, char** argv) { parametric = true; } else if (option == "--expectedtime") { assert(targetFormula.empty()); - operatorType = "ET"; + operatorType = "T"; targetFormula = "F \"failed\""; allowModular = false; } else if (option == "--probability") { diff --git a/src/utility/storm.h b/src/utility/storm.h index 96087e30a..ea58705b8 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -356,10 +356,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The parametric engine currently does not support MDPs."); } else if (model->getType() == storm::models::ModelType::Ctmc) { // Hack to avoid instantiating the CTMC Model Checker which currently does not work for rational functions - if (formula->isExpectedTimeOperatorFormula()) { + if (formula->isTimeOperatorFormula()) { // Compute expected time for pCTMCs - STORM_LOG_THROW(formula->asExpectedTimeOperatorFormula().getSubformula().isReachbilityExpectedTimeFormula(), storm::exceptions::NotSupportedException, "The parametric engine only supports Eventually formulas for this property"); - storm::logic::EventuallyFormula eventuallyFormula = formula->asExpectedTimeOperatorFormula().getSubformula().asEventuallyFormula(); + STORM_LOG_THROW(formula->asTimeOperatorFormula().getSubformula().isReachabilityTimeFormula(), storm::exceptions::NotSupportedException, "The parametric engine only supports reachability formulas for this property"); + storm::logic::EventuallyFormula eventuallyFormula = formula->asTimeOperatorFormula().getSubformula().asReachabilityTimeFormula(); STORM_LOG_THROW(eventuallyFormula.getSubformula().isInFragment(storm::logic::propositional()), storm::exceptions::NotSupportedException, "The parametric engine does not support nested formulas on CTMCs"); // Compute goal states @@ -368,7 +368,7 @@ namespace storm { std::unique_ptr subResultPointer = propositionalModelchecker.check(eventuallyFormula.getSubformula()); storm::storage::BitVector const& targetStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector(); - std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeExpectedTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false); + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeReachabilityTimesElimination(ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), targetStates, false); result = std::unique_ptr(new storm::modelchecker::ExplicitQuantitativeCheckResult(std::move(numericResult))); } else if (formula->isProbabilityOperatorFormula()) {