From e8d5caa78d12409ba9b32f52f7aeb504728e8304 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Sun, 7 Aug 2016 17:25:26 +0200
Subject: [PATCH] added support for implies

Former-commit-id: 0a4b510b7416349cfda317f157d4a5d0bc6b869f [formerly 32a59d85f935cc700690fc2c733d65dc471aa250]
Former-commit-id: 1582f84bf111479fb6cbfe0822b39ad1b7762e4a
---
 src/parser/JaniParser.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp
index 03b3e3063..2cb834742 100644
--- a/src/parser/JaniParser.cpp
+++ b/src/parser/JaniParser.cpp
@@ -326,6 +326,12 @@ namespace storm {
                         ensureBooleanType(arguments[0], opstring, 0, scopeDescription);
                         ensureBooleanType(arguments[1], opstring, 1, scopeDescription);
                         return arguments[0] && arguments[1];
+                    } else if (opstring == "⇒") {
+                        arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars);
+                        assert(arguments.size() == 2);
+                        ensureBooleanType(arguments[0], opstring, 0, scopeDescription);
+                        ensureBooleanType(arguments[0], opstring, 1, scopeDescription);
+                        return (!arguments[0]) || arguments[1];
                     } else if (opstring == "¬") {
                         arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars);
                         assert(arguments.size() == 1);