diff --git a/NEWS b/NEWS
index 4a0b72e72..919e5b84f 100644
--- a/NEWS
+++ b/NEWS
@@ -37,6 +37,16 @@ New in spot 2.6.2.dev (not yet released)
       formula::F(unsigned, unsigned, formula)
       formula::G(unsigned, unsigned, formula)
 
+  - spot::unabbreviate(), used to rewrite away operators such as M or
+    W, learned to use some shorter rewritings when an argument (e) is
+    a pure eventuality or (u) is purely universal:
+
+      Fe = e
+      Gu = u
+      f R u = u
+      f M e = F(f & e)
+      f W u = G(f | u)
+
   - The twa_graph class has a new dump_storage_as_dot() method
     to show its data structure.  This is more conveniently used
     as aut.show_storage() in a Jupyter notebook.  See
diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex
index b80191c00..41bb87fde 100644
--- a/doc/tl/tl.tex
+++ b/doc/tl/tl.tex
@@ -1272,18 +1272,23 @@ instance passing the string \texttt{"\^{}ei"} will rewrite all
 occurrences of $\XOR$, $\EQUIV$ and $\IMPLIES$.
 
 \[
-\begin{array}{l@{\qquad}r@{\;}c@{\;}l}
+\begin{array}{l@{\qquad}r@{\;}c@{\;}ll}
 ``\texttt{i}" & f\IMPLIES g &\equiv&  (\NOT f)\OR g\\
 ``\texttt{e}" & f\EQUIV g &\equiv&  (f\AND g)\OR ((\NOT g)\AND(\NOT f))\\
 ``\texttt{\^{}e}" & f\XOR g &\equiv&  (f\AND\NOT g)\OR (g\AND\NOT f)\\
 ``\texttt{\^{}}"\text{~without~}``\texttt{e}" & f\XOR g &\equiv&  \NOT(f\EQUIV g)\\
+``\texttt{F}" & \F e&\equiv& e & \text{when $e$ is a pure eventuality}\\
 ``\texttt{F}" & \F f&\equiv& \1\U f\\
+``\texttt{G}" & \G u&\equiv& u & \text{when $u$ is purely universal}\\
 ``\texttt{G}"\text{~without~}``\texttt{R}" & \G f&\equiv& \0\R f \\
 ``\texttt{GR}"\text{~without~}``\texttt{W}" & \G f&\equiv& f \W \0 \\
 ``\texttt{GRW}" & \G f&\equiv& \NOT\F\NOT f \\
+``\texttt{M}" & f \M e&\equiv& \F(f\AND e) & \text{when $e$ is a pure eventuality} \\
 ``\texttt{M}" & f \M g&\equiv& g \U (g \AND f) \\
+``\texttt{R}" & f \R u&\equiv& u & \text{when $u$ is purely universal} \\
 ``\texttt{R}"\text{~without~}``\texttt{W}" & f \R g&\equiv&  g\W (f \AND g)\\
 ``\texttt{RW}" & f \R g&\equiv&  g\U ((f \AND g) \OR \G g) \\
+``\texttt{W}" & f \W u&\equiv& \G(f \OR u) & \text{when $u$ is purely universal} \\
 ``\texttt{W}"\text{~without~}``\texttt{R}" & f \W g&\equiv& g \R (g \OR f)\\
 ``\texttt{WR}" & f \W g&\equiv& f \U (g \OR \G f)\\
 \end{array}
diff --git a/spot/tl/unabbrev.cc b/spot/tl/unabbrev.cc
index c7bc01924..3238c079e 100644
--- a/spot/tl/unabbrev.cc
+++ b/spot/tl/unabbrev.cc
@@ -115,18 +115,30 @@ namespace spot
       case op::FStar:
         break;
       case op::F:
+        //  F e = e    if e eventual
         //  F f = true U f
         if (!re_f_)
           break;
+        if (out[0].is_eventual())
+          {
+            out = out[0];
+            break;
+          }
         out = formula::U(formula::tt(), out[0]);
         break;
       case op::G:
+        //  G u = u   if u universal
         //  G f = false R f
         //  G f = f W false
         //  G f = !F!f
         //  G f = !(true U !f)
         if (!re_g_)
           break;
+        if (out[0].is_universal())
+          {
+            out = out[0];
+            break;
+          }
         if (!re_r_)
           {
             out = formula::R(formula::ff(), out[0]);
@@ -188,6 +200,7 @@ namespace spot
           break;
         }
       case op::R:
+        // f1 R u = u   if u universal
         // f1 R f2 = f2 W (f1 & f2)
         // f1 R f2 = f2 U ((f1 & f2) | Gf2)
         // f1 R f2 = f2 U ((f1 & f2) | !F!f2)
@@ -195,8 +208,13 @@ namespace spot
         if (!re_r_)
           break;
         {
-          auto f1 = out[0];
           auto f2 = out[1];
+          if (f2.is_universal())
+            {
+              out = f2;
+              break;
+            }
+          auto f1 = out[0];
           auto f12 = formula::And({f1, f2});
           if (!re_w_)
             {
@@ -210,6 +228,7 @@ namespace spot
           break;
         }
       case op::W:
+        // f1 W u = G(f1 | u)   if u universal
         // f1 W f2 = f2 R (f2 | f1)
         // f1 W f2 = f1 U (f2 | G f1)
         // f1 W f2 = f1 U (f2 | !F !f1)
@@ -219,9 +238,15 @@ namespace spot
         {
           auto f1 = out[0];
           auto f2 = out[1];
+          if (f2.is_universal())
+            {
+              auto g = formula::G(formula::Or({f1, f2}));
+              out = re_g_ ? run(g) : g;
+              break;
+            }
           if (!re_r_)
             {
-              out = formula::R(f2, formula::Or({f2, f1}));
+              out = formula::R(f2, formula::Or({f1, f2}));
               break;
             }
           auto gf1 = formula::G(f1);
@@ -231,12 +256,21 @@ namespace spot
           break;
         }
       case op::M:
+        // f1 M e = F(f1 & e)   if e eventual
         // f1 M f2 = f2 U (g2 & f1)
         if (!re_m_)
           break;
         {
+          auto f1 = out[0];
           auto f2 = out[1];
-          out = formula::U(f2, formula::And({f2, out[0]}));
+          auto andf = formula::And({f1, f2});
+          if (f2.is_eventual())
+            {
+              auto f = formula::F(andf);
+              out = re_f_ ? run(f) : f;
+              break;
+            }
+          out = formula::U(f2, andf);
           break;
         }
       }
diff --git a/tests/core/unabbrevwm.test b/tests/core/unabbrevwm.test
index 089df24c3..622b5f7c2 100755
--- a/tests/core/unabbrevwm.test
+++ b/tests/core/unabbrevwm.test
@@ -1,6 +1,6 @@
 #! /bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2012, 2015, 2017 Laboratoire de Recherche et Développement
+# Copyright (C) 2012, 2015, 2017, 2018 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -26,16 +26,33 @@
 set -e
 
 # Removing W,M in this formula caused a segfault at some point.
-run 0 ltlfilt --remove-wm >out <<EOF
+run 0 ltlfilt --remove-wm <<EOF | uniq >out
 (!((G(p0)) U ((F(p0)) M ((F(X(p1))) & ((p2) W (G(p2))))))) M (F(p0))
-(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))
+F(Fp0 & !(Gp0 U ((FXp1 & G(p2 | Gp2)) U (Fp0 & FXp1 & G(p2 | Gp2)))))
 EOF
 
 # The first formula will be simplified to the second, so after uniq
 # the output should have one line.
