diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp new file mode 100644 index 000000000..1b52092bb --- /dev/null +++ b/src/storm-conv/api/storm-conv.cpp @@ -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> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties, storm::converter::PrismToJaniConverterOptions options) { + std::pair> 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 const& properties, std::string const& filename) { + storm::jani::JsonExporter::toFile(model, properties, filename); + } + + void printJaniToStream(storm::jani::Model const& model, std::vector const& properties, std::ostream& ostream) { + storm::jani::JsonExporter::toStream(model, properties, ostream); + } + + + } +} \ No newline at end of file diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h index 499777517..ec8a306df 100644 --- a/src/storm-conv/api/storm-conv.h +++ b/src/storm-conv/api/storm-conv.h @@ -3,58 +3,25 @@ #include "storm-conv/converter/options/PrismToJaniConverterOptions.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 prism { + class Program; + } + namespace jani { + class Model; + class Property; + } + 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(); - } - } + void postprocessJani(storm::jani::Model& janiModel, storm::converter::JaniConversionOptions options); - if (options.exportFlattened) { - janiModel = janiModel.flattenComposition(); - } - - if (options.standardCompliant) { - janiModel.makeStandardJaniCompliant(); - } - } - - std::pair> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties = std::vector(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions()) { - std::pair> 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; - } + std::pair> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties = std::vector(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions()); - void exportJaniToFile(storm::jani::Model const& model, std::vector const& properties, std::string const& filename) { - storm::jani::JsonExporter::toFile(model, properties, filename); - } + void exportJaniToFile(storm::jani::Model const& model, std::vector const& properties, std::string const& filename); - void printJaniToStream(storm::jani::Model const& model, std::vector const& properties, std::ostream& ostream) { - storm::jani::JsonExporter::toStream(model, properties, ostream); - } + void printJaniToStream(storm::jani::Model const& model, std::vector const& properties, std::ostream& ostream); }