adapted relevant parts to new way of specifying initial values/restrictions

Former-commit-id: a55abbe3b6 [formerly 6a9d8a6a55]
Former-commit-id: 47799adaf2

src/parser/JaniParser.cpp

@@ -587,7 +587,7 @@ namespace storm {
             if(automatonStructure.count("restrict-initial") > 0) {
                 initialValueRestriction  = parseExpression(automatonStructure.at("restrict-initial"), "Initial value restriction for automaton " + name);
             }
-            automaton.setInitialStatesExpression(initialValueRestriction);
+            automaton.setInitialStatesRestriction(initialValueRestriction);
             uint64_t varDeclCount = automatonStructure.count("variables");
             STORM_LOG_THROW(varDeclCount < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has more than one list of variables");
             std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> localVars;

src/storage/jani/Automaton.cpp

@@ -305,16 +305,39 @@ namespace storm {
             return edges.size();
         }
 
-        bool Automaton::hasInitialStatesExpression() const {
+        bool Automaton::hasInitialStatesRestriction() const {
-            return initialStatesExpression.isInitialized();
+            return initialStatesRestriction.isInitialized();
         }
         
-        storm::expressions::Expression const& Automaton::getInitialStatesExpression() const {
+        storm::expressions::Expression const& Automaton::getInitialStatesRestriction() const {
-            return initialStatesExpression;
+            return initialStatesRestriction;
         }
         
-        void Automaton::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
+        void Automaton::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
-            this->initialStatesExpression = initialStatesExpression;
+            this->initialStatesRestriction = initialStatesRestriction;
+        }
+        
+        storm::expressions::Expression Automaton::getInitialStatesExpression() const {
+            storm::expressions::Expression result;
+            
+            // Add initial state restriction if there is one.
+            if (this->hasInitialStatesRestriction()) {
+                result = this->getInitialStatesRestriction();
+            }
+            
+            // Add the expressions for all variables that have initial expressions.
+            for (auto const& variable : this->getVariables()) {
+                if (variable.hasInitExpression()) {
+                    storm::expressions::Expression newInitExpression = variable.isBooleanVariable() ? storm::expressions::iff(variable.getExpressionVariable(), variable.getInitExpression()) : variable.getExpressionVariable() == variable.getInitExpression();
+                    if (result.isInitialized()) {
+                        result = result && newInitExpression;
+                    } else {
+                        result = newInitExpression;
+                    }
+                }
+            }
+            
+            return result;
         }
         
         bool Automaton::hasEdgeLabeledWithActionIndex(uint64_t actionIndex) const {

src/storage/jani/Automaton.h

@@ -232,21 +232,26 @@ namespace storm {
              * Retrieves the number of edges.
              */
             uint64_t getNumberOfEdges() const;
-
+            
             /*!
-             * Retrieves whether there is an expression defining the legal initial values of the automaton's variables.
+             * Retrieves whether this automaton has an initial states restriction.
              */
-            bool hasInitialStatesExpression() const;
+            bool hasInitialStatesRestriction() const;
             
             /*!
-             * Retrieves the expression defining the legal initial values of the automaton's variables.
+             * Gets the expression restricting the legal initial values of the automaton's variables.
              */
-            storm::expressions::Expression const& getInitialStatesExpression() const;
+            storm::expressions::Expression const& getInitialStatesRestriction() const;
             
             /*!
-             * Sets the expression defining the legal initial values of the automaton's variables.
+             * Sets the expression restricting the legal initial values of the automaton's variables.
+             */
+            void setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction);
+            
+            /*!
+             * Retrieves the expression defining the legal initial values of the automaton's variables.
              */
-            void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
+            storm::expressions::Expression getInitialStatesExpression() const;
             
             /*!
              * Retrieves whether there is an edge labeled with the action with the given index in this automaton.
@@ -287,8 +292,8 @@ namespace storm {
             /// The indices of the initial locations.
             std::set<uint64_t> initialLocationIndices;
             
-            /// The expression characterizing the legal initial values of the variables of the automaton.
+            /// The expression restricting the legal initial values of the variables of the automaton.
-            storm::expressions::Expression initialStatesExpression;
+            storm::expressions::Expression initialStatesRestriction;
             
             /// The set of action indices that label some action in this automaton.
             std::set<uint64_t> actionIndices;

src/storage/jani/Exporter.cpp

@@ -355,7 +355,7 @@ namespace storm {
             appendIndent(out, indent + 1);
             out << "]";
             clearLine(out);
-            if (automaton.hasInitialStatesExpression()) {
+            if (automaton.hasInitialStatesRestriction()) {
                 appendIndent(out, indent + 1);
                 appendField(out, "initial-states");
                 clearLine(out);
@@ -413,21 +413,19 @@ namespace storm {
             appendVariables(out, model.getGlobalVariables(), 1);
             clearLine(out);
             
-            if (model.hasInitialStatesExpression()) {
+            appendIndent(out, 1);
-                appendIndent(out, 1);
+            appendField(out, "initial-states");
-                appendField(out, "initial-states");
+            clearLine(out);
-                clearLine(out);
+            appendIndent(out, 2);
-                appendIndent(out, 2);
+            out << "{";
-                out << "{";
+            clearLine(out);
-                clearLine(out);
+            appendIndent(out, 3);
-                appendIndent(out, 3);
+            appendField(out, "exp");
-                appendField(out, "exp");
+            appendValue(out, expressionToString(model.getInitialStatesRestriction()));
-                appendValue(out, expressionToString(model.getInitialStatesExpression()));
+            clearLine(out);
-                clearLine(out);
+            appendIndent(out, 2);
-                appendIndent(out, 2);
+            out << "}";
-                out << "}";
+            clearLine(out);
-                clearLine(out);
-            }
             
             appendAutomata(out, model, 1);
             clearLine(out);

src/storage/jani/Model.cpp

@@ -27,6 +27,9 @@ namespace storm {
                 this->expressionManager = std::make_shared<storm::expressions::ExpressionManager>();
             }
             
+            // Create an initial restriction.
+            initialStatesRestriction = this->expressionManager->boolean(true);
+            
             // Add a prefined action that represents the silent action.
             silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME));
         }
@@ -301,25 +304,23 @@ namespace storm {
             
             // Substitute constants in all global variables.
             for (auto& variable : result.getGlobalVariables().getBoundedIntegerVariables()) {
+                variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
                 variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
                 variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
             }
             
             // Substitute constants in initial states expression.
-            if (this->hasInitialStatesExpression()) {
+            result.setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(constantSubstitution));
-                result.setInitialStatesExpression(this->getInitialStatesExpression().substitute(constantSubstitution));
-            }
             
             // Substitute constants in variables of automata and their edges.
             for (auto& automaton : result.getAutomata()) {
                 for (auto& variable : automaton.getVariables().getBoundedIntegerVariables()) {
+                    variable.setInitExpression(variable.getInitExpression().substitute(constantSubstitution));
                     variable.setLowerBound(variable.getLowerBound().substitute(constantSubstitution));
                     variable.setUpperBound(variable.getUpperBound().substitute(constantSubstitution));
                 }
                 
-                if (automaton.hasInitialStatesExpression()) {
+                automaton.setInitialStatesRestriction(automaton.getInitialStatesExpression().substitute(constantSubstitution));
-                    automaton.setInitialStatesExpression(automaton.getInitialStatesExpression().substitute(constantSubstitution));
-                }
                 
                 for (auto& edge : automaton.getEdges()) {
                     edge.setGuard(edge.getGuard().substitute(constantSubstitution));
@@ -350,28 +351,39 @@ namespace storm {
             return result;
         }
         
-        bool Model::hasInitialStatesExpression() const {
+        void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
-            return initialStatesExpression.isInitialized();
+            this->initialStatesRestriction = initialStatesRestriction;
         }
-     
+        storm::expressions::Expression const& Model::getInitialStatesRestriction() const {
+            return initialStatesRestriction;
+        }
+        
         storm::expressions::Expression Model::getInitialStatesExpression(bool includeAutomataInitialStatesExpressions) const {
-            STORM_LOG_THROW(globalVariables.empty() || this->hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve global initial states expression, because there is none.");
+            // Start with the restriction of variables.
-            storm::expressions::Expression result = this->hasInitialStatesExpression() ? initialStatesExpression : expressionManager->boolean(true);
+            storm::expressions::Expression result = initialStatesRestriction;
+            
+            // Then add initial values for those variables that have one.
+            for (auto const& variable : globalVariables) {
+                if (variable.hasInitExpression()) {
+                    result = result && (variable.isBooleanVariable() ? storm::expressions::iff(variable.getExpressionVariable(), variable.getInitExpression()) : variable.getExpressionVariable() == variable.getInitExpression());
+                }
+            }
+            
+            // If we are to include the expressions for the automata, do so now.
             if (includeAutomataInitialStatesExpressions) {
                 for (auto const& automaton : automata) {
-                    STORM_LOG_THROW(automaton.getVariables().empty() || automaton.hasInitialStatesExpression(), storm::exceptions::InvalidOperationException, "Cannot retrieve initial states expression from automaton '" << automaton.getName() << "', because there is none.");
                     if (!automaton.getVariables().empty()) {
-                        result = result && automaton.getInitialStatesExpression();
+                        storm::expressions::Expression automatonInitialStatesExpression = automaton.getInitialStatesExpression();
+                        if (automatonInitialStatesExpression.isInitialized() && !automatonInitialStatesExpression.isTrue()) {
+                            result = result && automatonInitialStatesExpression;
+                        }
                     }
                 }
             }
             return result;
         }
         
-        void Model::setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression) {
-            this->initialStatesExpression = initialStatesExpression;
-        }
-        
         bool Model::isDeterministicModel() const {
             return this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::CTMC;
         }

src/storage/jani/Model.h

@@ -236,9 +236,19 @@ namespace storm {
             std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
             
             /*!
-             * Retrieves whether there is an expression defining the legal initial values of the global variables.
+             * Retrieves whether there is an expression restricting the legal initial values of the global variables.
              */
-            bool hasInitialStatesExpression() const;
+            bool hasInitialStatesRestriction() const;
+            
+            /*!
+             * Sets the expression restricting the legal initial values of the global variables.
+             */
+            void setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction);
+
+            /*!
+             * Gets the expression restricting the legal initial values of the global variables.
+             */
+            storm::expressions::Expression const& getInitialStatesRestriction() const;
             
             /*!
              * Retrieves the expression defining the legal initial values of the variables.
@@ -248,11 +258,6 @@ namespace storm {
              */
             storm::expressions::Expression getInitialStatesExpression(bool includeAutomataInitialStatesExpressions = false) const;
             
-            /*!
-             * Sets the expression defining the legal initial values of the global variables.
-             */
-            void setInitialStatesExpression(storm::expressions::Expression const& initialStatesExpression);
-            
             /*!
              * Determines whether this model is a deterministic one in the sense that each state only has one choice.
              */
@@ -329,8 +334,8 @@ namespace storm {
             /// An expression describing how the system is composed of the automata.
             std::shared_ptr<Composition> composition;
             
-            // The expression characterizing the legal initial values of the global variables.
+            // The expression restricting the legal initial values of the global variables.
-            storm::expressions::Expression initialStatesExpression;
+            storm::expressions::Expression initialStatesRestriction;
         };
     }
 }

src/storage/jani/Variable.cpp

@@ -48,6 +48,10 @@ namespace storm {
             return this->init.get();
         }
         
+        void Variable::setInitExpression(storm::expressions::Expression const& initialExpression) {
+            this->init = initialExpression;
+        }
+        
         BooleanVariable& Variable::asBooleanVariable() {
             return dynamic_cast<BooleanVariable&>(*this);
         }

src/storage/jani/Variable.h

@@ -49,6 +49,11 @@ namespace storm {
              */
             storm::expressions::Expression const& getInitExpression() const;
             
+            /*!
+             * Sets the initial expression for this variable.
+             */
+            void setInitExpression(storm::expressions::Expression const& initialExpression);
+            
             // Methods to determine the type of the variable.
             virtual bool isBooleanVariable() const;
             virtual bool isBoundedIntegerVariable() const;

src/storage/prism/Program.cpp

@@ -1527,7 +1527,6 @@ namespace storm {
                 default: modelType = storm::jani::ModelType::UNDEFINED;
             }
             storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager);
-            storm::expressions::Expression globalInitialStatesExpression;
 
             // Add all constants of the PRISM program to the JANI model.
             for (auto const& constant : constants) {
@@ -1540,16 +1539,12 @@ namespace storm {
             
             // Add all global variables of the PRISM program to the JANI model.
             for (auto const& variable : globalIntegerVariables) {
-                storm::jani::BoundedIntegerVariable const& newVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
+                storm::jani::BoundedIntegerVariable const& newVariable = janiModel.addBoundedIntegerVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression()));
                 variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
-                storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
-                globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
             }
             for (auto const& variable : globalBooleanVariables) {
-                storm::jani::BooleanVariable const& newVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable()));
+                storm::jani::BooleanVariable const& newVariable = janiModel.addBooleanVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression()));
                 variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
