From 4ec2bc0583fe32a66fe0d2e9ded208e4c863c241 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 14 May 2018 16:42:27 +0200 Subject: [PATCH] fixed bug in jani model generation --- src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp | 11 +++++------ .../abstraction/prism/PrismMenuGameAbstractor.cpp | 9 +++------ src/storm/generator/JaniNextStateGenerator.cpp | 5 ++++- 3 files changed, 12 insertions(+), 13 deletions(-) diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 4b30c61bd..35c61caeb 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -184,21 +184,20 @@ namespace storm { initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + // Cut transition relation to the reachable states for backward search. + transitionRelation &= reachableStates; + relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { - // Cut transition relation to the reachable states for backward search. - transitionRelation &= reachableStates; - // Get the target state BDD. storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); // In the presence of target states, we keep only states that can reach the target states. reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; - // Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self- - // loops of (now) deadlock states. + // Cut the transition relation source blocks to the backward reachable states. transitionRelation &= reachableStates; - + // Include all successors of reachable states, because the backward search otherwise potentially // cuts probability 0 choices of these states. reachableStates |= reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 7908a5a5e..3490c5a45 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -182,23 +182,20 @@ namespace storm { relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) { - // Get the target state BDD. storm::dd::Bdd targetStates = reachableStates && this->getStates(this->getTargetStateExpression()); // In the presence of target states, we keep only states that can reach the target states. reachableStates = storm::utility::dd::computeBackwardsReachableStates(targetStates, reachableStates && !initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()) || initialStates; + // Cut the transition relation source blocks to the backward reachable states. + transitionRelation &= reachableStates; + // Include all successors of reachable states, because the backward search otherwise potentially // cuts probability 0 choices of these states. reachableStates = reachableStates || reachableStates.relationalProduct(transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); - // Cut the transition relation to the 'extended backward reachable states', so we have the appropriate self- - // loops of (now) deadlock states. - transitionRelation &= reachableStates; - relevantStatesWatch.stop(); - STORM_LOG_TRACE("Restricting to relevant states took " << relevantStatesWatch.getTimeInMilliseconds() << "ms."); } diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index a1a683b5b..256e3933e 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -432,6 +432,9 @@ namespace storm { // As long as there is one feasible combination of commands, keep on expanding it. bool done = false; while (!done) { + currentDistribution.clear(); + nextDistribution.clear(); + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); currentDistribution.add(state, storm::utility::one()); @@ -504,7 +507,7 @@ namespace storm { if (this->options.isExplorationChecksSet()) { // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ")."); + STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some edge (actually sum to " << probabilitySum << ")."); } // Now, check whether there is one more command combination to consider.