jani transformer which changes a variable into a location

src/storm/api/export.cpp

@@ -1,17 +1,27 @@
 #include "storm/api/export.h"
+#include "storm/storage/jani/JaniLocationExpander.h"
 
 namespace storm {
     namespace api {
         
         void exportJaniModel(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
             auto janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
-            
+
+            storm::jani::Model exportModel = model;
+            if (janiSettings.isLocationVariablesSet()) {
+                for(auto const& pair : janiSettings.getLocationVariables()) {
+                    storm::jani::JaniLocationExpander expander(exportModel);
+                    expander.transform(pair.first, pair.second);
+                    exportModel = expander.getResult();
+                }
+            }
+
             if (janiSettings.isExportAsStandardJaniSet()) {
-                storm::jani::Model normalisedModel = model;
+                storm::jani::Model normalisedModel = exportModel;
                 normalisedModel.makeStandardJaniCompliant();
                 storm::jani::JsonExporter::toFile(normalisedModel, properties, filename);
             } else {
-                storm::jani::JsonExporter::toFile(model, properties, filename);
+                storm::jani::JsonExporter::toFile(exportModel, properties, filename);
             }
         }
 

src/storm/settings/modules/JaniExportSettings.cpp

@@ -7,6 +7,8 @@
 #include "storm/settings/ArgumentBuilder.h"
 #include "storm/settings/Argument.h"
 
+#include <boost/algorithm/string.hpp>
+
 namespace storm {
     namespace settings {
         namespace modules {
@@ -17,12 +19,15 @@ namespace storm {
             const std::string JaniExportSettings::standardCompliantOptionName = "standard-compliant";
             const std::string JaniExportSettings::standardCompliantOptionShortName = "standard";
             const std::string JaniExportSettings::exportFlattenOptionName = "flatten";
+            const std::string JaniExportSettings::locationVariablesOptionName = "location-variables";
 
             
             JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiFileOptionName, false, "Destination for the jani model.").setShortName(janiFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list with local variables.").setDefaultValueString("").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Export in standard compliant variant.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, true, "Export in standard compliant variant.").build());
+
             }
             
             bool JaniExportSettings::isJaniFileSet() const {
@@ -40,7 +45,25 @@ namespace storm {
             bool JaniExportSettings::isExportFlattenedSet() const {
                 return this->getOption(exportFlattenOptionName).getHasOptionBeenSet();
             }
-            
+
+            bool JaniExportSettings::isLocationVariablesSet() const {
+                return this->getOption(locationVariablesOptionName).getHasOptionBeenSet();
+            }
+
+            std::vector<std::pair<std::string, std::string>> JaniExportSettings::getLocationVariables() const {
+                std::string argument = this->getOption(locationVariablesOptionName).getArgumentByName("variables").getValueAsString();
+                std::vector<std::string> arguments;
+                boost::split( arguments, argument, boost::is_any_of(","));
+                std::vector<std::pair<std::string, std::string>> result;
+                for (auto const& pair : arguments) {
+                    std::vector<std::string> keyvaluepair;
+                    boost::split( keyvaluepair, pair, boost::is_any_of("."));
+                    STORM_LOG_THROW(keyvaluepair.size() == 2, storm::exceptions::IllegalArgumentException, "Expected a name of the form AUTOMATON.VARIABLE (with no further dots) but got " << pair);
+                    result.emplace_back(keyvaluepair.at(0), keyvaluepair.at(1));
+                }
+                return result;
+            }
+
             void JaniExportSettings::finalize() {
                 
             }

src/storm/settings/modules/JaniExportSettings.h

@@ -28,6 +28,10 @@ namespace storm {
 
                 bool isExportFlattenedSet() const;
 
+                bool isLocationVariablesSet() const;
+
+                std::vector<std::pair<std::string, std::string>> getLocationVariables() const;
+
                 bool check() const override;
                 void finalize() override;
                 
@@ -39,6 +43,7 @@ namespace storm {
                 static const std::string standardCompliantOptionName;
                 static const std::string standardCompliantOptionShortName;
                 static const std::string exportFlattenOptionName;
+                static const std::string locationVariablesOptionName;
                 
             };
         }

src/storm/storage/jani/JaniLocationExpander.cpp

@@ -0,0 +1,121 @@
+#include "storm/storage/jani/JaniLocationExpander.h"
+
+#include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/IllegalArgumentException.h"
+
+
+namespace storm {
+    namespace jani {
+        JaniLocationExpander::JaniLocationExpander(Model const& origModel) : original(origModel) {
+
+        }
+
+        void JaniLocationExpander::transform(std::string const& automatonName, std::string const& variableName) {
+            STORM_LOG_THROW(original.hasAutomaton(automatonName), storm::exceptions::IllegalArgumentException, "Model has no automaton with name " << automatonName << ". ");
+            STORM_LOG_THROW(original.getAutomaton(automatonName).hasVariable(variableName), storm::exceptions::IllegalArgumentException, "Automaton " << automatonName << " has no variable with name " << variableName << ". ");
+            newModel = original;
+            newModel.replaceAutomaton(newModel.getAutomatonIndex(automatonName), transformAutomaton(original.getAutomaton(automatonName), variableName));
+        }
+
+
+        Model const& JaniLocationExpander::getResult() const {
+            return newModel;
+        }
+
+        Automaton JaniLocationExpander::transformAutomaton(Automaton const& automaton, std::string const& variableName) {
+
+            Automaton newAutomaton(automaton.getName(), automaton.getLocationExpressionVariable());
+            int64_t initialVariableValue;
+            int64_t variableLowerBound;
+            int64_t variableUpperBound;
+            storm::expressions::Variable eliminatedExpressionVariable;
+            const storm::jani::Variable* variable;
+
+            for (auto const& var : automaton.getVariables()) {
+                if (var.getName() == variableName) {
+                    // This variable will be eliminated in the new automaton.
+                    STORM_LOG_THROW(var.hasInitExpression(), storm::exceptions::IllegalArgumentException, "Variable to be eliminated has to have an initexpression.");
+                    STORM_LOG_THROW(var.isBoundedIntegerVariable(), storm::exceptions::IllegalArgumentException, "Variable to be eliminated has to be an bounded integer variable.");
+                    STORM_LOG_THROW(!var.isTransient(), storm::exceptions::IllegalArgumentException, "Cannot eliminate transient variable");
+
+                    variableUpperBound = var.asBoundedIntegerVariable().getUpperBound().evaluateAsInt();
+                    variableLowerBound  = var.asBoundedIntegerVariable().getLowerBound().evaluateAsInt();
+                    initialVariableValue = var.getInitExpression().evaluateAsInt();
+                    variable = &var;
+                    eliminatedExpressionVariable = var.getExpressionVariable();
+
+                } else {
+                    // Other variables are just copied.
+                    newAutomaton.addVariable(var);
+                }
+            }
+
+            STORM_LOG_THROW(!automaton.getInitialStatesRestriction().containsVariable({eliminatedExpressionVariable}), storm::exceptions::NotSupportedException, "Elimination of variable that occurs in the initial state restriction is not allowed");
+            newAutomaton.setInitialStatesRestriction(automaton.getInitialStatesRestriction());
+
+
+            std::map<storm::expressions::Variable, storm::expressions::Expression> substitutionMap;
+            std::map<std::string, std::vector<std::string>> locationNames;
+            std::map<uint64_t, std::map<int64_t, uint64_t>> locationVariableValueMap;
+            for (auto const& loc : automaton.getLocations()) {
+                locationNames[loc.getName()] = std::vector<std::string>();
+                uint64_t origIndex = automaton.getLocationIndex(loc.getName());
+
+                for (int64_t i = variableLowerBound; i <= variableUpperBound; i++) {
+                    std::string newLocationName = loc.getName() + "_" + variableName + "_" + std::to_string(i);
+                    substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(i);
+                    std::cout << "eliminate " << eliminatedExpressionVariable.getName() << " with " << i << std::endl;
+                    OrderedAssignments newAssignments = loc.getAssignments().clone();
+                    newAssignments.substitute(substitutionMap);
+                    std::cout << newAssignments << std::endl;
+                    uint64_t newLocationIndex = newAutomaton.addLocation(Location(newLocationName, newAssignments));
+
+                    locationVariableValueMap[origIndex][i] = newLocationIndex;
+                    locationNames[loc.getName()].push_back(newLocationName);
+                }
+            }
+
+
+
+            for (auto const& edge : automaton.getEdges()) {
+                for (auto const& newValueAndLocation : locationVariableValueMap[edge.getSourceLocationIndex()]) {
+                    substitutionMap[eliminatedExpressionVariable] = original.getExpressionManager().integer(newValueAndLocation.first);
+
+                    uint64_t newSourceIndex = newValueAndLocation.second;
+                    storm::expressions::Expression newGuard = edge.getGuard().substitute(substitutionMap).simplify();
+                    if (!newGuard.containsVariables() && !newGuard.evaluateAsBool()) {
+                        continue;
+                    }
+                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(newGuard);
+
+                    STORM_LOG_THROW(edge.getAssignments().empty(), storm::exceptions::NotImplementedException, "Support for edge-assignments is not implemented");
+
+                    std::vector<std::pair<uint64_t, storm::expressions::Expression>> destinationLocationsAndProbabilities;
+                    for (auto const& destination : edge.getDestinations()) {
+                        OrderedAssignments oa(destination.getOrderedAssignments().clone());
+                        oa.substitute(substitutionMap);
+                        int64_t value;
+                        for (auto const& assignment : oa) {
+                            if (assignment.getVariable() == *variable) {
+                                oa.remove(assignment);
+                                value = assignment.getAssignedExpression().evaluateAsInt();
+                                break;
+                            }
+                        }
+                        TemplateEdgeDestination ted(oa);
+                        templateEdge->addDestination(ted);
+                        destinationLocationsAndProbabilities.emplace_back(locationVariableValueMap[destination.getLocationIndex()][value], destination.getProbability().substitute((substitutionMap)));
+                    }
+                    newAutomaton.addEdge(storm::jani::Edge(newSourceIndex, edge.getActionIndex(), edge.hasRate() ? boost::optional<storm::expressions::Expression>(edge.getRate().substitute(substitutionMap)) : boost::none, templateEdge, destinationLocationsAndProbabilities));
+
+                }
+            }
+            return newAutomaton;
+
+
+        }
+
+
+    }
+}

src/storm/storage/jani/JaniLocationExpander.h

@@ -0,0 +1,26 @@
+#pragma once
+
+#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Automaton.h"
+
+
+namespace storm {
+    namespace jani {
+        class JaniLocationExpander {
+        public:
+            JaniLocationExpander(Model const& original);
+            void transform(std::string const& automatonName, std::string const& variableName);
+            Model const& getResult() const;
+
+        private:
+            Model const& original;
+            Model newModel;
+
+            Automaton transformAutomaton(Automaton const& automaton, std::string const& variableName);
+
+
+
+        };
+    }
+
+}