-                storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
-                globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
             }
             
             // Add all actions of the PRISM program to the JANI model.
@@ -1589,45 +1584,34 @@ namespace storm {
             // previously built mapping to make variables global that are read by more than one module.
             for (auto const& module : modules) {
                 storm::jani::Automaton automaton(module.getName());
-                storm::expressions::Expression initialStatesExpression;
 
                 for (auto const& variable : module.getIntegerVariables()) {
-                    storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
+                    storm::jani::BoundedIntegerVariable newIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
                     std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
                     // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
                     if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
                         storm::jani::BoundedIntegerVariable const& newVariable = automaton.addBoundedIntegerVariable(newIntegerVariable);
                         variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
-                        storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
-                        initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
                     } else if (!accessingModuleIndices.empty()) {
                         // Otherwise, we need to make it global.
                         storm::jani::BoundedIntegerVariable const& newVariable = janiModel.addBoundedIntegerVariable(newIntegerVariable);
                         variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
-                        storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression();
-                        globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
                     }
                 }
                 for (auto const& variable : module.getBooleanVariables()) {
-                    storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable());
+                    storm::jani::BooleanVariable newBooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression());
                     std::set<uint_fast64_t> const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()];
                     // If there is exactly one module reading and writing the variable, we can make the variable local to this module.
                     if (!allVariablesGlobal && accessingModuleIndices.size() == 1) {
                         storm::jani::BooleanVariable const& newVariable = automaton.addBooleanVariable(newBooleanVariable);
                         variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
-                        storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
-                        initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression;
                     } else if (!accessingModuleIndices.empty()) {
                         // Otherwise, we need to make it global.
                         storm::jani::BooleanVariable const& newVariable = janiModel.addBooleanVariable(newBooleanVariable);
                         variableToVariableMap.emplace(variable.getExpressionVariable(), newVariable);
-                        storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression());
-                        globalInitialStatesExpression = globalInitialStatesExpression.isInitialized() ? globalInitialStatesExpression && variableInitialExpression : variableInitialExpression;
                     }
                 }
-                
+                automaton.setInitialStatesRestriction(manager->boolean(true));
-                // Set the proper expression characterizing the initial values of the automaton's variables.
-                automaton.setInitialStatesExpression(initialStatesExpression);
                 
                 // Create a single location that will have all the edges.
                 uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l"));
@@ -1663,9 +1647,7 @@ namespace storm {
                 
                 janiModel.addAutomaton(automaton);
             }
-            
+            janiModel.setInitialStatesRestriction(manager->boolean(true));
-            // Set the proper expression characterizing the initial values of the global variables.
-            janiModel.setInitialStatesExpression(globalInitialStatesExpression);
             
             // Set the standard system composition. This is possible, because we reject non-standard compositions anyway.
             if (this->specifiesSystemComposition()) {