Browse Source

made storm-pgcl use storm-conv

tempestpy_adaptions
TimQu 6 years ago
parent
commit
9563cb44cb
  1. 13
      src/storm-pgcl-cli/storm-pgcl.cpp
  2. 2
      src/storm-pgcl/CMakeLists.txt
  3. 7
      src/storm-pgcl/settings/modules/PGCLSettings.cpp
  4. 5
      src/storm-pgcl/settings/modules/PGCLSettings.h

13
src/storm-pgcl-cli/storm-pgcl.cpp

@ -18,7 +18,8 @@
#include "storm-pgcl/settings/modules/PGCLSettings.h" #include "storm-pgcl/settings/modules/PGCLSettings.h"
#include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/DebugSettings.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" #include "storm/utility/file.h"
@ -38,11 +39,13 @@ void initializeSettings() {
} }
void handleJani(storm::jani::Model& model) { void handleJani(storm::jani::Model& model) {
if (!storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
// For now, we have to have a jani file
storm::jani::JsonExporter::toStream(model, {}, std::cout);
auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
storm::converter::JaniConversionOptions options(jani);
storm::api::postprocessJani(model, options);
if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
storm::api::exportJaniToFile(model, {}, storm::settings::getModule<storm::settings::modules::PGCLSettings>().getWriteToJaniFilename());
} else { } else {
storm::jani::JsonExporter::toFile(model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
storm::api::printJaniToStream(model, {}, std::cout);
} }
} }

2
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. # Create storm-pgcl.
add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS}) 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 # installation
install(TARGETS storm-pgcl EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) install(TARGETS storm-pgcl EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)

7
src/storm-pgcl/settings/modules/PGCLSettings.cpp

@ -26,7 +26,7 @@ namespace storm {
PGCLSettings::PGCLSettings() : ModuleSettings(moduleName) { 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, 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, 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()); 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(); return this->getOption(pgclToJaniOptionName).getHasOptionBeenSet();
} }
std::string const& PGCLSettings::getWriteToJaniFilename() const {
return this->getOption(pgclToJaniOptionName).getArgumentByName("filename").getValueAsString();
}
bool PGCLSettings::isProgramGraphToDotSet() const { bool PGCLSettings::isProgramGraphToDotSet() const {
return this->getOption(programGraphToDotOptionName).getHasOptionBeenSet(); return this->getOption(programGraphToDotOptionName).getHasOptionBeenSet();
} }

5
src/storm-pgcl/settings/modules/PGCLSettings.h

@ -29,6 +29,11 @@ namespace storm {
*/ */
bool isToJaniSet() const; 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) * Whether the program graph should be drawn (dot output)
*/ */

Loading…
Cancel
Save