diff --git a/resources/examples/testfiles/dtmc/die.pm b/resources/examples/testfiles/dtmc/die.pm index 5b7eb8e36..e41139001 100644 --- a/resources/examples/testfiles/dtmc/die.pm +++ b/resources/examples/testfiles/dtmc/die.pm @@ -24,3 +24,6 @@ rewards "coin_flips" endrewards label "one" = s=7&d=1; +label "two" = s=7&d=2; +label "three" = s=7&d=3; +label "done" = s=7; diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 9de544e7b..665190e6c 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -306,7 +306,7 @@ namespace storm { // initialize the model components with the obtained information. storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); - + // Now finalize all reward models. for (auto& rewardModelBuilder : rewardModelBuilders) { modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 6b80e8c52..bf9d73876 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -216,7 +216,6 @@ namespace storm { for (auto& choice : allLabeledChoices) { allChoices.push_back(std::move(choice)); } - std::size_t totalNumberOfChoices = allChoices.size(); // If there is not a single choice, we return immediately, because the state has no behavior (other than @@ -283,9 +282,9 @@ namespace storm { for (auto& choice : allChoices) { result.addChoice(std::move(choice)); } - + this->postprocess(result); - + return result; } @@ -394,7 +393,7 @@ namespace storm { if (!this->evaluator->asBool(command.getGuardExpression())) { continue; } - + result.push_back(Choice(command.getActionIndex(), command.isMarkovian())); Choice& choice = result.back(); diff --git a/src/storm/modelchecker/exploration/Bounds.cpp b/src/storm/modelchecker/exploration/Bounds.cpp index 55ed075a9..a3600707d 100644 --- a/src/storm/modelchecker/exploration/Bounds.cpp +++ b/src/storm/modelchecker/exploration/Bounds.cpp @@ -98,11 +98,13 @@ 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 de099d655..c5cd4ba6a 100644 --- a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -476,12 +476,25 @@ namespace storm { } // Set the bounds of the identified states. + std::cout << "prob0: " << statesWithProbability0 << std::endl; 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); } for (auto state : statesWithProbability1) { + // Skip the sink state as it is not contained in the original system. + if (state == sink) { + continue; + } + StateType originalState = relevantStates[state]; bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one()); explorationInformation.addTerminalState(originalState); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 7e239c14e..38c43f6cf 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -193,13 +193,15 @@ namespace storm { ++currentRowGroup; // Close all rows from the most recent one to the starting row. - for (index_type i = lastRow + 1; i <= startingRow; ++i) { + for (index_type i = lastRow + 1; i < startingRow; ++i) { rowIndications.push_back(currentEntryCount); } - // Reset the most recently seen row/column to allow for proper insertion of the following elements. - lastRow = startingRow; - lastColumn = 0; + if (lastRow + 1 < startingRow) { + // Reset the most recently seen row/column to allow for proper insertion of the following elements. + lastRow = startingRow - 1; + lastColumn = 0; + } } template @@ -228,7 +230,7 @@ namespace storm { // as now the indices of row i are always between rowIndications[i] and rowIndications[i + 1], also for // the first and last row. rowIndications.push_back(currentEntryCount); - assert(rowCount == rowIndications.size() - 1); + STORM_LOG_ASSERT(rowCount == rowIndications.size() - 1, "Wrong sizes of vectors."); uint_fast64_t columnCount = hasEntries ? highestColumn + 1 : 0; if (initialColumnCountSet && forceInitialDimensions) { STORM_LOG_THROW(columnCount <= initialColumnCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialColumnCount << " columns, but got " << columnCount << "."); @@ -1589,8 +1591,9 @@ namespace storm { template bool SparseMatrix::isProbabilistic() const { storm::utility::ConstantsComparator comparator; - for(index_type row = 0; row < this->rowCount; ++row) { - if(!comparator.isOne(getRowSum(row))) { + for (index_type row = 0; row < this->rowCount; ++row) { + ValueType sum = getRowSum(row); + if (!comparator.isOne(sum)) { return false; } }