diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp index bfbb6cad4..5ae5248b3 100644 --- a/src/storm-pgcl-cli/storm-pgcl.cpp +++ b/src/storm-pgcl-cli/storm-pgcl.cpp @@ -18,7 +18,8 @@ #include "storm-pgcl/settings/modules/PGCLSettings.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/JaniExportSettings.h" +#include "storm-conv/settings/modules/JaniExportSettings.h" +#include "storm-conv/api/storm-conv.h" #include "storm/utility/file.h" @@ -38,11 +39,13 @@ void initializeSettings() { } void handleJani(storm::jani::Model& model) { - if (!storm::settings::getModule().isJaniFileSet()) { - // For now, we have to have a jani file - storm::jani::JsonExporter::toStream(model, {}, std::cout); + auto const& jani = storm::settings::getModule(); + storm::converter::JaniConversionOptions options(jani); + storm::api::postprocessJani(model, options); + if (storm::settings::getModule().isToJaniSet()) { + storm::api::exportJaniToFile(model, {}, storm::settings::getModule().getWriteToJaniFilename()); } else { - storm::jani::JsonExporter::toFile(model, {}, storm::settings::getModule().getJaniFilename()); + storm::api::printJaniToStream(model, {}, std::cout); } } diff --git a/src/storm-pgcl/CMakeLists.txt b/src/storm-pgcl/CMakeLists.txt index 7b86f73c3..1adf442c6 100644 --- a/src/storm-pgcl/CMakeLists.txt +++ b/src/storm-pgcl/CMakeLists.txt @@ -10,7 +10,7 @@ file(GLOB_RECURSE STORM_PGCL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pgcl/*/*.h) # Create storm-pgcl. add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS}) -target_link_libraries(storm-pgcl storm storm-parsers) +target_link_libraries(storm-pgcl storm storm-parsers storm-conv) # installation install(TARGETS storm-pgcl EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pgcl/settings/modules/PGCLSettings.cpp b/src/storm-pgcl/settings/modules/PGCLSettings.cpp index a70b87f6f..4225dcd39 100644 --- a/src/storm-pgcl/settings/modules/PGCLSettings.cpp +++ b/src/storm-pgcl/settings/modules/PGCLSettings.cpp @@ -26,7 +26,7 @@ namespace storm { PGCLSettings::PGCLSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("description", "description of the variable restrictions").build()).build()); } @@ -43,6 +43,11 @@ namespace storm { return this->getOption(pgclToJaniOptionName).getHasOptionBeenSet(); } + std::string const& PGCLSettings::getWriteToJaniFilename() const { + return this->getOption(pgclToJaniOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool PGCLSettings::isProgramGraphToDotSet() const { return this->getOption(programGraphToDotOptionName).getHasOptionBeenSet(); } diff --git a/src/storm-pgcl/settings/modules/PGCLSettings.h b/src/storm-pgcl/settings/modules/PGCLSettings.h index 29e689366..5870ccbe5 100644 --- a/src/storm-pgcl/settings/modules/PGCLSettings.h +++ b/src/storm-pgcl/settings/modules/PGCLSettings.h @@ -29,6 +29,11 @@ namespace storm { */ bool isToJaniSet() const; + /** + * returns the file name where jani output should be stored. + */ + std::string const& getWriteToJaniFilename() const; + /** * Whether the program graph should be drawn (dot output) */