-test `uniq out | wc -l` = 1
+test `wc -l <out` = 1
 
-for i in 'GFa' 'a R b' 'a W b' 'a M b'; do
+f='(Fp0 U(Fp0&!(Gp0 U((FXp1 &(Gp2 R(p2|Gp2))) U(Fp0&FXp1&(Gp2 R(p2|Gp2)))))))'
+test `ltlfilt -c --equivalent-to="$f" out` = 1
+
+
+# From issue #362.
+simon='!p0 W (p0 W (!p0 W (p0 W G!p0)))'
+ltlfilt --unabbrev=WRMF -f "$simon" -f 'FGFa' -f 'a M Fb' -f 'a R Gb' >out
+cat out
+cat >expected <<EOF
+G(!p0 | G(p0 | G(!p0 | G(p0 | G!p0))))
+G(1 U a)
+1 U (a & (1 U b))
+Gb
+EOF
+diff out expected
+
+
+for i in 'GFa' 'a R b' 'a W b' 'a M b' "$simon"; do
     for fg in '' F G GF; do
 	for rwm in '' R W M RW RM WM RWM; do
 	    ltlfilt -f "$i" --unabbrev=$fg$rwm --equivalent-to "$i" >out
diff --git a/tests/python/randltl.ipynb b/tests/python/randltl.ipynb
index f777ed6b1..b607d4beb 100644
--- a/tests/python/randltl.ipynb
+++ b/tests/python/randltl.ipynb
@@ -4,15 +4,13 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "# Documentation for spot's randltl python binding"
+    "# Documentation for Spot's randltl Python binding"
    ]
   },
   {
    "cell_type": "code",
    "execution_count": 1,
-   "metadata": {
-    "collapsed": true
-   },
+   "metadata": {},
    "outputs": [],
    "source": [
     "import spot"
@@ -35,9 +33,7 @@
   {
    "cell_type": "code",
    "execution_count": 2,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -65,9 +61,7 @@
   {
    "cell_type": "code",
    "execution_count": 3,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -96,9 +90,7 @@
   {
    "cell_type": "code",
    "execution_count": 4,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -141,9 +133,7 @@
   {
    "cell_type": "code",
    "execution_count": 5,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -175,9 +165,7 @@
   {
    "cell_type": "code",
    "execution_count": 6,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -209,9 +197,7 @@
   {
    "cell_type": "code",
    "execution_count": 7,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -247,9 +233,7 @@
   {
    "cell_type": "code",
    "execution_count": 8,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -274,9 +258,7 @@
   {
    "cell_type": "code",
    "execution_count": 9,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -303,9 +285,7 @@
   {
    "cell_type": "code",
    "execution_count": 10,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -335,9 +315,7 @@
   {
    "cell_type": "code",
    "execution_count": 11,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -468,9 +446,7 @@
   {
    "cell_type": "code",
    "execution_count": 12,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -505,9 +481,7 @@
   {
    "cell_type": "code",
    "execution_count": 13,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -540,9 +514,7 @@
   {
    "cell_type": "code",
    "execution_count": 14,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -573,9 +545,7 @@
   {
    "cell_type": "code",
    "execution_count": 15,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -601,9 +571,7 @@
   {
    "cell_type": "code",
    "execution_count": 16,
-   "metadata": {
-    "collapsed": false
-   },
+   "metadata": {},
    "outputs": [
     {
      "name": "stdout",
@@ -615,7 +583,7 @@
       "1 U (!p2 U ((p0 & !p2) | !(1 U p2)))\n",
       "(!p1 U ((!p1 & (1 U !(1 U !p1))) | !(1 U p1))) | !(1 U !(p0 | (1 U p1)))\n",
       "X(p2 & X(p2 U (!p0 | !(1 U !p2))))\n",
-      "(1 U p2) | (X(!p2 | !(1 U !p2)) U ((1 U p2) U (!p1 & (1 U p2))))\n",
+      "(1 U p2) | (X(!p2 | !(1 U !p2)) U (1 U (!p1 & (1 U p2))))\n",
       "XX!(1 U !((X!p1 U (!p2 U (!p0 & !p2))) | X!(1 U !p0)))\n",
       "XX(1 U (p1 U ((p0 & p1) | !(1 U !p1))))\n",
       "p2 & Xp0\n"
@@ -628,10 +596,8 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 16,
-   "metadata": {
-    "collapsed": false
-   },
+   "execution_count": null,
+   "metadata": {},
    "outputs": [],
    "source": []
   }
@@ -652,7 +618,7 @@
    "name": "python",
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
-   "version": "3.4.3+"
+   "version": "3.6.6+"
   }
  },
  "nbformat": 4,