diff --git a/src/storm/api/export.cpp b/src/storm/api/export.cpp index 193ec0668..78951fd27 100644 --- a/src/storm/api/export.cpp +++ b/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 const& properties, std::string const& filename) { auto janiSettings = storm::settings::getModule(); - + + 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); } } diff --git a/src/storm/settings/modules/JaniExportSettings.cpp b/src/storm/settings/modules/JaniExportSettings.cpp index d6275834b..a47a9914b 100644 --- a/src/storm/settings/modules/JaniExportSettings.cpp +++ b/src/storm/settings/modules/JaniExportSettings.cpp @@ -7,6 +7,8 @@ #include "storm/settings/ArgumentBuilder.h" #include "storm/settings/Argument.h" +#include + 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> JaniExportSettings::getLocationVariables() const { + std::string argument = this->getOption(locationVariablesOptionName).getArgumentByName("variables").getValueAsString(); + std::vector arguments; + boost::split( arguments, argument, boost::is_any_of(",")); + std::vector> result; + for (auto const& pair : arguments) { + std::vector 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() { } diff --git a/src/storm/settings/modules/JaniExportSettings.h b/src/storm/settings/modules/JaniExportSettings.h index fd6639869..d61b923fc 100644 --- a/src/storm/settings/modules/JaniExportSettings.h +++ b/src/storm/settings/modules/JaniExportSettings.h @@ -28,6 +28,10 @@ namespace storm { bool isExportFlattenedSet() const; + bool isLocationVariablesSet() const; + + std::vector> 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; }; } diff --git a/src/storm/storage/jani/JaniLocationExpander.cpp b/src/storm/storage/jani/JaniLocationExpander.cpp new file mode 100644 index 000000000..d955a7754 --- /dev/null +++ b/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 substitutionMap; + std::map> locationNames; + std::map> locationVariableValueMap; + for (auto const& loc : automaton.getLocations()) { + locationNames[loc.getName()] = std::vector(); + 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 templateEdge = std::make_shared(newGuard); + + STORM_LOG_THROW(edge.getAssignments().empty(), storm::exceptions::NotImplementedException, "Support for edge-assignments is not implemented"); + + std::vector> 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(edge.getRate().substitute(substitutionMap)) : boost::none, templateEdge, destinationLocationsAndProbabilities)); + + } + } + return newAutomaton; + + + } + + + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/JaniLocationExpander.h b/src/storm/storage/jani/JaniLocationExpander.h new file mode 100644 index 000000000..6b4ec0709 --- /dev/null +++ b/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); + + + + }; + } + +}