diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index c133d1673..aa5c1896e 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/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 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; } } - - } } diff --git a/src/storm/modelchecker/results/FilterType.cpp b/src/storm/modelchecker/results/FilterType.cpp index e7eac999b..5ef67b036 100644 --- a/src/storm/modelchecker/results/FilterType.cpp +++ b/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"); + } } } diff --git a/src/storm/modelchecker/results/FilterType.h b/src/storm/modelchecker/results/FilterType.h index a683574c1..2aff071d5 100644 --- a/src/storm/modelchecker/results/FilterType.h +++ b/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); } } diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp index 999968e12..d24b3a3fe 100644 --- a/src/storm/storage/jani/Property.cpp +++ b/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 const& substitution) const { std::set remainingUndefinedConstants; for (auto const& constant : undefinedConstants) { diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h index 213c2e273..199dbe19f 100644 --- a/src/storm/storage/jani/Property.h +++ b/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 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 const& getUndefinedConstants() const; bool containsUndefinedConstants() const; std::set getUsedVariablesAndConstants() const;