fixed bug in jani model generation

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -184,21 +184,20 @@ namespace storm {
                 initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
                 storm::dd::Bdd<DdType> 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<DdType> 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());

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<DdType> 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.");
                 }
                 

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<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
                 
                 currentDistribution.add(state, storm::utility::one<ValueType>());
@@ -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.