diff --git a/randmu.py b/randmu.py
index 0179c5a3ebe217f56d279394c74d06f6fbd3e9e1..3431ef12fe4710ba3a2554ed98102fabce37ac3d 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):