started on making jani available from cli, commit to switch workplace

Former-commit-id: 4c04d77409 [formerly 279141117d]
Former-commit-id: e05805177e

src/cli/cli.cpp

@@ -3,6 +3,8 @@
 
 #include "../utility/storm.h"
 
+#include "src/storage/SymbolicModelDescription.h"
+
 #include "src/settings/modules/DebugSettings.h"
 #include "src/settings/modules/IOSettings.h"
 #include "src/settings/modules/CoreSettings.h"
@@ -206,19 +208,27 @@ namespace storm {
                 storm::utility::initializeFileLogging();
             }
 
-            if (storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet()) {
-                // If we have to build the model from a symbolic representation, we need to parse the representation first.
-                storm::prism::Program program = storm::parseProgram(storm::settings::getModule<storm::settings::modules::IOSettings>().getSymbolicModelFilename());
+            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            if (ioSettings.isPrismOrJaniInputSet()) {
+                storm::storage::SymbolicModelDescription model;
+                if (ioSettings.isPrismInputSet()) {
+                    model = storm::parseProgram(ioSettings.getPrismInputFilename());
+                } else if (ioSettings.isJaniInputSet()) {
+                    model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first;
+                }
                 
                 // Get the string that assigns values to the unknown currently undefined constants in the model.
-                std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
-                storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess(program, constantDefinitionString);
-                std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preprocessedProgram.getConstantsSubstitution();
+                std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
+                model.preprocess(constantDefinitionString);
 
                 // Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
-                    formulas = storm::parseFormulasForProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), preprocessedProgram);
+                    if (model.isJaniModel()) {
+                        formulas = storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel());
+                    } else {
+                        formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram());
+                    }
                 }
 
                 // There may be constants of the model appearing in the formulas, so we replace all their occurrences

src/parser/FormulaParser.cpp

@@ -4,6 +4,9 @@
 
 #include "src/parser/SpiritErrorHandler.h"
 
+#include "src/storage/prism/Program.h"
+#include "src/storage/jani/Model.h"
+
 // If the parser fails due to ill-formed data, this exception is thrown.
 #include "src/exceptions/WrongFormatException.h"
 
@@ -176,7 +179,7 @@ namespace storm {
             phoenix::function<SpiritErrorHandler> handler;
         };
         
