sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Bugfix for topological equation solver. 

Former-commit-id: b8563f8b3e
tempestpy_adaptions
dehnert 11 years ago
parent
19ca7bedaa
commit
f049a9f0af
3 changed files with 57 additions and 41 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 49
      src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
  2. 2
      src/utility/ErrorHandling.h
  3. 43
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

49
src/solver/TopologicalValueIterationNondeterministicLinearEquationSolver.cpp
View File

@ -56,6 +56,9 @@ namespace storm {
std::cout << std::endl;
}
std::cout << A << std::endl;
std::cout << nondeterministicChoiceIndices << std::endl;
std::cout << b << std::endl;
storm::models::NonDeterministicMatrixBasedPseudoModel<ValueType> pseudoModel(A, nondeterministicChoiceIndices);
//storm::storage::StronglyConnectedComponentDecomposition<ValueType> sccDecomposition(*static_cast<storm::models::AbstractPseudoModel<ValueType>*>(&pseudoModel), false, false);
@ -70,11 +73,11 @@ namespace storm {
std::vector<uint_fast64_t> topologicalSort = storm::utility::graph::getTopologicalSort(stronglyConnectedComponentsDependencyGraph);
// Set up the environment for the power method.
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<ValueType>(A.getRowCount());
multiplyResultMemoryProvided = false;
}
// bool multiplyResultMemoryProvided = true;
// if (multiplyResult == nullptr) {
// multiplyResult = new std::vector<ValueType>(A.getRowCount());
// multiplyResultMemoryProvided = false;
// }
std::vector<ValueType>* currentX = nullptr;
//bool xMemoryProvided = true;
//if (newX == nullptr) {
@ -104,12 +107,13 @@ namespace storm {
std::cout << std::endl;
// Generate a submatrix
storm::storage::BitVector subMatrixIndices(rowCount, scc.cbegin(), scc.cend());
storm::storage::SparseMatrix<ValueType> sccSubmatrix = A.getSubmatrix(subMatrixIndices, nondeterministicChoiceIndices, true);
storm::storage::BitVector subMatrixIndices(A.getColumnCount(), scc.cbegin(), scc.cend());
storm::storage::SparseMatrix<ValueType> sccSubmatrix = A.getSubmatrix(subMatrixIndices, nondeterministicChoiceIndices);
std::vector<ValueType> sccSubB(sccSubmatrix.getRowCount());
storm::utility::vector::selectVectorValues<ValueType>(sccSubB, subMatrixIndices, nondeterministicChoiceIndices, b);
std::vector<ValueType> sccSubX(sccSubmatrix.getColumnCount());
std::vector<ValueType> sccSubXSwap(sccSubmatrix.getColumnCount());
std::vector<ValueType> sccMultiplyResult(sccSubmatrix.getRowCount());
// Prepare the pointers for swapping in the calculation
currentX = &sccSubX;
@ -119,33 +123,40 @@ namespace storm {
std::vector<uint_fast64_t> 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<ValueType>::const_rows row = A.getRow(rowGroupIt);
typename storm::storage::SparseMatrix<ValueType>::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<ValueType>(*multiplyResult, sccSubB);
sccSubmatrix.multiplyWithVector(*currentX, sccMultiplyResult);
storm::utility::vector::addVectorsInPlace<ValueType>(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<ValueType>(*multiplyResult, *swap, sccSubNondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMin<ValueType>(sccMultiplyResult, *swap, sccSubNondeterministicChoiceIndices);
}
else {
storm::utility::vector::reduceVectorMax<ValueType>(*multiplyResult, *swap, sccSubNondeterministicChoiceIndices);
storm::utility::vector::reduceVectorMax<ValueType>(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) {

2
src/utility/ErrorHandling.h
View File

@ -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<UINT>(timeoutSeconds * 1000), static_cast<TIMERPROC>(&stormWindowsSetTimerCallBack));

43
test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -8,50 +8,53 @@
#include "src/parser/AutoParser.h"
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, SmallLinEqSystem) {
storm::storage::SparseMatrixBuilder<double> 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<double> 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<double> 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<double> topoSolver;
std::vector<double> x(3);
std::vector<double> b = { 5, 8, 2 };
std::vector<uint_fast64_t> choices = { 0, 1, 2, 3 };
std::vector<double> x(4);
std::vector<double> b = { 1, 2, 3, 4 };
std::vector<uint_fast64_t> 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<double> 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<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.tra", STORM_CPP_BASE_PATH "/examples/mdp/scc/scc.lab", "");
storm::parser::AutoParser<double> 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<double> 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<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 11ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 18ull);
// ASSERT_EQ(mdp->getNumberOfStates(), 11ull);
// ASSERT_EQ(mdp->getNumberOfTransitions(), 18ull);
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("end");
// storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("end");
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);

Write Preview
Loading…
Cancel
Save