sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

separating declaration/implementation for storm-conv api

tempestpy_adaptions
TimQu 6 years ago
parent
3e8959c866
commit
19c6472843
2 changed files with 71 additions and 46 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 58
      src/storm-conv/api/storm-conv.cpp
  2. 57
      src/storm-conv/api/storm-conv.h

58
src/storm-conv/api/storm-conv.cpp
View File

@ -0,0 +1,58 @@
#include "storm-conv/api/storm-conv.h"
#include "storm/storage/prism/Program.h"
#include "storm/storage/jani/Property.h"
#include "storm/storage/jani/JaniLocationExpander.h"
#include "storm/storage/jani/JSONExporter.h"
namespace storm {
namespace api {
void postprocessJani(storm::jani::Model& janiModel, storm::converter::JaniConversionOptions options) {
if (!options.locationVariables.empty()) {
for (auto const& pair : options.locationVariables) {
storm::jani::JaniLocationExpander expander(janiModel);
expander.transform(pair.first, pair.second);
janiModel = expander.getResult();
}
}
if (options.exportFlattened) {
janiModel = janiModel.flattenComposition();
}
if (options.standardCompliant) {
janiModel.makeStandardJaniCompliant();
}
}
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, storm::converter::PrismToJaniConverterOptions options) {
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> res;
// Perform conversion
auto modelAndRenaming = program.toJaniWithLabelRenaming(options.allVariablesGlobal, options.suffix, options.janiOptions.standardCompliant);
res.first = std::move(modelAndRenaming.first);
// Amend properties to potentially changed labels
for (auto const& property : properties) {
res.second.emplace_back(property.substituteLabels(modelAndRenaming.second));
}
// Postprocess Jani model based on the options
postprocessJani(res.first, options.janiOptions);
return res;
}
void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
storm::jani::JsonExporter::toFile(model, properties, filename);
}
void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream) {
storm::jani::JsonExporter::toStream(model, properties, ostream);
}
}
}

57
src/storm-conv/api/storm-conv.h
View File

@ -3,58 +3,25 @@
#include "storm-conv/converter/options/PrismToJaniConverterOptions.h" #include "storm-conv/converter/options/PrismToJaniConverterOptions.h"
#include "storm-conv/converter/options/JaniConversionOptions.h" #include "storm-conv/converter/options/JaniConversionOptions.h"
#include "storm/storage/prism/Program.h"
#include "storm/storage/jani/Property.h"
#include "storm/storage/jani/JaniLocationExpander.h"
#include "storm/storage/jani/JSONExporter.h"
namespace storm { namespace storm {
namespace api {
void postprocessJani(storm::jani::Model& janiModel, storm::converter::JaniConversionOptions options) {
if (!options.locationVariables.empty()) {
for (auto const& pair : options.locationVariables) {
storm::jani::JaniLocationExpander expander(janiModel);
expander.transform(pair.first, pair.second);
janiModel = expander.getResult();
}
}
if (options.exportFlattened) {
janiModel = janiModel.flattenComposition();
}
if (options.standardCompliant) {
janiModel.makeStandardJaniCompliant();
}
}
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties = std::vector<storm::jani::Property>(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions()) {
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> res;
// Perform conversion
auto modelAndRenaming = program.toJaniWithLabelRenaming(options.allVariablesGlobal, options.suffix, options.janiOptions.standardCompliant);
res.first = std::move(modelAndRenaming.first);
namespace prism {
class Program;
}
namespace jani {
class Model;
class Property;
}
// Amend properties to potentially changed labels
for (auto const& property : properties) {
res.second.emplace_back(property.substituteLabels(modelAndRenaming.second));
}
namespace api {
// Postprocess Jani model based on the options
postprocessJani(res.first, options.janiOptions);
void postprocessJani(storm::jani::Model& janiModel, storm::converter::JaniConversionOptions options);
return res;
}
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties = std::vector<storm::jani::Property>(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions());
void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
storm::jani::JsonExporter::toFile(model, properties, filename);
}
void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename);
void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream) {
storm::jani::JsonExporter::toStream(model, properties, ostream);
}
void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream);
} }
Write Preview
Loading…
Cancel
Save