From f049a9f0af8ced590af0906f69c4bbf8e22b3e5c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 24 Feb 2014 16:24:48 +0100 Subject: [PATCH] Bugfix for topological equation solver. Former-commit-id: b8563f8b3e03e4141096d488494889a53f2ad139 --- ...onNondeterministicLinearEquationSolver.cpp | 53 ++++++++++++------- src/utility/ErrorHandling.h | 2 +- ...ValueIterationMdpPrctlModelCheckerTest.cpp | 43 ++++++++------- 3 files changed, 57 insertions(+), 41 deletions(-) diff --git a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp index c82a40af5..2d1573f94 100644 --- a/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp +++ b/src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp @@ -56,7 +56,10 @@ namespace storm { std::cout << std::endl; } - + std::cout << A << std::endl; + std::cout << nondeterministicChoiceIndices << std::endl; + std::cout << b << std::endl; + storm::models::NonDeterministicMatrixBasedPseudoModel pseudoModel(A, nondeterministicChoiceIndices); //storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(*static_cast*>(&pseudoModel), false, false); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(pseudoModel, false, false); @@ -70,11 +73,11 @@ namespace storm { std::vector topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph); // Set up the environment for the power method. - bool multiplyResultMemoryProvided = true; - if (multiplyResult == nullptr) { - multiplyResult = new std::vector(A.getRowCount()); - multiplyResultMemoryProvided = false; - } +// bool multiplyResultMemoryProvided = true; +// if (multiplyResult == nullptr) { +// multiplyResult = new std::vector(A.getRowCount()); +// multiplyResultMemoryProvided = false; +// } std::vector* currentX = nullptr; //bool xMemoryProvided = true; //if (newX == nullptr) { @@ -104,13 +107,14 @@ namespace storm { std::cout << std::endl; // Generate a submatrix - storm::storage::BitVector subMatrixIndices(rowCount, scc.cbegin(), scc.cend()); - storm::storage::SparseMatrix sccSubmatrix = A.getSubmatrix(subMatrixIndices, nondeterministicChoiceIndices, true); + storm::storage::BitVector subMatrixIndices(A.getColumnCount(), scc.cbegin(), scc.cend()); + storm::storage::SparseMatrix sccSubmatrix = A.getSubmatrix(subMatrixIndices, nondeterministicChoiceIndices); std::vector sccSubB(sccSubmatrix.getRowCount()); storm::utility::vector::selectVectorValues(sccSubB, subMatrixIndices, nondeterministicChoiceIndices, b); std::vector sccSubX(sccSubmatrix.getColumnCount()); std::vector sccSubXSwap(sccSubmatrix.getColumnCount()); - + std::vector sccMultiplyResult(sccSubmatrix.getRowCount()); + // Prepare the pointers for swapping in the calculation currentX = &sccSubX; swap = &sccSubXSwap; @@ -119,33 +123,40 @@ namespace storm { std::vector sccSubNondeterministicChoiceIndices(sccSubmatrix.getColumnCount() + 1); sccSubNondeterministicChoiceIndices.at(0) = 0; + std::cout << "subb: " << sccSubB << std::endl; // Preprocess all dependant states // Remove outgoing transitions and create the ChoiceIndices uint_fast64_t innerIndex = 0; + uint_fast64_t outerIndex = 0; for (uint_fast64_t state: scc) { // Choice Indices - sccSubNondeterministicChoiceIndices.at(innerIndex + 1) = sccSubNondeterministicChoiceIndices.at(innerIndex) + (nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]); + sccSubNondeterministicChoiceIndices.at(outerIndex + 1) = sccSubNondeterministicChoiceIndices.at(outerIndex) + (nondeterministicChoiceIndices[state + 1] - nondeterministicChoiceIndices[state]); for (auto rowGroupIt = nondeterministicChoiceIndices[state]; rowGroupIt != nondeterministicChoiceIndices[state + 1]; ++rowGroupIt) { - storm::storage::SparseMatrix::const_rows row = A.getRow(rowGroupIt); + typename storm::storage::SparseMatrix::const_rows row = A.getRow(rowGroupIt); for (auto rowIt = row.begin(); rowIt != row.end(); ++rowIt) { if (!subMatrixIndices.get(rowIt->first)) { // This is an outgoing transition of a state in the SCC to a state not included in the SCC // Subtracting Pr(tau) * x_other from b fixes that - sccSubB.at(innerIndex) = sccSubB.at(innerIndex) - (rowIt->second * x.at(rowIt->first)); + sccSubB.at(innerIndex) = sccSubB.at(innerIndex) + (rowIt->second * x.at(rowIt->first)); } } + ++innerIndex; } - ++innerIndex; + ++outerIndex; } + + std::cout << sccSubmatrix << std::endl; + std::cout << sccSubNondeterministicChoiceIndices << std::endl; + std::cout << sccSubB << std::endl; // For the current SCC, we need to perform value iteration until convergence. localIterations = 0; converged = false; while (!converged && localIterations < this->maximalNumberOfIterations) { // Compute x' = A*x + b. - sccSubmatrix.multiplyWithVector(*currentX, *multiplyResult); - storm::utility::vector::addVectorsInPlace(*multiplyResult, sccSubB); + sccSubmatrix.multiplyWithVector(*currentX, sccMultiplyResult); + storm::utility::vector::addVectorsInPlace(sccMultiplyResult, sccSubB); //A.multiplyWithVector(scc, nondeterministicChoiceIndices, *currentX, multiplyResult); //storm::utility::addVectors(scc, nondeterministicChoiceIndices, multiplyResult, b); @@ -158,10 +169,10 @@ namespace storm { // Reduce the vector x' by applying min/max for all non-deterministic choices. if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *swap, sccSubNondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMin(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices); } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *swap, sccSubNondeterministicChoiceIndices); + storm::utility::vector::reduceVectorMax(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices); } // Determine whether the method converged. @@ -180,9 +191,11 @@ namespace storm { // The Result of this SCC has to be taken back into the main result vector innerIndex = 0; for (uint_fast64_t state: scc) { + std::cout << state << " = " << currentX->at(innerIndex) << std::endl; x.at(state) = currentX->at(innerIndex); ++innerIndex; } + std::cout << x << std::endl; // Since the pointers for swapping in the calculation point to temps they should not be valide anymore currentX = nullptr; @@ -199,9 +212,9 @@ namespace storm { // delete newX; //} - if (!multiplyResultMemoryProvided) { - delete multiplyResult; - } +// if (!multiplyResultMemoryProvided) { +// delete multiplyResult; +// } // Check if the solver converged and issue a warning otherwise. if (converged) { diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h index 0872757b6..5b9b50bdc 100644 --- a/src/utility/ErrorHandling.h +++ b/src/utility/ErrorHandling.h @@ -164,7 +164,7 @@ VOID CALLBACK stormWindowsSetTimerCallBack( void stormSetAlarm(uint_fast64_t timeoutSeconds) { #ifndef WINDOWS - alarm(timeout); + alarm(timeoutSeconds); #else // This needs more research (http://msdn.microsoft.com/en-us/library/windows/desktop/ms644906(v=vs.85).aspx) UINT_PTR retVal = SetTimer(NULL, 0, static_cast(timeoutSeconds * 1000), static_cast(&stormWindowsSetTimerCallBack)); diff --git a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp index c2956f779..41f75fd46 100644 --- a/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp @@ -8,50 +8,53 @@ #include "src/parser/AutoParser.h" TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, SmallLinEqSystem) { - storm::storage::SparseMatrixBuilder matrixBuilder(3, 3); - ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 1.0)); - ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 0, 4.0)); - ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 7.0)); - ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 1, 7.0)); - ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 2, -1.0)); + storm::storage::SparseMatrixBuilder matrixBuilder(4, 4); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 1, 0.1)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(0, 2, 0.9)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(1, 1, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(2, 3, 1.0)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 2, 0.8)); + ASSERT_NO_THROW(matrixBuilder.addNextValue(3, 3, 0.2)); storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = matrixBuilder.build()); - ASSERT_EQ(3, matrix.getRowCount()); - ASSERT_EQ(3, matrix.getColumnCount()); - ASSERT_EQ(5, matrix.getEntryCount()); + ASSERT_EQ(4, matrix.getRowCount()); + ASSERT_EQ(4, matrix.getColumnCount()); + ASSERT_EQ(6, matrix.getEntryCount()); // Solve the Linear Equation System storm::solver::TopologicalValueIterationNondeterministicLinearEquationSolver topoSolver; - std::vector x(3); - std::vector b = { 5, 8, 2 }; - std::vector choices = { 0, 1, 2, 3 }; + std::vector x(4); + std::vector b = { 1, 2, 3, 4 }; + std::vector choices = { 0, 1, 2, 3, 4 }; ASSERT_NO_THROW(topoSolver.solveEquationSystem(true, matrix, x, b, choices)); storm::settings::Settings* s = storm::settings::Settings::getInstance(); - ASSERT_LT(std::abs(x.at(0) - 0.25), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - ASSERT_LT(std::abs(x.at(1) - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); - ASSERT_LT(std::abs(x.at(2) - 5.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(x.at(0) - 2.9), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(x.at(1) - 2), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(x.at(2) - 3), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); + ASSERT_LT(std::abs(x.at(3) - 3.2), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble()); } TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - //storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.tra", STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.lab", ""); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); + //storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.tra", STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.lab", ""); ASSERT_EQ(parser.getType(), storm::models::MDP); std::shared_ptr> mdp = parser.getModel>(); - ASSERT_EQ(mdp->getNumberOfStates(), 11ull); - ASSERT_EQ(mdp->getNumberOfTransitions(), 18ull); +// ASSERT_EQ(mdp->getNumberOfStates(), 11ull); +// ASSERT_EQ(mdp->getNumberOfTransitions(), 18ull); storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker mc(*mdp); - storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("end"); +// storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("end"); + storm::property::prctl::Ap* apFormula = new storm::property::prctl::Ap("two"); storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(apFormula); storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true);