export formulae

Former-commit-id: 4932938e38 [formerly 95b3269c75]
Former-commit-id: 974a891cb6

src/cli/cli.cpp

@@ -222,13 +222,23 @@ namespace storm {
                     model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first;
                 }
                 
+                // 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()) {
+                    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());
+                    }
+                }
+                
                 if(model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
                     if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
                         storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel());
                         normalisedModel.makeStandardJaniCompliant();
-                        storm::jani::JsonExporter::toFile(normalisedModel, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+                        storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
                     } else {
-                        storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+                        storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
                     }
                 }
                 
@@ -236,15 +246,7 @@ namespace storm {
                 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
                 model = 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()) {
-                    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());
-                    }
-                }
+                
 
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
 #ifdef STORM_HAVE_CARL

src/parser/JaniParser.cpp

@@ -110,6 +110,13 @@ namespace storm {
             for (auto const& automataEntry : parsedStructure.at("automata")) {
                 model.addAutomaton(parseAutomaton(automataEntry, model));
             }
+            STORM_LOG_THROW(parsedStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Model has multiple initial value restrictions");
+            storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true);
+            if(parsedStructure.count("restrict-initial") > 0) {
+                STORM_LOG_THROW(parsedStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Model needs an expression inside the initial restricion");
+                initialValueRestriction  = parseExpression(parsedStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name);
+            }
+            model.setInitialStatesRestriction(initialValueRestriction);
             STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
             std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
             model.setSystemComposition(composition);

src/storage/jani/JSONExporter.cpp

@@ -9,6 +9,7 @@
 #include "src/exceptions/NotSupportedException.h"
 
 #include "src/exceptions/InvalidJaniException.h"
+#include "src/exceptions/NotImplementedException.h"
 
 #include "src/storage/expressions/RationalLiteralExpression.h"
 #include "src/storage/expressions/IntegerLiteralExpression.h"
@@ -25,6 +26,7 @@
 
 #include "src/storage/jani/AutomatonComposition.h"
 #include "src/storage/jani/ParallelComposition.h"
+#include "src/storage/jani/Property.h"
 
 namespace storm {
     namespace jani {
@@ -128,6 +130,11 @@ namespace storm {
             return iDecl;
         }
         
+        modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, bool continuousTime) {
+            FormulaToJaniJson translator(continuousTime);
+            return boost::any_cast<modernjson::json>(formula.accept(translator));
+        }
+        
         boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const {
             return ExpressionToJson::translate(f.getExpression());
         }
@@ -178,16 +185,44 @@ namespace storm {
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae");
-
+            modernjson::json opDecl;
+            std::vector<std::string> tvec;
+            tvec.push_back("time");
+            if(f.hasBound()) {
+                auto bound = f.getBound();
+                opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
+                if(f.hasOptimalityType()) {
+                    opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
+                    opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                } else {
+                    opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin";
+                    opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                }
+                opDecl["left"]["exp"] = modernjson::json(1);
+                opDecl["left"]["accumulate"] = modernjson::json(tvec);
+                opDecl["right"] = numberToJson(bound.threshold);
+            } else {
+                if(f.hasOptimalityType()) {
+                    opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
+                    opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                    
+                } else {
+                    // TODO add checks
+                    opDecl["op"] = "Pmin";
+                    opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                }
+                opDecl["exp"] = modernjson::json(1);
+                opDecl["accumulate"] = modernjson::json(tvec);
+            }
+            return opDecl;
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae");
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a globally formulae");
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae");
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula");
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const {
@@ -219,7 +254,30 @@ namespace storm {
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const {
-            
+//            modernjson::json opDecl;
+//            if(f.()) {
+//                auto bound = f.getBound();
+//                opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
+//                if(f.hasOptimalityType()) {
+//                    opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
+//                    opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+//                } else {
+//                    opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin";
+//                    opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+//                }
+//                opDecl["right"] = numberToJson(bound.threshold);
+//            } else {
+//                if(f.hasOptimalityType()) {
+//                    opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
+//                    opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+//                    
+//                } else {
+//                    // TODO add checks
+//                    opDecl["op"] = "Pmin";
+//                    opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+//                }
+//            }
+//            return opDecl;
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const {
@@ -263,7 +321,40 @@ namespace storm {
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
-            
+            modernjson::json opDecl;
+            std::vector<std::string> accvec;
+            if(continuous) {
+                accvec.push_back("time");
+            } else {
+                accvec.push_back("steps");
+            }
+            if(f.hasBound()) {
+                auto bound = f.getBound();
+                opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
+                if(f.hasOptimalityType()) {
+                    opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
+                    opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                } else {
+                    opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin";
+                    opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                }
+                opDecl["left"]["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT";
+                opDecl["left"]["accumulate"] = modernjson::json(accvec);
+                opDecl["right"] = numberToJson(bound.threshold);
+            } else {
+                if(f.hasOptimalityType()) {
+                    opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
+                    opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                    
+                } else {
+                    // TODO add checks
+                    opDecl["op"] = "Pmin";
+                    opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
+                }
+                opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT";
+                opDecl["accumulate"] = modernjson::json(accvec);
+            }
+            return opDecl;
         }
         
         boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const {
@@ -402,22 +493,23 @@ namespace storm {
         
         
         
-        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid) {
+        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid) {
             std::ofstream ofs;
             ofs.open (filepath, std::ofstream::out );
             if(ofs.is_open()) {
-                toStream(janiModel, ofs, checkValid);
+                toStream(janiModel, formulas, ofs, checkValid);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
             }
         }
         
-        void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os, bool checkValid) {
+        void JsonExporter::toStream(storm::jani::Model const& janiModel,  std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& os, bool checkValid) {
             if(checkValid) {
                 janiModel.checkValid();
             }
             JsonExporter exporter;
             exporter.convertModel(janiModel);
+            exporter.convertProperties(formulas, !janiModel.isDiscreteTimeModel());
             os << exporter.finalize().dump(4) << std::endl;
         }
         
@@ -597,6 +689,54 @@ namespace storm {
         }
         
         
+        std::string janiFilterTypeString(storm::jani::FilterType const& ft) {
+            switch(ft) {
+                case storm::jani::FilterType::MIN:
+                    return "min";
+                case storm::jani::FilterType::MAX:
+                    return "max";
+                case storm::jani::FilterType::SUM:
+                    return "sum";
+                case storm::jani::FilterType::AVG:
+                    return "avg";
+                case storm::jani::FilterType::COUNT:
+                    return "count";
+                case storm::jani::FilterType::EXISTS:
+                    return "∃";
+                case storm::jani::FilterType::FORALL:
+                    return "∀";
+                case storm::jani::FilterType::ARGMIN:
+                    return "argmin";
+                case storm::jani::FilterType::ARGMAX:
+                    return "argmax";
+                case storm::jani::FilterType::VALUES:
+                    return "values";
+                    
+            }
+        }
+        
+        modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) {
+            modernjson::json propDecl;
+            propDecl["states"] = "initial";
+            propDecl["fun"] = janiFilterTypeString(fe.getFilterType());
+            propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel);
+            return propDecl;
+        }
+        
+        
+        void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool continuousModel) {
+            std::vector<modernjson::json> properties;
+            uint64_t index = 0;
+            for(auto const& f : formulas) {
+                modernjson::json propDecl;
+                propDecl["name"] = "prop" + std::to_string(index);
+                propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), continuousModel);
+                ++index;
+                properties.push_back(propDecl);
+            }
+            jsonStruct["properties"] = properties;
+        }
+        
         
     }
 }

src/storage/jani/JSONExporter.h

@@ -30,8 +30,9 @@ namespace storm {
         };
         
         class FormulaToJaniJson : public storm::logic::FormulaVisitor {
-            public:
-            static modernjson::json translate(storm::logic::Formula const& formula);
+        
+        public:
+            static modernjson::json translate(storm::logic::Formula const& formula, bool continuousTime);
             virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const;
@@ -51,19 +52,21 @@ namespace storm {
             virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const;
       
-            
+        private:
+            FormulaToJaniJson(bool continuousModel) : continuous(continuousModel) { }
+            bool continuous;
         };
         
         class JsonExporter {
             JsonExporter() = default;
             
         public:
-            static void toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid = true);
-            static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream, bool checkValid = false);
+            static void toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid = true);
+            static void toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& ostream, bool checkValid = false);
             
         private:
             void convertModel(storm::jani::Model const& model);
-            void convertProperty(storm::logic::Formula const& formula);
+            void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool timeContinuousModel);
             void appendVariableDeclaration(storm::jani::Variable const& variable);
             
             modernjson::json finalize() {

src/storage/jani/Property.cpp

@@ -1,11 +1,11 @@
 #include "Property.h"
 namespace storm {
     namespace jani {
-//        Property::Property(std::string const& name, std::string const& comment)
-//        : name(name), formula(formula), comment(comment)
-//        {
-//
-//        }
+        Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment)
+        : name(name), filterExpression(FilterExpression(formula)), comment(comment)
+        {
+
+        }
 
         std::string const& Property::getName() const {
             return this->name;

src/storage/jani/Property.h

@@ -8,20 +8,25 @@ namespace storm {
         enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES };
         
         
-        class PropertyExpression {
-            
-        };
         
-        class FilterExpression : public PropertyExpression {
-            std::shared_ptr<PropertyExpression> states;
-            std::shared_ptr<PropertyExpression> values;
-            FilterType ft;
+        class FilterExpression {
+        public:
+            explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula) : values(formula) {}
+            
+            std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
+                return values;
+            }
+            
+            FilterType getFilterType() const {
+                return ft;
+            }
+        private:
+            // For now, we assume that the states are always the initial states.
+            
+            std::shared_ptr<storm::logic::Formula const> values;
+            FilterType ft = FilterType::VALUES;
         };
         
-        class PathExpression : public PropertyExpression {
-            std::shared_ptr<PropertyExpression> leftStateExpression;
-            std::shared_ptr<PropertyExpression> rightStateExpression;
-        };
         
         
         
@@ -49,7 +54,7 @@ namespace storm {
         private:
             std::string name;
             std::string comment;
-            PropertyExpression propertyExpression;
+            FilterExpression filterExpression;
         };
     }
 }