From 749ba87254ada79ca0b0f9397dddf3e2db93bea8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 2 Jul 2018 10:57:13 +0200 Subject: [PATCH 1/6] Made SVI log output more clear --- src/storm/solver/helper/SoundValueIterationHelper.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storm/solver/helper/SoundValueIterationHelper.cpp b/src/storm/solver/helper/SoundValueIterationHelper.cpp index 6e47bfe3e..081c4a51d 100644 --- a/src/storm/solver/helper/SoundValueIterationHelper.cpp +++ b/src/storm/solver/helper/SoundValueIterationHelper.cpp @@ -301,14 +301,14 @@ namespace storm { storm::utility::vector::applyPointwise(x, y, x, [&meanBound] (ValueType const& xi, ValueType const& yi) -> ValueType { return xi + yi * meanBound; }); - STORM_LOG_INFO("Sound Value Iteration terminated with lower value bound " + STORM_LOG_INFO("Sound Value Iteration terminated with lower bound (over all states) " << (hasLowerBound ? lowerBound : storm::utility::zero()) << (hasLowerBound ? "" : "(none)") - << " and upper value bound " - << (hasUpperBound ? upperBound : storm::utility::zero()) << (hasUpperBound ? "" : "(none)") + << " and upper bound (over all states)" + << (hasUpperBound ? upperBound : storm::utility::infinity()) << (hasUpperBound ? "" : "(none)") << ". Decision value is " - << (hasDecisionValue ? decisionValue : storm::utility::zero()) << (hasDecisionValue ? "" : "(none)") + << (hasDecisionValue ? decisionValue : -storm::utility::infinity()) << (hasDecisionValue ? "" : "(none)") << "."); - } + } template bool SoundValueIterationHelper::checkCustomTerminationCondition(storm::solver::TerminationCondition const& condition) { From 0c0f61e27b726a5fb13aaf1a8453ea08c4d4aa7c Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 6 Jul 2018 09:28:54 +0200 Subject: [PATCH 2/6] Fix: Only access counterexample settings in model-handling, if they are available. --- src/storm-cli-utilities/model-handling.h | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 41faf8732..3f9967a3a 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -186,11 +186,15 @@ namespace storm { template std::shared_ptr buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) { - auto counterexampleGeneratorSettings = storm::settings::getModule(); storm::builder::BuilderOptions options(createFormulasToRespect(input.properties)); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); - options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) { + auto counterexampleGeneratorSettings = storm::settings::getModule(); + options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + } else { + options.setBuildChoiceOrigins(false); + } options.setBuildAllLabels(buildSettings.isBuildFullModelSet()); options.setBuildAllRewardModels(buildSettings.isBuildFullModelSet()); options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet()); From 33c189bd32e95c71ff9c70469a37ce4a26e287a2 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 30 Jun 2018 12:37:02 +0200 Subject: [PATCH 3/6] export setting for flattening --- src/storm/settings/modules/JaniExportSettings.cpp | 6 ++++++ src/storm/settings/modules/JaniExportSettings.h | 5 ++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/storm/settings/modules/JaniExportSettings.cpp b/src/storm/settings/modules/JaniExportSettings.cpp index a56cbc668..d6275834b 100644 --- a/src/storm/settings/modules/JaniExportSettings.cpp +++ b/src/storm/settings/modules/JaniExportSettings.cpp @@ -16,11 +16,13 @@ namespace storm { const std::string JaniExportSettings::janiFileOptionShortName = "output"; const std::string JaniExportSettings::standardCompliantOptionName = "standard-compliant"; const std::string JaniExportSettings::standardCompliantOptionShortName = "standard"; + const std::string JaniExportSettings::exportFlattenOptionName = "flatten"; 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, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Export in standard compliant variant.").build()); } bool JaniExportSettings::isJaniFileSet() const { @@ -34,6 +36,10 @@ namespace storm { bool JaniExportSettings::isExportAsStandardJaniSet() const { return this->getOption(standardCompliantOptionName).getHasOptionBeenSet(); } + + bool JaniExportSettings::isExportFlattenedSet() const { + return this->getOption(exportFlattenOptionName).getHasOptionBeenSet(); + } void JaniExportSettings::finalize() { diff --git a/src/storm/settings/modules/JaniExportSettings.h b/src/storm/settings/modules/JaniExportSettings.h index 397eb183a..fd6639869 100644 --- a/src/storm/settings/modules/JaniExportSettings.h +++ b/src/storm/settings/modules/JaniExportSettings.h @@ -25,7 +25,9 @@ namespace storm { std::string getJaniFilename() const; bool isExportAsStandardJaniSet() const; - + + bool isExportFlattenedSet() const; + bool check() const override; void finalize() override; @@ -36,6 +38,7 @@ namespace storm { static const std::string janiFileOptionShortName; static const std::string standardCompliantOptionName; static const std::string standardCompliantOptionShortName; + static const std::string exportFlattenOptionName; }; } From 6275c52779809fdcdf27d3e26d810b5e4752a664 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 11 Jul 2018 15:48:48 +0200 Subject: [PATCH 4/6] several convenience additions to jani data structures --- src/storm/storage/jani/Assignment.cpp | 2 +- src/storm/storage/jani/Assignment.h | 3 ++- src/storm/storage/jani/Automaton.cpp | 4 ++++ src/storm/storage/jani/Automaton.h | 2 ++ src/storm/storage/jani/JSONExporter.cpp | 1 + src/storm/storage/jani/Location.cpp | 4 ++++ src/storm/storage/jani/Location.h | 3 ++- src/storm/storage/jani/Model.cpp | 10 +++++++++- src/storm/storage/jani/Model.h | 13 +++++++++++++ src/storm/storage/jani/OrderedAssignments.cpp | 8 ++++++++ src/storm/storage/jani/OrderedAssignments.h | 4 +++- 11 files changed, 49 insertions(+), 5 deletions(-) diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp index 25fa036af..747679385 100644 --- a/src/storm/storage/jani/Assignment.cpp +++ b/src/storm/storage/jani/Assignment.cpp @@ -37,7 +37,7 @@ namespace storm { } void Assignment::substitute(std::map const& substitution) { - this->setAssignedExpression(this->getAssignedExpression().substitute(substitution)); + this->setAssignedExpression(this->getAssignedExpression().substitute(substitution).simplify()); } int64_t Assignment::getLevel() const { diff --git a/src/storm/storage/jani/Assignment.h b/src/storm/storage/jani/Assignment.h index a4e2dbd23..3ab3b5581 100644 --- a/src/storm/storage/jani/Assignment.h +++ b/src/storm/storage/jani/Assignment.h @@ -14,7 +14,8 @@ namespace storm { * Creates an assignment of the given expression to the given variable. */ Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t index = 0); - + + Assignment(Assignment const&) = default; bool operator==(Assignment const& other) const; /*! diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index f4c65c759..da0d0a91c 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -53,6 +53,10 @@ namespace storm { return variables.addVariable(variable); } + bool Automaton::hasVariable(std::string const& name) const { + return variables.hasVariable(name); + } + VariableSet& Automaton::getVariables() { return variables; } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index c549ecca8..986ea794d 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -79,6 +79,8 @@ namespace storm { * Retrieves the variables of this automaton. */ VariableSet const& getVariables() const; + + bool hasVariable(std::string const& name) const; /*! * Retrieves all expression variables used by this automaton. diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 0c0c212a0..435da6818 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -35,6 +35,7 @@ namespace storm { modernjson::json buildExpression(storm::expressions::Expression const& exp, std::vector const& constants, VariableSet const& globalVariables = VariableSet(), VariableSet const& localVariables = VariableSet()) { + STORM_LOG_TRACE("Exporting " << exp); return ExpressionToJson::translate(exp, constants, globalVariables, localVariables); } diff --git a/src/storm/storage/jani/Location.cpp b/src/storm/storage/jani/Location.cpp index b957d5e9a..5ab431734 100644 --- a/src/storm/storage/jani/Location.cpp +++ b/src/storm/storage/jani/Location.cpp @@ -10,6 +10,10 @@ namespace storm { Location::Location(std::string const& name, std::vector const& transientAssignments) : name(name), assignments(transientAssignments) { // Intentionally left empty. } + + Location::Location(std::string const& name, OrderedAssignments const& assignments) : name(name), assignments(assignments) { + // Intentionally left empty. + } std::string const& Location::getName() const { return name; diff --git a/src/storm/storage/jani/Location.h b/src/storm/storage/jani/Location.h index b2bda7b23..75e53d575 100644 --- a/src/storm/storage/jani/Location.h +++ b/src/storm/storage/jani/Location.h @@ -18,7 +18,8 @@ namespace storm { * Creates a new location. */ Location(std::string const& name, std::vector const& transientAssignments = {}); - + + Location(std::string const& name, OrderedAssignments const& assignments); /*! * Retrieves the name of the location. */ diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 47533126c..2d51910cc 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -711,7 +711,15 @@ namespace storm { std::vector const& Model::getAutomata() const { return automata; } - + + bool Model::hasAutomaton(std::string const& name) const { + return automatonToIndex.find(name) != automatonToIndex.end(); + } + + void Model::replaceAutomaton(uint64_t index, Automaton const& automaton) { + automata[index] = automaton; + } + Automaton& Model::getAutomaton(std::string const& name) { auto it = automatonToIndex.find(name); STORM_LOG_THROW(it != automatonToIndex.end(), storm::exceptions::InvalidOperationException, "Unable to retrieve unknown automaton '" << name << "'."); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 2dc69d147..86555a2d4 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -245,6 +245,19 @@ namespace storm { */ std::vector const& getAutomata() const; + /** + * Replaces the automaton at index with a new automaton. + * @param index + * @param newAutomaton + */ + void replaceAutomaton(uint64_t index, Automaton const& newAutomaton); + + /*! + * Rerieves whether there exists an automaton with the given name. + * @param name + * @return + */ + bool hasAutomaton(std::string const& name) const; /*! * Retrieves the automaton with the given name. */ diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 99eb415a8..68ae7f7c7 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -16,6 +16,14 @@ namespace storm { OrderedAssignments::OrderedAssignments(Assignment const& assignment) { add(assignment); } + + OrderedAssignments OrderedAssignments::clone() const { + OrderedAssignments result; + for (auto const& assignment : allAssignments) { + result.add(Assignment(*assignment)); + } + return result; + } bool OrderedAssignments::add(Assignment const& assignment) { // If the element is contained in this set of assignment, nothing needs to be added. diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h index 8e307e6e0..9d5a6a7b5 100644 --- a/src/storm/storage/jani/OrderedAssignments.h +++ b/src/storm/storage/jani/OrderedAssignments.h @@ -140,7 +140,9 @@ namespace storm { bool areLinear() const; friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments); - + + OrderedAssignments clone() const; + private: uint64_t isReadBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const; uint64_t isWrittenBeforeAssignment(Variable const& var, uint64_t assignmentNumber, uint64_t start = 0) const; From f9e420826849fa3674d3ea021343c588bbe49265 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 11 Jul 2018 15:49:37 +0200 Subject: [PATCH 5/6] export jani with comment expressions to ease debugging jani models --- src/storm/storage/jani/JSONExporter.cpp | 38 ++++++++++++++++--------- src/storm/storage/jani/JSONExporter.h | 4 +-- 2 files changed, 27 insertions(+), 15 deletions(-) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 435da6818..c829d3634 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -648,7 +648,7 @@ namespace storm { } - modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { + modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { std::vector assignmentDeclarations; bool addIndex = orderedAssignments.hasMultipleLevels(); for(auto const& assignment : orderedAssignments) { @@ -659,18 +659,21 @@ namespace storm { assignmentEntry["index"] = assignment.getLevel(); } assignmentDeclarations.push_back(assignmentEntry); + if (commentExpressions) { + assignmentEntry["comment"] = assignment.getVariable().getName() + " <- " + assignment.getAssignedExpression().toString(); + } } return modernjson::json(assignmentDeclarations); } - modernjson::json buildLocationsArray(std::vector const& locations, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { + modernjson::json buildLocationsArray(std::vector const& locations, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { std::vector locationDeclarations; for(auto const& location : locations) { modernjson::json locEntry; locEntry["name"] = location.getName(); // TODO support invariants? if (!location.getAssignments().empty()) { - locEntry["transient-values"] = buildAssignmentArray(location.getAssignments(), constants, globalVariables, localVariables); + locEntry["transient-values"] = buildAssignmentArray(location.getAssignments(), constants, globalVariables, localVariables, commentExpressions); } locationDeclarations.push_back(locEntry); } @@ -685,7 +688,7 @@ namespace storm { return modernjson::json(names); } - modernjson::json buildDestinations(std::vector const& destinations, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { + modernjson::json buildDestinations(std::vector const& destinations, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { assert(destinations.size() > 0); std::vector destDeclarations; for(auto const& destination : destinations) { @@ -699,16 +702,19 @@ namespace storm { } if (!prob1) { destEntry["probability"]["exp"] = buildExpression(destination.getProbability(), constants, globalVariables, localVariables); + if (commentExpressions) { + destEntry["probability"]["comment"] = destination.getProbability().toString(); + } } if (!destination.getOrderedAssignments().empty()) { - destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments(), constants, globalVariables, localVariables); + destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments(), constants, globalVariables, localVariables, commentExpressions); } destDeclarations.push_back(destEntry); } return modernjson::json(destDeclarations); } - modernjson::json buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables) { + modernjson::json buildEdges(std::vector const& edges , std::map const& actionNames, std::map const& locationNames, std::vector const& constants, VariableSet const& globalVariables, VariableSet const& localVariables, bool commentExpressions) { std::vector edgeDeclarations; for(auto const& edge : edges) { if (edge.getGuard().isFalse()) { @@ -722,13 +728,19 @@ namespace storm { } if(edge.hasRate()) { edgeEntry["rate"]["exp"] = buildExpression(edge.getRate(), constants, globalVariables, localVariables); + if (commentExpressions) { + edgeEntry["rate"]["comment"] = edge.getRate().toString(); + } } if (!edge.getGuard().isTrue()) { edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard(), constants, globalVariables, localVariables); + if (commentExpressions) { + edgeEntry["guard"]["comment"] = edge.getGuard().toString(); + } } - edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables); + edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames, constants, globalVariables, localVariables, commentExpressions); if (!edge.getAssignments().empty()) { - edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables); + edgeEntry["assignments"] = buildAssignmentArray(edge.getAssignments(), constants, globalVariables, localVariables, commentExpressions); } edgeDeclarations.push_back(edgeEntry); @@ -736,7 +748,7 @@ namespace storm { return modernjson::json(edgeDeclarations); } - modernjson::json buildAutomataArray(std::vector const& automata, std::map const& actionNames, std::vector const& constants, VariableSet const& globalVariables) { + modernjson::json buildAutomataArray(std::vector const& automata, std::map const& actionNames, std::vector const& constants, VariableSet const& globalVariables, bool commentExpressions) { std::vector automataDeclarations; for(auto const& automaton : automata) { modernjson::json autoEntry; @@ -745,16 +757,16 @@ namespace storm { if(automaton.hasRestrictedInitialStates()) { autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction(), constants, globalVariables, automaton.getVariables()); } - autoEntry["locations"] = buildLocationsArray(automaton.getLocations(), constants, globalVariables, automaton.getVariables()); + autoEntry["locations"] = buildLocationsArray(automaton.getLocations(), constants, globalVariables, automaton.getVariables(), commentExpressions); autoEntry["initial-locations"] = buildInitialLocations(automaton); - autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap(), constants, globalVariables, automaton.getVariables()); + autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap(), constants, globalVariables, automaton.getVariables(), commentExpressions); automataDeclarations.push_back(autoEntry); } return modernjson::json(automataDeclarations); } - void JsonExporter::convertModel(storm::jani::Model const& janiModel) { + void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) { jsonStruct["jani-version"] = janiModel.getJaniVersion(); jsonStruct["name"] = janiModel.getName(); jsonStruct["type"] = to_string(janiModel.getModelType()); @@ -762,7 +774,7 @@ namespace storm { jsonStruct["constants"] = buildConstantsArray(janiModel.getConstants()); jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables(), janiModel.getConstants(), janiModel.getGlobalVariables()); jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction(), janiModel.getConstants(), janiModel.getGlobalVariables()); - jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables()); + jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), commentExpressions); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); std::vector standardFeatureVector = {"derived-operators"}; jsonStruct["features"] = standardFeatureVector; diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 17fa97ad6..1bf098bca 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -3,7 +3,7 @@ #include "storm/storage/expressions/ExpressionVisitor.h" #include "storm/logic/FormulaVisitor.h" -#include "Model.h" +#include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" #include "storm/adapters/RationalNumberAdapter.h" // JSON parser @@ -80,7 +80,7 @@ namespace storm { private: - void convertModel(storm::jani::Model const& model); + void convertModel(storm::jani::Model const& model, bool commentExpressions = true); void convertProperties(std::vector const& formulas, storm::jani::Model const& model); void appendVariableDeclaration(storm::jani::Variable const& variable); From e64e293d59e18a4d035752c57b444d259a9498ae Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 11 Jul 2018 15:50:16 +0200 Subject: [PATCH 6/6] jani transformer which changes a variable into a location --- src/storm/api/export.cpp | 16 ++- .../settings/modules/JaniExportSettings.cpp | 27 +++- .../settings/modules/JaniExportSettings.h | 5 + .../storage/jani/JaniLocationExpander.cpp | 121 ++++++++++++++++++ src/storm/storage/jani/JaniLocationExpander.h | 26 ++++ 5 files changed, 190 insertions(+), 5 deletions(-) create mode 100644 src/storm/storage/jani/JaniLocationExpander.cpp create mode 100644 src/storm/storage/jani/JaniLocationExpander.h 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); + + + + }; + } + +}