Fixed output of properties in the prism syntax.

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

@@ -131,7 +131,8 @@ namespace storm {
             if (!properties.empty()) {
                 storm::utility::openFile(filename + ".props", stream);
                 for (auto const& prop : properties) {
-                    stream << prop << std::endl;
+                    stream << prop.asPrismSyntax() << std::endl;
+                    STORM_LOG_WARN_COND(!prop.containsUndefinedConstants(), "A property contains undefined constants. These might not be exported correctly.");
                 }
                 storm::utility::closeFile(stream);
             }
@@ -139,11 +140,10 @@ namespace storm {
         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;
+                STORM_LOG_WARN_COND(!prop.containsUndefinedConstants(), "A property contains undefined constants. These might not be exported correctly.");
+                ostream << prop.asPrismSyntax() << std::endl;
             }
         }
-
-
         
     }
 }

src/storm/modelchecker/results/FilterType.cpp

@@ -31,5 +31,31 @@ namespace storm {
             }
             STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType");
         }
+        
+        std::string toPrismSyntax(FilterType ft) {
+            switch(ft) {
+                case FilterType::ARGMAX:
+                    return "argmax";
+                case FilterType::ARGMIN:
+                    return "argmin";
+                case FilterType::AVG:
+                    return "avg";
+                case FilterType::COUNT:
+                    return "count";
+                case FilterType::EXISTS:
+                    return "exists";
+                case FilterType::FORALL:
+                    return "forall";
+                case FilterType::MAX:
+                    return "max";
+                case FilterType::MIN:
+                    return "min";
+                case FilterType::SUM:
+                    return "sum";
+                case FilterType::VALUES:
+                    return "printall";
+            }
+            STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown FilterType");
+        }
     }
 }

src/storm/modelchecker/results/FilterType.h

@@ -9,6 +9,7 @@ namespace storm {
         enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES };
         
         std::string toString(FilterType);
+        std::string toPrismSyntax(FilterType);
         bool isStateFilter(FilterType);
     }
 }

src/storm/storage/jani/Property.cpp

@@ -25,6 +25,29 @@ namespace storm {
             return this->comment;
         }
         
+        std::string Property::asPrismSyntax() const {
+            std::stringstream stream;
+            if (!this->getName().empty()) {
+                stream << "\"" << this->getName() << "\": ";
+            }
+            auto fe = this->getFilter();
+            if (fe.isDefault()) {
+                stream << *fe.getFormula();
+            } else {
+                stream << "filter(" << storm::modelchecker::toString(fe.getFilterType()) << ", " << *fe.getFormula();
+                if (fe.getStatesFormula() && !fe.getStatesFormula()->isInitialFormula()) {
+                    stream << ", " << *fe.getFormula();
+                }
+                stream << ")";
+            }
+            stream << ";";
+            
+            if (!this->getComment().empty()) {
+                stream << " // " << this->getComment();
+            }
+            return stream.str();
+        }
+        
         Property Property::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             std::set<storm::expressions::Variable> remainingUndefinedConstants;
             for (auto const& constant : undefinedConstants) {

src/storm/storage/jani/Property.h

@@ -53,6 +53,10 @@ namespace storm {
                 return ft;
             }
             
+            bool isDefault() const {
+                return (ft == storm::modelchecker::FilterType::VALUES) && statesFormula && statesFormula->isInitialFormula();
+            }
+            
             FilterExpression substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
                 return FilterExpression(formula->substitute(substitution), ft, statesFormula->substitute(substitution));
             }
@@ -127,6 +131,8 @@ namespace storm {
             
             FilterExpression const& getFilter() const;
             
+            std::string asPrismSyntax() const;
+            
             std::set<storm::expressions::Variable> const& getUndefinedConstants() const;
             bool containsUndefinedConstants() const;
             std::set<storm::expressions::Variable> getUsedVariablesAndConstants() const;