Browse Source

actually fixed model feature support

tempestpy_adaptions
TimQu 6 years ago
parent
commit
3cf9553126
  1. 4
      src/storm/storage/jani/JSONExporter.cpp
  2. 5
      src/storm/storage/jani/JSONExporter.h
  3. 5
      src/storm/storage/jani/ModelFeatures.cpp

4
src/storm/storage/jani/JSONExporter.cpp

@ -1094,6 +1094,10 @@ namespace storm {
jsonStruct["properties"] = properties;
}
modernjson::json JsonExporter::finalize() {
jsonStruct["features"] = modernjson::json::parse(modelFeatures.toString());
return jsonStruct;
}
}
}

5
src/storm/storage/jani/JSONExporter.h

@ -97,10 +97,7 @@ namespace storm {
void convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);
void appendVariableDeclaration(storm::jani::Variable const& variable);
modernjson::json finalize() {
jsonStruct["features"] = modelFeatures.toString();
return jsonStruct;
}
modernjson::json finalize();
modernjson::json jsonStruct;
storm::jani::ModelFeatures modelFeatures;

5
src/storm/storage/jani/ModelFeatures.cpp

@ -21,15 +21,16 @@ namespace storm {
}
std::string ModelFeatures::toString() const {
std::string res;
std::string res = "[";
bool first = true;
for (auto const& f : features) {
if (!first) {
res += ", ";
}
res += storm::jani::toString(f);
res += "\"" + storm::jani::toString(f) + "\"";
first = false;
}
res += "]";
return res;
}

Loading…
Cancel
Save