Browse Source

no need anymore to create files from formulas if properties are present anyway

tempestpy_adaptions
Sebastian Junges 8 years ago
parent
commit
c2ea78b880
  1. 10
      src/storm/storage/jani/JSONExporter.cpp
  2. 8
      src/storm/storage/jani/JSONExporter.h
  3. 4
      src/storm/utility/storm.cpp

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

@ -516,7 +516,7 @@ namespace storm {
void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid) {
void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid) {
std::ofstream ofs;
ofs.open (filepath, std::ofstream::out );
if(ofs.is_open()) {
@ -526,7 +526,7 @@ namespace storm {
}
}
void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& os, bool checkValid) {
void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid) {
if(checkValid) {
janiModel.checkValid();
}
@ -759,13 +759,13 @@ namespace storm {
}
void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model) {
void JsonExporter::convertProperties( std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model) {
std::vector<modernjson::json> properties;
uint64_t index = 0;
for(auto const& f : formulas) {
modernjson::json propDecl;
propDecl["name"] = "prop" + std::to_string(index);
propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), model);
propDecl["name"] = f.getName();
propDecl["expression"] = convertFilterExpression(f.getFilter(), model);
++index;
properties.push_back(propDecl);
}

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

@ -4,6 +4,7 @@
#include "storm/storage/expressions/ExpressionVisitor.h"
#include "storm/logic/FormulaVisitor.h"
#include "Model.h"
#include "storm/storage/jani/Property.h"
#include "storm/adapters/NumberAdapter.h"
// JSON parser
#include "json.hpp"
@ -66,12 +67,13 @@ namespace storm {
JsonExporter() = default;
public:
static void toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid = true);
static void toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& ostream, bool checkValid = false);
static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true);
static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false);
private:
void convertModel(storm::jani::Model const& model);
void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model);
void convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);
void appendVariableDeclaration(storm::jani::Variable const& variable);
modernjson::json finalize() {

4
src/storm/utility/storm.cpp

@ -36,9 +36,9 @@ namespace storm{
if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
storm::jani::Model normalisedModel = model;
normalisedModel.makeStandardJaniCompliant();
storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), filepath);
storm::jani::JsonExporter::toFile(normalisedModel, properties, filepath);
} else {
storm::jani::JsonExporter::toFile(model, formulasInProperties(properties), filepath);
storm::jani::JsonExporter::toFile(model, properties, filepath);
}
}

Loading…
Cancel
Save