diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 9923330d0..4ded8bf55 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -3,6 +3,7 @@ #include "storm-dft/settings/DftSettings.h" #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/ResourceSettings.h" @@ -14,103 +15,106 @@ */ template void processOptions() { - // Start by setting some urgent options (log levels, resources, etc.) - storm::cli::setUrgentOptions(); + // Start by setting some urgent options (log levels, resources, etc.) + storm::cli::setUrgentOptions(); - storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); - storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); - storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); + storm::settings::modules::DftIOSettings const& dftIOSettings = storm::settings::getModule(); + storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); + storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); + storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); - } - // Build DFT from given file - std::shared_ptr> dft; - if (dftIOSettings.isDftJsonFileSet()) { - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); - dft = storm::api::loadDFTJson(dftIOSettings.getDftJsonFilename()); - } else { - STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); - dft = storm::api::loadDFTGalileo(dftIOSettings.getDftFilename()); - } + if (!dftIOSettings.isDftFileSet() && !dftIOSettings.isDftJsonFileSet()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); + } - if (dftIOSettings.isDisplayStatsSet()) { - std::cout << "=============DFT Statistics==============" << std::endl; - dft->writeStatsToStream(std::cout); - std::cout << "=========================================" << std::endl; - } + // Build DFT from given file + std::shared_ptr> dft; + if (dftIOSettings.isDftJsonFileSet()) { + STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename()); + dft = storm::api::loadDFTJson(dftIOSettings.getDftJsonFilename()); + } else { + STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename()); + dft = storm::api::loadDFTGalileo(dftIOSettings.getDftFilename()); + } - if (dftIOSettings.isExportToJson()) { - // Export to json - storm::api::exportDFTToJson(*dft, dftIOSettings.getExportJsonFilename()); - return; - } + if (dftIOSettings.isDisplayStatsSet()) { + std::cout << "=============DFT Statistics==============" << std::endl; + dft->writeStatsToStream(std::cout); + std::cout << "=========================================" << std::endl; + } + + if (dftIOSettings.isExportToJson()) { + // Export to json + storm::api::exportDFTToJson(*dft, dftIOSettings.getExportJsonFilename()); + return; + } + + if (dftGspnSettings.isTransformToGspn()) { + // Transform to GSPN + storm::api::transformToGSPN(*dft); + return; + } - if (dftIOSettings.isTransformToGspn()) { - // Transform to GSPN - storm::api::transformToGSPN(*dft); - return; - } - #ifdef STORM_HAVE_Z3 - if (faultTreeSettings.solveWithSMT()) { - // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); - storm::api::exportDFTToSMT(*dft, "test.smt2"); - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only exported to SMT file 'test.smt2' but analysis is not supported."); - return; - } + if (faultTreeSettings.solveWithSMT()) { + // Solve with SMT + STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + storm::api::exportDFTToSMT(*dft, "test.smt2"); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only exported to SMT file 'test.smt2' but analysis is not supported."); + return; + } #endif - - // Set min or max - std::string optimizationDirection = "min"; - if (dftIOSettings.isComputeMaximalValue()) { - STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); - optimizationDirection = "max"; - } - - // Construct properties to analyse - std::vector properties; - if (ioSettings.isPropertySet()) { - properties.push_back(ioSettings.getProperty()); - } - if (dftIOSettings.usePropExpectedTime()) { - properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); - } - if (dftIOSettings.usePropProbability()) { - properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); - } - if (dftIOSettings.usePropTimebound()) { + + // Set min or max + std::string optimizationDirection = "min"; + if (dftIOSettings.isComputeMaximalValue()) { + STORM_LOG_THROW(!dftIOSettings.isComputeMinimalValue(), storm::exceptions::InvalidSettingsException, "Cannot compute minimal and maximal values at the same time."); + optimizationDirection = "max"; + } + + // Construct properties to analyse + std::vector properties; + if (ioSettings.isPropertySet()) { + properties.push_back(ioSettings.getProperty()); + } + if (dftIOSettings.usePropExpectedTime()) { + properties.push_back("T" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftIOSettings.usePropProbability()) { + properties.push_back("P" + optimizationDirection + "=? [F \"failed\"]"); + } + if (dftIOSettings.usePropTimebound()) { + std::stringstream stream; + stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]"; + properties.push_back(stream.str()); + } + if (dftIOSettings.usePropTimepoints()) { + for (double timepoint : dftIOSettings.getPropTimepoints()) { std::stringstream stream; - stream << "P" << optimizationDirection << "=? [F<=" << dftIOSettings.getPropTimebound() << " \"failed\"]"; + stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; properties.push_back(stream.str()); } - if (dftIOSettings.usePropTimepoints()) { - for (double timepoint : dftIOSettings.getPropTimepoints()) { - std::stringstream stream; - stream << "P" << optimizationDirection << "=? [F<=" << timepoint << " \"failed\"]"; - properties.push_back(stream.str()); - } - } - - // Build properties - STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidSettingsException, "No property given."); - std::string propString = properties[0]; - for (size_t i = 1; i < properties.size(); ++i) { - propString += ";" + properties[i]; - } - std::vector> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString)); - STORM_LOG_ASSERT(props.size() > 0, "No properties found."); + } - // Carry out the actual analysis - if (faultTreeSettings.isApproximationErrorSet()) { - // Approximate analysis - storm::api::analyzeDFTApprox(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), faultTreeSettings.getApproximationError(), true); - } else { - storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true); - } + // Build properties + STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidSettingsException, "No property given."); + std::string propString = properties[0]; + for (size_t i = 1; i < properties.size(); ++i) { + propString += ";" + properties[i]; + } + std::vector> props = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propString)); + STORM_LOG_ASSERT(props.size() > 0, "No properties found."); + + // Carry out the actual analysis + if (faultTreeSettings.isApproximationErrorSet()) { + // Approximate analysis + storm::api::analyzeDFTApprox(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), + faultTreeSettings.getApproximationError(), true); + } else { + storm::api::analyzeDFT(*dft, props, faultTreeSettings.useSymmetryReduction(), faultTreeSettings.useModularisation(), !faultTreeSettings.isDisableDC(), true); + } } /*! diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index f6b12a965..fb6994224 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -1,6 +1,7 @@ #include "storm-dft/api/storm-dft.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm-dft/settings/modules/DftGspnSettings.h" namespace storm { namespace api { @@ -29,13 +30,11 @@ namespace storm { template<> void transformToGSPN(storm::storage::DFT const& dft) { - // TODO make choosable - bool smart = true; - bool mergeDCFailed = true; + storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); + storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); // Set Don't Care elements std::set dontCareElements; - storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); if (!ftSettings.isDisableDC()) { // Insert all elements as Don't Care elements for (std::size_t i = 0; i < dft.nrElements(); i++) { @@ -46,7 +45,7 @@ namespace storm { // Transform to GSPN storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); auto priorities = gspnTransformator.computePriorities(); - gspnTransformator.transform(priorities, dontCareElements, smart, mergeDCFailed); + gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed()); storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); @@ -55,7 +54,7 @@ namespace storm { std::shared_ptr const& exprManager = gspn->getExpressionManager(); storm::builder::JaniGSPNBuilder builder(*gspn); - storm::jani::Model* model = builder.build(); + storm::jani::Model* model = builder.build(); storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index 361ccdc8f..0b98c5373 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -2,6 +2,7 @@ #include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" +#include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" @@ -33,6 +34,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-dft/settings/modules/DftGspnSettings.cpp b/src/storm-dft/settings/modules/DftGspnSettings.cpp new file mode 100644 index 000000000..952d127f0 --- /dev/null +++ b/src/storm-dft/settings/modules/DftGspnSettings.cpp @@ -0,0 +1,52 @@ +#include "DftGspnSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/SettingMemento.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" +#include "storm/exceptions/InvalidSettingsException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string DftGspnSettings::moduleName = "dftGspn"; + const std::string DftGspnSettings::transformToGspnOptionName = "to-gspn"; + const std::string DftGspnSettings::disableSmartTransformationOptionName = "disable-smart"; + const std::string DftGspnSettings::mergeDCFailedOptionName = "merge-dc-failed"; + + + DftGspnSettings::DftGspnSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, disableSmartTransformationOptionName, false, "Disable smart transformation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, mergeDCFailedOptionName, false, "Enable merging of Don't Care and Failed places into a combined place.").build()); + } + + bool DftGspnSettings::isTransformToGspn() const { + return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); + } + + bool DftGspnSettings::isDisableSmartTransformation() const { + return this->getOption(disableSmartTransformationOptionName).getHasOptionBeenSet(); + } + + bool DftGspnSettings::isMergeDCFailed() const { + return this->getOption(mergeDCFailedOptionName).getHasOptionBeenSet(); + } + + void DftGspnSettings::finalize() { + } + + bool DftGspnSettings::check() const { + // Ensure that GSPN option is set if other options are set. + STORM_LOG_THROW(isTransformToGspn() || (!isDisableSmartTransformation() && !isMergeDCFailed()), storm::exceptions::InvalidSettingsException, + "GSPN transformation should be enabled when giving options for the transformation."); + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm + diff --git a/src/storm-dft/settings/modules/DftGspnSettings.h b/src/storm-dft/settings/modules/DftGspnSettings.h new file mode 100644 index 000000000..784438f0d --- /dev/null +++ b/src/storm-dft/settings/modules/DftGspnSettings.h @@ -0,0 +1,58 @@ +#pragma once + +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the settings for operations concerning the DFT to GSPN transformation. + */ + class DftGspnSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of DFT-GSPN settings. + */ + DftGspnSettings(); + + /*! + * Retrieves whether the DFT should be transformed into a GSPN. + * + * @return True iff the option was set. + */ + bool isTransformToGspn() const; + + /*! + * Retrieves whether the smart transformation should be disabled. + * + * @return True if the smart transformation should be disabled. + */ + bool isDisableSmartTransformation() const; + + /*! + * Retrieves whether the DC and failed place should be merged. + * + * @return True if the merge of DC and failed place is enabled. + */ + bool isMergeDCFailed() const; + + bool check() const override; + + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + private: + // Define the string names of the options as constants. + static const std::string transformToGspnOptionName; + static const std::string disableSmartTransformationOptionName; + static const std::string mergeDCFailedOptionName; + + }; + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp index 8704cd036..2c4caeb8e 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.cpp +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -11,7 +11,7 @@ namespace storm { namespace settings { namespace modules { - + const std::string DftIOSettings::moduleName = "dftIO"; const std::string DftIOSettings::dftFileOptionName = "dftfile"; const std::string DftIOSettings::dftFileOptionShortName = "dft"; @@ -24,32 +24,45 @@ namespace storm { const std::string DftIOSettings::propTimepointsOptionName = "timepoints"; const std::string DftIOSettings::minValueOptionName = "min"; const std::string DftIOSettings::maxValueOptionName = "max"; - const std::string DftIOSettings::transformToGspnOptionName = "gspn"; const std::string DftIOSettings::exportToJsonOptionName = "export-json"; const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats"; DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.") + .addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName) - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.") + .addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.") + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.") + .addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()) + .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]") + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.") + .addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()) + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.") + .addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()) + .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.") + .addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build()); - } bool DftIOSettings::isDftFileSet() const { return this->getOption(dftFileOptionName).getHasOptionBeenSet(); } - + std::string DftIOSettings::getDftFilename() const { return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString(); } @@ -65,11 +78,11 @@ namespace storm { bool DftIOSettings::usePropExpectedTime() const { return this->getOption(propExpectedTimeOptionName).getHasOptionBeenSet(); } - + bool DftIOSettings::usePropProbability() const { return this->getOption(propProbabilityOptionName).getHasOptionBeenSet(); } - + bool DftIOSettings::usePropTimebound() const { return this->getOption(propTimeboundOptionName).getHasOptionBeenSet(); } @@ -96,14 +109,10 @@ namespace storm { bool DftIOSettings::isComputeMinimalValue() const { return this->getOption(minValueOptionName).getHasOptionBeenSet(); } - + bool DftIOSettings::isComputeMaximalValue() const { return this->getOption(maxValueOptionName).getHasOptionBeenSet(); } - - bool DftIOSettings::isTransformToGspn() const { - return this->getOption(transformToGspnOptionName).getHasOptionBeenSet(); - } bool DftIOSettings::isExportToJson() const { return this->getOption(exportToJsonOptionName).getHasOptionBeenSet(); @@ -125,7 +134,7 @@ namespace storm { STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set."); return true; } - + } // namespace modules } // namespace settings } // namespace storm diff --git a/src/storm-dft/settings/modules/DftIOSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h index f57f9ed44..d99e6d970 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -101,13 +101,6 @@ namespace storm { */ bool isComputeMaximalValue() const; - /*! - * Retrieves whether the DFT should be transformed into a GSPN. - * - * @return True iff the option was set. - */ - bool isTransformToGspn() const; - /*! * Retrieves whether the export to Json file option was set. * @@ -148,7 +141,6 @@ namespace storm { static const std::string propTimepointsOptionName; static const std::string minValueOptionName; static const std::string maxValueOptionName; - static const std::string transformToGspnOptionName; static const std::string exportToJsonOptionName; static const std::string displayStatsOptionName;