fixed a bug related to closing symbolic Markov automata

src/storm/builder/DdJaniModelBuilder.cpp

@@ -1667,7 +1667,7 @@ namespace storm {
                         
                         result += extendedTransitions;
                     }
-                                        
+                    
                     return ComposerResult<Type, ValueType>(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<Type, ValueType> 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<Type, ValueType> composer(preparedModel, actionInformation, variables, rewardVariables);
             ComposerResult<Type, ValueType> 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<Type> terminalStates = postprocessSystem(preparedModel, system, variables, options);
             

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<ValueType>();
 
@@ -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));
 

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<ValueType>()).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<ValueType>());
@@ -105,7 +105,7 @@ namespace storm {
             template<storm::dd::DdType Type, typename ValueType>
             MarkovAutomaton<Type, ValueType> MarkovAutomaton<Type, ValueType>::close() {
                 // Create the new transition matrix by deleting all Markovian transitions from probabilistic states.
-                storm::dd::Add<Type, ValueType> newTransitionMatrix = this->probabilisticStates.ite(this->getTransitionMatrix() * (!this->getMarkovianMarker()).template toAdd<ValueType>(), this->getTransitionMatrix());
+                storm::dd::Add<Type, ValueType> newTransitionMatrix = this->probabilisticStates.ite(this->getTransitionMatrix() * (!this->getMarkovianMarker()).template toAdd<ValueType>(), this->getTransitionMatrix() * this->getExitRateVector());
                 
                 return MarkovAutomaton<Type, ValueType>(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());
             }

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@@ -913,7 +913,7 @@ namespace storm {
                     boost::optional<storm::storage::BitVector> markovianStates = sparseExtractor.extractSetExists(markovAutomaton.getMarkovianStates());
                     storm::storage::sparse::ModelComponents<ExportValueType> modelComponents(std::move(quotientTransitionMatrix), std::move(quotientStateLabeling), std::move(quotientRewardModels), false, std::move(markovianStates));
                     modelComponents.exitRates = sparseExtractor.extractStateVector(markovAutomaton.getExitRateVector());
-                    
+                                        
                     result = std::make_shared<storm::models::sparse::MarkovAutomaton<ExportValueType>>(std::move(modelComponents));
                 }