From e5e6e1bd79d61a4c66a95868493589f9d0136efe Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 24 Jul 2018 10:55:01 +0200 Subject: [PATCH] worked on prism to jani converter --- src/storm-conv-cli/storm-conv.cpp | 568 +++--------------- src/storm-conv/api/storm-conv.h | 61 +- .../options/JaniConversionOptions.cpp | 11 + .../converter/options/JaniConversionOptions.h | 25 + .../options/PrismToJaniConverterOptions.cpp | 12 + .../options/PrismToJaniConverterOptions.h | 21 + src/storm-conv/settings/ConvSettings.cpp | 22 + src/storm-conv/settings/ConvSettings.h | 11 + .../modules/ConversionGeneralSettings.cpp | 77 +++ .../modules/ConversionGeneralSettings.h | 88 +++ .../modules/ConversionInputSettings.cpp | 82 +++ .../modules/ConversionInputSettings.h | 86 +++ .../modules/ConversionOutputSettings.cpp | 59 ++ .../modules/ConversionOutputSettings.h | 49 ++ .../settings/modules/JaniExportSettings.cpp | 3 +- .../settings/modules/JaniExportSettings.h | 0 16 files changed, 696 insertions(+), 479 deletions(-) create mode 100644 src/storm-conv/converter/options/JaniConversionOptions.cpp create mode 100644 src/storm-conv/converter/options/JaniConversionOptions.h create mode 100644 src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp create mode 100644 src/storm-conv/converter/options/PrismToJaniConverterOptions.h create mode 100644 src/storm-conv/settings/ConvSettings.cpp create mode 100644 src/storm-conv/settings/ConvSettings.h create mode 100644 src/storm-conv/settings/modules/ConversionGeneralSettings.cpp create mode 100644 src/storm-conv/settings/modules/ConversionGeneralSettings.h create mode 100644 src/storm-conv/settings/modules/ConversionInputSettings.cpp create mode 100644 src/storm-conv/settings/modules/ConversionInputSettings.h create mode 100644 src/storm-conv/settings/modules/ConversionOutputSettings.cpp create mode 100644 src/storm-conv/settings/modules/ConversionOutputSettings.h rename src/{storm => storm-conv}/settings/modules/JaniExportSettings.cpp (96%) rename src/{storm => storm-conv}/settings/modules/JaniExportSettings.h (100%) diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index badcb0212..97fbcdfaf 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -1,539 +1,157 @@ -#include "storm-pars/api/storm-pars.h" -#include "storm-pars/settings/ParsSettings.h" -#include "storm-pars/settings/modules/ParametricSettings.h" -#include "storm-pars/settings/modules/RegionSettings.h" +#include "storm-conv/api/storm-conv.h" #include "storm/settings/SettingsManager.h" +#include "storm-conv/settings/ConvSettings.h" +#include "storm-conv/settings/modules/ConversionGeneralSettings.h" +#include "storm-conv/settings/modules/ConversionInputSettings.h" +#include "storm-conv/settings/modules/ConversionOutputSettings.h" + #include "storm/api/storm.h" -#include "storm-cli-utilities/cli.h" -#include "storm-cli-utilities/model-handling.h" -#include "storm/models/ModelBase.h" -#include "storm/storage/SymbolicModelDescription.h" -#include "storm/utility/file.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/utility/initialize.h" -#include "storm/utility/Stopwatch.h" #include "storm/utility/macros.h" -#include "storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h" +#include "storm/storage/SymbolicModelDescription.h" -#include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/CoreSettings.h" -#include "storm/settings/modules/IOSettings.h" -#include "storm/settings/modules/BisimulationSettings.h" -#include "storm/exceptions/BaseException.h" -#include "storm/exceptions/InvalidSettingsException.h" -#include "storm/exceptions/NotSupportedException.h" +#include "storm-cli-utilities/cli.h" namespace storm { - namespace pars { - - typedef typename storm::cli::SymbolicInput SymbolicInput; - - template - struct SampleInformation { - SampleInformation(bool graphPreserving = false, bool exact = false) : graphPreserving(graphPreserving), exact(exact) { - // Intentionally left empty. - } - - bool empty() const { - return cartesianProducts.empty(); - } - - std::vector::type, std::vector::type>>> cartesianProducts; - bool graphPreserving; - bool exact; - }; - - template - std::vector> parseRegions(std::shared_ptr const& model) { - std::vector> result; - auto regionSettings = storm::settings::getModule(); - if (regionSettings.isRegionSet()) { - result = storm::api::parseRegions(regionSettings.getRegionString(), *model); - } - return result; - } + namespace conv { - template - SampleInformation parseSamples(std::shared_ptr const& model, std::string const& sampleString, bool graphPreserving) { - STORM_LOG_THROW(!model || model->isSparseModel(), storm::exceptions::NotSupportedException, "Sampling is only supported for sparse models."); - - SampleInformation sampleInfo(graphPreserving); - if (sampleString.empty()) { - return sampleInfo; - } - - // Get all parameters from the model. - std::set::type> modelParameters; - auto const& sparseModel = *model->as>(); - modelParameters = storm::models::sparse::getProbabilityParameters(sparseModel); - auto rewParameters = storm::models::sparse::getRewardParameters(sparseModel); - modelParameters.insert(rewParameters.begin(), rewParameters.end()); - - std::vector cartesianProducts; - boost::split(cartesianProducts, sampleString, boost::is_any_of(";")); - for (auto& product : cartesianProducts) { - boost::trim(product); - - // Get the values string for each variable. - std::vector valuesForVariables; - boost::split(valuesForVariables, product, boost::is_any_of(",")); - for (auto& values : valuesForVariables) { - boost::trim(values); - } - - std::set::type> encounteredParameters; - sampleInfo.cartesianProducts.emplace_back(); - auto& newCartesianProduct = sampleInfo.cartesianProducts.back(); - for (auto const& varValues : valuesForVariables) { - auto equalsPosition = varValues.find("="); - STORM_LOG_THROW(equalsPosition != varValues.npos, storm::exceptions::WrongFormatException, "Incorrect format of samples."); - std::string variableName = varValues.substr(0, equalsPosition); - boost::trim(variableName); - std::string values = varValues.substr(equalsPosition + 1); - boost::trim(values); - - bool foundParameter = false; - typename utility::parametric::VariableType::type theParameter; - for (auto const& parameter : modelParameters) { - std::stringstream parameterStream; - parameterStream << parameter; - if (parameterStream.str() == variableName) { - foundParameter = true; - theParameter = parameter; - encounteredParameters.insert(parameter); - } - } - STORM_LOG_THROW(foundParameter, storm::exceptions::WrongFormatException, "Unknown parameter '" << variableName << "'."); - - std::vector splitValues; - boost::split(splitValues, values, boost::is_any_of(":")); - STORM_LOG_THROW(!splitValues.empty(), storm::exceptions::WrongFormatException, "Expecting at least one value per parameter."); - - auto& list = newCartesianProduct[theParameter]; - - for (auto& value : splitValues) { - boost::trim(value); - list.push_back(storm::utility::convertNumber::type>(value)); - } - } - - STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples."); - } - - return sampleInfo; - } - - template - std::pair, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { - auto generalSettings = storm::settings::getModule(); - auto bisimulationSettings = storm::settings::getModule(); - auto parametricSettings = storm::settings::getModule(); - - std::pair, bool> result = std::make_pair(model, false); - - if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { - result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as>()); - result.second = true; - } + void setUrgentOptions() { - if (generalSettings.isBisimulationSet()) { - result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as>(), input, bisimulationSettings); - result.second = true; - } - - if (parametricSettings.transformContinuousModel() && (result.first->isOfType(storm::models::ModelType::Ctmc) || result.first->isOfType(storm::models::ModelType::MarkovAutomaton))) { - result.first = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*result.first->template as>()), storm::api::extractFormulasFromProperties(input.properties)); - result.second = true; - } - - return result; - } - - template - std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { - - std::pair, bool> result = std::make_pair(model, false); - - auto coreSettings = storm::settings::getModule(); - if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) { - // Currently, hybrid engine for parametric models just referrs to building the model symbolically. - STORM_LOG_INFO("Translating symbolic model to sparse model..."); - result.first = storm::api::transformSymbolicToSparseModel(model); - result.second = true; - // Invoke preprocessing on the sparse model - auto sparsePreprocessingResult = storm::pars::preprocessSparseModel(result.first->as>(), input); - if (sparsePreprocessingResult.second) { - result.first = sparsePreprocessingResult.first; - } - } - return result; - } - - template - std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { - storm::utility::Stopwatch preprocessingWatch(true); - - std::pair, bool> result = std::make_pair(model, false); - if (model->isSparseModel()) { - result = storm::pars::preprocessSparseModel(result.first->as>(), input); + // Set the correct log level + if (storm::settings::getModule().isStdOutOutputEnabled()) { + storm::utility::setLogLevel(l3pp::LogLevel::OFF); } else { - STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - result = storm::pars::preprocessDdModel(result.first->as>(), input); - } - - if (result.second) { - STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl); - } - return result; - } - - template - void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr, storm::utility::parametric::Valuation const* valuation = nullptr) { - if (result) { - STORM_PRINT_AND_LOG("Result (initial states)"); - if (valuation) { - bool first = true; - std::stringstream ss; - for (auto const& entry : *valuation) { - if (!first) { - ss << ", "; - } else { - first = false; - } - ss << entry.first << "=" << entry.second; - } - - STORM_PRINT_AND_LOG(" for instance [" << ss.str() << "]"); + auto const& general = storm::settings::getModule(); + if (general.isVerboseSet()) { + storm::utility::setLogLevel(l3pp::LogLevel::INFO); } - STORM_PRINT_AND_LOG(": ") - - auto const* regionCheckResult = dynamic_cast const*>(result.get()); - if (regionCheckResult != nullptr) { - auto regionSettings = storm::settings::getModule(); - std::stringstream outStream; - if (regionSettings.isPrintFullResultSet()) { - regionCheckResult->writeToStream(outStream); - } else { - regionCheckResult->writeCondensedToStream(outStream); - } - outStream << std::endl; - if (!regionSettings.isPrintNoIllustrationSet()) { - auto const* regionRefinementCheckResult = dynamic_cast const*>(regionCheckResult); - if (regionRefinementCheckResult != nullptr) { - regionRefinementCheckResult->writeIllustrationToStream(outStream); - } - } - outStream << std::endl; - STORM_PRINT_AND_LOG(outStream.str()); - } else { - STORM_PRINT_AND_LOG(*result << std::endl); + if (general.isDebugOutputSet()) { + storm::utility::setLogLevel(l3pp::LogLevel::DEBUG); } - if (watch) { - STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl << std::endl); + if (general.isTraceOutputSet()) { + storm::utility::setLogLevel(l3pp::LogLevel::TRACE); } - } else { - STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); } } - template - void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback) { - for (auto const& property : properties) { - storm::cli::printModelCheckingProperty(property); - storm::utility::Stopwatch watch(true); - std::unique_ptr result = verificationCallback(property.getRawFormula()); - watch.stop(); - printInitialStatesResult(result, property, &watch); - postprocessingCallback(result); - } - } - - template class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double> - void verifyPropertiesAtSamplePoints(ModelType const& model, SymbolicInput const& input, SampleInformation const& samples) { + void processPrismInputJaniOutput(storm::prism::Program const& prismProg, std::vector const& properties) { - // When samples are provided, we create an instantiation model checker. - ModelCheckerType modelchecker(model); - - for (auto const& property : input.properties) { - storm::cli::printModelCheckingProperty(property); - - modelchecker.specifyFormula(storm::api::createTask(property.getRawFormula(), true)); - modelchecker.setInstantiationsAreGraphPreserving(samples.graphPreserving); - - storm::utility::parametric::Valuation valuation; - - std::vector::type> parameters; - std::vector::type>::const_iterator> iterators; - std::vector::type>::const_iterator> iteratorEnds; - - storm::utility::Stopwatch watch(true); - for (auto const& product : samples.cartesianProducts) { - parameters.clear(); - iterators.clear(); - iteratorEnds.clear(); - - for (auto const& entry : product) { - parameters.push_back(entry.first); - iterators.push_back(entry.second.cbegin()); - iteratorEnds.push_back(entry.second.cend()); - } - - bool done = false; - while (!done) { - // Read off valuation. - for (uint64_t i = 0; i < parameters.size(); ++i) { - valuation[parameters[i]] = *iterators[i]; - } - - storm::utility::Stopwatch valuationWatch(true); - std::unique_ptr result = modelchecker.check(Environment(), valuation); - valuationWatch.stop(); - - if (result) { - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates())); - } - printInitialStatesResult(result, property, &valuationWatch, &valuation); - - for (uint64_t i = 0; i < parameters.size(); ++i) { - ++iterators[i]; - if (iterators[i] == iteratorEnds[i]) { - // Reset iterator and proceed to move next iterator. - iterators[i] = product.at(parameters[i]).cbegin(); - - // If the last iterator was removed, we are done. - if (i == parameters.size() - 1) { - done = true; - } - } else { - // If an iterator was moved but not reset, we have another valuation to check. - break; - } - } - - } - } - - watch.stop(); - STORM_PRINT_AND_LOG("Overall time for sampling all instances: " << watch << std::endl << std::endl); - } - } - - template - void verifyPropertiesAtSamplePoints(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { - if (model->isOfType(storm::models::ModelType::Dtmc)) { - verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); - } else if (model->isOfType(storm::models::ModelType::Ctmc)) { - verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); - } else if (model->isOfType(storm::models::ModelType::Ctmc)) { - verifyPropertiesAtSamplePoints, ValueType, SolveValueType>(*model->template as>(), input, samples); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs."); - } - } - - template - void verifyPropertiesWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, SampleInformation const& samples) { + storm::converter::PrismToJaniConverterOptions options; + options.allVariablesGlobal = true; + // TODO: fill in options + auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options); + - if (samples.empty()) { - verifyProperties(input.properties, - [&model] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formula, true)); - if (result) { - result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - } - return result; - }, - [&model] (std::unique_ptr const& result) { - auto parametricSettings = storm::settings::getModule(); - if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) { - auto dtmc = model->template as>(); - boost::optional rationalFunction = result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]; - storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector(*dtmc), parametricSettings.exportResultPath()); - } - }); - } else { - STORM_LOG_TRACE("Sampling the model at given points."); - - if (samples.exact) { - verifyPropertiesAtSamplePoints(model, input, samples); - } else { - verifyPropertiesAtSamplePoints(model, input, samples); + auto const& output = storm::settings::getModule(); + auto const& input = storm::settings::getModule(); + std::string outputFilename = ""; + if (output.isJaniOutputFilenameSet()) { + outputFilename = output.getJaniOutputFilename(); + } else if (input.isPrismInputSet() && !output.isStdOutOutputEnabled()) { + std::string suffix = ""; + if (input.isConstantsSet()) { + suffix = input.getConstantDefinitionString(); + std::replace(suffix.begin(), suffix.end(), ',', '_'); } + suffix = suffix + ".jani"; + outputFilename = input.getPrismInputFilename() + suffix; } - } - - template - void verifyRegionsWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions) { - STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions."); - auto parametricSettings = storm::settings::getModule(); - auto regionSettings = storm::settings::getModule(); - - std::function(std::shared_ptr const& formula)> verificationCallback; - std::function const&)> postprocessingCallback; - - STORM_PRINT_AND_LOG(std::endl); - if (regionSettings.isHypothesisSet()) { - STORM_PRINT_AND_LOG("Checking hypothesis " << regionSettings.getHypothesis() << " on "); - } else { - STORM_PRINT_AND_LOG("Analyzing "); + if (outputFilename != "") { + storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename); } - if (regions.size() == 1) { - STORM_PRINT_AND_LOG("parameter region " << regions.front()); - } else { - STORM_PRINT_AND_LOG(regions.size() << " parameter regions"); - } - auto engine = regionSettings.getRegionCheckEngine(); - STORM_PRINT_AND_LOG(" using " << engine); - - // Check the given set of regions with or without refinement - if (regionSettings.isRefineSet()) { - STORM_LOG_THROW(regions.size() == 1, storm::exceptions::NotSupportedException, "Region refinement is not supported for multiple initial regions."); - STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getCoverageThreshold()) * 100.0 << "% is covered." << (regionSettings.isDepthLimitSet() ? " Depth limit is " + std::to_string(regionSettings.getDepthLimit()) + "." : "") << std::endl); - verificationCallback = [&] (std::shared_ptr const& formula) { - ValueType refinementThreshold = storm::utility::convertNumber(regionSettings.getCoverageThreshold()); - boost::optional optionalDepthLimit; - if (regionSettings.isDepthLimitSet()) { - optionalDepthLimit = regionSettings.getDepthLimit(); - } - std::unique_ptr> result = storm::api::checkAndRefineRegionWithSparseEngine(model, storm::api::createTask(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis()); - return result; - }; - } else { - STORM_PRINT_AND_LOG("." << std::endl); - verificationCallback = [&] (std::shared_ptr const& formula) { - std::unique_ptr result = storm::api::checkRegionsWithSparseEngine(model, storm::api::createTask(formula, true), regions, engine, regionSettings.getHypothesis()); - return result; - }; - } - - postprocessingCallback = [&] (std::unique_ptr const& result) { - if (parametricSettings.exportResultToFile()) { - storm::api::exportRegionCheckResultToFile(result, parametricSettings.exportResultPath()); - } - }; - verifyProperties(input.properties, verificationCallback, postprocessingCallback); - } - - template - void verifyWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { - if (regions.empty()) { - storm::pars::verifyPropertiesWithSparseEngine(model, input, samples); - } else { - storm::pars::verifyRegionsWithSparseEngine(model, input, regions); + if (output.isStdOutOutputEnabled()) { + storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout); } } - template - void verifyParametricModel(std::shared_ptr const& model, SymbolicInput const& input, std::vector> const& regions, SampleInformation const& samples) { - STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type."); - storm::pars::verifyWithSparseEngine(model->as>(), input, regions, samples); - } - - template - void processInputWithValueTypeAndDdlib(SymbolicInput& input) { - auto coreSettings = storm::settings::getModule(); - auto ioSettings = storm::settings::getModule(); + void processPrismInput() { + auto const& input = storm::settings::getModule(); - auto buildSettings = storm::settings::getModule(); - auto parSettings = storm::settings::getModule(); - - auto engine = coreSettings.getEngine(); - STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models."); - - std::shared_ptr model; - if (!buildSettings.isNoBuildModelSet()) { - model = storm::cli::buildModel(engine, input, ioSettings); - } - - if (model) { - model->printModelInformationToStream(std::cout); - } - - STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); - - if (model) { - auto preprocessingResult = storm::pars::preprocessModel(model, input); - if (preprocessingResult.second) { - model = preprocessingResult.first; - model->printModelInformationToStream(std::cout); - } + // Parse the prism program + storm::storage::SymbolicModelDescription prismProg = storm::api::parseProgram(input.getPrismInputFilename(), input.isPrismCompatibilityEnabled()); + + // Parse properties (if available) + std::vector properties; + if (input.isPropertyInputSet()) { + boost::optional> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter()); + properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), prismProg, propertyFilter); } - std::vector> regions = parseRegions(model); - std::string samplesAsString = parSettings.getSamples(); - SampleInformation samples; - if (!samplesAsString.empty()) { - samples = parseSamples(model, samplesAsString, parSettings.isSamplesAreGraphPreservingSet()); - samples.exact = parSettings.isSampleExactSet(); + // Substitute constant definitions in program and properties. + std::string constantDefinitionString = input.getConstantDefinitionString(); + auto constantDefinitions = prismProg.parseConstantDefinitions(constantDefinitionString); + prismProg = prismProg.preprocess(constantDefinitions); + if (!properties.empty()) { + properties = storm::api::substituteConstantsInProperties(properties, constantDefinitions); } - if (model) { - storm::cli::exportModel(model, input); - } - - if (parSettings.onlyObtainConstraints()) { - STORM_LOG_THROW(parSettings.exportResultToFile(), storm::exceptions::InvalidSettingsException, "When computing constraints, export path has to be specified."); - storm::api::exportParametricResultToFile(boost::none, storm::analysis::ConstraintCollector(*(model->as>())), parSettings.exportResultPath()); - return; - } - - if (model) { - verifyParametricModel(model, input, regions, samples); + // Branch on the type of output + auto const& output = storm::settings::getModule(); + if (output.isJaniOutputSet()) { + processPrismInputJaniOutput(prismProg.asPrismProgram(), properties); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "There is either no outputformat specified or the provided combination of input and output format is not compatible."); } } void processOptions() { - // Start by setting some urgent options (log levels, resources, etc.) - storm::cli::setUrgentOptions(); - - // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) - SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(); + // Start by setting some urgent options (log levels, etc.) + setUrgentOptions(); - auto coreSettings = storm::settings::getModule(); - auto engine = coreSettings.getEngine(); - STORM_LOG_WARN_COND(engine != storm::settings::modules::CoreSettings::Engine::Dd || engine != storm::settings::modules::CoreSettings::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); - - processInputWithValueTypeAndDdlib(symbolicInput); + // Branch on the type of input + auto const& input = storm::settings::getModule(); + if (input.isPrismInputSet()) { + processPrismInput(); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Could not find a supported input format."); + } } - } } /*! - * Main entry point of the executable storm-pars. + * Main entry point of the executable storm-conv. */ int main(const int argc, const char** argv) { try { storm::utility::setUp(); - storm::cli::printHeader("Storm-pars", argc, argv); - storm::settings::initializeParsSettings("Storm-pars", "storm-pars"); - - storm::utility::Stopwatch totalTimer(true); + + // Print header info only if output to sdtout is disabled + bool outputToStdOut = false; + for (int i = 1; i < argc; ++i) { + if (std::string(argv[i]) == "--" + storm::settings::modules::ConversionOutputSettings::stdoutOptionName) { + outputToStdOut = false; + } + } + if (outputToStdOut) { + storm::utility::setLogLevel(l3pp::LogLevel::OFF); + } else { + storm::cli::printHeader("Storm-conv", argc, argv); + } + + storm::settings::initializeConvSettings("Storm-conv", "storm-conv"); if (!storm::cli::parseOptions(argc, argv)) { return -1; } - storm::pars::processOptions(); - - totalTimer.stop(); - if (storm::settings::getModule().isPrintTimeAndMemorySet()) { - storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); - } + storm::conv::processOptions(); storm::utility::cleanUp(); return 0; } catch (storm::exceptions::BaseException const& exception) { - STORM_LOG_ERROR("An exception caused Storm-pars to terminate. The message of the exception is: " << exception.what()); + STORM_LOG_ERROR("An exception caused Storm-conv to terminate. The message of the exception is: " << exception.what()); return 1; } catch (std::exception const& exception) { - STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-pars to terminate. The message of this exception is: " << exception.what()); + STORM_LOG_ERROR("An unexpected exception occurred and caused Storm-conv to terminate. The message of this exception is: " << exception.what()); return 2; } } diff --git a/src/storm-conv/api/storm-conv.h b/src/storm-conv/api/storm-conv.h index a1a32ac05..6e05795a8 100644 --- a/src/storm-conv/api/storm-conv.h +++ b/src/storm-conv/api/storm-conv.h @@ -1,4 +1,61 @@ #pragma once -#include "storm-pars/api/region.h" -#include "storm-pars/api/export.h" \ No newline at end of file +#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 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 = std::vector(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions()) { + std::pair> res; + + // Perform conversion + auto modelAndRenaming = program.toJaniWithLabelRenaming(options.allVariablesGlobal, options.suffix); + 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/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp new file mode 100644 index 000000000..8e9ba344d --- /dev/null +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -0,0 +1,11 @@ +#include "storm-conv/converter/options/PrismToJaniConverterOptions.h" + +namespace storm { + namespace converter { + + JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), exportFlattened(false) { + // Intentionally left empty + }; + } +} + diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h new file mode 100644 index 000000000..ddd0d88cc --- /dev/null +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -0,0 +1,25 @@ +#pragma once + +#include +#include + +namespace storm { + namespace converter { + + struct JaniConversionOptions { + + JaniConversionOptions(); + + /// (Automaton,Variable)-pairs that will be transformed to location variables of the respective automaton. + std::vector> locationVariables; + + /// If set, the model will be made standard compliant (e.g. no state rewards for discrete time models) + bool standardCompliant; + + /// If set, the model is transformed into a single automaton + bool exportFlattened; + + }; + } +} + diff --git a/src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp b/src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp new file mode 100644 index 000000000..a64f9edbc --- /dev/null +++ b/src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp @@ -0,0 +1,12 @@ +#include "storm-conv/converter/options/PrismToJaniConverterOptions.h" + + +namespace storm { + namespace converter { + + PrismToJaniConverterOptions::PrismToJaniConverterOptions() : allVariablesGlobal(false), suffix("") { + // Intentionally left empty + }; + } +} + diff --git a/src/storm-conv/converter/options/PrismToJaniConverterOptions.h b/src/storm-conv/converter/options/PrismToJaniConverterOptions.h new file mode 100644 index 000000000..0d3d02c85 --- /dev/null +++ b/src/storm-conv/converter/options/PrismToJaniConverterOptions.h @@ -0,0 +1,21 @@ +#pragma once + +#include +#include "storm-conv/converter/options/JaniConversionOptions.h" + + +namespace storm { + namespace converter { + + + struct PrismToJaniConverterOptions { + + PrismToJaniConverterOptions(); + + bool allVariablesGlobal; + std::string suffix; + JaniConversionOptions janiOptions; + }; + } +} + diff --git a/src/storm-conv/settings/ConvSettings.cpp b/src/storm-conv/settings/ConvSettings.cpp new file mode 100644 index 000000000..0582b80d8 --- /dev/null +++ b/src/storm-conv/settings/ConvSettings.cpp @@ -0,0 +1,22 @@ +#include "storm-conv/settings/ConvSettings.h" + +#include "storm-conv/settings/modules/ConversionGeneralSettings.h" +#include "storm-conv/settings/modules/ConversionInputSettings.h" +#include "storm-conv/settings/modules/ConversionOutputSettings.h" + +#include "storm/settings/SettingsManager.h" + + +namespace storm { + namespace settings { + void initializeParsSettings(std::string const& name, std::string const& executableName) { + storm::settings::mutableManager().setName(name, executableName); + + // Register relevant settings modules. + storm::settings::addModule(); + storm::settings::addModule(); + storm::settings::addModule(); + } + + } +} diff --git a/src/storm-conv/settings/ConvSettings.h b/src/storm-conv/settings/ConvSettings.h new file mode 100644 index 000000000..21cbcab31 --- /dev/null +++ b/src/storm-conv/settings/ConvSettings.h @@ -0,0 +1,11 @@ +#pragma once + +#include + +namespace storm { + namespace settings { + + void initializeConvSettings(std::string const& name, std::string const& executableName); + + } +} \ No newline at end of file diff --git a/src/storm-conv/settings/modules/ConversionGeneralSettings.cpp b/src/storm-conv/settings/modules/ConversionGeneralSettings.cpp new file mode 100644 index 000000000..4f1c65e74 --- /dev/null +++ b/src/storm-conv/settings/modules/ConversionGeneralSettings.cpp @@ -0,0 +1,77 @@ +#include "storm-conv/settings/modules/ConversionGeneralSettings.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/settings/Argument.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string ConversionGeneralSettings::moduleName = "general"; + const std::string ConversionGeneralSettings::helpOptionName = "help"; + const std::string ConversionGeneralSettings::helpOptionShortName = "h"; + const std::string ConversionGeneralSettings::versionOptionName = "version"; + const std::string ConversionGeneralSettings::verboseOptionName = "verbose"; + const std::string ConversionGeneralSettings::verboseOptionShortName = "v"; + const std::string ConversionGeneralSettings::debugOptionName = "debug"; + const std::string ConversionGeneralSettings::traceOptionName = "trace"; + const std::string ConversionGeneralSettings::configOptionName = "config"; + const std::string ConversionGeneralSettings::configOptionShortName = "c"; + + ConversionGeneralSettings::ConversionGeneralSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint", "A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, versionOptionName, false, "Prints the version information.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, verboseOptionName, false, "Enables more verbose output.").setShortName(verboseOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, false, "Enables verbose and debug output.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, traceOptionName, false, "Enables verbose and debug and trace output.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + } + + bool ConversionGeneralSettings::isHelpSet() const { + return this->getOption(helpOptionName).getHasOptionBeenSet(); + } + + bool ConversionGeneralSettings::isVersionSet() const { + return this->getOption(versionOptionName).getHasOptionBeenSet(); + } + + std::string ConversionGeneralSettings::getHelpModuleName() const { + return this->getOption(helpOptionName).getArgumentByName("hint").getValueAsString(); + } + + bool ConversionGeneralSettings::isVerboseSet() const { + return this->getOption(verboseOptionName).getHasOptionBeenSet(); + } + + bool ConversionGeneralSettings::isDebugOutputSet() const { + return this->getOption(debugOptionName).getHasOptionBeenSet(); + } + + bool ConversionGeneralSettings::isTraceOutputSet() const { + return this->getOption(traceOptionName).getHasOptionBeenSet(); + } + + bool ConversionGeneralSettings::isConfigSet() const { + return this->getOption(configOptionName).getHasOptionBeenSet(); + } + + std::string ConversionGeneralSettings::getConfigFilename() const { + return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString(); + } + + void ConversionGeneralSettings::finalize() { + // Intentionally left empty. + } + + bool ConversionGeneralSettings::check() const { + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-conv/settings/modules/ConversionGeneralSettings.h b/src/storm-conv/settings/modules/ConversionGeneralSettings.h new file mode 100644 index 000000000..dc7e79f27 --- /dev/null +++ b/src/storm-conv/settings/modules/ConversionGeneralSettings.h @@ -0,0 +1,88 @@ +#pragma once +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + class ConversionGeneralSettings : public ModuleSettings { + public: + + ConversionGeneralSettings(); + + /*! + * Retrieves whether the help option was set. + * + * @return True if the help option was set. + */ + bool isHelpSet() const; + + /*! + * Retrieves whether the version option was set. + * + * @return True if the version option was set. + */ + bool isVersionSet() const; + + /*! + * Retrieves the name of the module for which to show the help or "all" to indicate that the full help + * needs to be shown. + * + * @return The name of the module for which to show the help or "all". + */ + std::string getHelpModuleName() const; + + /*! + * Retrieves whether the verbose option was set. + * + * @return True if the verbose option was set. + */ + bool isVerboseSet() const; + + /*! + * Retrieves whether the debug output option was set. + * + */ + bool isDebugOutputSet() const; + + /*! + * Retrieves whether the trace output option was set. + * + */ + bool isTraceOutputSet() const; + + /*! + * Retrieves whether the config option was set. + * + * @return True if the config option was set. + */ + bool isConfigSet() const; + + /*! + * Retrieves the name of the file that is to be scanned for settings. + * + * @return The name of the file that is to be scanned for settings. + */ + std::string getConfigFilename() 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 helpOptionName; + static const std::string helpOptionShortName; + static const std::string versionOptionName; + static const std::string verboseOptionName; + static const std::string verboseOptionShortName; + static const std::string debugOptionName; + static const std::string traceOptionName; + static const std::string configOptionName; + static const std::string configOptionShortName; + }; + } + } +} \ No newline at end of file diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.cpp b/src/storm-conv/settings/modules/ConversionInputSettings.cpp new file mode 100644 index 000000000..e608aa0f3 --- /dev/null +++ b/src/storm-conv/settings/modules/ConversionInputSettings.cpp @@ -0,0 +1,82 @@ +#include "storm-conv/settings/modules/ConversionInputSettings.h" + +#include "storm/settings/SettingsManager.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 ConversionInputSettings::moduleName = "input"; + const std::string ConversionInputSettings::propertyOptionName = "prop"; + const std::string ConversionInputSettings::propertyOptionShortName = "prop"; + const std::string ConversionInputSettings::constantsOptionName = "constants"; + const std::string ConversionInputSettings::constantsOptionShortName = "const"; + const std::string ConversionInputSettings::prismInputOptionName = "prism"; + const std::string ConversionInputSettings::prismCompatibilityOptionName = "prismcompat"; + const std::string ConversionInputSettings::prismCompatibilityOptionShortName = "pc"; + + + ConversionInputSettings::ConversionInputSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build()) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build()) + .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + ").").setShortName(constantsOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, prismInputOptionName, false, "Parses the model given in the PRISM format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); + } + + bool ConversionInputSettings::isPrismInputSet() const { + return this->getOption(prismInputOptionName).getHasOptionBeenSet(); + } + + std::string ConversionInputSettings::getPrismInputFilename() const { + return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool ConversionInputSettings::isPrismCompatibilityEnabled() const { + return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); + } + + bool ConversionInputSettings::isConstantsSet() const { + return this->getOption(constantsOptionName).getHasOptionBeenSet(); + } + + std::string ConversionInputSettings::getConstantDefinitionString() const { + return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); + } + + bool ConversionInputSettings::isPropertyInputSet() const { + return this->getOption(propertyOptionName).getHasOptionBeenSet(); + } + + std::string ConversionInputSettings::getPropertyInput() const { + return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString(); + } + + std::string ConversionInputSettings::getPropertyInputFilter() const { + return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString(); + } + + void ConversionInputSettings::finalize() { + // Intentionally left empty. + } + + bool ConversionInputSettings::check() const { + // Ensure that exactly one input is specified + STORM_LOG_THROW(isPrismInputSet(), storm::exceptions::InvalidSettingsException, "No Input specified."); + return true; + } + + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-conv/settings/modules/ConversionInputSettings.h b/src/storm-conv/settings/modules/ConversionInputSettings.h new file mode 100644 index 000000000..41cf6549e --- /dev/null +++ b/src/storm-conv/settings/modules/ConversionInputSettings.h @@ -0,0 +1,86 @@ +#pragma once +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + class ConversionInputSettings : public ModuleSettings { + public: + + ConversionInputSettings(); + + /*! + * Retrieves whether the property option was set. + * + * @return True if the property option was set. + */ + bool isPropertyInputSet() const; + + /*! + * Retrieves the property specified with the property option. + * + * @return The property specified with the property option. + */ + std::string getPropertyInput() const; + + /*! + * Retrieves the property filter. + * + * @return The property filter. + */ + std::string getPropertyInputFilter() const; + + /*! + * Retrieves whether constant definition option was set. + * + * @return True if the constant definition option was set. + */ + bool isConstantsSet() const; + + /*! + * Retrieves the string that defines the constants of a symbolic model (given via the symbolic option). + * + * @return The string that defines the constants of a symbolic model. + */ + std::string getConstantDefinitionString() const; + + /*! + * Retrieves whether the PRISM language option was set. + */ + bool isPrismInputSet() const; + + /*! + * Retrieves the name of the file that contains the PRISM model specification if the model was given + * using the PRISM input option. + */ + std::string getPrismInputFilename() const; + + /*! + * Retrieves whether the PRISM compatibility mode was enabled. + * + * @return True iff the PRISM compatibility mode was enabled. + */ + bool isPrismCompatibilityEnabled() 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 propertyOptionName; + static const std::string propertyOptionShortName; + static const std::string constantsOptionName; + static const std::string constantsOptionShortName; + static const std::string prismInputOptionName; + static const std::string prismCompatibilityOptionName; + static const std::string prismCompatibilityOptionShortName; + }; + + + } + } +} \ No newline at end of file diff --git a/src/storm-conv/settings/modules/ConversionOutputSettings.cpp b/src/storm-conv/settings/modules/ConversionOutputSettings.cpp new file mode 100644 index 000000000..958bdfdd9 --- /dev/null +++ b/src/storm-conv/settings/modules/ConversionOutputSettings.cpp @@ -0,0 +1,59 @@ +#include "storm-conv/settings/modules/ConversionOutputSettings.h" + +#include "storm/settings/SettingsManager.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" +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string ConversionOutputSettings::moduleName = "output"; + const std::string ConversionOutputSettings::stdoutOptionName = "stdout"; + const std::string ConversionOutputSettings::janiOutputOptionName = "tojani"; + + ConversionOutputSettings::ConversionOutputSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, stdoutOptionName, false, "If set, the output will be printed to stdout.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, janiOutputOptionName, false, "converts the input model to Jani.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("")).build()); + } + + bool ConversionOutputSettings::isStdOutOutputEnabled() const { + return this->getOption(stdoutOptionName).getHasOptionBeenSet(); + } + + bool ConversionOutputSettings::isJaniOutputSet() const { + return this->getOption(janiOutputOptionName).getHasOptionBeenSet(); + } + + bool ConversionOutputSettings::isJaniOutputFilenameSet() const { + return isJaniOutputSet() + && !this->getOption(janiOutputOptionName).getArgumentByName("filename").wasSetFromDefaultValue() + && this->getOption(janiOutputOptionName).getArgumentByName("filename").getHasBeenSet() + && this->getOption(janiOutputOptionName).getArgumentByName("filename").getValueAsString() != ""; + } + + std::string ConversionOutputSettings::getJaniOutputFilename() const { + STORM_LOG_THROW(isJaniOutputFilenameSet(), storm::exceptions::InvalidOperationException, "Tried to get the jani output name although none was specified."); + return this->getOption(janiOutputOptionName).getArgumentByName("filename").getValueAsString(); + } + + void ConversionOutputSettings::finalize() { + // Intentionally left empty. + } + + bool ConversionOutputSettings::check() const { + // Ensure that exactly one Output is specified + STORM_LOG_THROW(isJaniOutputSet(), storm::exceptions::InvalidSettingsException, "No Output specified."); + STORM_LOG_THROW(!isJaniOutputFilenameSet() || ArgumentValidatorFactory::createWritableFileValidator()->isValid(getJaniOutputFilename()), storm::exceptions::InvalidSettingsException, "Unable to write at file " + getJaniOutputFilename()); + return true; + } + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm-conv/settings/modules/ConversionOutputSettings.h b/src/storm-conv/settings/modules/ConversionOutputSettings.h new file mode 100644 index 000000000..e429cdd93 --- /dev/null +++ b/src/storm-conv/settings/modules/ConversionOutputSettings.h @@ -0,0 +1,49 @@ +#pragma once +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + class ConversionOutputSettings : public ModuleSettings { + public: + + ConversionOutputSettings(); + + /*! + * Retrieves whether the output should be printed to stdout + */ + bool isStdOutOutputEnabled() const; + + /*! + * Retrieves whether the output should be in the Jani format + */ + bool isJaniOutputSet() const; + + /*! + * Retrieves whether an output filename for the jani file was specified + */ + bool isJaniOutputFilenameSet() const; + + /*! + * Retrieves the name of the jani output (if specified) + */ + std::string getJaniOutputFilename() const; + + bool check() const override; + void finalize() override; + + // The name of the module. + static const std::string moduleName; + // name of the option that enables output to stdout. It needs to be public because we have to check this option very early + static const std::string stdoutOptionName; + + private: + // Define the string names of the options as constants. + static const std::string janiOutputOptionName; + }; + + + } + } +} \ No newline at end of file diff --git a/src/storm/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp similarity index 96% rename from src/storm/settings/modules/JaniExportSettings.cpp rename to src/storm-conv/settings/modules/JaniExportSettings.cpp index a47a9914b..09e236431 100644 --- a/src/storm/settings/modules/JaniExportSettings.cpp +++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp @@ -26,8 +26,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, janiFileOptionName, false, "Destination for the jani model.").setShortName(janiFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list with local variables.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, true, "Export in standard compliant variant.").build()); - + this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, true, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build()); } bool JaniExportSettings::isJaniFileSet() const { diff --git a/src/storm/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h similarity index 100% rename from src/storm/settings/modules/JaniExportSettings.h rename to src/storm-conv/settings/modules/JaniExportSettings.h