From be3e506cbee9f4883faadaacbc04d18c93c767ac Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 18 Dec 2016 18:08:21 +0100
Subject: [PATCH] ltl formulae

---
 formula_ltl.py | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 formula_ltl.py

diff --git a/formula_ltl.py b/formula_ltl.py
new file mode 100644
index 0000000..479b89e
--- /dev/null
+++ b/formula_ltl.py
@@ -0,0 +1,57 @@
+from enum import Enum
+
+LTL_form_type = Enum('LTL_form_type', 'proposition negation globally next until release')
+
+class FormulaLTL(object):
+    
+    def __init__(self, type, L_oper = None, R_oper = None, proposition = ""):
+        self.type = type
+        self.left_operand = L_oper
+        self.right_operand = R_oper
+        self.proposition = proposition
+    
+    def __repr__(self):
+        if self.type == LTL_form_type.proposition:
+            return self.proposition
+        if self.type == LTL_form_type.negation:
+            return "NOT( " + repr(self.left_operand) + " )"
+        if self.type == LTL_form_type.globally:
+            return "G( " + repr(self.left_operand) + " )"
+        if self.type == LTL_form_type.next:
+            return "X( " + repr(self.left_operand) + " )"
+        if self.type == LTL_form_type.until:
+            return "( " + repr(self.left_operand) + " U " + repr(self.right_operand) + " )"
+        if self.type == LTL_form_type.release:
+            return "( " + repr(self.left_operand) + " R " + repr(self.right_operand) + " )"
+
+    @classmethod
+    def f_prop(cls, proposition_name):
+        return cls(LTL_form_type.proposition, proposition = proposition_name)
+
+    @classmethod
+    def f_NOT(cls, arg):
+        return cls(LTL_form_type.negation, L_oper = arg)
+
+    @classmethod
+    def f_X(cls, arg):
+        return cls(LTL_form_type.next, L_oper = arg)
+
+    @classmethod
+    def f_G(cls, arg):
+        return cls(LTL_form_type.globally, L_oper = arg)
+    
+    @classmethod
+    def f_U(cls, arg_L, arg_R):
+        return cls(LTL_form_type.until, L_oper = arg_L, R_oper = arg_R)
+
+    @classmethod
+    def f_R(cls, arg_L, arg_R):
+        return cls(LTL_form_type.release, L_oper = arg_L, R_oper = arg_R)
+    
+
+x = FormulaLTL.f_NOT( FormulaLTL.f_X( FormulaLTL.f_prop("a") ) )
+
+print(x)
+
+        
+