From ae2b950e8627ff575725d08e866c7ba35d4c009c Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 27 Jan 2015 16:55:57 +0100 Subject: [PATCH] Fixed some issue in model builder. Former-commit-id: 12a4afd59166b77a33beb7dcaf0a0c44ab0fd597 --- src/builder/ExplicitPrismModelBuilder.cpp | 4 ++- .../SparseDtmcEliminationModelChecker.cpp | 26 +++++++++++++------ src/utility/cli.h | 4 ++- 3 files changed, 24 insertions(+), 10 deletions(-) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 6cc9b37ce..d00054963 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -156,7 +156,9 @@ namespace storm { while (assignmentIt->getVariable() != integerIt->variable) { ++integerIt; } - newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, evaluator.asInt(assignmentIt->getExpression()) - integerIt->lowerBound); + int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); + STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); + newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); } // Check that we processed all assignments. diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index fcf1067c0..7fbf70b7f 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -280,6 +280,7 @@ namespace storm { } STORM_LOG_INFO("Eliminated " << states.size() << " states." << std::endl); + // Eliminate the transitions going into the initial state. eliminateState(flexibleMatrix, oneStepProbabilities, *newInitialStates.begin(), flexibleBackwardTransitions, missingStateRewards, false); // Now eliminate all chains of phi or psi states. @@ -309,12 +310,14 @@ namespace storm { ValueType numerator = storm::utility::zero(); ValueType denominator = storm::utility::zero(); + flexibleMatrix.print(); + for (auto const& trans1 : flexibleMatrix.getRow(*newInitialStates.begin())) { auto initialStateSuccessor = trans1.getColumn(); if (phiStates.get(initialStateSuccessor)) { ValueType additiveTerm = storm::utility::zero(); for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) { - STORM_LOG_ASSERT(psiStates.get(trans2.getColumn()), "Expected psi state."); + STORM_LOG_ASSERT(psiStates.get(trans2.getColumn()), "Expected " << trans2.getColumn() << " to be a psi state."); additiveTerm += trans2.getValue(); } additiveTerm *= trans1.getValue(); @@ -325,7 +328,7 @@ namespace storm { denominator += trans1.getValue(); ValueType additiveTerm = storm::utility::zero(); for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) { - STORM_LOG_ASSERT(phiStates.get(trans2.getColumn()), "Expected phi state."); + STORM_LOG_ASSERT(phiStates.get(trans2.getColumn()), "Expected " << trans2.getColumn() << " to be a phi state."); additiveTerm += trans2.getValue(); } numerator += trans1.getValue() * additiveTerm; @@ -625,11 +628,17 @@ namespace storm { // Start by finding loop probability. typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state); - for (auto const& entry : currentStateSuccessors) { - if (entry.getColumn() >= state) { - if (entry.getColumn() == state) { - loopProbability = entry.getValue(); + for (auto entryIt = currentStateSuccessors.begin(), entryIte = currentStateSuccessors.end(); entryIt != entryIte; ++entryIt) { + if (entryIt->getColumn() >= state) { + if (entryIt->getColumn() == state) { + loopProbability = entryIt->getValue(); hasSelfLoop = true; + + // If we do not clear the forward transitions completely, we need to remove the self-loop, + // because we scale all the other outgoing transitions with it anyway.. + if (!removeForwardTransitions) { + currentStateSuccessors.erase(entryIt); + } } break; } @@ -679,6 +688,9 @@ namespace storm { typename FlexibleSparseMatrix::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry const& a) { return a.getColumn() == state; }); // Make sure we have found the probability and set it to zero. + if (multiplyElement == predecessorForwardTransitions.end()) { + + } STORM_LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found."); ValueType multiplyFactor = multiplyElement->getValue(); multiplyElement->setValue(storm::utility::zero()); @@ -739,7 +751,6 @@ namespace storm { // If we are computing rewards, we basically scale the state reward of the state to eliminate and // add the result to the state reward of the predecessor. if (hasSelfLoop) { -// stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * storm::utility::pow(loopProbability, 2) * stateRewards.get()[state]); stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * loopProbability * stateRewards.get()[state]); } else { stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * stateRewards.get()[state]); @@ -791,7 +802,6 @@ namespace storm { // Now move the new predecessors in place. successorBackwardTransitions = std::move(newPredecessors); - } STORM_LOG_DEBUG("Fixed predecessor lists of successor states."); diff --git a/src/utility/cli.h b/src/utility/cli.h index 71067daf9..985be9f87 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -57,6 +57,7 @@ log4cplus::Logger logger; // Headers for model checking. #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" // Headers for counterexample generation. @@ -340,7 +341,8 @@ namespace storm { std::unique_ptr result; if (model->getType() == storm::models::DTMC) { std::shared_ptr> dtmc = model->as>(); - storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); +// storm::modelchecker::SparseDtmcPrctlModelChecker modelchecker(*dtmc); + storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker(*dtmc); result = modelchecker.check(*formula); } else if (model->getType() == storm::models::MDP) { std::shared_ptr> mdp = model->as>();