From c3837968dda8b117d68db427bbd5e913c3b830de Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 20 Sep 2018 09:58:49 +0200 Subject: [PATCH] nicer output for storm-conv and fixed an issue in storm-conv related to substituting constants before translating the functions --- src/storm-conv-cli/storm-conv.cpp | 46 ++++++++++++++++--- src/storm-conv/api/storm-conv.cpp | 4 ++ .../options/JaniConversionOptions.cpp | 4 +- .../converter/options/JaniConversionOptions.h | 3 ++ src/storm-parsers/api/model_descriptions.cpp | 7 ++- src/storm-parsers/api/model_descriptions.h | 2 +- 6 files changed, 54 insertions(+), 12 deletions(-) diff --git a/src/storm-conv-cli/storm-conv.cpp b/src/storm-conv-cli/storm-conv.cpp index 4bed40567..12d4a11d8 100644 --- a/src/storm-conv-cli/storm-conv.cpp +++ b/src/storm-conv-cli/storm-conv.cpp @@ -11,6 +11,7 @@ #include "storm-parsers/api/storm-parsers.h" #include "storm/utility/initialize.h" #include "storm/utility/macros.h" +#include "storm/utility/Stopwatch.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/jani/Model.h" @@ -42,15 +43,28 @@ namespace storm { } } + storm::utility::Stopwatch startStopwatch(std::string const& message) { + STORM_PRINT_AND_LOG(message); + return storm::utility::Stopwatch(true); + } + + void stopStopwatch(storm::utility::Stopwatch& stopWatch) { + stopWatch.stop(); + STORM_PRINT_AND_LOG(" done. (" << stopWatch << " seconds)." << std::endl); + } + void processPrismInputJaniOutput(storm::prism::Program const& prismProg, std::vector const& properties) { auto const& output = storm::settings::getModule(); auto const& input = storm::settings::getModule(); auto const& jani = storm::settings::getModule(); + auto conversionTime = startStopwatch("Converting PRISM Program to JANI model ... " ); + storm::converter::PrismToJaniConverterOptions options; options.allVariablesGlobal = jani.isGlobalVarsSet(); options.suffix = ""; options.janiOptions = storm::converter::JaniConversionOptions(jani); + options.janiOptions.substituteConstants = true; // Get the name of the output file std::string outputFilename = ""; @@ -89,20 +103,27 @@ namespace storm { auto janiModelProperties = storm::api::convertPrismToJani(prismProg, properties, options); + stopStopwatch(conversionTime); + auto exportingTime = startStopwatch("Exporting JANI model ... "); + if (outputFilename != "") { storm::api::exportJaniToFile(janiModelProperties.first, janiModelProperties.second, outputFilename, jani.isCompactJsonSet()); + STORM_PRINT_AND_LOG("Stored to file '" << outputFilename << "'"); } if (output.isStdOutOutputEnabled()) { storm::api::printJaniToStream(janiModelProperties.first, janiModelProperties.second, std::cout, jani.isCompactJsonSet()); } + stopStopwatch(exportingTime); } void processPrismInput() { + auto parsingTime = startStopwatch("Parsing PRISM input ... " ); + auto const& input = storm::settings::getModule(); // Parse the prism program - storm::storage::SymbolicModelDescription prismProg = storm::api::parseProgram(input.getPrismInputFilename(), input.isPrismCompatibilityEnabled()); + storm::storage::SymbolicModelDescription prismProg = storm::api::parseProgram(input.getPrismInputFilename(), input.isPrismCompatibilityEnabled(), false); // Parse properties (if available) std::vector properties; @@ -111,13 +132,14 @@ namespace storm { properties = storm::api::parsePropertiesForSymbolicModelDescription(input.getPropertyInput(), prismProg, propertyFilter); } - // Substitute constant definitions in program and properties. + // Set constant definitions in program std::string constantDefinitionString = input.getConstantDefinitionString(); auto constantDefinitions = prismProg.parseConstantDefinitions(constantDefinitionString); - prismProg = storm::storage::SymbolicModelDescription(prismProg.asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstants()); - if (!properties.empty()) { - properties = storm::api::substituteConstantsInProperties(properties, constantDefinitions); - } + prismProg = storm::storage::SymbolicModelDescription(prismProg.asPrismProgram().defineUndefinedConstants(constantDefinitions)); + // Substitution of constants can only be done after conversion in order to preserve formula definitions in which + // constants appear that are renamed in some modules... + + stopStopwatch(parsingTime); // Branch on the type of output auto const& output = storm::settings::getModule(); @@ -129,6 +151,8 @@ namespace storm { } void processJaniInputJaniOutput(storm::jani::Model const& janiModel, std::vector const& properties) { + auto conversionTime = startStopwatch("Performing transformations on JANI model ... " ); + auto const& output = storm::settings::getModule(); auto const& input = storm::settings::getModule(); auto const& jani = storm::settings::getModule(); @@ -166,16 +190,23 @@ namespace storm { auto transformedProperties = properties; storm::api::transformJani(transformedJaniModel, transformedProperties, options); + stopStopwatch(conversionTime); + auto exportingTime = startStopwatch("Exporting JANI model ... "); + if (outputFilename != "") { storm::api::exportJaniToFile(transformedJaniModel, transformedProperties, outputFilename, jani.isCompactJsonSet()); + STORM_PRINT_AND_LOG("Stored to file '" << outputFilename << "'"); } if (output.isStdOutOutputEnabled()) { storm::api::printJaniToStream(transformedJaniModel, transformedProperties, std::cout, jani.isCompactJsonSet()); } + stopStopwatch(exportingTime); } void processJaniInput() { + auto parsingTime = startStopwatch("Parsing JANI input ... " ); + auto const& input = storm::settings::getModule(); // Parse the jani model @@ -200,8 +231,9 @@ namespace storm { if (!properties.empty()) { properties = storm::api::substituteConstantsInProperties(properties, constantDefinitions); } + stopStopwatch(parsingTime); + // Branch on the type of output - auto const& output = storm::settings::getModule(); if (output.isJaniOutputSet()) { processJaniInputJaniOutput(janiModel, properties); diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index 7431b38be..f8e956a94 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -13,6 +13,10 @@ namespace storm { void transformJani(storm::jani::Model& janiModel, std::vector& properties, storm::converter::JaniConversionOptions const& options) { + if (options.substituteConstants) { + janiModel = janiModel.substituteConstants(); + } + if (!options.locationVariables.empty()) { for (auto const& pair : options.locationVariables) { storm::jani::JaniLocationExpander expander(janiModel); diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index 1fe36cfe2..123d281b3 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.cpp +++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp @@ -3,11 +3,11 @@ namespace storm { namespace converter { - JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), flatten(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { + JaniConversionOptions::JaniConversionOptions() : standardCompliant(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { // Intentionally left empty }; - JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), flatten(settings.isExportFlattenedSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { + JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { if (settings.isEliminateFunctionsSet()) { allowedModelFeatures.remove(storm::jani::ModelFeature::Functions); } diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h index 8758d480f..68dfd7d5a 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.h +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -24,6 +24,9 @@ namespace storm { /// If set, the model is transformed into a single automaton bool flatten; + /// If set, constants in expressions are substituted with their definition + bool substituteConstants; + /// If given, the model will get this name boost::optional modelName; diff --git a/src/storm-parsers/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp index fd26422af..16419945d 100644 --- a/src/storm-parsers/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -13,8 +13,11 @@ namespace storm { namespace api { - storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility) { - storm::prism::Program program = storm::parser::PrismParser::parse(filename, prismCompatibility).simplify().simplify(); + storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility, bool simplify) { + storm::prism::Program program = storm::parser::PrismParser::parse(filename, prismCompatibility); + if (simplify) { + program = program.simplify().simplify(); + } program.checkValidity(); return program; } diff --git a/src/storm-parsers/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h index ff1a44bcd..e23cf7c33 100644 --- a/src/storm-parsers/api/model_descriptions.h +++ b/src/storm-parsers/api/model_descriptions.h @@ -15,7 +15,7 @@ namespace storm { namespace api { - storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false); + storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false, bool simplify = true); std::pair> parseJaniModel(std::string const& filename); std::pair> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures);