,,,,,,,,,,,,,,,,,,,          ,,,,,,,,,,,,,,,,,,,,,,,,,,,,
        : LTL formula `f' :_____     : Negated LTL formula `!f' :
        '''''''T''''''T''''     \ ___'''''''T'''''''''''T''''''''
               |       \      ___X         /            |
               |        \ ___/    \______ /             |
               |      ___X               X_______       |
               |     /    \             /        \      |
               V    V      V           V          V     V
        ::::::::::::::::  ::::::::::::::::       ::::::::::::::::
        : LTL-to-Buchi :  : LTL-to-Buchi : . . . : LTL-to-Buchi :
        : translator 1 :  : translator 2 :       : translator n :
        ::::::::::::::::  ::::::::::::::::       ::::::::::::::::
           |        |            |   |              /       |
           |        |            |   |             /        |
           V        V            |   |            V         V
    ,,,,,,,,,,,,, ,,,,,,,,,,,,,, |   | ,,,,,,,,,,,,, ,,,,,,,,,,,,,,
    : Automaton : : Automaton  : |   | : Automaton : : Automaton  :
    : 1 for `f' : : 1 for `!f' : |   | : n for `f' : : n for `!f' :
    ''''''''''''' ''T''''''''''' |   | ''''''''''T'' ''''''''''''''
   /       ________/             |   |            \_________       \
  /       /                      V   V                      \       \ 
 /       /            ,,,,,,,,,,,,, ,,,,,,,,,,,,,,           \       \
|       |             : Automaton : : Automaton  :            |       |
|      / \            : 2 for `f' : : 2 for `!f' :           / \      |
|     |   |           ''T''''T''T'' ''T''T''''T'''          |   |     |
|     |   |             |    |  |     |  |    |             |   |     |
|     |   V             V    |  |     |  |    V             V   |     |
|     |  #################   |   \   /   |   #################  |     |
|     |  # Intersection  #   |    \ /    |   # Intersection  #  |     |
|     |  #   emptiness   #   |     X     |   #   emptiness   #  |     |
|     |  #     check     #   !    / \    !   #     check     #  |     |
|\    |  #################   :   /   \   :   #################  |    /|
| \    \___________        _____/     \_____        ___________/    / |
|  \               \      /  .           .  \      /               /  |
|   \             / \    |   :           :   |    / \             /   |
|    V           V   \   |   |           |   |   /   V           V    |
|  #################  \ /    V           V    \ /  #################  |
|  # Intersection  #   X   #################   X   # Intersection  #  |
|  #   emptiness   #  / \  # Intersection  #  / \  #   emptiness   #  |
|  #     check     # |   | #   emptiness   # |   | #     check     #  |
|  ################# |   | #     check     # |   | #################  |
|\                   |   | ################# |   |                   /|
| \                 /     \                 /     \                 / |
|  V               V       V               V       V               V  |
|   #################      #################      #################   |
|   # Intersection  #      # Intersection  #      # Intersection  #   |
|   #   emptiness   #      #   emptiness   #      #   emptiness   #   |
|   #     check     #      #     check     #      #     check     #   |
|   #################      #################      #################   |
 \                                                                   /
  \                        #################                        /
   \                       # Intersection  #                       /
    +--------------------->#   emptiness   #<---------------------+
                           #     check     #
                           #################