From 7d83cfb6993ce630734116caea2f4094461b00f3 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 23 May 2016 01:28:19 +0200
Subject: [PATCH] use correct modal operator for ATL
---
randmu.py | 12 ++++++------
1 file changed, 6 insertions(+), 6 deletions(-)
diff --git a/randmu.py b/randmu.py
index 0179c5a..3431ef1 100755
--- a/randmu.py
+++ b/randmu.py
@@ -410,9 +410,9 @@ class Next(ATL):
def __str__(self):
subformula = str(self._subformula)
if syntax == 'tatl':
- return "<<%s>>X (%s)" % (self.coalition(), subformula,)
+ return "<<%s>>X(%s)" % (self.coalition(), subformula,)
else:
- return "<<%s>>(%s)" % (self.coalition(), subformula,)
+ return "[{%s}](%s)" % (self.coalition(), subformula,)
def replace(self, what, withw):
@@ -433,9 +433,9 @@ class Always(ATL):
def __str__(self):
subformula = str(self._subformula)
if syntax == 'tatl':
- return "<<%s>>G (%s)" % (self.coalition(), subformula,)
+ return "<<%s>>G(%s)" % (self.coalition(), subformula,)
else:
- return "(ν X . (%s) & <<%s>>X" % (subformula,self.coalition())
+ return "(ν X . ((%s) & [{%s}]X))" % (subformula,self.coalition())
def replace(self, what, withw):
@@ -458,7 +458,7 @@ class Eventually(ATL):
if syntax == 'tatl':
return "<<%s>>F(%s)" % (self.coalition(), subformula,)
else:
- return "(μ X . (%s | <<%s>>X))" % (subformula,self.coalition())
+ return "(μ X . ((%s) | [{%s}]X))" % (subformula, self.coalition())
def replace(self, what, withw):
@@ -483,7 +483,7 @@ class Until(ATL):
if syntax == 'tatl':
return "<<%s>>((%s) U (%s))" % (self.coalition(),left, right)
else:
- return "(μ X . ((%s) | <<%s>>(%s))))" % (right,self.coalition(),left)
+ return "(μ X . ((%s) | ((%s) & [{%s}]X)))" % (right,left,self.coalition())
def replace(self, what, withw):
--
GitLab