-        FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : manager(manager->getSharedPointer()), grammar(new FormulaParserGrammar(manager)) {
+        FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : manager(manager), grammar(new FormulaParserGrammar(manager)) {
             // Intentionally left empty.
         }
         

src/parser/FormulaParser.h

@@ -9,9 +9,11 @@
 #include "src/storage/expressions/Expression.h"
 #include "src/utility/macros.h"
 
-#include "src/storage/prism/Program.h"
-
 namespace storm {
+    namespace prism {
+        class Program;
+    }
+    
     namespace parser {
         
         // Forward-declare grammar.

src/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -48,7 +48,7 @@ namespace storm {
             
             bool CounterexampleGeneratorSettings::check() const {
                 // Ensure that the model was given either symbolically or explicitly.
-                STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified symbolically.");
+                STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM format.");
                 
                 if (isMinimalCommandSetGenerationSet()) {
                     STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");

src/settings/modules/IOSettings.cpp

@@ -17,8 +17,8 @@ namespace storm {
             const std::string IOSettings::exportMatOptionName = "exportmat";
             const std::string IOSettings::explicitOptionName = "explicit";
             const std::string IOSettings::explicitOptionShortName = "exp";
-            const std::string IOSettings::symbolicOptionName = "symbolic";
-            const std::string IOSettings::symbolicOptionShortName = "s";
+            const std::string IOSettings::prismInputOptionName = "prism";
+            const std::string IOSettings::janiInputOptionName = "jani";
             const std::string IOSettings::explorationOrderOptionName = "explorder";
             const std::string IOSettings::explorationOrderOptionShortName = "eo";
             const std::string IOSettings::transitionRewardsOptionName = "transrew";
@@ -38,8 +38,10 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).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.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 
                 std::vector<std::string> explorationOrders = {"dfs", "bfs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
@@ -51,7 +53,7 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
+                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 + " or --" + janiInputOptionName + ").").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());
             }
 
@@ -75,14 +77,26 @@ namespace storm {
                 return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString();
             }
             
-            bool IOSettings::isSymbolicSet() const {
-                return this->getOption(symbolicOptionName).getHasOptionBeenSet();
+            bool IOSettings::isPrismInputSet() const {
+                return this->getOption(prismInputOptionName).getHasOptionBeenSet();
             }
             
-            std::string IOSettings::getSymbolicModelFilename() const {
-                return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString();
+            bool IOSettings::isPrismOrJaniInputSet() const {
+                return isJaniInputSet() || isPrismInputSet();
             }
             
+            std::string IOSettings::getPrismInputFilename() const {
+                return this->getOption(prismInputOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
+            bool IOSettings::isJaniInputSet() const {
+                return this->getOption(janiInputOptionName).getHasOptionBeenSet();
+            }
+
+            std::string IOSettings::getJaniInputFilename() const {
+                return this->getOption(janiInputOptionName).getArgumentByName("filename").getValueAsString();
+            }
+
             bool IOSettings::isExplorationOrderSet() const {
                 return this->getOption(explorationOrderOptionName).getHasOptionBeenSet();
             }
@@ -141,8 +155,11 @@ namespace storm {
             }
 
             bool IOSettings::check() const {
+                // Ensure that not two symbolic input models were given.
+                STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet(), storm::exceptions::InvalidSettingsException, "Symbolic model ");
+                
                 // Ensure that the model was given either symbolically or explicitly.
-                STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");
+                STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both.");
                 return true;
             }
 

src/settings/modules/IOSettings.h

@@ -59,20 +59,42 @@ namespace storm {
                 std::string getLabelingFilename() const;
 
                 /*!
-                 * Retrieves whether the symbolic option was set.
+                 * Retrieves whether the PRISM language option was set.
                  *
-                 * @return True if the symbolic option was set.
+                 * @return True if the PRISM input option was set.
                  */
-                bool isSymbolicSet() const;
+                bool isPrismInputSet() const;
+                
+                /*!
+                 * Retrieves whether the JANI input option was set.
+                 *
+                 * @return True if the JANI input option was set.
+                 */
+                bool isJaniInputSet() const;
 
                 /*!
-                 * Retrieves the name of the file that contains the symbolic model specification if the model was given
-                 * using the symbolic option.
+                 * Retrieves whether the JANI or PRISM input option was set.
                  *
-                 * @return The name of the file that contains the symbolic model specification.
+                 * @return True if either of the two options was set.
                  */
-                std::string getSymbolicModelFilename() const;
+                bool isPrismOrJaniInputSet() const;
                 
+                /*!
+                 * Retrieves the name of the file that contains the PRISM model specification if the model was given
+                 * using the PRISM input option.
+                 *
+                 * @return The name of the file that contains the PRISM model specification.
+                 */
+                std::string getPrismInputFilename() const;
+
+                /*!
+                 * Retrieves the name of the file that contains the JANI model specification if the model was given
+                 * using the JANI input option.
+                 *
+                 * @return The name of the file that contains the JANI model specification.
+                 */
+                std::string getJaniInputFilename() const;
+
                 /*!
                  * Retrieves whether the model exploration order was set.
                  *
@@ -174,8 +196,8 @@ namespace storm {
                 static const std::string exportMatOptionName;
                 static const std::string explicitOptionName;
                 static const std::string explicitOptionShortName;
-                static const std::string symbolicOptionName;
-                static const std::string symbolicOptionShortName;
+                static const std::string prismInputOptionName;
+                static const std::string janiInputOptionName;
                 static const std::string explorationOrderOptionName;
                 static const std::string explorationOrderOptionShortName;
                 static const std::string transitionRewardsOptionName;

src/storage/SymbolicModelDescription.cpp

@@ -1,35 +1,62 @@
 #include "src/storage/SymbolicModelDescription.h"
 
+#include "src/utility/prism.h"
+#include "src/utility/jani.h"
+
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
 
 namespace storm {
     namespace storage {
         
-        SymbolicModelDescription::SymbolicModelDescription(storm::jani::Model const& model) {
+        SymbolicModelDescription::SymbolicModelDescription(storm::jani::Model const& model) : modelDescription(model) {
             // Intentionally left empty.
         }
         
-        SymbolicModelDescription::SymbolicModelDescription(storm::prism::Program const& program) {
+        SymbolicModelDescription::SymbolicModelDescription(storm::prism::Program const& program) : modelDescription(program) {
             // Intentionally left empty.
         }
-                
+        
+        bool SymbolicModelDescription::hasModel() const {
+            return static_cast<bool>(modelDescription);
+        }
+        
         bool SymbolicModelDescription::isJaniModel() const {
-            return modelDescription.which() == 0;
+            return modelDescription.get().which() == 0;
         }
         
         bool SymbolicModelDescription::isPrismProgram() const {
-            return modelDescription.which() == 1;
+            return modelDescription.get().which() == 1;
+        }
+        
+        void SymbolicModelDescription::setModel(storm::jani::Model const& model) {
+            modelDescription = model;
+        }
+        
+        void SymbolicModelDescription::setModel(storm::prism::Program const& program) {
+            modelDescription = program;
         }
         
         storm::jani::Model const& SymbolicModelDescription::asJaniModel() const {
             STORM_LOG_THROW(isJaniModel(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type.");
-            return boost::get<storm::jani::Model>(modelDescription);
+            return boost::get<storm::jani::Model>(modelDescription.get());
         }
         
         storm::prism::Program const& SymbolicModelDescription::asPrismProgram() const {
             STORM_LOG_THROW(isPrismProgram(), storm::exceptions::InvalidOperationException, "Cannot retrieve JANI model, because the symbolic description has a different type.");
-            return boost::get<storm::prism::Program>(modelDescription);
+            return boost::get<storm::prism::Program>(modelDescription.get());
+        }
+        
+        void SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) {
+            if (this->isJaniModel()) {
+                std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString);
+                this->modelDescription = this->asJaniModel().defineUndefinedConstants(substitution);
+                this->modelDescription = this->asJaniModel().substituteConstants();
+            } else if (this->isPrismProgram()) {
+                std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString);
+                this->modelDescription = this->asPrismProgram().defineUndefinedConstants(substitution);
+                this->modelDescription = this->asPrismProgram().substituteConstants();
+            }
         }
         
     }

src/storage/SymbolicModelDescription.h

@@ -10,17 +10,24 @@ namespace storm {
         
         class SymbolicModelDescription {
         public:
+            SymbolicModelDescription();
             SymbolicModelDescription(storm::jani::Model const& model);
             SymbolicModelDescription(storm::prism::Program const& program);
 
+            bool hasModel() const;
             bool isJaniModel() const;
             bool isPrismProgram() const;
+
+            void setModel(storm::jani::Model const& model);
+            void setModel(storm::prism::Program const& program);
             
             storm::jani::Model const& asJaniModel() const;
             storm::prism::Program const& asPrismProgram() const;
             
+            void preprocess(std::string const& constantDefinitionString = "");
+            
         private:
-            boost::variant<storm::jani::Model, storm::prism::Program> modelDescription;
+            boost::optional<boost::variant<storm::jani::Model, storm::prism::Program>> modelDescription;
         };
         
     }

src/utility/storm.cpp

@@ -43,7 +43,11 @@ namespace storm {
         return parseFormulas(formulaParser, inputString);
     }
 
-    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) {
+    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForJaniModel(std::string const& inputString, storm::jani::Model const& model) {
+        storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer());
+        return parseFormulas(formulaParser, inputString);
+    }
+    std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program) {
         storm::parser::FormulaParser formulaParser(program);
         return parseFormulas(formulaParser, inputString);
     } 

src/utility/storm.h

@@ -208,7 +208,6 @@ namespace storm {
     void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
         if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {
             STORM_LOG_THROW(model->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
-            STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
 
             std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();