sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

worked on prism to jani converter

main
TimQu 7 years ago
parent
2e035f3957
commit
e5e6e1bd79
16 changed files with 696 additions and 479 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 558
      src/storm-conv-cli/storm-conv.cpp
  2. 61
      src/storm-conv/api/storm-conv.h
  3. 11
      src/storm-conv/converter/options/JaniConversionOptions.cpp
  4. 25
      src/storm-conv/converter/options/JaniConversionOptions.h
  5. 12
      src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp
  6. 21
      src/storm-conv/converter/options/PrismToJaniConverterOptions.h
  7. 22
      src/storm-conv/settings/ConvSettings.cpp
  8. 11
      src/storm-conv/settings/ConvSettings.h
  9. 77
      src/storm-conv/settings/modules/ConversionGeneralSettings.cpp
  10. 88
      src/storm-conv/settings/modules/ConversionGeneralSettings.h
  11. 82
      src/storm-conv/settings/modules/ConversionInputSettings.cpp
  12. 86
      src/storm-conv/settings/modules/ConversionInputSettings.h
  13. 59
      src/storm-conv/settings/modules/ConversionOutputSettings.cpp
  14. 49
      src/storm-conv/settings/modules/ConversionOutputSettings.h
  15. 3
      src/storm-conv/settings/modules/JaniExportSettings.cpp
  16. 0
      src/storm-conv/settings/modules/JaniExportSettings.h

558
src/storm-conv-cli/storm-conv.cpp
View File

@ -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;
}
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>();
namespace conv {
std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
void setUrgentOptions() {
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;
}
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() << "]");
}
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 (watch) {
STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl << std::endl);
}
} else {
STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl);
}
auto const& general = storm::settings::getModule<storm::settings::modules::ConversionGeneralSettings>();
if (general.isVerboseSet()) {
storm::utility::setLogLevel(l3pp::LogLevel::INFO);
}
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);
if (general.isDebugOutputSet()) {
storm::utility::setLogLevel(l3pp::LogLevel::DEBUG);
}
if (general.isTraceOutputSet()) {
storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
}
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) {
// 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();
void processPrismInputJaniOutput(storm::prism::Program const& prismProg, std::vector<storm::jani::Property> const& properties) {
if (result) {
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates()));
}
printInitialStatesResult<ValueType>(result, property, &valuationWatch, &valuation);
storm::converter::PrismToJaniConverterOptions options;
options.allVariablesGlobal = true;
// TODO: fill in options
auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options);
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;
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;
}
}
if (outputFilename != "") {
storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename);
}
watch.stop();
STORM_PRINT_AND_LOG("Overall time for sampling all instances: " << watch << std::endl << std::endl);
if (output.isStdOutOutputEnabled()) {
storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout);
}
}
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.");
}
}
void processPrismInput() {
auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
template <typename ValueType>
void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
// Parse the prism program
storm::storage::SymbolicModelDescription prismProg = storm::api::parseProgram(input.getPrismInputFilename(), input.isPrismCompatibilityEnabled());
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());
// 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);
}
});
} 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);
}
// 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);
}
}
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 ");
// 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_PRINT_AND_LOG("Analyzing ");
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.");
}
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);
}
void processOptions() {
// Start by setting some urgent options (log levels, etc.)
setUrgentOptions();
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);
// Branch on the type of input
auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
if (input.isPrismInputSet()) {
processPrismInput();
} else {
storm::pars::verifyRegionsWithSparseEngine(model, input, regions);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Could not find a supported input format.");
}
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>();
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);
}
}
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();
}
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);
}
}
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();
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);
}
}
}
/*!
* 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;
}
}

61
src/storm-conv/api/storm-conv.h
View File

@ -1,4 +1,61 @@
#pragma once
#include "storm-pars/api/region.h"
#include "storm-pars/api/export.h"
#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);
}
}
}

11
src/storm-conv/converter/options/JaniConversionOptions.cpp
View File

@ -0,0 +1,11 @@
#include "storm-conv/converter/options/PrismToJaniConverterOptions.h"
namespace storm {
namespace converter {
JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), exportFlattened(false) {
// Intentionally left empty
};
}
}

25
src/storm-conv/converter/options/JaniConversionOptions.h
View File

@ -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;
};
}
}

12
src/storm-conv/converter/options/PrismToJaniConverterOptions.cpp
View File

@ -0,0 +1,12 @@
#include "storm-conv/converter/options/PrismToJaniConverterOptions.h"
namespace storm {
namespace converter {
PrismToJaniConverterOptions::PrismToJaniConverterOptions() : allVariablesGlobal(false), suffix("") {
// Intentionally left empty
};
}
}

21
src/storm-conv/converter/options/PrismToJaniConverterOptions.h
View File

@ -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;
};
}
}

22
src/storm-conv/settings/ConvSettings.cpp
View File

@ -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>();
}
}
}

11
src/storm-conv/settings/ConvSettings.h
View File

@ -0,0 +1,11 @@
#pragma once
#include <string>
namespace storm {
namespace settings {
void initializeConvSettings(std::string const& name, std::string const& executableName);
}
}

77
src/storm-conv/settings/modules/ConversionGeneralSettings.cpp
View File

@ -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

88
src/storm-conv/settings/modules/ConversionGeneralSettings.h
View File

@ -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;
};
}
}
}

82
src/storm-conv/settings/modules/ConversionInputSettings.cpp
View File

@ -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

86
src/storm-conv/settings/modules/ConversionInputSettings.h
View File

@ -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;
};
}
}
}

59
src/storm-conv/settings/modules/ConversionOutputSettings.cpp
View File

@ -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

49
src/storm-conv/settings/modules/ConversionOutputSettings.h
View File

@ -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;
};
}
}
}

3
src/storm/settings/modules/JaniExportSettings.cpp → src/storm-conv/settings/modules/JaniExportSettings.cpp
View File

@ -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 {

0
src/storm/settings/modules/JaniExportSettings.h → src/storm-conv/settings/modules/JaniExportSettings.h
View File

Write Preview
Loading…
Cancel
Save