From 435b3084cb3ce58e18839824ecc9a228f14bff4d Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 19 Oct 2016 19:21:05 +0200
Subject: [PATCH] Finally, Globally

Former-commit-id: fa2ff942debbd67dfe6ef818b29d8ab8f88a706e [formerly 105d3af63147bd53e591b7d0329fbe363c7dc01e]
Former-commit-id: 1560f7cfce335ce66278b63a4016b482b66da0b5
---
 src/parser/JaniParser.cpp | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index db1819643..b328969d9 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -313,9 +313,17 @@ namespace storm {
                 } else if (opString == "Smin" || opString == "Smax") {
                     std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, "");
                     STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported");
-                } else if (opString == "U") {
+                } else if (opString == "U" || opString == "F") {
                     assert(bound == boost::none);
-                    std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, "");
+                    std::vector<std::shared_ptr<storm::logic::Formula const>> args;
+                    if (opString == "U") {
+                        args = parseBinaryFormulaArguments(propertyStructure, opString, "");
+                    } else {
+                        assert(opString == "F");
+                        args = parseUnaryFormulaArgument(propertyStructure, opString, "");
+                        args.push_back(args[0]);
+                        args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula();
+                    }
                     if (propertyStructure.count("step-bounds") > 0) {
                         storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds"));
                         STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound");
@@ -348,9 +356,24 @@ namespace storm {
                     } else {
                         return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]);
                     }
+                } else if (opString == "G") {
+                    assert(bound == boost::none);
+                    std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, "Subformula of globally operator " + context);
+                    if (propertyStructure.count("step-bounds") > 0) {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently");
+                    } else if (propertyStructure.count("time-bounds") > 0) {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by Storm");
+                    } else if (propertyStructure.count("reward-bounds") > 0 ) {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");
+                    }
+                    return std::make_shared<storm::logic::GloballyFormula const>(args[1]);
+
                 } else if (opString == "W") {
                     assert(bound == boost::none);
                     STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported");
+                } else if (opString == "R") {
+                    assert(bound == boost::none);
+                    STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Release is not supported");
                 } else if (opString == "∧" || opString == "∨") {
                     assert(bound == boost::none);
                     std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, "");