From 316412c5d316041b9df88723af431b50bc375398 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Mar 2018 10:46:06 +0100 Subject: [PATCH] fixed a bug related to closing symbolic Markov automata --- src/storm/builder/DdJaniModelBuilder.cpp | 8 ++++---- .../csl/helper/SparseMarkovAutomatonCslHelper.cpp | 2 ++ src/storm/models/symbolic/MarkovAutomaton.cpp | 4 ++-- src/storm/storage/dd/bisimulation/QuotientExtractor.cpp | 2 +- 4 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index a6620492e..507cde01a 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -1667,7 +1667,7 @@ namespace storm { result += extendedTransitions; } - + return ComposerResult(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, numberOfUsedNondeterminismVariables); } else if (modelType == storm::jani::ModelType::DTMC || modelType == storm::jani::ModelType::CTMC) { // Simply add all actions, but make sure to include the missing global variable identities. @@ -1830,7 +1830,7 @@ namespace storm { // For DTMCs, we can simply add the identity of the global module for all deadlock states. transitionMatrix += deadlockStatesAdd * globalIdentity; } else if (modelType == storm::jani::ModelType::MDP || modelType == storm::jani::ModelType::LTS || modelType == storm::jani::ModelType::MA) { - // For MDPs, however, we need to select an action associated with the self-loop, if we do not + // For nondeterministic models, however, we need to select an action associated with the self-loop, if we do not // want to attach a lot of self-loops to the deadlock states. storm::dd::Add action = encodeAction(boost::none, modelType == storm::jani::ModelType::MA ? boost::make_optional(true) : boost::none, variables); @@ -1967,10 +1967,10 @@ namespace storm { // Create a builder to compose and build the model. CombinedEdgesSystemComposer composer(preparedModel, actionInformation, variables, rewardVariables); ComposerResult system = composer.compose(); - + // Postprocess the variables in place. postprocessVariables(preparedModel.getModelType(), system, variables); - + // Postprocess the system in place and get the states that were terminal (i.e. whose transitions were cut off). storm::dd::Bdd terminalStates = postprocessSystem(preparedModel, system, variables, options); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 7bf5f10f5..164310b20 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -261,6 +261,7 @@ namespace storm { for (ValueType const& rate : exitRateVector) { lambda = std::max(rate, lambda); } + STORM_LOG_TRACE("Initial lambda is " << lambda << "."); uint64_t N; ValueType maxNorm = storm::utility::zero(); @@ -369,6 +370,7 @@ namespace storm { // (6) Double lambda. lambda *= 2; + STORM_LOG_TRACE("Increased lambda to " << lambda << ", max diff is " << maxNorm << "."); } while (maxNorm > epsilon * (1 - kappa)); diff --git a/src/storm/models/symbolic/MarkovAutomaton.cpp b/src/storm/models/symbolic/MarkovAutomaton.cpp index add866c8b..111890edd 100644 --- a/src/storm/models/symbolic/MarkovAutomaton.cpp +++ b/src/storm/models/symbolic/MarkovAutomaton.cpp @@ -66,7 +66,7 @@ namespace storm { // Compute the vector of exit rates. this->exitRateVector = (this->getTransitionMatrix() * this->markovianMarker.template toAdd()).sumAbstract(columnAndNondeterminsmVariables); - + // Modify the transition matrix so all choices are probabilistic and the Markovian choices additionally // have a rate. this->transitionMatrix = this->transitionMatrix / this->markovianChoices.ite(this->exitRateVector, this->getManager().template getAddOne()); @@ -105,7 +105,7 @@ namespace storm { template MarkovAutomaton MarkovAutomaton::close() { // Create the new transition matrix by deleting all Markovian transitions from probabilistic states. - storm::dd::Add newTransitionMatrix = this->probabilisticStates.ite(this->getTransitionMatrix() * (!this->getMarkovianMarker()).template toAdd(), this->getTransitionMatrix()); + storm::dd::Add newTransitionMatrix = this->probabilisticStates.ite(this->getTransitionMatrix() * (!this->getMarkovianMarker()).template toAdd(), this->getTransitionMatrix() * this->getExitRateVector()); return MarkovAutomaton(this->getManagerAsSharedPointer(), this->getMarkovianMarker(), this->getReachableStates(), this->getInitialStates(), this->getDeadlockStates(), newTransitionMatrix, this->getRowVariables(), this->getRowExpressionAdapter(), this->getColumnVariables(), this->getRowColumnMetaVariablePairs(), this->getNondeterminismVariables(), this->getLabelToExpressionMap(), this->getRewardModels()); } diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 25075a0e9..a4c3b014a 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -913,7 +913,7 @@ namespace storm { boost::optional markovianStates = sparseExtractor.extractSetExists(markovAutomaton.getMarkovianStates()); storm::storage::sparse::ModelComponents modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates)); modelComponents.exitRates = sparseExtractor.extractStateVector(markovAutomaton.getExitRateVector()); - + result = std::make_shared>(std::move(modelComponents)); }