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 <typename ValueType>
- struct SampleInformation {
- SampleInformation(bool graphPreserving = false, bool exact = false) : graphPreserving(graphPreserving), exact(exact) {
- // Intentionally left empty.
- }
-
- bool empty() const {
- return cartesianProducts.empty();
- }
-
- std::vector<std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>>> cartesianProducts;
- bool graphPreserving;
- bool exact;
- };
-
- template <typename ValueType>
- std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared_ptr<storm::models::ModelBase> const& model) {
- std::vector<storm::storage::ParameterRegion<ValueType>> result;
- auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
- if (regionSettings.isRegionSet()) {
- result = storm::api::parseRegions<ValueType>(regionSettings.getRegionString(), *model);
- }
- return result;
- }
+ namespace conv {
- template <typename ValueType>
- SampleInformation<ValueType> parseSamples(std::shared_ptr<storm::models::ModelBase> 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<ValueType> sampleInfo(graphPreserving);
- if (sampleString.empty()) {
- return sampleInfo;
- }
-
- // Get all parameters from the model.
- std::set<typename utility::parametric::VariableType<ValueType>::type> modelParameters;
- auto const& sparseModel = *model->as<storm::models::sparse::Model<ValueType>>();
- modelParameters = storm::models::sparse::getProbabilityParameters(sparseModel);
- auto rewParameters = storm::models::sparse::getRewardParameters(sparseModel);
- modelParameters.insert(rewParameters.begin(), rewParameters.end());
-
- std::vector<std::string> 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<std::string> valuesForVariables;
- boost::split(valuesForVariables, product, boost::is_any_of(","));
- for (auto& values : valuesForVariables) {
- boost::trim(values);
- }
-
- std::set<typename utility::parametric::VariableType<ValueType>::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<ValueType>::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<std::string> 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<typename utility::parametric::CoefficientType<ValueType>::type>(value));
- }
- }
-
- STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples.");
- }
-
- return sampleInfo;
- }
-
- template <typename ValueType>
- std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
- auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
- auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
- auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
-
- std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
-
- if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
- result.first = storm::cli::preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
- result.second = true;
- }
+ void setUrgentOptions() {
- if (generalSettings.isBisimulationSet()) {
- result.first = storm::cli::preprocessSparseModelBisimulation(result.first->template as<storm::models::sparse::Model<ValueType>>(), 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::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
- result.second = true;
- }
-
- return result;
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input) {
-
- std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
-
- auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
- 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<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
- if (sparsePreprocessingResult.second) {
- result.first = sparsePreprocessingResult.first;
- }
- }
- return result;
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- std::pair<std::shared_ptr<storm::models::ModelBase>, bool> preprocessModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
- storm::utility::Stopwatch preprocessingWatch(true);
-
- std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
- if (model->isSparseModel()) {
- result = storm::pars::preprocessSparseModel<ValueType>(result.first->as<storm::models::sparse::Model<ValueType>>(), input);
+ // Set the correct log level
+ if (storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>().isStdOutOutputEnabled()) {
+ storm::utility::setLogLevel(l3pp::LogLevel::OFF);
} else {
- STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
- result = storm::pars::preprocessDdModel<DdType, ValueType>(result.first->as<storm::models::symbolic::Model<DdType, ValueType>>(), input);
- }
-
- if (result.second) {
- STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
- }
- return result;
- }
-
- template<typename ValueType>
- void printInitialStatesResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr, storm::utility::parametric::Valuation<ValueType> 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<storm::settings::modules::ConversionGeneralSettings>();
+ if (general.isVerboseSet()) {
+ storm::utility::setLogLevel(l3pp::LogLevel::INFO);
}
- STORM_PRINT_AND_LOG(": ")
-
- auto const* regionCheckResult = dynamic_cast<storm::modelchecker::RegionCheckResult<ValueType> const*>(result.get());
- if (regionCheckResult != nullptr) {
- auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
- std::stringstream outStream;
- if (regionSettings.isPrintFullResultSet()) {
- regionCheckResult->writeToStream(outStream);
- } else {
- regionCheckResult->writeCondensedToStream(outStream);
- }
- outStream << std::endl;
- if (!regionSettings.isPrintNoIllustrationSet()) {
- auto const* regionRefinementCheckResult = dynamic_cast<storm::modelchecker::RegionRefinementCheckResult<ValueType> 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<typename ValueType>
- void verifyProperties(std::vector<storm::jani::Property> const& properties, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback) {
- for (auto const& property : properties) {
- storm::cli::printModelCheckingProperty(property);
- storm::utility::Stopwatch watch(true);
- std::unique_ptr<storm::modelchecker::CheckResult> result = verificationCallback(property.getRawFormula());
- watch.stop();
- printInitialStatesResult<ValueType>(result, property, &watch);
- postprocessingCallback(result);
- }
- }
-
- template<template<typename, typename> class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double>
- void verifyPropertiesAtSamplePoints(ModelType const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
+ void processPrismInputJaniOutput(storm::prism::Program const& prismProg, std::vector<storm::jani::Property> const& properties) {
- // When samples are provided, we create an instantiation model checker.
- ModelCheckerType<ModelType, SolveValueType> modelchecker(model);
-
- for (auto const& property : input.properties) {
- storm::cli::printModelCheckingProperty(property);
-
- modelchecker.specifyFormula(storm::api::createTask<ValueType>(property.getRawFormula(), true));
- modelchecker.setInstantiationsAreGraphPreserving(samples.graphPreserving);
-
- storm::utility::parametric::Valuation<ValueType> valuation;
-
- std::vector<typename utility::parametric::VariableType<ValueType>::type> parameters;
- std::vector<typename std::vector<typename utility::parametric::CoefficientType<ValueType>::type>::const_iterator> iterators;
- std::vector<typename std::vector<typename utility::parametric::CoefficientType<ValueType>::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<storm::modelchecker::CheckResult> result = modelchecker.check(Environment(), valuation);
- valuationWatch.stop();
-
- if (result) {
- result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates()));
- }
- printInitialStatesResult<ValueType>(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 <typename ValueType, typename SolveValueType = double>
- void verifyPropertiesAtSamplePoints(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
- if (model->isOfType(storm::models::ModelType::Dtmc)) {
- verifyPropertiesAtSamplePoints<storm::modelchecker::SparseDtmcInstantiationModelChecker, storm::models::sparse::Dtmc<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Dtmc<ValueType>>(), input, samples);
- } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
- verifyPropertiesAtSamplePoints<storm::modelchecker::SparseCtmcInstantiationModelChecker, storm::models::sparse::Ctmc<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), input, samples);
- } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
- verifyPropertiesAtSamplePoints<storm::modelchecker::SparseMdpInstantiationModelChecker, storm::models::sparse::Mdp<ValueType>, ValueType, SolveValueType>(*model->template as<storm::models::sparse::Mdp<ValueType>>(), input, samples);
- } else {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs.");
- }
- }
-
- template <typename ValueType>
- void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> 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<ValueType>(input.properties,
- [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
- std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
- if (result) {
- result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
- }
- return result;
- },
- [&model] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
- auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
- if (parametricSettings.exportResultToFile() && model->isOfType(storm::models::ModelType::Dtmc)) {
- auto dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
- boost::optional<ValueType> rationalFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
- storm::api::exportParametricResultToFile(rationalFunction, storm::analysis::ConstraintCollector<ValueType>(*dtmc), parametricSettings.exportResultPath());
- }
- });
- } else {
- STORM_LOG_TRACE("Sampling the model at given points.");
-
- if (samples.exact) {
- verifyPropertiesAtSamplePoints<ValueType, storm::RationalNumber>(model, input, samples);
- } else {
- verifyPropertiesAtSamplePoints<ValueType, double>(model, input, samples);
+ auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+ auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+ 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 <typename ValueType>
- void verifyRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions) {
- STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions.");
- auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
- auto regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
-
- std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> verificationCallback;
- std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> 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<storm::logic::Formula const> const& formula) {
- ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(regionSettings.getCoverageThreshold());
- boost::optional<uint64_t> optionalDepthLimit;
- if (regionSettings.isDepthLimitSet()) {
- optionalDepthLimit = regionSettings.getDepthLimit();
- }
- std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions.front(), engine, refinementThreshold, optionalDepthLimit, regionSettings.getHypothesis());
- return result;
- };
- } else {
- STORM_PRINT_AND_LOG("." << std::endl);
- verificationCallback = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {
- std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkRegionsWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions, engine, regionSettings.getHypothesis());
- return result;
- };
- }
-
- postprocessingCallback = [&] (std::unique_ptr<storm::modelchecker::CheckResult> const& result) {
- if (parametricSettings.exportResultToFile()) {
- storm::api::exportRegionCheckResultToFile<ValueType>(result, parametricSettings.exportResultPath());
- }
- };
- verifyProperties<ValueType>(input.properties, verificationCallback, postprocessingCallback);
- }
-
- template <typename ValueType>
- void verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> 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 <storm::dd::DdType DdType, typename ValueType>
- void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
- STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type.");
- storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
- }
-
- template <storm::dd::DdType DdType, typename ValueType>
- void processInputWithValueTypeAndDdlib(SymbolicInput& input) {
- auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
- auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+ void processPrismInput() {
+ auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
- auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
- auto parSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
-
- 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<storm::models::ModelBase> model;
- if (!buildSettings.isNoBuildModelSet()) {
- model = storm::cli::buildModel<DdType, ValueType>(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<DdType, ValueType>(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<storm::jani::Property> properties;
+ if (input.isPropertyInputSet()) {
+ boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(input.getPropertyInputFilter());
+ properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), prismProg, propertyFilter);
}
- std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
- std::string samplesAsString = parSettings.getSamples();
- SampleInformation<ValueType> samples;
- if (!samplesAsString.empty()) {
- samples = parseSamples<ValueType>(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<DdType, ValueType>(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<ValueType>(boost::none, storm::analysis::ConstraintCollector<ValueType>(*(model->as<storm::models::sparse::Model<ValueType>>())), parSettings.exportResultPath());
- return;
- }
-
- if (model) {
- verifyParametricModel<DdType, ValueType>(model, input, regions, samples);
+ // Branch on the type of output
+ auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+ 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<storm::settings::modules::CoreSettings>();
- 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<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput);
+ // Branch on the type of input
+ auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+ 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<storm::settings::modules::ResourceSettings>().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<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties = std::vector<storm::jani::Property>(), storm::converter::PrismToJaniConverterOptions options = storm::converter::PrismToJaniConverterOptions()) {
+ std::pair<storm::jani::Model, std::vector<storm::jani::Property>> 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<storm::jani::Property> const& properties, std::string const& filename) {
+ storm::jani::JsonExporter::toFile(model, properties, filename);
+ }
+
+ void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> 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 <string>
+#include <vector>
+
+namespace storm {
+ namespace converter {
+
+ struct JaniConversionOptions {
+
+ JaniConversionOptions();
+
+ /// (Automaton,Variable)-pairs that will be transformed to location variables of the respective automaton.
+ std::vector<std::pair<std::string, std::string>> 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 <string>
+#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::modules::ConversionGeneralSettings>();
+ storm::settings::addModule<storm::settings::modules::ConversionInputSettings>();
+ storm::settings::addModule<storm::settings::modules::ConversionOutputSettings>();
+ }
+
+ }
+}
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 <string>
+
+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