diff --git a/src/storm/modelchecker/exploration/Bounds.cpp b/src/storm/modelchecker/exploration/Bounds.cpp index a3600707d..55ed075a9 100644 --- a/src/storm/modelchecker/exploration/Bounds.cpp +++ b/src/storm/modelchecker/exploration/Bounds.cpp @@ -98,13 +98,11 @@ namespace storm { template void Bounds::setUpperBoundForState(StateType const& state, ExplorationInformation const& explorationInformation, ValueType const& value) { - std::cout << "setting value " << value << " for state " << state << " with row group " << explorationInformation.getRowGroup(state) << std::endl; setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value); } template void Bounds::setUpperBoundForRowGroup(StateType const& group, ValueType const& value) { - std::cout << "setting value " << value << " for state (row group) " << group << " where size is " << boundsPerState.size() << std::endl; boundsPerState[group].second = value; } diff --git a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp index c5cd4ba6a..e13192034 100644 --- a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -440,8 +440,9 @@ namespace storm { // duplicate work is the following. Optimally, we would only do the MEC decomposition, because we need // it anyway. However, when only detecting (accepting) MECs, we do not infer which of the other states // (not contained in MECs) also have probability 0/1. - statesWithProbability0 = storm::utility::graph::performProb0A(transposedMatrix, allStates, targetStates); targetStates.set(sink, true); + statesWithProbability0 = storm::utility::graph::performProb0A(transposedMatrix, allStates, targetStates); + targetStates.set(sink, false); statesWithProbability1 = storm::utility::graph::performProb1E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); storm::storage::MaximalEndComponentDecomposition mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true)); @@ -449,7 +450,8 @@ namespace storm { STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s)."); // If the decomposition contains only the MEC consisting of the sink state, we count it as 'failed'. - if (mecDecomposition.size() > 1) { + STORM_LOG_ASSERT(mecDecomposition.size() > 0, "Expected at least one MEC (the trivial sink MEC)."); + if (mecDecomposition.size() == 1) { ++stats.failedEcDetections; } else { stats.totalNumberOfEcDetected += mecDecomposition.size() - 1; @@ -476,16 +478,14 @@ namespace storm { } // Set the bounds of the identified states. - std::cout << "prob0: " << statesWithProbability0 << std::endl; + STORM_LOG_ASSERT((statesWithProbability0 & statesWithProbability1).empty(), "States with probability 0 and 1 overlap."); for (auto state : statesWithProbability0) { // Skip the sink state as it is not contained in the original system. if (state == sink) { continue; } - std::cout << "setting 0 for state " << state << std::endl; StateType originalState = relevantStates[state]; - std::cout << "original state is " << originalState << ", size: " << relevantStates.size() << std::endl; bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero()); explorationInformation.addTerminalState(originalState); } diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp index 7503584c8..d1eec14cb 100644 --- a/src/storm/solver/GmmxxLinearEquationSolver.cpp +++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp @@ -224,10 +224,11 @@ namespace storm { template void GmmxxLinearEquationSolver::multiply(std::vector& x, std::vector const* b, std::vector& result) const { - if(!gmmxxA) { + if (!gmmxxA) { gmmxxA = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(*A); } if (b) { + std::cout << "A: " << A->getRowCount() << "x" << A->getColumnCount() << ", x: " << x.size() << ", b: " << b->size() << ", r: " << result.size() << std::endl; gmm::mult_add(*gmmxxA, x, *b, result); } else { gmm::mult(*gmmxxA, x, result); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 38c43f6cf..aa7ec3087 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -210,10 +210,19 @@ namespace storm { bool hasEntries = currentEntryCount != 0; uint_fast64_t rowCount = hasEntries ? lastRow + 1 : 0; + + // If the last row group was empty, we need to add one more to the row count, because otherwise this empty row is not counted. + if (hasCustomRowGrouping) { + if (lastRow < rowGroupIndices->back()) { + ++rowCount; + } + } + if (initialRowCountSet && forceInitialDimensions) { STORM_LOG_THROW(rowCount <= initialRowCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowCount << " rows, but got " << rowCount << "."); rowCount = std::max(rowCount, initialRowCount); } + rowCount = std::max(rowCount, overriddenRowCount); // If the current row count was overridden, we may need to add empty rows. diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index bd8c1bad1..6a613dd3d 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -293,6 +293,9 @@ namespace storm { // Stores the currently active row group. This is used for correctly constructing the row grouping of the // matrix. index_type currentRowGroup; + + // A flag that stores whether the current row group does not yet contain an element. + bool currentRowGroupEmpty; }; /*!