removed standard-compliant option: storm-conv now produces standard compliant jani code by default

src/storm-cli-utilities/model-handling.h

@@ -136,7 +136,7 @@ namespace storm {
                 
                 if (transformToJani) {
                     storm::prism::Program const& model = output.model.get().asPrismProgram();
-                    auto modelAndProperties = model.toJani(output.properties, true, "", false);
+                    auto modelAndProperties = model.toJani(output.properties);
                     output.model = modelAndProperties.first;
                     
                     if (!modelAndProperties.second.empty()) {

src/storm-conv/api/storm-conv.cpp

@@ -35,8 +35,8 @@ namespace storm {
                 janiModel = janiModel.flattenComposition(smtSolverFactory);
             }
 
-            if (options.standardCompliant) {
-                janiModel.makeStandardJaniCompliant();
+            if (!options.edgeAssignments) {
+                janiModel.pushEdgeAssignmentsToDestinations();
             }
             
             auto uneliminatedFeatures = janiModel.restrictToFeatures(options.allowedModelFeatures);
@@ -50,7 +50,7 @@ namespace storm {
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, storm::converter::PrismToJaniConverterOptions options) {
         
             // Perform conversion
-            auto res = program.toJani(properties, true, "", false);
+            auto res = program.toJani(properties, options.allVariablesGlobal);
             if (res.second.empty()) {
                 std::vector<storm::jani::Property> clondedProperties;
                 for (auto const& p : properties) {

src/storm-conv/converter/options/JaniConversionOptions.cpp

@@ -3,11 +3,11 @@
 namespace storm {
     namespace converter {
 
-        JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
+        JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
             // Intentionally left empty
         };
 
-        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
+        JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) {
             if (settings.isEliminateFunctionsSet()) {
                 allowedModelFeatures.remove(storm::jani::ModelFeature::Functions);
             }

src/storm-conv/converter/options/JaniConversionOptions.h

@@ -18,8 +18,8 @@ namespace storm {
             /// (Automaton,Variable)-pairs that will be transformed to location variables of the respective automaton.
             std::vector<std::pair<std::string, std::string>> locationVariables;
             
-            /// If set, the model will be made standard compliant (e.g. no state rewards for discrete time models)
-            bool standardCompliant;
+            /// If set, the model might have transient assignments to the edges
+            bool edgeAssignments;
             
             /// If set, the model is transformed into a single automaton
             bool flatten;

src/storm-conv/settings/modules/JaniExportSettings.cpp

@@ -14,19 +14,17 @@ namespace storm {
         namespace modules {
             const std::string JaniExportSettings::moduleName = "exportJani";
             
-            const std::string JaniExportSettings::standardCompliantOptionName = "standard-compliant";
-            const std::string JaniExportSettings::standardCompliantOptionShortName = "standard";
+            const std::string JaniExportSettings::edgeAssignmentsOptionName = "edge-assignments";
             const std::string JaniExportSettings::exportFlattenOptionName = "flatten";
             const std::string JaniExportSettings::locationVariablesOptionName = "location-variables";
             const std::string JaniExportSettings::globalVariablesOptionName = "globalvars";
             const std::string JaniExportSettings::compactJsonOptionName = "compactjson";
-            const std::string JaniExportSettings::eliminateArraysOptionName = "eliminate-arrays";
-            const std::string JaniExportSettings::eliminateFunctionsOptionName = "eliminate-functions";
-
+            const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays";
+            const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions";
             
             JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list of automaton and local variable names seperated by a dot, e.g. A.x,B.y.").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, edgeAssignmentsOptionName, false, "If set, the output model can have transient edge assignments. This can simplify the jani model but is not compliant to the jani standard.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build());
@@ -34,8 +32,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build());
             }
             
-            bool JaniExportSettings::isExportAsStandardJaniSet() const {
-                return this->getOption(standardCompliantOptionName).getHasOptionBeenSet();
+            bool JaniExportSettings::isAllowEdgeAssignmentsSet() const {
+                return this->getOption(edgeAssignmentsOptionName).getHasOptionBeenSet();
             }
 
             bool JaniExportSettings::isExportFlattenedSet() const {

src/storm-conv/settings/modules/JaniExportSettings.h

@@ -14,7 +14,7 @@ namespace storm {
                  */
                 JaniExportSettings();
                 
-                bool isExportAsStandardJaniSet() const;
+                bool isAllowEdgeAssignmentsSet() const;
 
                 bool isExportFlattenedSet() const;
 
@@ -36,8 +36,7 @@ namespace storm {
                 static const std::string moduleName;
                 
             private:
-                static const std::string standardCompliantOptionName;
-                static const std::string standardCompliantOptionShortName;
+                static const std::string edgeAssignmentsOptionName;
                 static const std::string exportFlattenOptionName;
                 static const std::string locationVariablesOptionName;
                 static const std::string globalVariablesOptionName;

src/storm/storage/SymbolicModelDescription.cpp

@@ -120,23 +120,23 @@ namespace storm {
             return result;
         }
         
-        SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal, bool standardCompliant) const {
+        SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const {
             if (this->isJaniModel()) {
                 return *this;
             }
             if (this->isPrismProgram()) {
-                return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal, "", standardCompliant));
+                return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal, ""));
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
             }
         }
         
-        std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> SymbolicModelDescription::toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal, bool standardCompliant) const {
+        std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> SymbolicModelDescription::toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal) const {
             if (this->isJaniModel()) {
                 return std::make_pair(*this, std::vector<storm::jani::Property>());
             }
             if (this->isPrismProgram()) {
-                auto modelProperties = this->asPrismProgram().toJani(properties, makeVariablesGlobal, "", standardCompliant);
+                auto modelProperties = this->asPrismProgram().toJani(properties, makeVariablesGlobal, "");
                 return std::make_pair(SymbolicModelDescription(modelProperties.first), modelProperties.second);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");

src/storm/storage/SymbolicModelDescription.h

@@ -38,7 +38,7 @@ namespace storm {
             
             std::vector<std::string> getParameterNames() const;
             
-            SymbolicModelDescription toJani(bool makeVariablesGlobal = true, bool standardCompliant = false) const;
+            SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const;
             
             /*!
              * Ensures that this model is a JANI model by, e.g., converting prism to jani.
@@ -48,7 +48,7 @@ namespace storm {
              *
              * @note The returned property vector might be empty in case no renaming is necessary.
              */
-            std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal, bool standardCompliant) const;
+            std::pair<SymbolicModelDescription, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool makeVariablesGlobal) const;
             
             SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
             SymbolicModelDescription preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;

src/storm/storage/jani/Model.cpp

@@ -1276,6 +1276,12 @@ namespace storm {
                 automaton.pushEdgeAssignmentsToDestinations();
             }
         }
+     
+        void Model::pushEdgeAssignmentsToDestinations() {
+            for (auto& automaton : automata) {
+                automaton.pushEdgeAssignmentsToDestinations();
+            }
+        }
         
         void Model::liftTransientEdgeDestinationAssignments(int64_t maxLevel) {
             for (auto& automaton : this->getAutomata()) {

src/storm/storage/jani/Model.h

@@ -546,6 +546,9 @@ namespace storm {
             
             void makeStandardJaniCompliant();
 
+            // Pushes all edge assignments to their destination
+            void pushEdgeAssignmentsToDestinations();
+            
             /*!
              * Checks whether in the composition, actions are reused: That is, if the model is put in parallel composition and the same action potentially leads to multiple edges from the same state.
              * @return
@@ -612,6 +615,7 @@ namespace storm {
             VariableSet globalVariables;
             
             /// A mapping from names to function definitions
+            /// Since we use an unordered_map, references to function definitions will not get invalidated when more function definitions are added
             std::unordered_map<std::string, FunctionDefinition> globalFunctions;
             
             /// The list of automata.

src/storm/storage/prism/Program.cpp

@@ -1795,17 +1795,17 @@ namespace storm {
             return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0);
         }
         
-        storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const {
+        storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const {
             ToJaniConverter converter;
-            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant);
+            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix);
             STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
             STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
             return janiModel;
         }
 
-        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> Program::toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal, std::string suffix, bool standardCompliant) const {
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> Program::toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal, std::string suffix) const {
             ToJaniConverter converter;
-            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant);
+            auto janiModel = converter.convert(*this, allVariablesGlobal, suffix);
             std::vector<storm::jani::Property> newProperties;
             if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
                 newProperties = converter.applyRenaming(properties);

src/storm/storage/prism/Program.h

@@ -649,14 +649,14 @@ namespace storm {
             /*!
              * Converts the PRISM model into an equivalent JANI model.
              */
-            storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const;
+            storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "") const;
             
             /*!
              * Converts the PRISM model into an equivalent JANI model and if labels or reward models had
              * to be renamed in the process, the renamings are applied to the given properties
              * @return The jani model of this and either the new set of properties or an empty vector if no renamings were necessary
              */
-            std::pair<storm::jani::Model, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const;
+            std::pair<storm::jani::Model, std::vector<storm::jani::Property>> toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal = true, std::string suffix = "") const;
             
         private:
             /*!

src/storm/storage/prism/ToJaniConverter.cpp

@@ -18,15 +18,13 @@
 namespace storm {
     namespace prism {
         
-        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix, bool standardCompliant) {
+        storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) {
             labelRenaming.clear();
             rewardModelRenaming.clear();
             formulaToFunctionCallMap.clear();
 
             std::shared_ptr<storm::expressions::ExpressionManager> manager = program.getManager().getSharedPointer();
             
-            bool produceStateRewards = !standardCompliant || program.getModelType() == storm::prism::Program::ModelType::CTMC || program.getModelType() == storm::prism::Program::ModelType::MA;
-                        
             // Start by creating an empty JANI model.
             storm::jani::ModelType modelType;
             switch (program.getModelType()) {
@@ -254,20 +252,6 @@ namespace storm {
             }
             STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition.");
             
-            // If we are not allowed to produce state rewards, we need to create a mapping from action indices to transient
-            // location assignments. This is done so that all assignments are added only *once* for synchronizing actions.
-            std::map<uint_fast64_t, std::vector<storm::jani::Assignment>> transientRewardLocationAssignmentsPerAction;
-            if (!produceStateRewards) {
-                for (auto const& action : program.getActions()) {
-                    auto& list = transientRewardLocationAssignmentsPerAction[janiModel.getActionIndex(action)];
-                    for (auto const& assignment : transientLocationAssignments) {
-                        if (assignment.isTransient() && assignment.getVariable().isRealVariable()) {
-                            list.emplace_back(assignment);
-                        }
-                    }
-                }
-            }
-            
             // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
             // previously built mapping to make variables global that are read by more than one module.
             std::set<uint64_t> firstModules;
@@ -310,9 +294,7 @@ namespace storm {
                 if (firstModule) {
                     storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex);
                     for (auto const& assignment : transientLocationAssignments) {
-                        if (assignment.getVariable().isBooleanVariable() || produceStateRewards) {
-                            onlyLocation.addTransientAssignment(assignment);
-                        }
+                        onlyLocation.addTransientAssignment(assignment);
                     }
                 }
                 
@@ -357,12 +339,6 @@ namespace storm {
                             templateEdge->addTransientAssignment(assignment);
                         }
                     }
-                    if (!produceStateRewards) {
-                        transientEdgeAssignmentsToAdd = transientRewardLocationAssignmentsPerAction.find(janiModel.getActionIndex(command.getActionName()));
-                        for (auto const& assignment : transientEdgeAssignmentsToAdd->second) {
-                            templateEdge->addTransientAssignment(assignment, true);
-                        }
-                    }
 
                     // Create the edge object.
                     storm::jani::Edge newEdge;

src/storm/storage/prism/ToJaniConverter.h

@@ -18,7 +18,7 @@ namespace storm {
         
         class ToJaniConverter {
         public:
-            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false);
+            storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = "");
             
             bool labelsWereRenamed() const;
             bool rewardModelsWereRenamed() const;