started on introducing multiple initial locations in JANI models

Former-commit-id: cf009b3e14

src/builder/DdJaniModelBuilder.cpp

@@ -1654,7 +1654,11 @@ namespace storm {
         storm::dd::Bdd<Type> computeInitialStates(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) {
             storm::dd::Bdd<Type> initialStates = variables.rowExpressionAdapter->translateExpression(model.getInitialStatesExpression(true)).toBdd();
             for (auto const& automaton : model.getAutomata()) {
-                initialStates &= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, automaton.getInitialLocationIndex());
+                storm::dd::Bdd<Type> initialLocationIndices = variables.manager->getBddZero();
+                for (auto const& locationIndex : automaton.getInitialLocationIndices()) {
+                    initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, locationIndex);
+                }
+                initialStates &= initialLocationIndices;
             }
             for (auto const& metaVariable : variables.rowMetaVariables) {
                 initialStates &= variables.variableToRangeMap.at(metaVariable);

src/generator/JaniNextStateGenerator.cpp

@@ -95,6 +95,8 @@ namespace storm {
                     initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
                 }
                 
+                // FIXME: iterate through all combinations of initial locations and set them in the initial state.
+                
                 // Register initial state and return it.
                 StateType id = stateToIdCallback(initialState);
                 initialStateIndices.push_back(id);

src/storage/jani/Automaton.cpp

@@ -95,23 +95,19 @@ namespace storm {
             return locationToIndex.at(name);
         }
 
-        void Automaton::setInitialLocation(std::string const& name) {
+        void Automaton::addInitialLocation(std::string const& name) {
             auto it = locationToIndex.find(name);
             STORM_LOG_THROW(it != locationToIndex.end(), storm::exceptions::InvalidArgumentException, "Cannot make unknown location '" << name << "' the initial location.");
-            return setInitialLocation(it->second);
+            return addInitialLocation(it->second);
         }
         
-        void Automaton::setInitialLocation(uint64_t index) {
+        void Automaton::addInitialLocation(uint64_t index) {
             STORM_LOG_THROW(index < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot make location with index " << index << " initial: out of bounds.");
-            initialLocationIndex = index;
+            initialLocationIndices.insert(index);
         }
         
-        Location const& Automaton::getInitialLocation() const {
-            return locations[getInitialLocationIndex()];
-        }
-        
-        uint64_t Automaton::getInitialLocationIndex() const {
-            return initialLocationIndex;
+        std::set<uint64_t> Automaton::getInitialLocationIndices() const {
+            return initialLocationIndices;
         }
 
         Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) {

src/storage/jani/Automaton.h

@@ -141,24 +141,19 @@ namespace storm {
             uint64_t addLocation(Location const& location);
             
             /*!
-             * Uses the location with the given name as the initial location.
+             * Adds the location with the given name to the initial locations.
              */
-            void setInitialLocation(std::string const& name);
+            void addInitialLocation(std::string const& name);
 
             /*!
-             * Uses the location with the given index as the initial location.
+             * Adds the location with the given index to the initial locations.
              */
-            void setInitialLocation(uint64_t index);
+            void addInitialLocation(uint64_t index);
             
             /*!
-             * Retrieves the initial location of the automaton.
+             * Retrieves the indices of the initial locations.
              */
-            Location const& getInitialLocation() const;
-            
-            /*!
-             * Retrieves the index of the initial location.
-             */
-            uint64_t getInitialLocationIndex() const;
+            std::set<uint64_t> getInitialLocationIndices() const;
 
             /*!
              * Retrieves the edges of the location with the given name.
@@ -255,8 +250,8 @@ namespace storm {
             /// leaving location l start at index i of the edges vector.
             std::vector<uint64_t> locationToStartingIndex;
 
-            /// The index of the initial location.
-            uint64_t initialLocationIndex;
+            /// The indices of the initial locations.
+            std::set<uint64_t> initialLocationIndices;
             
             /// The expression characterizing the legal initial values of the variables of the automaton.
             storm::expressions::Expression initialStatesExpression;

src/storage/jani/Exporter.cpp

@@ -344,8 +344,16 @@ namespace storm {
             out << ",";
             clearLine(out);
             appendIndent(out, indent + 1);
-            appendField(out, "initial-location");
-            appendValue(out, std::to_string(automaton.getInitialLocationIndex()));
+            appendField(out, "initial-locations");
+            out << " [";
+            clearLine(out);
+            for (auto const& index : automaton.getInitialLocationIndices()) {
+                appendIndent(out, indent + 2);
+                appendValue(out, automaton.getLocation(index).getName());
+                clearLine(out);
+            }
+            appendIndent(out, indent + 1);
+            out << "]";
             clearLine(out);
             if (automaton.hasInitialStatesExpression()) {
                 appendIndent(out, indent + 1);

src/storage/prism/Program.cpp

@@ -1622,7 +1622,7 @@ namespace storm {
                 
                 // Create a single location that will have all the edges.
                 uint64_t onlyLocation = automaton.addLocation(storm::jani::Location("l"));
-                automaton.setInitialLocation(onlyLocation);
+                automaton.addInitialLocation(onlyLocation);
                 
                 for (auto const& command : module.getCommands()) {
                     boost::optional<storm::expressions::Expression> rateExpression;