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<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,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<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");
}
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<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.
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<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;
}