From 577e48f8bf43a58d1276d23729d7b1d88f7cefd3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 3 Aug 2014 22:50:51 +0200 Subject: [PATCH] Bugfix for the dimensions of some data of parsed Markov automata. Former-commit-id: ab11be9ec4c8eeb013e401bd48c3bd24568a225b --- src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h | 6 +++--- src/models/MarkovAutomaton.h | 2 +- src/parser/MarkovAutomatonSparseTransitionParser.cpp | 3 --- 3 files changed, 4 insertions(+), 7 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index dbcf4d8b1..e634ad597 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -302,8 +302,8 @@ namespace storm { // Finally, we are ready to create the SSP matrix and right-hand side of the SSP. std::vector b; - typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, true, numberOfStatesNotInMecs + mecDecomposition.size() + 1); - + typename storm::storage::SparseMatrixBuilder sspMatrixBuilder(0, 0, 0, true, numberOfStatesNotInMecs + mecDecomposition.size()); + // If the source state is not contained in any MEC, we copy its choices (and perform the necessary modifications). uint_fast64_t currentChoice = 0; for (auto state : statesNotContainedInAnyMec) { @@ -385,7 +385,7 @@ namespace storm { } // Finalize the matrix and solve the corresponding system of equations. - storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice + 1); + storm::storage::SparseMatrix sspMatrix = sspMatrixBuilder.build(currentChoice); std::vector x(numberOfStatesNotInMecs + mecDecomposition.size()); nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b); diff --git a/src/models/MarkovAutomaton.h b/src/models/MarkovAutomaton.h index 89ce7ccee..387590df6 100644 --- a/src/models/MarkovAutomaton.h +++ b/src/models/MarkovAutomaton.h @@ -126,7 +126,7 @@ namespace storm { //uint_fast64_t newNumberOfRows = this->getNumberOfChoices() - numberOfHybridStates; // Create the matrix for the new transition relation and the corresponding nondeterministic choice vector. - storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates() + 1); + storm::storage::SparseMatrixBuilder newTransitionMatrixBuilder(0, 0, 0, true, this->getNumberOfStates()); // Now copy over all choices that need to be kept. uint_fast64_t currentChoice = 0; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 21403c3be..6e02df99d 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -257,9 +257,6 @@ namespace storm { ++currentChoice; } - // Put a sentinel element at the end. - result.transitionMatrixBuilder.newRowGroup(currentChoice); - return result; }