check validity, set standard composition

Former-commit-id: 526d484fd5 [formerly 3fac58583a]
Former-commit-id: fbb770a840

src/parser/JaniParser.cpp

@@ -88,29 +88,29 @@ namespace storm {
             parseActions(parsedStructure.at("actions"), model);
             size_t constantsCount = parsedStructure.count("constants");
             STORM_LOG_THROW(constantsCount < 2, storm::exceptions::InvalidJaniException, "Constant-declarations can be given at most once.");
-            if(constantsCount == 1) {
+            if (constantsCount == 1) {
                 for (auto const &constStructure : parsedStructure.at("constants")) {
                     model.addConstant(*parseConstant(constStructure, "global"));
                 }
             }
             size_t variablesCount = parsedStructure.count("variables");
             STORM_LOG_THROW(variablesCount < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables.");
-            if(variablesCount == 1) {
-                for(auto const& varStructure : parsedStructure.at("variables")) {
+            if (variablesCount == 1) {
+                for (auto const& varStructure : parsedStructure.at("variables")) {
                     model.addVariable(*parseVariable(varStructure, "global"));
                 }
             }
             STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given");
             STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array");
             // Automatons can only be parsed after constants and variables.
-            for(auto const& automataEntry : parsedStructure.at("automata")) {
+            for (auto const& automataEntry : parsedStructure.at("automata")) {
                 model.addAutomaton(parseAutomaton(automataEntry, model));
             }
             //STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
             //std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
             STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given");
             PropertyVector properties;
-            if(parseProperties && parsedStructure.count("properties") == 1) {
+            if (parseProperties && parsedStructure.count("properties") == 1) {
                 STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array");
                 for(auto const& propertyEntry : parsedStructure.at("properties")) {
                     properties.push_back(this->parseProperty(propertyEntry));
@@ -125,10 +125,11 @@ namespace storm {
             // TODO check unique name
             std::string name = getString(propertyStructure.at("name"), "property-name");
             std::string comment = "";
-            if(propertyStructure.count("comment") > 0) {
+            if (propertyStructure.count("comment") > 0) {
                 comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'.");
             }
             
+
         }
 
         std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) {
@@ -141,13 +142,13 @@ namespace storm {
             size_t valueCount = constantStructure.count("value");
             storm::expressions::Expression initExpr;
             STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name +  "'  (scope: " + scopeDescription + ") must be given at most once.");
-            if(valueCount == 1) {
+            if (valueCount == 1) {
                 // Read initial value before; that makes creation later on a bit easier, and has as an additional benefit that we do not need to check whether the variable occurs also on the assignment.
                 initExpr = parseExpression(constantStructure.at("value"), "Value of constant " + name + " (scope: " + scopeDescription + ")");
                 assert(initExpr.isInitialized());
             }
 
-            if(constantStructure.at("type").is_object()) {
+            if (constantStructure.at("type").is_object()) {
 //                STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ")  kind must be given");
 //                std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name  + "(scope: " + scopeDescription + ") ");
 //                if(kind == "bounded") {
@@ -336,7 +337,7 @@ namespace storm {
 
         storm::jani::Variable const& getLValue(std::string const& ident, storm::jani::VariableSet const& globalVars, storm::jani::VariableSet const& localVars, std::string const& scopeDescription) {
             if(localVars.hasVariable(ident)) {
-                return globalVars.getVariable(ident);
+                return localVars.getVariable(ident);
             } else if(globalVars.hasVariable(ident)) {
                 return globalVars.getVariable(ident);
             } else {
@@ -675,7 +676,7 @@ namespace storm {
                         storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
                         // value
                         STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "'  must have one value field");
-                        storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
+                        storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars);
                         // TODO check types
                         assignments.emplace_back(lhs, assignmentExpr);
                     }

src/storage/jani/JSONExporter.cpp

@@ -142,17 +142,20 @@ namespace storm {
         
         
         
-        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath) {
+        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid) {
             std::ofstream ofs;
             ofs.open (filepath, std::ofstream::out );
             if(ofs.is_open()) {
-                toStream(janiModel, ofs);
+                toStream(janiModel, ofs, checkValid);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
             }
         }
         
-        void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os) {
+        void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os, bool checkValid) {
+            if(checkValid) {
+                janiModel.checkValid();
+            }
             JsonExporter exporter;
             exporter.convertModel(janiModel);
             os << exporter.finalize().dump(4) << std::endl;
@@ -308,7 +311,9 @@ namespace storm {
                 modernjson::json autoEntry;
                 autoEntry["name"] = automaton.getName();
                 autoEntry["variables"] = buildVariablesArray(automaton.getVariables());
-                autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction());
+                if(automaton.hasRestrictedInitialStates()) {
+                    autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction());
+                }
                 autoEntry["locations"] = buildLocationsArray(automaton.getLocations());
                 autoEntry["initial-locations"] = buildInitialLocations(automaton);
                 autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap());

src/storage/jani/JSONExporter.h

@@ -32,8 +32,8 @@ namespace storm {
             JsonExporter() = default;
             
         public:
-            static void toFile(storm::jani::Model const& janiModel, std::string const& filepath);
-            static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream);
+            static void toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid = true);
+            static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream, bool checkValid = false);
             
         private:
             void convertModel(storm::jani::Model const& model);

src/storage/jani/Model.cpp

@@ -252,6 +252,10 @@ namespace storm {
             this->composition = composition;
         }
         
+        void Model::setStandardSystemComposition() {
+            setSystemComposition(getStandardSystemComposition());
+        }
+        
         std::set<std::string> Model::getActionNames(bool includeSilent) const {
             std::set<std::string> result;
             for (auto const& entry : actionToIndex) {
@@ -435,25 +439,11 @@ namespace storm {
             }
         }
         
-        bool Model::checkValidity(bool logdbg) const {
+        void Model::checkValid() const {
             // TODO switch to exception based return value.
-            
-            if (version == 0) {
-                if(logdbg) STORM_LOG_DEBUG("Jani version is unspecified");
-                return false;
-            }
-            
-            if(modelType == ModelType::UNDEFINED) {
-                if(logdbg) STORM_LOG_DEBUG("Model type is unspecified");
-                return false;
-            }
-            
-            if(automata.empty()) {
-                if(logdbg) STORM_LOG_DEBUG("No automata specified");
-                return false;
-            }
-            // All checks passed.
-            return true;
+            STORM_LOG_ASSERT(getModelType() != storm::jani::ModelType::UNDEFINED, "Model type not set");
+            STORM_LOG_ASSERT(!automata.empty(), "No automata set");
+            STORM_LOG_ASSERT(composition != nullptr, "Composition is not set");
             
         }
         

src/storage/jani/Model.h

@@ -221,6 +221,11 @@ namespace storm {
              */
             void setSystemComposition(std::shared_ptr<Composition> const& composition);
             
+            /*!
+             * Sets the system composition to be the fully-synchronizing parallel composition of all automat
+             * @see getStandardSystemComposition
+             */
+            void setStandardSystemComposition();
             /*!
              * Gets the system composition as the standard, fully-synchronizing parallel composition.
              */
@@ -328,7 +333,7 @@ namespace storm {
             /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */
-            bool checkValidity(bool logdbg = true) const;
+            void checkValid() const;
             
         private:
             /// The model name.

src/utility/storm.cpp

@@ -17,9 +17,7 @@ namespace storm {
 
     std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path) {
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path);
-        if(!modelAndFormulae.first.checkValidity(true)) {
-            STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Jani file parsing yields invalid model.");
-        }
+        modelAndFormulae.first.checkValid();
         return modelAndFormulae;
     }