From b3204a178a2ef646aaa587e28204f7ca4128cd29 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 17 Sep 2016 13:48:56 +0200 Subject: [PATCH] check validity, set standard composition Former-commit-id: 526d484fd5f501fb8a7b9538dc04ee41ed58b45a [formerly 3fac58583a3ecfcfbd285d5416477cf1fc6cc06e] Former-commit-id: fbb770a8402cbfef27ab56f7aa3e41fec6efe127 --- src/parser/JaniParser.cpp | 21 +++++++++++---------- src/storage/jani/JSONExporter.cpp | 13 +++++++++---- src/storage/jani/JSONExporter.h | 4 ++-- src/storage/jani/Model.cpp | 26 ++++++++------------------ src/storage/jani/Model.h | 7 ++++++- src/utility/storm.cpp | 4 +--- 6 files changed, 37 insertions(+), 38 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 39e5e39b8..7e54d15fb 100644 --- a/src/parser/JaniParser.cpp +++ b/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 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,9 +125,10 @@ 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 + "'."); } + } @@ -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); } diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 14813a38a..cfadf0c41 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/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()); diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 35fb567fa..a52b84b5d 100644 --- a/src/storage/jani/JSONExporter.h +++ b/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); diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 668e54528..5a528b631 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -252,6 +252,10 @@ namespace storm { this->composition = composition; } + void Model::setStandardSystemComposition() { + setSystemComposition(getStandardSystemComposition()); + } + std::set Model::getActionNames(bool includeSilent) const { std::set 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"); } diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index b4f42a87c..eaf0f9d0f 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -221,6 +221,11 @@ namespace storm { */ void setSystemComposition(std::shared_ptr 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. diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index c567c05cb..b1ad84cc6 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -17,9 +17,7 @@ namespace storm { std::pair> parseJaniModel(std::string const& path) { std::pair> 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; }