Allow to add properties to a PGCL program.

src/storm-pgcl-cli/storm-pgcl.cpp

@@ -20,6 +20,8 @@
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm-conv/settings/modules/JaniExportSettings.h"
 #include "storm-conv/api/storm-conv.h"
+#include "storm-parsers/api/storm-parsers.h"
+#include "storm/storage/SymbolicModelDescription.h"
 
 #include "storm/utility/file.h"
 
@@ -38,15 +40,14 @@ void initializeSettings() {
     storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
 }
 
-void handleJani(storm::jani::Model& model) {
+void handleJani(storm::jani::Model& model, std::vector<storm::jani::Property>& properties) {
     auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
     storm::converter::JaniConversionOptions options(jani);
-    std::vector<storm::jani::Property> properties;
     storm::api::transformJani(model, properties, options);
     if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
-        storm::api::exportJaniToFile(model, {}, storm::settings::getModule<storm::settings::modules::PGCLSettings>().getWriteToJaniFilename(), jani.isCompactJsonSet());
+        storm::api::exportJaniToFile(model, properties, storm::settings::getModule<storm::settings::modules::PGCLSettings>().getWriteToJaniFilename(), jani.isCompactJsonSet());
     } else {
-        storm::api::printJaniToStream(model, {}, std::cout);
+        storm::api::printJaniToStream(model, properties, std::cout);
     }
 }
 
@@ -69,30 +70,39 @@ int main(const int argc, const char** argv) {
             return -1;
         }
     
-        if (!storm::settings::getModule<storm::settings::modules::PGCLSettings>().isPgclFileSet()) {
+        auto pgcl = storm::settings::getModule<storm::settings::modules::PGCLSettings>();
+        if (!pgcl.isPgclFileSet()) {
             return -1;
         }
-        storm::pgcl::PgclProgram prog = storm::parser::PgclParser::parse(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getPgclFilename());
+        
+        storm::pgcl::PgclProgram prog = storm::parser::PgclParser::parse(pgcl.getPgclFilename());
         storm::ppg::ProgramGraph* progGraph = storm::builder::ProgramGraphBuilder::build(prog);
     
         progGraph->printInfo(std::cout);
-        if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isProgramGraphToDotSet()) {
+        if (pgcl.isProgramGraphToDotSet()) {
             programGraphToDotFile(*progGraph);
         }
-        if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
+        if (pgcl.isToJaniSet()) {
             storm::builder::JaniProgramGraphBuilderSetting settings;
             // To disable reward detection, uncomment the following line
             // TODO add a setting for this.
             // settings.filterRewardVariables = false;
             storm::builder::JaniProgramGraphBuilder builder(*progGraph, settings);
-            if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isProgramVariableRestrictionSet()) {
+            if (pgcl.isProgramVariableRestrictionSet()) {
                 // TODO More fine grained control
-                storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getProgramVariableRestrictions());
+                storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(pgcl.getProgramVariableRestrictions());
                 builder.restrictAllVariables(restr);
             }
             storm::jani::Model* model = builder.build();
+            
             delete progGraph;
-            handleJani(*model);
+            std::vector<storm::jani::Property> properties;
+            if (pgcl.isPropertyInputSet()) {
+                boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(pgcl.getPropertyInputFilter());
+                properties = storm::api::parsePropertiesForSymbolicModelDescription(pgcl.getPropertyInput(), *model, propertyFilter);
+            }
+            
+            handleJani(*model, properties);
             delete model;
         } else {
             

src/storm-pgcl/settings/modules/PGCLSettings.cpp

@@ -22,13 +22,18 @@ namespace storm {
             const std::string PGCLSettings::programGraphToDotShortOptionName = "pg";
             const std::string PGCLSettings::programVariableRestrictionsOptionName = "variable-restrictions";
             const std::string PGCLSettings::programVariableRestrictionShortOptionName = "rvar";
-            
+            const std::string PGCLSettings::propertyOptionName = "prop";
+            const std::string PGCLSettings::propertyOptionShortName = "prop";
             
             PGCLSettings::PGCLSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("description", "description of the variable restrictions").build()).build());
+                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());
             }
             
             bool PGCLSettings::isPgclFileSet() const {
@@ -64,6 +69,18 @@ namespace storm {
                 return this->getOption(programVariableRestrictionsOptionName).getArgumentByName("description").getValueAsString();
             }
             
+            bool PGCLSettings::isPropertyInputSet() const {
+                return this->getOption(propertyOptionName).getHasOptionBeenSet();
+            }
+
+            std::string PGCLSettings::getPropertyInput() const {
+                return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString();
+            }
+
+            std::string PGCLSettings::getPropertyInputFilter() const {
+                return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString();
+            }
+            
             void PGCLSettings::finalize() {
                 
             }

src/storm-pgcl/settings/modules/PGCLSettings.h

@@ -54,6 +54,26 @@ namespace storm {
                  */
                 std::string getProgramVariableRestrictions() const;
                 
+                /*!
+                 * 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;
                 
                 bool check() const override;
                 void finalize() override;
@@ -69,7 +89,8 @@ namespace storm {
                 static const std::string programGraphToDotShortOptionName;
                 static const std::string programVariableRestrictionsOptionName;
                 static const std::string programVariableRestrictionShortOptionName;
-                
+                static const std::string propertyOptionName;
+                static const std::string propertyOptionShortName;
             };
         }
     }