storm-conv: Added support for transformations on prism programs (such as flattening of modules).

CHANGELOG.md

@@ -20,6 +20,7 @@ Version 1.3.x
 - JANI: Support for non-trivial reward accumulations.
 - JANI: Fixed support for reward expressions over non-transient variables.
 - DRN: Added support for exact parsing and action-based rewards
+- storm-conv can now apply transformations on a prism file
 - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial)
 - Fixed linking with Mathsat on macOS
 - Fixed compilation for macOS mojave

src/storm-conv-cli/storm-conv.cpp

@@ -6,6 +6,8 @@
 #include "storm-conv/settings/modules/ConversionGeneralSettings.h"
 #include "storm-conv/settings/modules/ConversionInputSettings.h"
 #include "storm-conv/settings/modules/ConversionOutputSettings.h"
+#include "storm-conv/settings/modules/JaniExportSettings.h"
+#include "storm-conv/settings/modules/PrismExportSettings.h"
 
 #include "storm/api/storm.h"
 #include "storm-parsers/api/storm-parsers.h"
@@ -117,6 +119,52 @@ namespace storm {
             stopStopwatch(exportingTime);
         }
         
+        void processPrismInputPrismOutput(storm::prism::Program const& prismProg, std::vector<storm::jani::Property> const& properties) {
+            auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
+            auto const& input = storm::settings::getModule<storm::settings::modules::ConversionInputSettings>();
+            auto const& prism = storm::settings::getModule<storm::settings::modules::PrismExportSettings>();
+            
+            auto conversionTime = startStopwatch("Processing Prism Program ... " );
+
+            // Get the name of the output file
+            std::string outputFilename = "";
+            if (output.isPrismOutputFilenameSet()) {
+                outputFilename = output.getPrismOutputFilename();
+            } else if (input.isPrismInputSet() && !output.isStdOutOutputEnabled()) {
+                outputFilename = input.getPrismInputFilename();
+                // Remove extension if present
+                auto dotPos = outputFilename.rfind('.');
+                if (dotPos != std::string::npos) {
+                    outputFilename.erase(dotPos);
+                }
+                std::string suffix = "";
+                if (input.isConstantsSet()) {
+                    suffix = input.getConstantDefinitionString();
+                    std::replace(suffix.begin(), suffix.end(), ',', '_');
+                    std::replace(suffix.begin(), suffix.end(), '=', '-');
+                }
+                suffix += "_converted.prism";
+                outputFilename += suffix;
+            }
+            
+            storm::prism::Program outputProgram = prismProg;
+            std::vector<storm::jani::Property> outputProperties = properties;
+            storm::api::transformPrism(outputProgram, outputProperties, prism.isSimplifySet(), prism.isExportFlattenedSet());
+            
+            stopStopwatch(conversionTime);
+            auto exportingTime = startStopwatch("Exporting Prism program ... ");
+            
+            if (outputFilename != "") {
+                storm::api::exportPrismToFile(outputProgram, outputProperties, outputFilename);
+                STORM_PRINT_AND_LOG("Stored to file '" << outputFilename << "'");
+            }
+            
+            if (output.isStdOutOutputEnabled()) {
+                storm::api::printPrismToStream(outputProgram, outputProperties, std::cout);
+            }
+            stopStopwatch(exportingTime);
+        }
+        
         void processPrismInput() {
             auto parsingTime = startStopwatch("Parsing PRISM input ... " );
 
@@ -145,6 +193,8 @@ namespace storm {
             auto const& output = storm::settings::getModule<storm::settings::modules::ConversionOutputSettings>();
             if (output.isJaniOutputSet()) {
                 processPrismInputJaniOutput(prismProg.asPrismProgram(), properties);
+            } else if (output.isPrismOutputSet()) {
+                processPrismInputPrismOutput(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.");
             }
@@ -251,6 +301,7 @@ namespace storm {
             if (output.isJaniOutputSet()) {
                 processJaniInputJaniOutput(janiModel, properties);
             } else {
+                STORM_LOG_THROW(!output.isPrismOutputSet(), storm::exceptions::InvalidSettingsException, "Conversion from Jani to Prism is not supported.");
                 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.");
             }
         }

src/storm-conv/api/storm-conv.cpp

@@ -7,6 +7,9 @@
 #include "storm/storage/jani/JaniScopeChanger.h"
 #include "storm/storage/jani/JSONExporter.h"
 
+#include "storm/utility/file.h"
+#include "storm/api/properties.h"
+
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
 
@@ -79,6 +82,20 @@ namespace storm {
             
         }
         
+        void transformPrism(storm::prism::Program& prismProgram, std::vector<storm::jani::Property>& properties, bool simplify, bool flatten) {
+            if (simplify) {
+                prismProgram = prismProgram.simplify().simplify();
+                properties = storm::api::substituteConstantsInProperties(properties, prismProgram.getConstantsFormulasSubstitution());
+            }
+            if (flatten) {
+               prismProgram = prismProgram.flattenModules();
+               if (simplify) {
+                    // Let's simplify the flattened program again ... just to be sure ... twice ...
+                    prismProgram = prismProgram.simplify().simplify();
+               }
+            }
+        }
+        
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> convertPrismToJani(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, storm::converter::PrismToJaniConverterOptions options) {
         
             // Perform conversion
@@ -104,6 +121,28 @@ namespace storm {
         void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact) {
             storm::jani::JsonExporter::toStream(model, properties, ostream, true, compact);
         }
+        
+        void exportPrismToFile(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::string const& filename) {
+            std::ofstream stream;
+            storm::utility::openFile(filename, stream);
+            stream << program << std::endl;
+            storm::utility::closeFile(stream);
+            
+            if (!properties.empty()) {
+                storm::utility::openFile(filename + ".props", stream);
+                for (auto const& prop : properties) {
+                    stream << prop << std::endl;
+                }
+                storm::utility::closeFile(stream);
+            }
+        }
+        void printPrismToStream(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::ostream& ostream) {
+            ostream << program << std::endl;
+            for (auto const& prop : properties) {
+                ostream << prop << std::endl;
+            }
+        }
+
 
         
     }

src/storm-conv/api/storm-conv.h

@@ -16,12 +16,15 @@ namespace storm {
     namespace api {
         
         void transformJani(storm::jani::Model& janiModel, std::vector<storm::jani::Property>& properties, storm::converter::JaniConversionOptions const& options);
+        
+        void transformPrism(storm::prism::Program& prismProgram, std::vector<storm::jani::Property>& properties, bool simplify = false, bool flatten = false);
 
         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());
         
         void exportJaniToFile(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filename, bool compact = false);
-        
         void printJaniToStream(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::ostream& ostream, bool compact = false);
+        void exportPrismToFile(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::string const& filename);
+        void printPrismToStream(storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, std::ostream& ostream);
 
         
     }

src/storm-conv/settings/ConvSettings.cpp

@@ -4,6 +4,7 @@
 #include "storm-conv/settings/modules/ConversionInputSettings.h"
 #include "storm-conv/settings/modules/ConversionOutputSettings.h"
 #include "storm-conv/settings/modules/JaniExportSettings.h"
+#include "storm-conv/settings/modules/PrismExportSettings.h"
 
 #include "storm/settings/SettingsManager.h"
 
@@ -18,6 +19,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::ConversionInputSettings>();
             storm::settings::addModule<storm::settings::modules::ConversionOutputSettings>();
             storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
+            storm::settings::addModule<storm::settings::modules::PrismExportSettings>();
         }
     
     }

src/storm-conv/settings/modules/ConversionOutputSettings.cpp

@@ -16,10 +16,13 @@ namespace storm {
             const std::string ConversionOutputSettings::moduleName = "output";
             const std::string ConversionOutputSettings::stdoutOptionName = "stdout";
             const std::string ConversionOutputSettings::janiOutputOptionName = "tojani";
+            const std::string ConversionOutputSettings::prismOutputOptionName = "toprism";
 
             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.")
+                this->addOption(storm::settings::OptionBuilder(moduleName, janiOutputOptionName, false, "exports the model as Jani file.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, prismOutputOptionName, false, "exports the model as Prism file.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the output file (if not empty).").setDefaultValueString("").build()).build());
             }
             
@@ -42,6 +45,22 @@ namespace storm {
                 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();
             }
+            
+            bool ConversionOutputSettings::isPrismOutputSet() const {
+                return this->getOption(prismOutputOptionName).getHasOptionBeenSet();
+            }
+            
+            bool ConversionOutputSettings::isPrismOutputFilenameSet() const {
+                return isPrismOutputSet()
+                       && !this->getOption(prismOutputOptionName).getArgumentByName("filename").wasSetFromDefaultValue()
+                       && this->getOption(prismOutputOptionName).getArgumentByName("filename").getHasBeenSet()
+                       && this->getOption(prismOutputOptionName).getArgumentByName("filename").getValueAsString() != "";
+            }
+
+            std::string ConversionOutputSettings::getPrismOutputFilename() const {
+                STORM_LOG_THROW(isPrismOutputFilenameSet(), storm::exceptions::InvalidOperationException, "Tried to get the prism output name although none was specified.");
+                return this->getOption(prismOutputOptionName).getArgumentByName("filename").getValueAsString();
+            }
 
 			void ConversionOutputSettings::finalize() {
                 // Intentionally left empty.
@@ -49,6 +68,8 @@ namespace storm {
 
             bool ConversionOutputSettings::check() const {
                 STORM_LOG_THROW(!isJaniOutputFilenameSet() || ArgumentValidatorFactory::createWritableFileValidator()->isValid(getJaniOutputFilename()), storm::exceptions::InvalidSettingsException, "Unable to write at file " + getJaniOutputFilename());
+                STORM_LOG_THROW(!isPrismOutputFilenameSet() || ArgumentValidatorFactory::createWritableFileValidator()->isValid(getPrismOutputFilename()), storm::exceptions::InvalidSettingsException, "Unable to write at file " + getPrismOutputFilename());
+                STORM_LOG_THROW(!(isJaniOutputSet() && isPrismOutputSet()), storm::exceptions::InvalidSettingsException, "Can not export to both, prism and jani");
                 return true;
             }
             

src/storm-conv/settings/modules/ConversionOutputSettings.h

@@ -30,6 +30,21 @@ namespace storm {
                  */
                 std::string getJaniOutputFilename() const;
                 
+                /*!
+                 * Retrieves whether the output should be in the Prism format
+                 */
+                bool isPrismOutputSet() const;
+                
+                /*!
+                 * Retrieves whether an output filename for the prism file was specified
+                 */
+                bool isPrismOutputFilenameSet() const;
+
+                /*!
+                 * Retrieves the name of the prism output (if specified)
+                 */
+                std::string getPrismOutputFilename() const;
+                
                 bool check() const override;
                 void finalize() override;
 
@@ -41,6 +56,8 @@ namespace storm {
             private:
                 // Define the string names of the options as constants.
                 static const std::string janiOutputOptionName;
+                // Define the string names of the options as constants.
+                static const std::string prismOutputOptionName;
             };
             
                 

src/storm-conv/settings/modules/PrismExportSettings.cpp

@@ -0,0 +1,42 @@
+#include "PrismExportSettings.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/SettingMemento.h"
+#include "storm/settings/Option.h"
+#include "storm/settings/OptionBuilder.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/Argument.h"
+
+#include <boost/algorithm/string.hpp>
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            const std::string PrismExportSettings::moduleName = "exportPrism";
+            
+            const std::string PrismExportSettings::exportFlattenOptionName = "flatten";
+            const std::string PrismExportSettings::exportSimplifyOptionName = "simplify";
+            
+            PrismExportSettings::PrismExportSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of modules to obtain an equivalent program that contains exactly one module").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportSimplifyOptionName, false, "Applies static analysis to simplify the program.").build());
+            }
+            
+            bool PrismExportSettings::isExportFlattenedSet() const {
+                return this->getOption(exportFlattenOptionName).getHasOptionBeenSet();
+            }
+            
+            bool PrismExportSettings::isSimplifySet() const {
+                return this->getOption(exportSimplifyOptionName).getHasOptionBeenSet();
+            }
+
+            void PrismExportSettings::finalize() {
+                
+            }
+            
+            bool PrismExportSettings::check() const {
+                return true;
+            }
+        }
+    }
+}

src/storm-conv/settings/modules/PrismExportSettings.h

@@ -0,0 +1,32 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            class PrismExportSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new PrismExport setting
+                 */
+                PrismExportSettings();
+                
+                bool isExportFlattenedSet() const;
+                bool isSimplifySet() const;
+
+                bool check() const override;
+                void finalize() override;
+                
+                static const std::string moduleName;
+                
+            private:
+                static const std::string exportFlattenOptionName;
+                static const std::string exportSimplifyOptionName;
+                
+            };
+        }
+    }
+}