Merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support

Former-commit-id: 2ae1483c69 [formerly 264860a3db]
Former-commit-id: ff24a83736

src/builder/DdJaniModelBuilder.cpp

@@ -895,7 +895,6 @@ namespace storm {
                     if (action.isInputEnabled()) {
                         // If the action is input-enabled, we add self-loops to all states.
                         transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second);
-                        actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second).exportToDot("this.dot");
                     } else {
                         transitions *= action.transitions;
                     }
@@ -1107,7 +1106,8 @@ namespace storm {
                     }
                     
                     // Add the source location and the guard.
-                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
+                    storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
+                    transitions *= sourceLocationAndGuard;
                     
                     // If we multiply the ranges of global variables, make sure everything stays within its bounds.
                     if (!globalVariablesInSomeDestination.empty()) {
@@ -1124,7 +1124,9 @@ namespace storm {
                     // Finally treat the transient assignments.
                     std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
                     if (!this->transientVariables.empty()) {
-                        performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = guard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } );
+                        performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) {
+                            transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
+                        } );
                     }
                     
                     return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);

src/generator/VariableInformation.cpp

@@ -63,26 +63,33 @@ namespace storm {
             }
             
             for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
+                if (!variable.isTransient()) {
                     booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true);
                     ++totalBitOffset;
                 }
+            }
             for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) {
+                if (!variable.isTransient()) {
                     int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
                     int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
                     uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
                     integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
                     totalBitOffset += bitwidth;
                 }
+            }
             for (auto const& automaton : model.getAutomata()) {
                 uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
                 locationVariables.emplace_back(model.getManager().declareFreshIntegerVariable(false, "loc"), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
                 totalBitOffset += bitwidth;
                 
                 for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
+                    if (!variable.isTransient()) {
                         booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
                         ++totalBitOffset;
                     }
+                }
                 for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                    if (!variable.isTransient()) {
                         int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
                         int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
                         uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
@@ -90,6 +97,7 @@ namespace storm {
                         totalBitOffset += bitwidth;
                     }
                 }
+            }
             
             sortVariables();
         }

src/storage/prism/Module.cpp

@@ -196,12 +196,12 @@ namespace storm {
         
         bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
             for (auto const& booleanVariable : this->getBooleanVariables()) {
-                if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
             }
             for (auto const& integerVariable : this->getIntegerVariables()) {
-                if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
+                if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
                     return false;
                 }
                 if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {