From 1713a2cbe569c07d345bf7929f350a924f46fea6 Mon Sep 17 00:00:00 2001
From: Paul Tristan Wagner <paultristanwagner@gmail.com>
Date: Wed, 27 Sep 2023 13:35:26 +0200
Subject: [PATCH] Reformat code

---
 README.md                                     |  87 ++-
 examples/ts0.json                             |  80 ++-
 .../modelchecking/Formula.java                |   3 +-
 .../paultristanwagner/modelchecking/Main.java | 336 +++++-----
 .../modelchecking/ModelChecker.java           |   2 +-
 .../modelchecking/ModelCheckingResult.java    |  14 +-
 .../modelchecking/automaton/GNBA.java         | 252 +++----
 .../modelchecking/automaton/GNBABuilder.java  |  92 +--
 .../modelchecking/automaton/NBA.java          | 346 +++++-----
 .../modelchecking/automaton/NBABuilder.java   | 102 +--
 .../automaton/NBAEmptinessResult.java         |  36 +-
 .../automaton/NBATransition.java              |  98 +--
 .../ctl/BasicCTLModelChecker.java             | 321 +++++----
 .../modelchecking/ctl/CTLENFConverter.java    | 199 +++---
 .../modelchecking/ctl/CTLModelChecker.java    |   4 +-
 .../ctl/CTLModelCheckingResult.java           |  18 +-
 .../ctl/formula/path/CTLAlwaysFormula.java    |  18 +-
 .../formula/path/CTLEventuallyFormula.java    |  20 +-
 .../ctl/formula/path/CTLNextFormula.java      |   4 +-
 .../ctl/formula/path/CTLPathFormula.java      |   4 +-
 .../ctl/formula/path/CTLUntilFormula.java     |  42 +-
 .../ctl/formula/state/CTLAllFormula.java      |  20 +-
 .../ctl/formula/state/CTLAndFormula.java      |  32 +-
 .../ctl/formula/state/CTLExistsFormula.java   |  20 +-
 .../ctl/formula/state/CTLFalseFormula.java    |   3 +-
 .../ctl/formula/state/CTLFormula.java         |   4 +-
 .../formula/state/CTLIdentifierFormula.java   |  16 +-
 .../ctl/formula/state/CTLNotFormula.java      |  12 +-
 .../ctl/formula/state/CTLOrFormula.java       |   4 +-
 .../formula/state/CTLParenthesisFormula.java  |  12 +-
 .../ctl/formula/state/CTLTrueFormula.java     |   9 +-
 .../modelchecking/ctl/parse/CTLLexer.java     |  72 +-
 .../modelchecking/ctl/parse/CTLParser.java    |  64 +-
 .../ltl/BasicLTLModelChecker.java             | 628 +++++++++---------
 .../modelchecking/ltl/LTLModelChecker.java    |   5 +-
 .../ltl/LTLModelCheckingResult.java           |  28 +-
 .../ltl/formula/LTLAlwaysFormula.java         |  76 +--
 .../ltl/formula/LTLAndFormula.java            |  88 +--
 .../ltl/formula/LTLEventuallyFormula.java     |  77 +--
 .../ltl/formula/LTLFalseFormula.java          |  55 +-
 .../modelchecking/ltl/formula/LTLFormula.java |  39 +-
 .../ltl/formula/LTLIdentifierFormula.java     |  71 +-
 .../ltl/formula/LTLNextFormula.java           |  76 +--
 .../ltl/formula/LTLNotFormula.java            |   4 +-
 .../ltl/formula/LTLOrFormula.java             |  88 +--
 .../ltl/formula/LTLParenthesisFormula.java    |  73 +-
 .../ltl/formula/LTLTrueFormula.java           |  55 +-
 .../ltl/formula/LTLUntilFormula.java          |  92 +--
 .../modelchecking/ltl/parse/LTLLexer.java     |  47 +-
 .../modelchecking/ltl/parse/LTLParser.java    | 277 ++++----
 .../modelchecking/parse/Lexer.java            |  20 +-
 .../modelchecking/parse/Parser.java           |   8 +-
 .../modelchecking/parse/SyntaxError.java      |  64 +-
 .../modelchecking/parse/Token.java            |  16 +-
 .../modelchecking/parse/TokenType.java        |  16 +-
 .../modelchecking/ts/InfinitePath.java        |   4 +-
 .../modelchecking/ts/TSPersistenceResult.java |  36 +-
 .../modelchecking/ts/TSTransition.java        |   4 +-
 .../modelchecking/ts/TransitionSystem.java    |  69 +-
 .../ts/TransitionSystemBuilder.java           |  71 +-
 .../modelchecking/util/AnsiColor.java         |   2 +-
 .../modelchecking/util/Symbol.java            |  28 +-
 .../modelchecking/util/TupleUtil.java         |  22 +-
 .../modelchecking/GNBATest.java               |   5 +-
 .../modelchecking/SynchronousProductTest.java |  33 +-
 65 files changed, 2324 insertions(+), 2199 deletions(-)

diff --git a/README.md b/README.md
index 6c34d21..b3bf948 100644
--- a/README.md
+++ b/README.md
@@ -1,15 +1,21 @@
 # Model Checking
+
 This project is a practice environment for implementing algorithms related to model checking.
-The techniques used here are used here are introduced in the RWTH Aachen University lecture 'Model Checking' by [Prof. Dr. Ir. Dr. h. c. Joost-Pieter Katoen](https://moves.rwth-aachen.de/people/katoen/) 
-and can be read up in the book [Principles of Model Checking](https://mitpress.mit.edu/9780262026499/principles-of-model-checking/) by Christel Baier and Joost-Pieter Katoen.
+The techniques used here are used here are introduced in the RWTH Aachen University lecture 'Model Checking'
+by [Prof. Dr. Ir. Dr. h. c. Joost-Pieter Katoen](https://moves.rwth-aachen.de/people/katoen/)
+and can be read up in the
+book [Principles of Model Checking](https://mitpress.mit.edu/9780262026499/principles-of-model-checking/) by Christel
+Baier and Joost-Pieter Katoen.
 
-Model checking is a technique used to formally verify whether a given system model satisfies a desired property or specification. In this project, model checking algorithms are implemented to analyze transition systems.
+Model checking is a technique used to formally verify whether a given system model satisfies a desired property or
+specification. In this project, model checking algorithms are implemented to analyze transition systems.
 
 ## How to build and run the project
-Clone the git repository: <br> 
+
+Clone the git repository: <br>
 ``git clone https://github.com/paultristanwagner/model-checking.git`` <br>
 Navigate into the created directory: <br>
-``cd model-checking`` <br> 
+``cd model-checking`` <br>
 Let Gradle build the project (Use the Gradle wrapper as shown here or install Gradle >= 8.1.1): <br>
 ``./gradlew jar`` <br>
 Run the project: <br>
@@ -17,10 +23,14 @@ Run the project: <br>
 Now you should see the command line asking you to specify a file defining a transition system.
 
 ## Transition systems
-A transition system is a tuple (S, Act, T, I, AP, L) where S is a set of states, Act is a set of actions, T is a transition relation, I is a set of initial states, AP is a set of atomic propositions and L is a labeling function that assigns a subset of the atomic propositions to each state.
+
+A transition system is a tuple (S, Act, T, I, AP, L) where S is a set of states, Act is a set of actions, T is a
+transition relation, I is a set of initial states, AP is a set of atomic propositions and L is a labeling function that
+assigns a subset of the atomic propositions to each state.
 In this project, transition systems can be defined in files in json format.
 (For simplicity, the set of actions is not needed for now.)
 Example: See examples/ts0.json
+
 ```
 {
 	"states": ["s0","s1","s2","s3","s4"],
@@ -48,70 +58,109 @@ Example: See examples/ts0.json
 <img src="images/ts0.png" alt="Transition system defined in examples/ts0.json" width="500" /> <br>
 
 ### Load a transition system from a file
+
 To load a transition system from a file, enter the path to the file in the command line. <br>
 Example: <br>
 <img src="images/load_transition_system.png" alt="Loading a transition system from a file" width="500" />
 
 ## LTL: Linear Temporal Logic
-[Linear Temporal Logic (LTL)](https://en.wikipedia.org/wiki/Linear_temporal_logic) is a modal temporal logic used for reasoning about the behavior of systems over time. It provides a formal language for expressing properties and conditions that hold in the future of paths or sequences of events. LTL allows us to describe assertions such as "a condition will eventually be true" or "a condition will hold until another fact becomes true.
+
+[Linear Temporal Logic (LTL)](https://en.wikipedia.org/wiki/Linear_temporal_logic) is a modal temporal logic used for
+reasoning about the behavior of systems over time. It provides a formal language for expressing properties and
+conditions that hold in the future of paths or sequences of events. LTL allows us to describe assertions such as "a
+condition will eventually be true" or "a condition will hold until another fact becomes true.
 Example LTL formulas:
+
 - □(safe) - "The system is always in a safe state"
 - ◇(response) - "At some point in the future, the system will respond to a request"
 - ◇□(a) - "At some point in the future, the system will always be in a state where a is true"
 
 ## CTL: Computation Tree Logic
-[Computation Tree Logic (CTL)](https://en.wikipedia.org/wiki/Computation_tree_logic) is a formal logic used for specifying and verifying properties of concurrent and reactive systems. It stands out among other temporal logics due to its branching-time nature, which allows for modeling and reasoning about systems where multiple alternative paths and future outcomes are possible. In CTL, the notion of time is represented as a tree-like structure, reflecting the non-deterministic nature of system behavior. This tree encompasses different branches, each corresponding to a distinct possible future path that the system may take.
+
+[Computation Tree Logic (CTL)](https://en.wikipedia.org/wiki/Computation_tree_logic) is a formal logic used for
+specifying and verifying properties of concurrent and reactive systems. It stands out among other temporal logics due to
+its branching-time nature, which allows for modeling and reasoning about systems where multiple alternative paths and
+future outcomes are possible. In CTL, the notion of time is represented as a tree-like structure, reflecting the
+non-deterministic nature of system behavior. This tree encompasses different branches, each corresponding to a distinct
+possible future path that the system may take.
 Example CTL formulas:
+
 - ∃◇(error) - "There exists a way for the system to reach an error state"
 - ∀◇(error) - "For all possible ways the system can evolve, there exists a way to reach an error state"
 - ∀□(∃◇(reset)) - "For all possible ways the system can evolve, it is always possible to reset the system"
 
 ## Model checking of LTL and CTL formulas
+
 In this project, model checking algorithms for LTL as well as CTL formulas are implemented.
 A simple parser is used to parse LTL and CTL formulas based on a flexible grammar.
 
 ### Examples of LTL model checking
+
 We can check LTL properties for the previously shown transition system defined in ``examples/ts0.json``: <br>
 
 φ := □(a) - "The system is always in a state where a is true" <br>
 <img src="images/always_a.png" alt="□(a)" width="500" /> <br>
-Explanation: The formula does not hold for the transition system because there exists a path starting in s0 that leads to s4 where a is already initially false.
+Explanation: The formula does not hold for the transition system because there exists a path starting in s0 that leads
+to s4 where a is already initially false.
 
 φ := ◇(b) - "At some point in the future, the system will be in a state where b is true" <br>
 <img src="images/eventually_b.png" alt="◇(b)" width="500" /> <br>
-Explanation: The formula holds for the transition system because every path of the transition system must visit either s3 or s4.
+Explanation: The formula holds for the transition system because every path of the transition system must visit either
+s3 or s4.
 
 φ := ◇□(a) - "From some point in the future, the system will always be in a state where a is true" <br>
 <img src="images/eventually_always_a.png" alt="◇□(a)" width="500" /> <br>
-Explanation: The formula does not hold for the transition system because there exists a path starting in s0 that leads to s4 where it stays forever. And a does not hold in s4.
+Explanation: The formula does not hold for the transition system because there exists a path starting in s0 that leads
+to s4 where it stays forever. And a does not hold in s4.
 
 ### Examples of CTL model checking
+
 We can check CTL properties for the previously shown transition system defined in ``examples/ts0.json``: <br>
 
 Φ := ∀◊(b) - "For all possible ways the system can evolve, there exists a way to reach a state where b is true" <br>
 <img src="images/all_eventually_b.png" alt="∀◊(b)" width="500" /> <br>
-Explanation: The formula holds for the transition system because every path in the transition system must visit either s3 or s4.
+Explanation: The formula holds for the transition system because every path in the transition system must visit either
+s3 or s4.
 
 Φ := ∀◯(¬a) - "For all possible ways the system can evolve the next state will not be a"
 <img src="images/all_next_not_a.png" alt="∀◯(¬a)" width="500" /> <br>
-Explanation: The formula does not hold for the transition system because there exists a path starting in s0 that leads to s1 where a is true.
+Explanation: The formula does not hold for the transition system because there exists a path starting in s0 that leads
+to s1 where a is true.
 
-Φ := ∀□(∃◊(¬a ∧ ¬b)) - "For all possible ways the system can evolve, it is always possible to reach a state where a and b are false" <br>
+Φ := ∀□(∃◊(¬a ∧ ¬b)) - "For all possible ways the system can evolve, it is always possible to reach a state where a and
+b are false" <br>
 <img src="images/all_always_ex_eventually_reset.png" alt="∀□(∃◊(¬a ∧ ¬b))" width="500" /> <br>
-Explanation: The formula does not hold for the transition system because for the path starting in s0 going to s4, it is not possible anymore to reach a state where a and b are false.
+Explanation: The formula does not hold for the transition system because for the path starting in s0 going to s4, it is
+not possible anymore to reach a state where a and b are false.
 
 ## Comparison of LTL and CTL
-CTL and LTL have distinct characteristics and expressiveness, making them incomparable in terms of their expressive power. CTL focuses on reasoning about paths in a computation tree and allows for the specification of temporal properties that hold on all or some of the paths. On the other hand, LTL deals with linear sequences of states and enables the specification of temporal properties that hold along all possible executions. Although they serve different purposes, CTL and LTL can complement each other in the context of model checking, as they provide different perspectives and approaches to reasoning about temporal properties in concurrent systems.
 
-The computational complexity of model checking for Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) differs, with LTL model checking being PSPACE-complete and CTL model checking being PTIME-complete. While it might seem that CTL model checking is more efficient due to its PTIME complexity, it is important to note that the length of the formula plays a significant role. In many cases, LTL formulas can be exponentially shorter than their CTL equivalents. This means that even though CTL model checking has a better complexity class, the actual runtime can be influenced by the size of the formula. Therefore, the efficiency of model checking depends not only on the computational complexity class but also on the specific properties being checked and the lengths of the corresponding formulas in LTL and CTL.
+CTL and LTL have distinct characteristics and expressiveness, making them incomparable in terms of their expressive
+power. CTL focuses on reasoning about paths in a computation tree and allows for the specification of temporal
+properties that hold on all or some of the paths. On the other hand, LTL deals with linear sequences of states and
+enables the specification of temporal properties that hold along all possible executions. Although they serve different
+purposes, CTL and LTL can complement each other in the context of model checking, as they provide different perspectives
+and approaches to reasoning about temporal properties in concurrent systems.
+
+The computational complexity of model checking for Linear Temporal Logic (LTL) and Computation Tree Logic (CTL) differs,
+with LTL model checking being PSPACE-complete and CTL model checking being PTIME-complete. While it might seem that CTL
+model checking is more efficient due to its PTIME complexity, it is important to note that the length of the formula
+plays a significant role. In many cases, LTL formulas can be exponentially shorter than their CTL equivalents. This
+means that even though CTL model checking has a better complexity class, the actual runtime can be influenced by the
+size of the formula. Therefore, the efficiency of model checking depends not only on the computational complexity class
+but also on the specific properties being checked and the lengths of the corresponding formulas in LTL and CTL.
 
 ## Contributing
-Thank you for your interest in contributing to this project! Contributions are welcome and greatly appreciated. 
+
+Thank you for your interest in contributing to this project! Contributions are welcome and greatly appreciated.
 
 ## Feedback and Troubleshooting
-If you have any feedback or encounter any issues, please open an issue on GitHub or E-Mail me at: [paultristanwagner@gmail.com](mailto:paultristanwagner@gmail.com).
+
+If you have any feedback or encounter any issues, please open an issue on GitHub or E-Mail me
+at: [paultristanwagner@gmail.com](mailto:paultristanwagner@gmail.com).
 
 ## Ideas for future work
+
 - Write tests for the CTL and LTL model checking algorithms
 - Optimize the lookup of the next states in the transition system
 - Implement linear-time fixpoint computation in CTL model checking
diff --git a/examples/ts0.json b/examples/ts0.json
index bc4f8a8..605201d 100644
--- a/examples/ts0.json
+++ b/examples/ts0.json
@@ -1,21 +1,63 @@
 {
-	"states": ["s0","s1","s2","s3","s4"],
-	"transitions": [
-		["s0","s1"],
-		["s1","s2"],
-		["s2","s3"],
-		["s3","s3"],
-		["s3","s0"],
-		["s0","s4"],
-		["s4","s4"]
-	],
-	"initialStates": ["s0","s3"],
-	"atomicPropositions": ["a","b"],
-	"labelingFunction": {
-		"s0": [],
-		"s1": ["a"],
-		"s2": ["a","b"],
-		"s3": ["b"],
-		"s4": ["b"]
-	}
+  "states": [
+    "s0",
+    "s1",
+    "s2",
+    "s3",
+    "s4"
+  ],
+  "transitions": [
+    [
+      "s0",
+      "s1"
+    ],
+    [
+      "s1",
+      "s2"
+    ],
+    [
+      "s2",
+      "s3"
+    ],
+    [
+      "s3",
+      "s3"
+    ],
+    [
+      "s3",
+      "s0"
+    ],
+    [
+      "s0",
+      "s4"
+    ],
+    [
+      "s4",
+      "s4"
+    ]
+  ],
+  "initialStates": [
+    "s0",
+    "s3"
+  ],
+  "atomicPropositions": [
+    "a",
+    "b"
+  ],
+  "labelingFunction": {
+    "s0": [],
+    "s1": [
+      "a"
+    ],
+    "s2": [
+      "a",
+      "b"
+    ],
+    "s3": [
+      "b"
+    ],
+    "s4": [
+      "b"
+    ]
+  }
 }
\ No newline at end of file
diff --git a/src/main/java/me/paultristanwagner/modelchecking/Formula.java b/src/main/java/me/paultristanwagner/modelchecking/Formula.java
index 8017bb2..68bb4d9 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/Formula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/Formula.java
@@ -1,4 +1,3 @@
 package me.paultristanwagner.modelchecking;
 
-public abstract class Formula {
-}
+public abstract class Formula {}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/Main.java b/src/main/java/me/paultristanwagner/modelchecking/Main.java
index cacee9e..c290245 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/Main.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/Main.java
@@ -1,5 +1,15 @@
 package me.paultristanwagner.modelchecking;
 
+import static java.nio.charset.StandardCharsets.UTF_8;
+import static me.paultristanwagner.modelchecking.util.AnsiColor.*;
+import static me.paultristanwagner.modelchecking.util.Symbol.MODELS_SYMBOL;
+import static me.paultristanwagner.modelchecking.util.Symbol.NOT_MODELS_SYMBOL;
+
+import java.io.*;
+import java.nio.file.Files;
+import java.util.NoSuchElementException;
+import java.util.Optional;
+import java.util.Scanner;
 import me.paultristanwagner.modelchecking.ctl.BasicCTLModelChecker;
 import me.paultristanwagner.modelchecking.ctl.CTLModelChecker;
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
@@ -14,185 +24,175 @@
 import me.paultristanwagner.modelchecking.ts.TransitionSystem;
 import me.paultristanwagner.modelchecking.util.Symbol;
 
-import java.io.*;
-import java.nio.file.Files;
-import java.util.NoSuchElementException;
-import java.util.Optional;
-import java.util.Scanner;
-
-import static java.nio.charset.StandardCharsets.UTF_8;
-import static me.paultristanwagner.modelchecking.util.AnsiColor.*;
-import static me.paultristanwagner.modelchecking.util.Symbol.MODELS_SYMBOL;
-import static me.paultristanwagner.modelchecking.util.Symbol.NOT_MODELS_SYMBOL;
-
 public class Main {
 
-    public static final PrintStream OUT = new PrintStream(new FileOutputStream(FileDescriptor.out), true, UTF_8);
-    public static final Scanner SCANNER = new Scanner(System.in);
-
-    public static void main(String[] args) {
-        TransitionSystem ts = enterTransitionSystem();
-
-        while (true) {
-            OUT.print("Enter formula: ");
-            String input;
-            try {
-                input = SCANNER.nextLine();
-            } catch (NoSuchElementException e) {
-                break;
-            }
-
-            if (input.equals("exit")) {
-                break;
-            }
-
-            long before = System.currentTimeMillis();
-            Formula formula = parseFormula(input);
-            if (formula == null) {
-                continue;
-            }
-
-            String phiSymbol;
-
-            ModelCheckingResult result;
-            Optional<InfinitePath> counterExample = Optional.empty();
-            if (formula instanceof LTLFormula ltlFormula) {
-                phiSymbol = Symbol.LOWERCASE_PHI_SYMBOL;
-                OUT.println(phiSymbol + " := " + formula + GRAY + " (LTL)" + RESET);
-
-                LTLModelChecker modelChecker = new BasicLTLModelChecker();
-                LTLModelCheckingResult ltlModelCheckingResult = modelChecker.check(ts, ltlFormula);
-                result = ltlModelCheckingResult;
-
-                if (!ltlModelCheckingResult.isModel()) {
-                    counterExample = Optional.of(ltlModelCheckingResult.getCounterExample());
-                }
-            } else if (formula instanceof CTLFormula ctlFormula) {
-                phiSymbol = Symbol.UPPERCASE_PHI_SYMBOL;
-
-                OUT.println(phiSymbol + " := " + formula + GRAY + " (CTL)" + RESET);
-
-                CTLModelChecker modelChecker = new BasicCTLModelChecker();
-                result = modelChecker.check(ts, ctlFormula);
-            } else {
-                OUT.println(RED + "Unknown formula type" + RESET);
-                continue;
-            }
-
-            if (result.isModel()) {
-                OUT.println(GREEN + "TS " + MODELS_SYMBOL + " " + phiSymbol + RESET);
-            } else {
-                OUT.println(RED + "TS " + NOT_MODELS_SYMBOL + " " + phiSymbol);
-                counterExample.ifPresent(infinitePath -> OUT.println("Counterexample: " + infinitePath));
-                OUT.print(RESET);
-            }
-
-            long after = System.currentTimeMillis();
-
-            long time_ms = after - before;
-            OUT.println(GRAY + "(" + time_ms + " ms)" + RESET);
-            OUT.println();
+  public static final PrintStream OUT =
+      new PrintStream(new FileOutputStream(FileDescriptor.out), true, UTF_8);
+  public static final Scanner SCANNER = new Scanner(System.in);
+
+  public static void main(String[] args) {
+    TransitionSystem ts = enterTransitionSystem();
+
+    while (true) {
+      OUT.print("Enter formula: ");
+      String input;
+      try {
+        input = SCANNER.nextLine();
+      } catch (NoSuchElementException e) {
+        break;
+      }
+
+      if (input.equals("exit")) {
+        break;
+      }
+
+      long before = System.currentTimeMillis();
+      Formula formula = parseFormula(input);
+      if (formula == null) {
+        continue;
+      }
+
+      String phiSymbol;
+
+      ModelCheckingResult result;
+      Optional<InfinitePath> counterExample = Optional.empty();
+      if (formula instanceof LTLFormula ltlFormula) {
+        phiSymbol = Symbol.LOWERCASE_PHI_SYMBOL;
+        OUT.println(phiSymbol + " := " + formula + GRAY + " (LTL)" + RESET);
+
+        LTLModelChecker modelChecker = new BasicLTLModelChecker();
+        LTLModelCheckingResult ltlModelCheckingResult = modelChecker.check(ts, ltlFormula);
+        result = ltlModelCheckingResult;
+
+        if (!ltlModelCheckingResult.isModel()) {
+          counterExample = Optional.of(ltlModelCheckingResult.getCounterExample());
         }
+      } else if (formula instanceof CTLFormula ctlFormula) {
+        phiSymbol = Symbol.UPPERCASE_PHI_SYMBOL;
+
+        OUT.println(phiSymbol + " := " + formula + GRAY + " (CTL)" + RESET);
+
+        CTLModelChecker modelChecker = new BasicCTLModelChecker();
+        result = modelChecker.check(ts, ctlFormula);
+      } else {
+        OUT.println(RED + "Unknown formula type" + RESET);
+        continue;
+      }
+
+      if (result.isModel()) {
+        OUT.println(GREEN + "TS " + MODELS_SYMBOL + " " + phiSymbol + RESET);
+      } else {
+        OUT.println(RED + "TS " + NOT_MODELS_SYMBOL + " " + phiSymbol);
+        counterExample.ifPresent(infinitePath -> OUT.println("Counterexample: " + infinitePath));
+        OUT.print(RESET);
+      }
+
+      long after = System.currentTimeMillis();
+
+      long time_ms = after - before;
+      OUT.println(GRAY + "(" + time_ms + " ms)" + RESET);
+      OUT.println();
     }
+  }
 
-    private static Formula parseFormula(String input) {
-        boolean ltl = input.toLowerCase().startsWith("ltl ");
-        boolean ctl = input.toLowerCase().startsWith("ctl ");
-
-        if (ltl || ctl) {
-            input = input.substring(4);
-        }
+  private static Formula parseFormula(String input) {
+    boolean ltl = input.toLowerCase().startsWith("ltl ");
+    boolean ctl = input.toLowerCase().startsWith("ctl ");
 
-        if (ltl) {
-            try {
-                return parseLTLFormula(input);
-            } catch (SyntaxError error) {
-                OUT.print(RED);
-                error.printWithContext();
-                OUT.print(RESET);
-            }
-        } else if (ctl) {
-            try {
-                return parseCTLFormula(input);
-            } catch (SyntaxError error) {
-                OUT.print(RED);
-                error.printWithContext();
-                OUT.print(RESET);
-            }
-        } else {
-            try {
-                return parseCTLFormula(input);
-            } catch (SyntaxError error1) {
-                try {
-                    return parseLTLFormula(input);
-                } catch (SyntaxError error2) {
-                    OUT.print(RED);
-                    OUT.println("Could not parse either CTL or LTL formula!");
-                    OUT.print("CTL: ");
-                    error1.printWithContext();
-                    OUT.print("LTL: ");
-                    error2.printWithContext();
-                    OUT.print(RESET);
-                }
-            }
-        }
-
-        return null;
-    }
-
-    private static LTLFormula parseLTLFormula(String string) {
-        LTLParser ltlParser = new LTLParser();
-        return ltlParser.parse(string);
+    if (ltl || ctl) {
+      input = input.substring(4);
     }
 
-    private static CTLFormula parseCTLFormula(String string) {
-        CTLParser ctlParser = new CTLParser();
-        return ctlParser.parse(string);
+    if (ltl) {
+      try {
+        return parseLTLFormula(input);
+      } catch (SyntaxError error) {
+        OUT.print(RED);
+        error.printWithContext();
+        OUT.print(RESET);
+      }
+    } else if (ctl) {
+      try {
+        return parseCTLFormula(input);
+      } catch (SyntaxError error) {
+        OUT.print(RED);
+        error.printWithContext();
+        OUT.print(RESET);
+      }
+    } else {
+      try {
+        return parseCTLFormula(input);
+      } catch (SyntaxError error1) {
+        try {
+          return parseLTLFormula(input);
+        } catch (SyntaxError error2) {
+          OUT.print(RED);
+          OUT.println("Could not parse either CTL or LTL formula!");
+          OUT.print("CTL: ");
+          error1.printWithContext();
+          OUT.print("LTL: ");
+          error2.printWithContext();
+          OUT.print(RESET);
+        }
+      }
     }
 
-    private static TransitionSystem enterTransitionSystem() {
-        TransitionSystem ts = null;
-        while (ts == null) {
-            File file = null;
-            while (file == null) {
-                OUT.print("Enter file for Transition System: ");
-                String input;
-                try {
-                    input = SCANNER.nextLine();
-                } catch (NoSuchElementException e) {
-                    return null;
-                }
-
-                file = new File(input);
-                if (!file.exists()) {
-                    OUT.println(RED + "Error: File does not exist!" + RESET);
-                    OUT.println();
-                    file = null;
-                } else if (file.isDirectory()) {
-                    OUT.println(RED + "Error: File is a directory!" + RESET);
-                    OUT.println();
-                    file = null;
-                }
-            }
-
-            String fileContent;
-            try {
-                fileContent = new String(Files.readAllBytes(file.toPath()));
-            } catch (IOException e) {
-                OUT.println(RED + "Error: Could not read file" + RESET);
-                continue;
-            }
-
-            try {
-                ts = TransitionSystem.fromJson(fileContent);
-                OUT.println(GREEN + "Transition System loaded!" + RESET);
-            } catch (SyntaxError error) {
-                OUT.print(RED);
-                error.printWithContext();
-                OUT.print(RESET);
-            }
+    return null;
+  }
+
+  private static LTLFormula parseLTLFormula(String string) {
+    LTLParser ltlParser = new LTLParser();
+    return ltlParser.parse(string);
+  }
+
+  private static CTLFormula parseCTLFormula(String string) {
+    CTLParser ctlParser = new CTLParser();
+    return ctlParser.parse(string);
+  }
+
+  private static TransitionSystem enterTransitionSystem() {
+    TransitionSystem ts = null;
+    while (ts == null) {
+      File file = null;
+      while (file == null) {
+        OUT.print("Enter file for Transition System: ");
+        String input;
+        try {
+          input = SCANNER.nextLine();
+        } catch (NoSuchElementException e) {
+          return null;
         }
 
-        return ts;
+        file = new File(input);
+        if (!file.exists()) {
+          OUT.println(RED + "Error: File does not exist!" + RESET);
+          OUT.println();
+          file = null;
+        } else if (file.isDirectory()) {
+          OUT.println(RED + "Error: File is a directory!" + RESET);
+          OUT.println();
+          file = null;
+        }
+      }
+
+      String fileContent;
+      try {
+        fileContent = new String(Files.readAllBytes(file.toPath()));
+      } catch (IOException e) {
+        OUT.println(RED + "Error: Could not read file" + RESET);
+        continue;
+      }
+
+      try {
+        ts = TransitionSystem.fromJson(fileContent);
+        OUT.println(GREEN + "Transition System loaded!" + RESET);
+      } catch (SyntaxError error) {
+        OUT.print(RED);
+        error.printWithContext();
+        OUT.print(RESET);
+      }
     }
+
+    return ts;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java
index 6f56ea4..16eebc0 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ModelChecker.java
@@ -4,5 +4,5 @@
 
 public interface ModelChecker<T extends Formula, R extends ModelCheckingResult> {
 
-    R check(TransitionSystem ts, T formula );
+  R check(TransitionSystem ts, T formula);
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ModelCheckingResult.java b/src/main/java/me/paultristanwagner/modelchecking/ModelCheckingResult.java
index d3ff7aa..5cd5d9d 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ModelCheckingResult.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ModelCheckingResult.java
@@ -2,13 +2,13 @@
 
 public abstract class ModelCheckingResult {
 
-    protected final boolean models;
+  protected final boolean models;
 
-    public ModelCheckingResult( boolean models) {
-        this.models = models;
-    }
+  public ModelCheckingResult(boolean models) {
+    this.models = models;
+  }
 
-    public boolean isModel() {
-        return models;
-    }
+  public boolean isModel() {
+    return models;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
index ff13e70..3533d2d 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBA.java
@@ -1,161 +1,165 @@
 package me.paultristanwagner.modelchecking.automaton;
 
+import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
+
 import com.google.gson.Gson;
 import com.google.gson.GsonBuilder;
-
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
 
-import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
-
 public final class GNBA {
 
-    private static final Gson GSON;
-    private final List<String> states;
-    private final List<String> alphabet;
-    private final List<String> initialStates;
-    private final List<List<String>> acceptingSets;
-    private final List<NBATransition> transitions;
-
-    public GNBA(List<String> states, List<String> alphabet, List<String> initialStates,
-                List<List<String>> acceptingSets, List<NBATransition> transitions) {
-        this.states = states;
-        this.alphabet = alphabet;
-        this.initialStates = initialStates;
-        this.acceptingSets = acceptingSets;
-        this.transitions = transitions;
+  private static final Gson GSON;
+  private final List<String> states;
+  private final List<String> alphabet;
+  private final List<String> initialStates;
+  private final List<List<String>> acceptingSets;
+  private final List<NBATransition> transitions;
+
+  public GNBA(
+      List<String> states,
+      List<String> alphabet,
+      List<String> initialStates,
+      List<List<String>> acceptingSets,
+      List<NBATransition> transitions) {
+    this.states = states;
+    this.alphabet = alphabet;
+    this.initialStates = initialStates;
+    this.acceptingSets = acceptingSets;
+    this.transitions = transitions;
+  }
+
+  static {
+    GSON =
+        new GsonBuilder()
+            .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
+            .setPrettyPrinting()
+            .create();
+  }
+
+  public Set<String> getSuccessors(String state) {
+    Set<String> successors = new HashSet<>();
+    for (NBATransition transition : transitions) {
+      if (transition.getFrom().equals(state)) {
+        successors.add(transition.getTo());
+      }
     }
-
-    static {
-        GSON = new GsonBuilder()
-                .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
-                .setPrettyPrinting()
-                .create();
-    }
-
-    public Set<String> getSuccessors(String state) {
-        Set<String> successors = new HashSet<>();
-        for (NBATransition transition : transitions) {
-            if (transition.getFrom().equals(state)) {
-                successors.add(transition.getTo());
-            }
-        }
-        return successors;
+    return successors;
+  }
+
+  public Set<String> getSuccessors(String state, String action) {
+    Set<String> successors = new HashSet<>();
+    for (NBATransition transition : transitions) {
+      if (transition.getFrom().equals(state) && transition.getAction().equals(action)) {
+        successors.add(transition.getTo());
+      }
     }
+    return successors;
+  }
 
-    public Set<String> getSuccessors(String state, String action) {
-        Set<String> successors = new HashSet<>();
-        for (NBATransition transition : transitions) {
-            if (transition.getFrom().equals(state) && transition.getAction().equals(action)) {
-                successors.add(transition.getTo());
-            }
-        }
-        return successors;
+  public NBA convertToNBA() {
+    if (acceptingSets.size() <= 1) {
+      return getCanonicalNBA();
     }
 
-    public NBA convertToNBA() {
-        if (acceptingSets.size() <= 1) {
-            return getCanonicalNBA();
-        }
-
-        NBABuilder builder = new NBABuilder();
-        builder.setAlphabet(alphabet);
-
-        for (String state : states) {
-            for (int i = 0; i < acceptingSets.size(); i++) {
-                String nbaState = stringTuple(state, i + 1);
-                builder.addState(nbaState);
-            }
-        }
-
-        for (String initialState : initialStates) {
-            String nbaInitialState = stringTuple(initialState, 1);
-            builder.addInitialState(nbaInitialState);
-        }
-
-        if (!acceptingSets.isEmpty()) {
-            List<String> acceptingSet = acceptingSets.get(0);
-            for (String acceptingState : acceptingSet) {
-                String nbaAcceptingState = stringTuple(acceptingState, 1);
-                builder.addAcceptingState(nbaAcceptingState);
-            }
-        }
-
-        for (NBATransition transition : transitions) {
-            for (int i = 0; i < acceptingSets.size(); i++) {
-                List<String> acceptingSet = acceptingSets.get(i);
-                String nbaFrom = stringTuple(transition.getFrom(), i + 1);
-                String nbaTo;
-                if (acceptingSet.contains(transition.getFrom())) {
-                    nbaTo = stringTuple(transition.getTo(), ((i + 1) % acceptingSets.size() + 1));
-                } else {
-                    nbaTo = stringTuple(transition.getTo(), (i + 1));
-                }
-                builder.addTransition(nbaFrom, transition.getAction(), nbaTo);
-            }
-        }
+    NBABuilder builder = new NBABuilder();
+    builder.setAlphabet(alphabet);
 
-        return builder.build();
+    for (String state : states) {
+      for (int i = 0; i < acceptingSets.size(); i++) {
+        String nbaState = stringTuple(state, i + 1);
+        builder.addState(nbaState);
+      }
     }
 
-    private NBA getCanonicalNBA() {
-        if (acceptingSets.size() > 1) {
-            throw new IllegalStateException("GNBA has more than one accepting set");
-        }
-
-        NBABuilder builder = new NBABuilder();
-        builder.setAlphabet(alphabet);
-        for (String state : states) {
-            builder.addState(state);
-        }
+    for (String initialState : initialStates) {
+      String nbaInitialState = stringTuple(initialState, 1);
+      builder.addInitialState(nbaInitialState);
+    }
 
-        for (String initialState : initialStates) {
-            builder.addInitialState(initialState);
-        }
+    if (!acceptingSets.isEmpty()) {
+      List<String> acceptingSet = acceptingSets.get(0);
+      for (String acceptingState : acceptingSet) {
+        String nbaAcceptingState = stringTuple(acceptingState, 1);
+        builder.addAcceptingState(nbaAcceptingState);
+      }
+    }
 
-        if (acceptingSets.isEmpty()) {
-            for (String state : states) {
-                builder.addAcceptingState(state);
-            }
+    for (NBATransition transition : transitions) {
+      for (int i = 0; i < acceptingSets.size(); i++) {
+        List<String> acceptingSet = acceptingSets.get(i);
+        String nbaFrom = stringTuple(transition.getFrom(), i + 1);
+        String nbaTo;
+        if (acceptingSet.contains(transition.getFrom())) {
+          nbaTo = stringTuple(transition.getTo(), ((i + 1) % acceptingSets.size() + 1));
         } else {
-            for (String acceptingState : acceptingSets.get(0)) {
-                builder.addAcceptingState(acceptingState);
-            }
+          nbaTo = stringTuple(transition.getTo(), (i + 1));
         }
+        builder.addTransition(nbaFrom, transition.getAction(), nbaTo);
+      }
+    }
 
-        for (NBATransition transition : transitions) {
-            builder.addTransition(transition.getFrom(), transition.getAction(), transition.getTo());
-        }
+    return builder.build();
+  }
 
-        return builder.build();
+  private NBA getCanonicalNBA() {
+    if (acceptingSets.size() > 1) {
+      throw new IllegalStateException("GNBA has more than one accepting set");
     }
 
-    public String toJson() {
-        return GSON.toJson(this);
+    NBABuilder builder = new NBABuilder();
+    builder.setAlphabet(alphabet);
+    for (String state : states) {
+      builder.addState(state);
     }
 
-    public static GNBA fromJson(String json) {
-        return GSON.fromJson(json, GNBA.class);
+    for (String initialState : initialStates) {
+      builder.addInitialState(initialState);
     }
 
-    public List<String> getStates() {
-        return states;
+    if (acceptingSets.isEmpty()) {
+      for (String state : states) {
+        builder.addAcceptingState(state);
+      }
+    } else {
+      for (String acceptingState : acceptingSets.get(0)) {
+        builder.addAcceptingState(acceptingState);
+      }
     }
 
-    public List<String> getInitialStates() {
-        return initialStates;
+    for (NBATransition transition : transitions) {
+      builder.addTransition(transition.getFrom(), transition.getAction(), transition.getTo());
     }
 
-    public List<String> getAlphabet() {
-        return alphabet;
-    }
+    return builder.build();
+  }
 
-    public List<List<String>> getAcceptingSets() {
-        return acceptingSets;
-    }
+  public String toJson() {
+    return GSON.toJson(this);
+  }
 
-    public List<NBATransition> getTransitions() {
-        return transitions;
-    }
+  public static GNBA fromJson(String json) {
+    return GSON.fromJson(json, GNBA.class);
+  }
+
+  public List<String> getStates() {
+    return states;
+  }
+
+  public List<String> getInitialStates() {
+    return initialStates;
+  }
+
+  public List<String> getAlphabet() {
+    return alphabet;
+  }
+
+  public List<List<String>> getAcceptingSets() {
+    return acceptingSets;
+  }
+
+  public List<NBATransition> getTransitions() {
+    return transitions;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
index 95d5ef5..3eebd52 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/GNBABuilder.java
@@ -6,60 +6,60 @@
 
 public class GNBABuilder {
 
-    private final List<String> states;
-    private final List<String> alphabet;
-    private final List<String> initialStates;
-    private final List<List<String>> acceptingSets;
-    private final List<NBATransition> transitions;
+  private final List<String> states;
+  private final List<String> alphabet;
+  private final List<String> initialStates;
+  private final List<List<String>> acceptingSets;
+  private final List<NBATransition> transitions;
 
-    public GNBABuilder() {
-        this.states = new ArrayList<>();
-        this.alphabet = new ArrayList<>();
-        this.initialStates = new ArrayList<>();
-        this.acceptingSets = new ArrayList<>();
-        this.transitions = new ArrayList<>();
-    }
-
-    public GNBABuilder addStates(String... states) {
-        for (String state : states) {
-            addState(state);
-        }
+  public GNBABuilder() {
+    this.states = new ArrayList<>();
+    this.alphabet = new ArrayList<>();
+    this.initialStates = new ArrayList<>();
+    this.acceptingSets = new ArrayList<>();
+    this.transitions = new ArrayList<>();
+  }
 
-        return this;
+  public GNBABuilder addStates(String... states) {
+    for (String state : states) {
+      addState(state);
     }
 
-    public GNBABuilder addState(String state) {
-        this.states.add(state);
-        return this;
-    }
+    return this;
+  }
 
-    public GNBABuilder setAlphabet(List<String> alphabet) {
-        this.alphabet.clear();
-        this.alphabet.addAll(alphabet);
-        return this;
-    }
+  public GNBABuilder addState(String state) {
+    this.states.add(state);
+    return this;
+  }
 
-    public GNBABuilder addInitialState(String initialState) {
-        this.initialStates.add(initialState);
-        return this;
-    }
+  public GNBABuilder setAlphabet(List<String> alphabet) {
+    this.alphabet.clear();
+    this.alphabet.addAll(alphabet);
+    return this;
+  }
 
-    public GNBABuilder addAcceptingSet(String... acceptingSet) {
-        this.acceptingSets.add(List.of(acceptingSet));
-        return this;
-    }
+  public GNBABuilder addInitialState(String initialState) {
+    this.initialStates.add(initialState);
+    return this;
+  }
 
-    public GNBABuilder addAcceptingSet(Set<String> acceptingSet) {
-        this.acceptingSets.add(new ArrayList<>(acceptingSet));
-        return this;
-    }
+  public GNBABuilder addAcceptingSet(String... acceptingSet) {
+    this.acceptingSets.add(List.of(acceptingSet));
+    return this;
+  }
 
-    public GNBABuilder addTransition(String from, String action, String to) {
-        this.transitions.add(NBATransition.of(from, action, to));
-        return this;
-    }
+  public GNBABuilder addAcceptingSet(Set<String> acceptingSet) {
+    this.acceptingSets.add(new ArrayList<>(acceptingSet));
+    return this;
+  }
 
-    public GNBA build() {
-        return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
-    }
+  public GNBABuilder addTransition(String from, String action, String to) {
+    this.transitions.add(NBATransition.of(from, action, to));
+    return this;
+  }
+
+  public GNBA build() {
+    return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
index 3ff6b4f..eb21154 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBA.java
@@ -1,215 +1,219 @@
 package me.paultristanwagner.modelchecking.automaton;
 
+import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
+
 import com.google.gson.Gson;
 import com.google.gson.GsonBuilder;
-import me.paultristanwagner.modelchecking.ts.InfinitePath;
-
 import java.util.*;
-
-import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
+import me.paultristanwagner.modelchecking.ts.InfinitePath;
 
 public class NBA {
 
-    private static final Gson GSON;
-
-    static {
-        GSON =
-                new GsonBuilder()
-                        .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
-                        .setPrettyPrinting()
-                        .create();
-    }
-
-    private final List<String> states;
-    private final List<String> alphabet;
-    private final List<String> initialStates;
-    private final List<String> acceptingStates;
-    private final List<NBATransition> transitions;
-
-    public NBA(List<String> states, List<String> alphabet, List<String> initialStates, List<String> acceptingStates, List<NBATransition> transitions) {
-        this.states = states;
-        this.alphabet = alphabet;
-        this.initialStates = initialStates;
-        this.acceptingStates = acceptingStates;
-        this.transitions = transitions;
+  private static final Gson GSON;
+
+  static {
+    GSON =
+        new GsonBuilder()
+            .registerTypeAdapter(NBATransition.class, new NBATransition.NBATransitionAdapter())
+            .setPrettyPrinting()
+            .create();
+  }
+
+  private final List<String> states;
+  private final List<String> alphabet;
+  private final List<String> initialStates;
+  private final List<String> acceptingStates;
+  private final List<NBATransition> transitions;
+
+  public NBA(
+      List<String> states,
+      List<String> alphabet,
+      List<String> initialStates,
+      List<String> acceptingStates,
+      List<NBATransition> transitions) {
+    this.states = states;
+    this.alphabet = alphabet;
+    this.initialStates = initialStates;
+    this.acceptingStates = acceptingStates;
+    this.transitions = transitions;
+  }
+
+  public Set<String> getSuccessors(String state) {
+    Set<String> successors = new HashSet<>();
+    for (NBATransition transition : transitions) {
+      if (transition.getFrom().equals(state)) {
+        successors.add(transition.getTo());
+      }
     }
-
-    public Set<String> getSuccessors(String state) {
-        Set<String> successors = new HashSet<>();
-        for (NBATransition transition : transitions) {
-            if (transition.getFrom().equals(state)) {
-                successors.add(transition.getTo());
-            }
-        }
-        return successors;
-    }
-
-    public Set<String> getSuccessors(String state, String action) {
-        Set<String> successors = new HashSet<>();
-        for (NBATransition transition : transitions) {
-            if (transition.getFrom().equals(state) && transition.getAction().equals(action)) {
-                successors.add(transition.getTo());
-            }
-        }
-        return successors;
+    return successors;
+  }
+
+  public Set<String> getSuccessors(String state, String action) {
+    Set<String> successors = new HashSet<>();
+    for (NBATransition transition : transitions) {
+      if (transition.getFrom().equals(state) && transition.getAction().equals(action)) {
+        successors.add(transition.getTo());
+      }
     }
-
-    private boolean cycleCheck(String s, Set<String> v, Stack<String> xi) {
+    return successors;
+  }
+
+  private boolean cycleCheck(String s, Set<String> v, Stack<String> xi) {
+    xi.push(s);
+    v.add(s);
+    while (!xi.isEmpty()) {
+      String s1 = xi.peek();
+      Set<String> successors = getSuccessors(s1);
+      if (successors.contains(s)) {
         xi.push(s);
-        v.add(s);
-        while (!xi.isEmpty()) {
-            String s1 = xi.peek();
-            Set<String> successors = getSuccessors(s1);
-            if (successors.contains(s)) {
-                xi.push(s);
-                return true;
-            } else if (!v.containsAll(successors)) {
-                Set<String> remainingSuccessors = new HashSet<>(successors);
-                remainingSuccessors.removeAll(v);
-
-                String s2 = remainingSuccessors.stream().findAny().get();
-                v.add(s2);
-                xi.push(s2);
-            } else {
-                xi.pop();
-            }
-        }
-
-        return false;
+        return true;
+      } else if (!v.containsAll(successors)) {
+        Set<String> remainingSuccessors = new HashSet<>(successors);
+        remainingSuccessors.removeAll(v);
+
+        String s2 = remainingSuccessors.stream().findAny().get();
+        v.add(s2);
+        xi.push(s2);
+      } else {
+        xi.pop();
+      }
     }
 
-    public NBAEmptinessResult checkEmptiness() {
-        // run a nested-depth-first-search
-        Set<String> u = new HashSet<>();
-        Set<String> v = new HashSet<>();
+    return false;
+  }
 
-        Stack<String> pi = new Stack<>();
-        Stack<String> xi = new Stack<>();
+  public NBAEmptinessResult checkEmptiness() {
+    // run a nested-depth-first-search
+    Set<String> u = new HashSet<>();
+    Set<String> v = new HashSet<>();
 
-        while (!u.containsAll(initialStates)) {
-            Set<String> remaining = new HashSet<>(initialStates);
-            remaining.removeAll(u);
+    Stack<String> pi = new Stack<>();
+    Stack<String> xi = new Stack<>();
 
-            String s0 = remaining.stream().findAny().get();
-            u.add(s0);
+    while (!u.containsAll(initialStates)) {
+      Set<String> remaining = new HashSet<>(initialStates);
+      remaining.removeAll(u);
 
-            pi.push(s0);
+      String s0 = remaining.stream().findAny().get();
+      u.add(s0);
 
-            while (!pi.isEmpty()) {
-                String s = pi.peek();
+      pi.push(s0);
 
-                Set<String> remainingSuccessors = new HashSet<>(getSuccessors(s));
-                remainingSuccessors.removeAll(u);
+      while (!pi.isEmpty()) {
+        String s = pi.peek();
 
-                if (!remainingSuccessors.isEmpty()) {
-                    String s1 = remainingSuccessors.stream().findAny().get();
-                    u.add(s1);
-                    pi.push(s1);
-                } else {
-                    pi.pop();
-                    if (acceptingStates.contains(s) && cycleCheck(s, v, xi)) {
-                        List<String> piList = new ArrayList<>(pi);
-                        List<String> xiList = new ArrayList<>(xi);
+        Set<String> remainingSuccessors = new HashSet<>(getSuccessors(s));
+        remainingSuccessors.removeAll(u);
 
-                        InfinitePath witness = new InfinitePath(piList, xiList);
-                        return NBAEmptinessResult.nonEmpty(witness);
-                    }
-                }
-            }
-        }
+        if (!remainingSuccessors.isEmpty()) {
+          String s1 = remainingSuccessors.stream().findAny().get();
+          u.add(s1);
+          pi.push(s1);
+        } else {
+          pi.pop();
+          if (acceptingStates.contains(s) && cycleCheck(s, v, xi)) {
+            List<String> piList = new ArrayList<>(pi);
+            List<String> xiList = new ArrayList<>(xi);
 
-        return NBAEmptinessResult.empty();
+            InfinitePath witness = new InfinitePath(piList, xiList);
+            return NBAEmptinessResult.nonEmpty(witness);
+          }
+        }
+      }
     }
 
-    public GNBA toGNBA() {
-        List<String> states = new ArrayList<>(this.states);
-        List<String> alphabet = new ArrayList<>(this.alphabet);
-        List<String> initialStates = new ArrayList<>(this.initialStates);
-        List<NBATransition> transitions = new ArrayList<>(this.transitions);
+    return NBAEmptinessResult.empty();
+  }
 
-        List<List<String>> acceptingSets = new ArrayList<>();
-        acceptingSets.add(new ArrayList<>(this.acceptingStates));
+  public GNBA toGNBA() {
+    List<String> states = new ArrayList<>(this.states);
+    List<String> alphabet = new ArrayList<>(this.alphabet);
+    List<String> initialStates = new ArrayList<>(this.initialStates);
+    List<NBATransition> transitions = new ArrayList<>(this.transitions);
 
-        return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
-    }
-
-    public GNBA product(NBA other) {
-        GNBABuilder builder = new GNBABuilder();
-        builder.setAlphabet(alphabet);
+    List<List<String>> acceptingSets = new ArrayList<>();
+    acceptingSets.add(new ArrayList<>(this.acceptingStates));
 
-        for (String state1 : states) {
-            for (String state2 : other.states) {
-                String state = stringTuple(state1, state2);
-                builder.addState(state);
-            }
-        }
-
-        for (String initialState : initialStates) {
-            for (String otherInitialState : other.initialStates) {
-                String state = stringTuple(initialState, otherInitialState);
-                builder.addInitialState(state);
-            }
-        }
+    return new GNBA(states, alphabet, initialStates, acceptingSets, transitions);
+  }
 
-        for (NBATransition transition : transitions) {
-            for (NBATransition otherTransition : other.transitions) {
-                if (!transition.getAction().equals(otherTransition.getAction())) {
-                    continue;
-                }
+  public GNBA product(NBA other) {
+    GNBABuilder builder = new GNBABuilder();
+    builder.setAlphabet(alphabet);
 
-                String from = stringTuple(transition.getFrom(), otherTransition.getFrom());
-                String to = stringTuple(transition.getTo(), otherTransition.getTo());
-                builder.addTransition(from, transition.getAction(), to);
-            }
-        }
+    for (String state1 : states) {
+      for (String state2 : other.states) {
+        String state = stringTuple(state1, state2);
+        builder.addState(state);
+      }
+    }
 
-        Set<String> acceptingSet1 = new HashSet<>();
-        for (String acceptingState : acceptingStates) {
-            for (String state : other.states) {
-                String newAcceptingState = stringTuple(acceptingState, state);
-                acceptingSet1.add(newAcceptingState);
-            }
-        }
+    for (String initialState : initialStates) {
+      for (String otherInitialState : other.initialStates) {
+        String state = stringTuple(initialState, otherInitialState);
+        builder.addInitialState(state);
+      }
+    }
 
-        Set<String> acceptingSet2 = new HashSet<>();
-        for (String acceptingState : other.acceptingStates) {
-            for (String state : states) {
-                String newAcceptingState = stringTuple(state, acceptingState);
-                acceptingSet2.add(newAcceptingState);
-            }
+    for (NBATransition transition : transitions) {
+      for (NBATransition otherTransition : other.transitions) {
+        if (!transition.getAction().equals(otherTransition.getAction())) {
+          continue;
         }
 
-        builder.addAcceptingSet(acceptingSet1);
-        builder.addAcceptingSet(acceptingSet2);
-
-        return builder.build();
+        String from = stringTuple(transition.getFrom(), otherTransition.getFrom());
+        String to = stringTuple(transition.getTo(), otherTransition.getTo());
+        builder.addTransition(from, transition.getAction(), to);
+      }
     }
 
-    public String toJson() {
-        return GSON.toJson(this);
+    Set<String> acceptingSet1 = new HashSet<>();
+    for (String acceptingState : acceptingStates) {
+      for (String state : other.states) {
+        String newAcceptingState = stringTuple(acceptingState, state);
+        acceptingSet1.add(newAcceptingState);
+      }
     }
 
-    public static NBA fromJson(String json) {
-        return GSON.fromJson(json, NBA.class);
+    Set<String> acceptingSet2 = new HashSet<>();
+    for (String acceptingState : other.acceptingStates) {
+      for (String state : states) {
+        String newAcceptingState = stringTuple(state, acceptingState);
+        acceptingSet2.add(newAcceptingState);
+      }
     }
 
-    public List<String> getStates() {
-        return states;
-    }
+    builder.addAcceptingSet(acceptingSet1);
+    builder.addAcceptingSet(acceptingSet2);
 
-    public List<String> getAlphabet() {
-        return alphabet;
-    }
+    return builder.build();
+  }
 
-    public List<String> getInitialStates() {
-        return initialStates;
-    }
+  public String toJson() {
+    return GSON.toJson(this);
+  }
 
-    public List<String> getAcceptingStates() {
-        return acceptingStates;
-    }
+  public static NBA fromJson(String json) {
+    return GSON.fromJson(json, NBA.class);
+  }
 
-    public List<NBATransition> getTransitions() {
-        return transitions;
-    }
+  public List<String> getStates() {
+    return states;
+  }
+
+  public List<String> getAlphabet() {
+    return alphabet;
+  }
+
+  public List<String> getInitialStates() {
+    return initialStates;
+  }
+
+  public List<String> getAcceptingStates() {
+    return acceptingStates;
+  }
+
+  public List<NBATransition> getTransitions() {
+    return transitions;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java
index 2c025d0..34527ce 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBABuilder.java
@@ -5,55 +5,55 @@
 
 public class NBABuilder {
 
-    private final List<String> states;
-    private final List<String> alphabet;
-    private final List<String> initialStates;
-    private final List<String> acceptingStates;
-    private final List<NBATransition> transitions;
-
-    public NBABuilder() {
-        this.states = new ArrayList<>();
-        this.alphabet = new ArrayList<>();
-        this.initialStates = new ArrayList<>();
-        this.acceptingStates = new ArrayList<>();
-        this.transitions = new ArrayList<>();
-    }
-
-    public NBABuilder addStates(String... states) {
-        for (String state : states) {
-            addState(state);
-        }
-
-        return this;
-    }
-
-    public NBABuilder addState(String state) {
-        this.states.add(state);
-        return this;
-    }
-
-    public NBABuilder setAlphabet(List<String> alphabet) {
-        this.alphabet.clear();
-        this.alphabet.addAll(alphabet);
-        return this;
-    }
-
-    public NBABuilder addInitialState(String initialState) {
-        this.initialStates.add(initialState);
-        return this;
-    }
-
-    public NBABuilder addAcceptingState(String acceptingState) {
-        this.acceptingStates.add(acceptingState);
-        return this;
-    }
-
-    public NBABuilder addTransition(String from, String action, String to) {
-        this.transitions.add(NBATransition.of(from, action, to));
-        return this;
-    }
-
-    public NBA build() {
-        return new NBA(states, alphabet, initialStates, acceptingStates, transitions);
-    }
+  private final List<String> states;
+  private final List<String> alphabet;
+  private final List<String> initialStates;
+  private final List<String> acceptingStates;
+  private final List<NBATransition> transitions;
+
+  public NBABuilder() {
+    this.states = new ArrayList<>();
+    this.alphabet = new ArrayList<>();
+    this.initialStates = new ArrayList<>();
+    this.acceptingStates = new ArrayList<>();
+    this.transitions = new ArrayList<>();
+  }
+
+  public NBABuilder addStates(String... states) {
+    for (String state : states) {
+      addState(state);
+    }
+
+    return this;
+  }
+
+  public NBABuilder addState(String state) {
+    this.states.add(state);
+    return this;
+  }
+
+  public NBABuilder setAlphabet(List<String> alphabet) {
+    this.alphabet.clear();
+    this.alphabet.addAll(alphabet);
+    return this;
+  }
+
+  public NBABuilder addInitialState(String initialState) {
+    this.initialStates.add(initialState);
+    return this;
+  }
+
+  public NBABuilder addAcceptingState(String acceptingState) {
+    this.acceptingStates.add(acceptingState);
+    return this;
+  }
+
+  public NBABuilder addTransition(String from, String action, String to) {
+    this.transitions.add(NBATransition.of(from, action, to));
+    return this;
+  }
+
+  public NBA build() {
+    return new NBA(states, alphabet, initialStates, acceptingStates, transitions);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBAEmptinessResult.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBAEmptinessResult.java
index 3f943b9..24c8b9c 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBAEmptinessResult.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBAEmptinessResult.java
@@ -3,27 +3,27 @@
 import me.paultristanwagner.modelchecking.ts.InfinitePath;
 
 public final class NBAEmptinessResult {
-    private final boolean isEmpty;
-    private final InfinitePath witness;
+  private final boolean isEmpty;
+  private final InfinitePath witness;
 
-    private NBAEmptinessResult(boolean isEmpty, InfinitePath witness) {
-        this.isEmpty = isEmpty;
-        this.witness = witness;
-    }
+  private NBAEmptinessResult(boolean isEmpty, InfinitePath witness) {
+    this.isEmpty = isEmpty;
+    this.witness = witness;
+  }
 
-    public static NBAEmptinessResult empty() {
-        return new NBAEmptinessResult(true, null);
-    }
+  public static NBAEmptinessResult empty() {
+    return new NBAEmptinessResult(true, null);
+  }
 
-    public static NBAEmptinessResult nonEmpty(InfinitePath witness) {
-        return new NBAEmptinessResult(false, witness);
-    }
+  public static NBAEmptinessResult nonEmpty(InfinitePath witness) {
+    return new NBAEmptinessResult(false, witness);
+  }
 
-    public boolean isEmpty() {
-        return isEmpty;
-    }
+  public boolean isEmpty() {
+    return isEmpty;
+  }
 
-    public InfinitePath getWitness() {
-        return witness;
-    }
+  public InfinitePath getWitness() {
+    return witness;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java
index 0d101ed..00f50d2 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/automaton/NBATransition.java
@@ -4,55 +4,57 @@
 
 public class NBATransition {
 
-    private final String from;
-    private final String action;
-    private final String to;
-
-    private NBATransition(String from, String action, String to) {
-        this.from = from;
-        this.action = action;
-        this.to = to;
+  private final String from;
+  private final String action;
+  private final String to;
+
+  private NBATransition(String from, String action, String to) {
+    this.from = from;
+    this.action = action;
+    this.to = to;
+  }
+
+  public static NBATransition of(String from, String action, String to) {
+    return new NBATransition(from, action, to);
+  }
+
+  public String getFrom() {
+    return from;
+  }
+
+  public String getAction() {
+    return action;
+  }
+
+  public String getTo() {
+    return to;
+  }
+
+  public static class NBATransitionAdapter
+      implements JsonSerializer<NBATransition>, JsonDeserializer<NBATransition> {
+
+    @Override
+    public JsonElement serialize(
+        NBATransition transition,
+        java.lang.reflect.Type typeOfSrc,
+        JsonSerializationContext context) {
+      JsonArray jsonArray = new JsonArray();
+      jsonArray.add(transition.getFrom());
+      jsonArray.add(transition.getAction());
+      jsonArray.add(transition.getTo());
+
+      return jsonArray;
     }
 
-    public static NBATransition of(String from, String action, String to) {
-        return new NBATransition(from, action, to);
-    }
-
-    public String getFrom() {
-        return from;
-    }
-
-    public String getAction() {
-        return action;
-    }
-
-    public String getTo() {
-        return to;
-    }
-
-    public static class NBATransitionAdapter
-            implements JsonSerializer<NBATransition>, JsonDeserializer<NBATransition> {
-
-        @Override
-        public JsonElement serialize(
-                NBATransition transition, java.lang.reflect.Type typeOfSrc, JsonSerializationContext context) {
-            JsonArray jsonArray = new JsonArray();
-            jsonArray.add(transition.getFrom());
-            jsonArray.add(transition.getAction());
-            jsonArray.add(transition.getTo());
-
-            return jsonArray;
-        }
-
-        @Override
-        public NBATransition deserialize(
-                JsonElement json, java.lang.reflect.Type typeOfT, JsonDeserializationContext context)
-                throws JsonParseException {
-            JsonArray tuple = json.getAsJsonArray();
-            String from = tuple.get(0).getAsString();
-            String action = tuple.get(1).getAsString();
-            String to = tuple.get(2).getAsString();
-            return NBATransition.of(from, action, to);
-        }
+    @Override
+    public NBATransition deserialize(
+        JsonElement json, java.lang.reflect.Type typeOfT, JsonDeserializationContext context)
+        throws JsonParseException {
+      JsonArray tuple = json.getAsJsonArray();
+      String from = tuple.get(0).getAsString();
+      String action = tuple.get(1).getAsString();
+      String to = tuple.get(2).getAsString();
+      return NBATransition.of(from, action, to);
     }
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java
index 3245654..495f0ef 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/BasicCTLModelChecker.java
@@ -1,5 +1,12 @@
 package me.paultristanwagner.modelchecking.ctl;
 
+import static me.paultristanwagner.modelchecking.ctl.CTLModelCheckingResult.doesNotModel;
+import static me.paultristanwagner.modelchecking.ctl.CTLModelCheckingResult.models;
+
+import java.util.HashSet;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Set;
 import me.paultristanwagner.modelchecking.ctl.formula.path.CTLAlwaysFormula;
 import me.paultristanwagner.modelchecking.ctl.formula.path.CTLNextFormula;
 import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula;
@@ -7,205 +14,197 @@
 import me.paultristanwagner.modelchecking.ctl.formula.state.*;
 import me.paultristanwagner.modelchecking.ts.TransitionSystem;
 
-import java.util.HashSet;
-import java.util.Iterator;
-import java.util.List;
-import java.util.Set;
-
-import static me.paultristanwagner.modelchecking.ctl.CTLModelCheckingResult.doesNotModel;
-import static me.paultristanwagner.modelchecking.ctl.CTLModelCheckingResult.models;
-
 public class BasicCTLModelChecker implements CTLModelChecker {
 
-    @Override
-    public CTLModelCheckingResult check(TransitionSystem ts, CTLFormula formula) {
-        CTLENFConverter converter = new CTLENFConverter();
-        CTLFormula enfFormula = converter.convert(formula);
+  @Override
+  public CTLModelCheckingResult check(TransitionSystem ts, CTLFormula formula) {
+    CTLENFConverter converter = new CTLENFConverter();
+    CTLFormula enfFormula = converter.convert(formula);
 
-        Set<String> satStates = sat(ts, enfFormula);
+    Set<String> satStates = sat(ts, enfFormula);
 
-        boolean models = satStates.containsAll(ts.getInitialStates());
+    boolean models = satStates.containsAll(ts.getInitialStates());
 
-        if (models) {
-            return models();
-        } else {
-            return doesNotModel();
-        }
+    if (models) {
+      return models();
+    } else {
+      return doesNotModel();
+    }
+  }
+
+  private Set<String> sat(TransitionSystem ts, CTLFormula formula) {
+    if (formula instanceof CTLIdentifierFormula identifierFormula) {
+      return satIdentifier(ts, identifierFormula);
+    } else if (formula instanceof CTLNotFormula notFormula) {
+      return satNot(ts, notFormula);
+    } else if (formula instanceof CTLOrFormula orFormula) {
+      return satOr(ts, orFormula);
+    } else if (formula instanceof CTLAndFormula andFormula) {
+      return satAnd(ts, andFormula);
+    } else if (formula instanceof CTLTrueFormula trueFormula) {
+      return satTrue(ts, trueFormula);
+    } else if (formula instanceof CTLFalseFormula falseFormula) {
+      return satFalse(ts, falseFormula);
+    } else if (formula instanceof CTLExistsFormula existsFormula) {
+      return satExists(ts, existsFormula);
+    } else if (formula instanceof CTLParenthesisFormula parenthesisFormula) {
+      return sat(ts, parenthesisFormula.getInner());
     }
 
-    private Set<String> sat(TransitionSystem ts, CTLFormula formula) {
-        if (formula instanceof CTLIdentifierFormula identifierFormula) {
-            return satIdentifier(ts, identifierFormula);
-        } else if (formula instanceof CTLNotFormula notFormula) {
-            return satNot(ts, notFormula);
-        } else if (formula instanceof CTLOrFormula orFormula) {
-            return satOr(ts, orFormula);
-        } else if (formula instanceof CTLAndFormula andFormula) {
-            return satAnd(ts, andFormula);
-        } else if (formula instanceof CTLTrueFormula trueFormula) {
-            return satTrue(ts, trueFormula);
-        } else if (formula instanceof CTLFalseFormula falseFormula) {
-            return satFalse(ts, falseFormula);
-        } else if (formula instanceof CTLExistsFormula existsFormula) {
-            return satExists(ts, existsFormula);
-        } else if (formula instanceof CTLParenthesisFormula parenthesisFormula) {
-            return sat(ts, parenthesisFormula.getInner());
-        }
-
-        throw new UnsupportedOperationException();
+    throw new UnsupportedOperationException();
+  }
+
+  private Set<String> satExists(TransitionSystem ts, CTLExistsFormula formula) {
+    CTLPathFormula pathFormula = formula.getPathFormula();
+    if (pathFormula instanceof CTLNextFormula nextFormula) {
+      return satExistsNext(ts, nextFormula);
+    } else if (pathFormula instanceof CTLUntilFormula untilFormula) {
+      return satExistsUntil(ts, untilFormula);
+    } else if (pathFormula instanceof CTLAlwaysFormula alwaysFormula) {
+      return satExistsAlways(ts, alwaysFormula);
     }
 
-    private Set<String> satExists(TransitionSystem ts, CTLExistsFormula formula) {
-        CTLPathFormula pathFormula = formula.getPathFormula();
-        if (pathFormula instanceof CTLNextFormula nextFormula) {
-            return satExistsNext(ts, nextFormula);
-        } else if (pathFormula instanceof CTLUntilFormula untilFormula) {
-            return satExistsUntil(ts, untilFormula);
-        } else if (pathFormula instanceof CTLAlwaysFormula alwaysFormula) {
-            return satExistsAlways(ts, alwaysFormula);
+    throw new UnsupportedOperationException();
+  }
+
+  private Set<String> satExistsNext(TransitionSystem ts, CTLNextFormula nextFormula) {
+    Set<String> result = new HashSet<>();
+    Set<String> satStates = sat(ts, nextFormula.getStateFormula());
+
+    for (String state : ts.getStates()) {
+      List<String> successors = ts.getSuccessors(state);
+
+      boolean hasSatSuccessor = false;
+      for (String successor : successors) {
+        if (satStates.contains(successor)) {
+          hasSatSuccessor = true;
+          break;
         }
+      }
 
-        throw new UnsupportedOperationException();
+      if (hasSatSuccessor) {
+        result.add(state);
+      }
     }
 
-    private Set<String> satExistsNext(TransitionSystem ts, CTLNextFormula nextFormula) {
-        Set<String> result = new HashSet<>();
-        Set<String> satStates = sat(ts, nextFormula.getStateFormula());
+    return result;
+  }
 
-        for (String state : ts.getStates()) {
-            List<String> successors = ts.getSuccessors(state);
+  private Set<String> satExistsUntil(TransitionSystem ts, CTLUntilFormula untilFormula) {
+    CTLFormula left = untilFormula.getLeft();
+    CTLFormula right = untilFormula.getRight();
 
-            boolean hasSatSuccessor = false;
-            for (String successor : successors) {
-                if (satStates.contains(successor)) {
-                    hasSatSuccessor = true;
-                    break;
-                }
-            }
+    Set<String> satLeft = sat(ts, left);
 
-            if (hasSatSuccessor) {
-                result.add(state);
-            }
-        }
+    Set<String> T = sat(ts, right);
 
-        return result;
-    }
+    boolean changed = true;
+    while (changed) {
+      changed = false;
 
-    private Set<String> satExistsUntil(TransitionSystem ts, CTLUntilFormula untilFormula) {
-        CTLFormula left = untilFormula.getLeft();
-        CTLFormula right = untilFormula.getRight();
-
-        Set<String> satLeft = sat(ts, left);
-
-        Set<String> T = sat(ts, right);
-
-        boolean changed = true;
-        while (changed) {
-            changed = false;
-
-            for (String state : satLeft) {
-                if (T.contains(state)) {
-                    continue;
-                }
-
-                List<String> successors = ts.getSuccessors(state);
-                boolean hasTSuccessor = false;
-                for (String successor : successors) {
-                    if (T.contains(successor)) {
-                        hasTSuccessor = true;
-                        break;
-                    }
-                }
-
-                if (hasTSuccessor) {
-                    T.add(state);
-                    changed = true;
-                }
-            }
+      for (String state : satLeft) {
+        if (T.contains(state)) {
+          continue;
         }
 
-        return T;
-    }
-
-    private Set<String> satExistsAlways(TransitionSystem ts, CTLAlwaysFormula formula) {
-        CTLFormula stateFormula = formula.getStateFormula();
-
-        Set<String> V = sat(ts, stateFormula);
-
-        boolean changed = true;
-        while (changed) {
-            changed = false;
-
-            Iterator<String> iterator = V.iterator();
-            while (iterator.hasNext()) {
-                String state = iterator.next();
-                List<String> successors = ts.getSuccessors(state);
-                boolean hasVSuccessor = false;
-                for (String successor : successors) {
-                    if (V.contains(successor)) {
-                        hasVSuccessor = true;
-                        break;
-                    }
-                }
-
-                if (!hasVSuccessor) {
-                    iterator.remove();
-                    changed = true;
-                }
-            }
+        List<String> successors = ts.getSuccessors(state);
+        boolean hasTSuccessor = false;
+        for (String successor : successors) {
+          if (T.contains(successor)) {
+            hasTSuccessor = true;
+            break;
+          }
         }
 
-        return V;
+        if (hasTSuccessor) {
+          T.add(state);
+          changed = true;
+        }
+      }
     }
 
-    private Set<String> satIdentifier(TransitionSystem ts, CTLIdentifierFormula formula) {
-        String atomicProposition = formula.getIdentifier();
+    return T;
+  }
+
+  private Set<String> satExistsAlways(TransitionSystem ts, CTLAlwaysFormula formula) {
+    CTLFormula stateFormula = formula.getStateFormula();
+
+    Set<String> V = sat(ts, stateFormula);
+
+    boolean changed = true;
+    while (changed) {
+      changed = false;
 
-        Set<String> satStates = new HashSet<>();
-        for (String state : ts.getStates()) {
-            if (ts.getLabel(state).contains(atomicProposition)) {
-                satStates.add(state);
-            }
+      Iterator<String> iterator = V.iterator();
+      while (iterator.hasNext()) {
+        String state = iterator.next();
+        List<String> successors = ts.getSuccessors(state);
+        boolean hasVSuccessor = false;
+        for (String successor : successors) {
+          if (V.contains(successor)) {
+            hasVSuccessor = true;
+            break;
+          }
         }
 
-        return satStates;
+        if (!hasVSuccessor) {
+          iterator.remove();
+          changed = true;
+        }
+      }
     }
 
-    private Set<String> satNot(TransitionSystem ts, CTLNotFormula formula) {
-        Set<String> satStates = sat(ts, formula.getArgument());
-        Set<String> allStates = new HashSet<>(ts.getStates());
+    return V;
+  }
 
-        Set<String> result = new HashSet<>(allStates);
-        result.removeAll(satStates);
+  private Set<String> satIdentifier(TransitionSystem ts, CTLIdentifierFormula formula) {
+    String atomicProposition = formula.getIdentifier();
 
-        return result;
+    Set<String> satStates = new HashSet<>();
+    for (String state : ts.getStates()) {
+      if (ts.getLabel(state).contains(atomicProposition)) {
+        satStates.add(state);
+      }
     }
 
-    private Set<String> satOr(TransitionSystem ts, CTLOrFormula formula) {
-        Set<String> result = new HashSet<>();
-        List<CTLFormula> components = formula.getComponents();
-        for (CTLFormula component : components) {
-            result.addAll(sat(ts, component));
-        }
+    return satStates;
+  }
 
-        return result;
-    }
+  private Set<String> satNot(TransitionSystem ts, CTLNotFormula formula) {
+    Set<String> satStates = sat(ts, formula.getArgument());
+    Set<String> allStates = new HashSet<>(ts.getStates());
 
-    private Set<String> satAnd(TransitionSystem ts, CTLAndFormula formula) {
-        Set<String> result = new HashSet<>(ts.getStates());
-        List<CTLFormula> components = formula.getComponents();
-        for (CTLFormula component : components) {
-            result.retainAll(sat(ts, component));
-        }
+    Set<String> result = new HashSet<>(allStates);
+    result.removeAll(satStates);
 
-        return result;
-    }
+    return result;
+  }
 
-    private Set<String> satTrue(TransitionSystem ts, CTLTrueFormula formula) {
-        return new HashSet<>(ts.getStates());
+  private Set<String> satOr(TransitionSystem ts, CTLOrFormula formula) {
+    Set<String> result = new HashSet<>();
+    List<CTLFormula> components = formula.getComponents();
+    for (CTLFormula component : components) {
+      result.addAll(sat(ts, component));
     }
 
-    private Set<String> satFalse(TransitionSystem ts, CTLFalseFormula formula) {
-        return new HashSet<>();
+    return result;
+  }
+
+  private Set<String> satAnd(TransitionSystem ts, CTLAndFormula formula) {
+    Set<String> result = new HashSet<>(ts.getStates());
+    List<CTLFormula> components = formula.getComponents();
+    for (CTLFormula component : components) {
+      result.retainAll(sat(ts, component));
     }
+
+    return result;
+  }
+
+  private Set<String> satTrue(TransitionSystem ts, CTLTrueFormula formula) {
+    return new HashSet<>(ts.getStates());
+  }
+
+  private Set<String> satFalse(TransitionSystem ts, CTLFalseFormula formula) {
+    return new HashSet<>();
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLENFConverter.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLENFConverter.java
index 44efe56..de56eee 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLENFConverter.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLENFConverter.java
@@ -1,11 +1,5 @@
 package me.paultristanwagner.modelchecking.ctl;
 
-import me.paultristanwagner.modelchecking.ctl.formula.path.*;
-import me.paultristanwagner.modelchecking.ctl.formula.state.*;
-
-import java.util.ArrayList;
-import java.util.List;
-
 import static me.paultristanwagner.modelchecking.ctl.formula.path.CTLAlwaysFormula.always;
 import static me.paultristanwagner.modelchecking.ctl.formula.path.CTLNextFormula.next;
 import static me.paultristanwagner.modelchecking.ctl.formula.path.CTLUntilFormula.until;
@@ -17,118 +11,121 @@
 import static me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula.parenthesis;
 import static me.paultristanwagner.modelchecking.ctl.formula.state.CTLTrueFormula.TRUE;
 
+import java.util.ArrayList;
+import java.util.List;
+import me.paultristanwagner.modelchecking.ctl.formula.path.*;
+import me.paultristanwagner.modelchecking.ctl.formula.state.*;
+
 public class CTLENFConverter {
 
-    // todo: improve code readability
-
-    /**
-     * <p>
-     * Converts a CTL formula into an equivalent formula in ENF <br>
-     * in which only existential quantifiers are allowed. <br>
-     * Furthermore we only allow the box and the until operator. <br>
-     * <br>
-     * Logical equivalences used: <br>
-     * ALL NEXT PHI = NOT EXISTS NEXT NOT PHI <br>
-     * ALL PHI UNTIL PSI = NOT EXISTS (NOT PSI UNTIL (NOT PHI AND NOT PSI)) AND NOT EXISTS ALWAYS NOT PSI <br>
-     * ALL ALWAYS PHI = NOT EXISTS EVENTUALLY NOT PHI <br>
-     *
-     * </p>
-     *
-     * @param formula the formula to convert
-     * @return the converted formula
-     */
-    public CTLFormula convert(CTLFormula formula) {
-        if (formula instanceof CTLExistsFormula existsFormula) {
-            return convertExistsFormula(existsFormula);
-        } else if (formula instanceof CTLAllFormula allFormula) {
-            return convertAllFormula(allFormula);
-        } else if (formula instanceof CTLIdentifierFormula) {
-            return formula;
-        } else if (formula instanceof CTLParenthesisFormula parenthesisFormula) {
-            return parenthesis(convert(parenthesisFormula.getInner()));
-        } else if (formula instanceof CTLTrueFormula || formula instanceof CTLFalseFormula) {
-            return formula;
-        } else if (formula instanceof CTLOrFormula orFormula) {
-            List<CTLFormula> arguments = orFormula.getComponents();
-            List<CTLFormula> convertedArguments = new ArrayList<>();
-            for (CTLFormula argument : arguments) {
-                convertedArguments.add(convert(argument));
-            }
-            return or(convertedArguments);
-        } else if (formula instanceof CTLAndFormula andFormula) {
-            List<CTLFormula> arguments = andFormula.getComponents();
-            List<CTLFormula> convertedArguments = new ArrayList<>();
-            for (CTLFormula argument : arguments) {
-                convertedArguments.add(convert(argument));
-            }
-            return and(convertedArguments);
-        } else if (formula instanceof CTLNotFormula notFormula) {
-            return not(convert(notFormula.getArgument()));
-        }
-
-        throw new UnsupportedOperationException();
+  // todo: improve code readability
+
+  /**
+   * Converts a CTL formula into an equivalent formula in ENF <br>
+   * in which only existential quantifiers are allowed. <br>
+   * Furthermore we only allow the box and the until operator. <br>
+   * <br>
+   * Logical equivalences used: <br>
+   * ALL NEXT PHI = NOT EXISTS NEXT NOT PHI <br>
+   * ALL PHI UNTIL PSI = NOT EXISTS (NOT PSI UNTIL (NOT PHI AND NOT PSI)) AND NOT EXISTS ALWAYS NOT
+   * PSI <br>
+   * ALL ALWAYS PHI = NOT EXISTS EVENTUALLY NOT PHI <br>
+   *
+   * @param formula the formula to convert
+   * @return the converted formula
+   */
+  public CTLFormula convert(CTLFormula formula) {
+    if (formula instanceof CTLExistsFormula existsFormula) {
+      return convertExistsFormula(existsFormula);
+    } else if (formula instanceof CTLAllFormula allFormula) {
+      return convertAllFormula(allFormula);
+    } else if (formula instanceof CTLIdentifierFormula) {
+      return formula;
+    } else if (formula instanceof CTLParenthesisFormula parenthesisFormula) {
+      return parenthesis(convert(parenthesisFormula.getInner()));
+    } else if (formula instanceof CTLTrueFormula || formula instanceof CTLFalseFormula) {
+      return formula;
+    } else if (formula instanceof CTLOrFormula orFormula) {
+      List<CTLFormula> arguments = orFormula.getComponents();
+      List<CTLFormula> convertedArguments = new ArrayList<>();
+      for (CTLFormula argument : arguments) {
+        convertedArguments.add(convert(argument));
+      }
+      return or(convertedArguments);
+    } else if (formula instanceof CTLAndFormula andFormula) {
+      List<CTLFormula> arguments = andFormula.getComponents();
+      List<CTLFormula> convertedArguments = new ArrayList<>();
+      for (CTLFormula argument : arguments) {
+        convertedArguments.add(convert(argument));
+      }
+      return and(convertedArguments);
+    } else if (formula instanceof CTLNotFormula notFormula) {
+      return not(convert(notFormula.getArgument()));
     }
 
-    private CTLFormula convertExistsFormula(CTLExistsFormula formula) {
-        CTLPathFormula pathFormula = formula.getPathFormula();
-        if (pathFormula instanceof CTLAlwaysFormula alwaysFormula) {
-            return exists(always(convert(alwaysFormula.getStateFormula())));
-        } else if (pathFormula instanceof CTLEventuallyFormula eventuallyFormula) {
-            // EXISTS EVENTUALLY PHI = EXISTS (TRUE UNTIL PHI)
-            CTLUntilFormula untilFormula = until(TRUE(), eventuallyFormula.getStateFormula());
-            return convert(exists(untilFormula));
-        } else if (pathFormula instanceof CTLNextFormula nextFormula) {
-            return exists(next(convert(nextFormula.getStateFormula())));
-        } else if (pathFormula instanceof CTLUntilFormula untilFormula) {
-            return exists(until(convert(untilFormula.getLeft()), convert(untilFormula.getRight())));
-        }
-
-        throw new UnsupportedOperationException();
+    throw new UnsupportedOperationException();
+  }
+
+  private CTLFormula convertExistsFormula(CTLExistsFormula formula) {
+    CTLPathFormula pathFormula = formula.getPathFormula();
+    if (pathFormula instanceof CTLAlwaysFormula alwaysFormula) {
+      return exists(always(convert(alwaysFormula.getStateFormula())));
+    } else if (pathFormula instanceof CTLEventuallyFormula eventuallyFormula) {
+      // EXISTS EVENTUALLY PHI = EXISTS (TRUE UNTIL PHI)
+      CTLUntilFormula untilFormula = until(TRUE(), eventuallyFormula.getStateFormula());
+      return convert(exists(untilFormula));
+    } else if (pathFormula instanceof CTLNextFormula nextFormula) {
+      return exists(next(convert(nextFormula.getStateFormula())));
+    } else if (pathFormula instanceof CTLUntilFormula untilFormula) {
+      return exists(until(convert(untilFormula.getLeft()), convert(untilFormula.getRight())));
     }
 
-    private CTLFormula convertAllFormula(CTLAllFormula formula) {
-        CTLPathFormula pathFormula = formula.getPathFormula();
-        if (pathFormula instanceof CTLNextFormula nextFormula) {
+    throw new UnsupportedOperationException();
+  }
 
-            CTLFormula stateFormula = nextFormula.getStateFormula();
-            return not(exists(next(not(convert(stateFormula)))));
-        } else if (pathFormula instanceof CTLUntilFormula untilFormula) {
-            CTLFormula phi = untilFormula.getLeft();
-            CTLFormula psi = untilFormula.getRight();
+  private CTLFormula convertAllFormula(CTLAllFormula formula) {
+    CTLPathFormula pathFormula = formula.getPathFormula();
+    if (pathFormula instanceof CTLNextFormula nextFormula) {
 
-            CTLFormula phiConverted = convert(phi);
-            CTLFormula psiConverted = convert(psi);
+      CTLFormula stateFormula = nextFormula.getStateFormula();
+      return not(exists(next(not(convert(stateFormula)))));
+    } else if (pathFormula instanceof CTLUntilFormula untilFormula) {
+      CTLFormula phi = untilFormula.getLeft();
+      CTLFormula psi = untilFormula.getRight();
 
-            CTLFormula notPhiConverted = not(phiConverted);
-            CTLFormula notPsiConverted = not(psiConverted);
+      CTLFormula phiConverted = convert(phi);
+      CTLFormula psiConverted = convert(psi);
 
-            CTLFormula notPhiAndNotPsi = and(notPhiConverted, notPsiConverted);
+      CTLFormula notPhiConverted = not(phiConverted);
+      CTLFormula notPsiConverted = not(psiConverted);
 
-            CTLFormula left = not(exists(until(notPsiConverted, notPhiAndNotPsi)));
-            CTLFormula right = not(exists(always(notPsiConverted)));
+      CTLFormula notPhiAndNotPsi = and(notPhiConverted, notPsiConverted);
 
-            return and(left, right);
-        } else if (pathFormula instanceof CTLAlwaysFormula alwaysFormula) {
-            CTLFormula stateFormula = alwaysFormula.getStateFormula();
-            CTLFormula stateFormulaConverted = convert(stateFormula);
+      CTLFormula left = not(exists(until(notPsiConverted, notPhiAndNotPsi)));
+      CTLFormula right = not(exists(always(notPsiConverted)));
 
-            // ALL ALWAYS PHI = NOT EXISTS EVENTUALLY NOT PHI = NOT EXISTS (TRUE UNTIL NOT PHI)
-            CTLFormula notConvertedStateFormula = not(stateFormulaConverted);
-            CTLUntilFormula untilFormula = until(TRUE(), notConvertedStateFormula);
-            CTLExistsFormula existsFormula = exists(untilFormula);
+      return and(left, right);
+    } else if (pathFormula instanceof CTLAlwaysFormula alwaysFormula) {
+      CTLFormula stateFormula = alwaysFormula.getStateFormula();
+      CTLFormula stateFormulaConverted = convert(stateFormula);
 
-            return not(existsFormula);
-        } else if (pathFormula instanceof CTLEventuallyFormula eventuallyFormula) {
-            CTLFormula stateFormula = eventuallyFormula.getStateFormula();
+      // ALL ALWAYS PHI = NOT EXISTS EVENTUALLY NOT PHI = NOT EXISTS (TRUE UNTIL NOT PHI)
+      CTLFormula notConvertedStateFormula = not(stateFormulaConverted);
+      CTLUntilFormula untilFormula = until(TRUE(), notConvertedStateFormula);
+      CTLExistsFormula existsFormula = exists(untilFormula);
 
-            // ALL EVENTUALLY PHI = ALL (TRUE UNTIL PHI)
+      return not(existsFormula);
+    } else if (pathFormula instanceof CTLEventuallyFormula eventuallyFormula) {
+      CTLFormula stateFormula = eventuallyFormula.getStateFormula();
 
-            CTLUntilFormula untilFormula = until(TRUE(), stateFormula);
-            CTLAllFormula allFormula = forAll(untilFormula);
+      // ALL EVENTUALLY PHI = ALL (TRUE UNTIL PHI)
 
-            return convertAllFormula(allFormula);
-        }
+      CTLUntilFormula untilFormula = until(TRUE(), stateFormula);
+      CTLAllFormula allFormula = forAll(untilFormula);
 
-        throw new UnsupportedOperationException();
+      return convertAllFormula(allFormula);
     }
+
+    throw new UnsupportedOperationException();
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelChecker.java
index 1b02f55..62471ee 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelChecker.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelChecker.java
@@ -3,6 +3,4 @@
 import me.paultristanwagner.modelchecking.ModelChecker;
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
 
-public interface CTLModelChecker extends ModelChecker<CTLFormula, CTLModelCheckingResult> {
-
-}
+public interface CTLModelChecker extends ModelChecker<CTLFormula, CTLModelCheckingResult> {}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelCheckingResult.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelCheckingResult.java
index 6300493..6b536b9 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelCheckingResult.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/CTLModelCheckingResult.java
@@ -4,15 +4,15 @@
 
 public class CTLModelCheckingResult extends ModelCheckingResult {
 
-    public CTLModelCheckingResult( boolean models ) {
-        super( models );
-    }
+  public CTLModelCheckingResult(boolean models) {
+    super(models);
+  }
 
-    public static CTLModelCheckingResult models() {
-        return new CTLModelCheckingResult( true );
-    }
+  public static CTLModelCheckingResult models() {
+    return new CTLModelCheckingResult(true);
+  }
 
-    public static CTLModelCheckingResult doesNotModel() {
-        return new CTLModelCheckingResult( false );
-    }
+  public static CTLModelCheckingResult doesNotModel() {
+    return new CTLModelCheckingResult(false);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java
index 041aca8..1a86c97 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLAlwaysFormula.java
@@ -1,29 +1,29 @@
 package me.paultristanwagner.modelchecking.ctl.formula.path;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS_SYMBOL;
+
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS_SYMBOL;
-
 public class CTLAlwaysFormula extends CTLPathFormula {
-  
+
   private final CTLFormula stateFormula;
-  
+
   private CTLAlwaysFormula(CTLFormula stateFormula) {
     this.stateFormula = stateFormula;
   }
-  
+
   public static CTLAlwaysFormula always(CTLFormula stateFormula) {
-    return new CTLAlwaysFormula( stateFormula );
+    return new CTLAlwaysFormula(stateFormula);
   }
-  
+
   public CTLFormula getStateFormula() {
     return stateFormula;
   }
-  
+
   @Override
   public String toString() {
-    if(stateFormula instanceof CTLParenthesisFormula ) {
+    if (stateFormula instanceof CTLParenthesisFormula) {
       return ALWAYS_SYMBOL + stateFormula;
     } else {
       return ALWAYS_SYMBOL + "(" + stateFormula + ")";
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java
index 7ce7e55..2125d92 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLEventuallyFormula.java
@@ -1,29 +1,29 @@
 package me.paultristanwagner.modelchecking.ctl.formula.path;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY_SYMBOL;
+
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY_SYMBOL;
-
 public class CTLEventuallyFormula extends CTLPathFormula {
-  
+
   private final CTLFormula stateFormula;
-  
-  private CTLEventuallyFormula( CTLFormula stateFormula) {
+
+  private CTLEventuallyFormula(CTLFormula stateFormula) {
     this.stateFormula = stateFormula;
   }
-  
+
   public static CTLEventuallyFormula eventually(CTLFormula stateFormula) {
-    return new CTLEventuallyFormula( stateFormula );
+    return new CTLEventuallyFormula(stateFormula);
   }
-  
+
   public CTLFormula getStateFormula() {
     return stateFormula;
   }
-  
+
   @Override
   public String toString() {
-    if(stateFormula instanceof CTLParenthesisFormula ) {
+    if (stateFormula instanceof CTLParenthesisFormula) {
       return EVENTUALLY_SYMBOL + stateFormula;
     } else {
       return EVENTUALLY_SYMBOL + "(" + stateFormula + ")";
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java
index dbdbcf1..26c1acf 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLNextFormula.java
@@ -1,10 +1,10 @@
 package me.paultristanwagner.modelchecking.ctl.formula.path;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL;
+
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
 import me.paultristanwagner.modelchecking.ctl.formula.state.CTLParenthesisFormula;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL;
-
 public class CTLNextFormula extends CTLPathFormula {
   
   private final CTLFormula stateFormula;
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLPathFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLPathFormula.java
index 43702ba..6ce4f64 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLPathFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLPathFormula.java
@@ -1,5 +1,3 @@
 package me.paultristanwagner.modelchecking.ctl.formula.path;
 
-public abstract class CTLPathFormula {
-
-}
+public abstract class CTLPathFormula {}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java
index 6d18ffc..d26bdff 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/path/CTLUntilFormula.java
@@ -1,33 +1,33 @@
 package me.paultristanwagner.modelchecking.ctl.formula.path;
 
-import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
-
 import static me.paultristanwagner.modelchecking.util.Symbol.UNTIL_SYMBOL;
 
+import me.paultristanwagner.modelchecking.ctl.formula.state.CTLFormula;
+
 public class CTLUntilFormula extends CTLPathFormula {
 
-    private final CTLFormula left;
-    private final CTLFormula right;
+  private final CTLFormula left;
+  private final CTLFormula right;
 
-    private CTLUntilFormula(CTLFormula left, CTLFormula right) {
-        this.left = left;
-        this.right = right;
-    }
+  private CTLUntilFormula(CTLFormula left, CTLFormula right) {
+    this.left = left;
+    this.right = right;
+  }
 
-    public static CTLUntilFormula until(CTLFormula left, CTLFormula right) {
-        return new CTLUntilFormula(left, right);
-    }
+  public static CTLUntilFormula until(CTLFormula left, CTLFormula right) {
+    return new CTLUntilFormula(left, right);
+  }
 
-    public CTLFormula getLeft() {
-        return left;
-    }
+  public CTLFormula getLeft() {
+    return left;
+  }
 
-    public CTLFormula getRight() {
-        return right;
-    }
+  public CTLFormula getRight() {
+    return right;
+  }
 
-    @Override
-    public String toString() {
-        return "(" + left.toString() + " " + UNTIL_SYMBOL + " " + right.toString() + ")";
-    }
+  @Override
+  public String toString() {
+    return "(" + left.toString() + " " + UNTIL_SYMBOL + " " + right.toString() + ")";
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java
index e8e2bf6..2ce12f2 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAllFormula.java
@@ -1,25 +1,25 @@
 package me.paultristanwagner.modelchecking.ctl.formula.state;
 
-import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula;
-
 import static me.paultristanwagner.modelchecking.util.Symbol.UNIVERSAL_QUANTIFIER_SYMBOL;
 
+import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula;
+
 public class CTLAllFormula extends CTLFormula {
-  
+
   private final CTLPathFormula pathFormula;
-  
-  private CTLAllFormula( CTLPathFormula pathFormula ) {
+
+  private CTLAllFormula(CTLPathFormula pathFormula) {
     this.pathFormula = pathFormula;
   }
-  
-  public static CTLAllFormula forAll(CTLPathFormula pathFormula ) {
-    return new CTLAllFormula( pathFormula );
+
+  public static CTLAllFormula forAll(CTLPathFormula pathFormula) {
+    return new CTLAllFormula(pathFormula);
   }
-  
+
   public CTLPathFormula getPathFormula() {
     return pathFormula;
   }
-  
+
   @Override
   public String toString() {
     return UNIVERSAL_QUANTIFIER_SYMBOL + pathFormula.toString();
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java
index 6ad96be..616bcb2 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLAndFormula.java
@@ -1,43 +1,43 @@
 package me.paultristanwagner.modelchecking.ctl.formula.state;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL;
+
 import java.util.Arrays;
 import java.util.List;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL;
-
 public class CTLAndFormula extends CTLFormula {
-  
+
   private final List<CTLFormula> components;
-  
+
   private CTLAndFormula(List<CTLFormula> components) {
     this.components = components;
   }
-  
+
   public static CTLAndFormula and(CTLFormula... components) {
-    return new CTLAndFormula( Arrays.asList( components ) );
+    return new CTLAndFormula(Arrays.asList(components));
   }
-  
+
   public static CTLAndFormula and(List<CTLFormula> components) {
-    return new CTLAndFormula( components );
+    return new CTLAndFormula(components);
   }
-  
+
   public List<CTLFormula> getComponents() {
     return components;
   }
-  
+
   @Override
   public String toString() {
     StringBuilder builder = new StringBuilder();
     for (int i = 0; i < components.size(); i++) {
-      builder.append( components.get( i ).toString() );
-      
+      builder.append(components.get(i).toString());
+
       if (i < components.size() - 1) {
-        builder.append( " " );
-        builder.append( AND_SYMBOL );
-        builder.append( " " );
+        builder.append(" ");
+        builder.append(AND_SYMBOL);
+        builder.append(" ");
       }
     }
-    
+
     return builder.toString();
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java
index 968c8cb..9c6335c 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLExistsFormula.java
@@ -1,25 +1,25 @@
 package me.paultristanwagner.modelchecking.ctl.formula.state;
 
-import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula;
-
 import static me.paultristanwagner.modelchecking.util.Symbol.EXISTENTIAL_QUANTIFIER_SYMBOL;
 
+import me.paultristanwagner.modelchecking.ctl.formula.path.CTLPathFormula;
+
 public class CTLExistsFormula extends CTLFormula {
-  
+
   private final CTLPathFormula pathFormula;
-  
-  private CTLExistsFormula( CTLPathFormula pathFormula ) {
+
+  private CTLExistsFormula(CTLPathFormula pathFormula) {
     this.pathFormula = pathFormula;
   }
-  
-  public static CTLExistsFormula exists(CTLPathFormula pathFormula ) {
-    return new CTLExistsFormula( pathFormula );
+
+  public static CTLExistsFormula exists(CTLPathFormula pathFormula) {
+    return new CTLExistsFormula(pathFormula);
   }
-  
+
   public CTLPathFormula getPathFormula() {
     return pathFormula;
   }
-  
+
   @Override
   public String toString() {
     return EXISTENTIAL_QUANTIFIER_SYMBOL + pathFormula.toString();
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFalseFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFalseFormula.java
index eaaccd5..23b6cf6 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFalseFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFalseFormula.java
@@ -2,8 +2,7 @@
 
 public class CTLFalseFormula extends CTLFormula {
 
-  private CTLFalseFormula() {
-  }
+  private CTLFalseFormula() {}
 
   public static CTLFalseFormula FALSE() {
     return new CTLFalseFormula();
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFormula.java
index 7e2f951..2f28d05 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLFormula.java
@@ -2,6 +2,4 @@
 
 import me.paultristanwagner.modelchecking.Formula;
 
-public abstract class CTLFormula  extends Formula {
-
-}
+public abstract class CTLFormula extends Formula {}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLIdentifierFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLIdentifierFormula.java
index bf35c61..48a4070 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLIdentifierFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLIdentifierFormula.java
@@ -1,21 +1,21 @@
 package me.paultristanwagner.modelchecking.ctl.formula.state;
 
 public class CTLIdentifierFormula extends CTLFormula {
-  
+
   private final String identifier;
-  
-  private CTLIdentifierFormula( String identifier ) {
+
+  private CTLIdentifierFormula(String identifier) {
     this.identifier = identifier;
   }
-  
-  public static CTLIdentifierFormula identifier(String identifier ) {
-    return new CTLIdentifierFormula( identifier );
+
+  public static CTLIdentifierFormula identifier(String identifier) {
+    return new CTLIdentifierFormula(identifier);
   }
-  
+
   public String getIdentifier() {
     return identifier;
   }
-  
+
   @Override
   public String toString() {
     return identifier;
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java
index 72d84f7..533992f 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLNotFormula.java
@@ -3,21 +3,21 @@
 import static me.paultristanwagner.modelchecking.util.Symbol.NOT_SYMBOL;
 
 public class CTLNotFormula extends CTLFormula {
-  
+
   private final CTLFormula argument;
-  
+
   private CTLNotFormula(CTLFormula argument) {
     this.argument = argument;
   }
-  
+
   public static CTLNotFormula not(CTLFormula argument) {
-    return new CTLNotFormula( argument );
+    return new CTLNotFormula(argument);
   }
-  
+
   public CTLFormula getArgument() {
     return argument;
   }
-  
+
   @Override
   public String toString() {
     return NOT_SYMBOL + argument.toString();
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java
index 81e89f2..816001d 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLOrFormula.java
@@ -1,10 +1,10 @@
 package me.paultristanwagner.modelchecking.ctl.formula.state;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL;
+
 import java.util.Arrays;
 import java.util.List;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL;
-
 public class CTLOrFormula extends CTLFormula {
 
   private final List<CTLFormula> components;
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLParenthesisFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLParenthesisFormula.java
index 78d09c0..1886875 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLParenthesisFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLParenthesisFormula.java
@@ -1,21 +1,21 @@
 package me.paultristanwagner.modelchecking.ctl.formula.state;
 
 public class CTLParenthesisFormula extends CTLFormula {
-  
+
   private final CTLFormula inner;
-  
+
   private CTLParenthesisFormula(CTLFormula inner) {
     this.inner = inner;
   }
-  
+
   public static CTLParenthesisFormula parenthesis(CTLFormula inner) {
-    return new CTLParenthesisFormula( inner );
+    return new CTLParenthesisFormula(inner);
   }
-  
+
   public CTLFormula getInner() {
     return inner;
   }
-  
+
   @Override
   public String toString() {
     if (inner instanceof CTLParenthesisFormula) {
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLTrueFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLTrueFormula.java
index 0a34b30..80c94d6 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLTrueFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/formula/state/CTLTrueFormula.java
@@ -2,12 +2,11 @@
 
 public class CTLTrueFormula extends CTLFormula {
 
-  private CTLTrueFormula() {
-  }
+  private CTLTrueFormula() {}
 
-    public static CTLTrueFormula TRUE() {
-        return new CTLTrueFormula();
-    }
+  public static CTLTrueFormula TRUE() {
+    return new CTLTrueFormula();
+  }
 
   @Override
   public String toString() {
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java
index 0bda645..f1b8f29 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLLexer.java
@@ -1,37 +1,51 @@
 package me.paultristanwagner.modelchecking.ctl.parse;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.*;
+
 import me.paultristanwagner.modelchecking.parse.Lexer;
 import me.paultristanwagner.modelchecking.parse.TokenType;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.*;
-
 public class CTLLexer extends Lexer {
 
-    static final TokenType LPAREN = TokenType.of("(", "^\\(");
-    static final TokenType RPAREN = TokenType.of(")", "^\\)");
-    static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)");
-    static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)");
-    static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)");
-    static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)");
-    static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)");
-    static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)");
-    static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)");
-    static final TokenType EVENTUALLY = TokenType.of("eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)");
-    static final TokenType ALWAYS = TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)");
-    static final TokenType ALL = TokenType.of("all", "^(" + UNIVERSAL_QUANTIFIER_SYMBOL + "|all|ALL|A)");
-    static final TokenType EXISTS = TokenType.of("exists", "^(" + EXISTENTIAL_QUANTIFIER_SYMBOL + "|exists|EXISTS|ex|EX|E)");
-    static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]");
-
-    public CTLLexer(String input) {
-        super(input);
-
-        registerTokenTypes(
-                LPAREN, RPAREN, TRUE, FALSE, NOT, AND, OR,
-                NEXT, UNTIL, EVENTUALLY, ALWAYS, ALL, EXISTS, IDENTIFIER
-        );
-
-        this.initialize(input);
-    }
-
-
+  static final TokenType LPAREN = TokenType.of("(", "^\\(");
+  static final TokenType RPAREN = TokenType.of(")", "^\\)");
+  static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)");
+  static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)");
+  static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)");
+  static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)");
+  static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)");
+  static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)");
+  static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)");
+  static final TokenType EVENTUALLY =
+      TokenType.of(
+          "eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)");
+  static final TokenType ALWAYS =
+      TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)");
+  static final TokenType ALL =
+      TokenType.of("all", "^(" + UNIVERSAL_QUANTIFIER_SYMBOL + "|all|ALL|A)");
+  static final TokenType EXISTS =
+      TokenType.of("exists", "^(" + EXISTENTIAL_QUANTIFIER_SYMBOL + "|exists|EXISTS|ex|EX|E)");
+  static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]");
+
+  public CTLLexer(String input) {
+    super(input);
+
+    registerTokenTypes(
+        LPAREN,
+        RPAREN,
+        TRUE,
+        FALSE,
+        NOT,
+        AND,
+        OR,
+        NEXT,
+        UNTIL,
+        EVENTUALLY,
+        ALWAYS,
+        ALL,
+        EXISTS,
+        IDENTIFIER);
+
+    this.initialize(input);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLParser.java b/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLParser.java
index 5f390c5..a4e1e9b 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLParser.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ctl/parse/CTLParser.java
@@ -50,11 +50,11 @@ public CTLFormula parse(String input, AtomicInteger index) {
     return formula;
   }
 
-  private CTLFormula parseStateFormula( Lexer lexer) {
+  private CTLFormula parseStateFormula(Lexer lexer) {
     return A(lexer);
   }
 
-  private CTLFormula A( Lexer lexer) {
+  private CTLFormula A(Lexer lexer) {
     List<CTLFormula> components = new ArrayList<>();
     CTLFormula first = B(lexer);
     components.add(first);
@@ -71,7 +71,7 @@ private CTLFormula A( Lexer lexer) {
     return CTLOrFormula.or(components);
   }
 
-  private CTLFormula B( Lexer lexer) {
+  private CTLFormula B(Lexer lexer) {
     List<CTLFormula> components = new ArrayList<>();
     CTLFormula first = C(lexer);
     components.add(first);
@@ -88,7 +88,7 @@ private CTLFormula B( Lexer lexer) {
     return CTLAndFormula.and(components);
   }
 
-  private CTLFormula C( Lexer lexer) {
+  private CTLFormula C(Lexer lexer) {
     lexer.requireNextToken();
 
     Token token = lexer.getLookahead();
@@ -111,28 +111,28 @@ private CTLFormula C( Lexer lexer) {
     }
   }
 
-  private CTLNotFormula parseNotFormula( Lexer lexer) {
+  private CTLNotFormula parseNotFormula(Lexer lexer) {
     lexer.consume(NOT);
 
     CTLFormula argument = C(lexer);
     return CTLNotFormula.not(argument);
   }
 
-  private CTLAllFormula parseAllFormula( Lexer lexer) {
+  private CTLAllFormula parseAllFormula(Lexer lexer) {
     lexer.consume(ALL);
 
     CTLPathFormula pathFormula = parsePathFormula(lexer);
     return CTLAllFormula.forAll(pathFormula);
   }
 
-  private CTLExistsFormula parseExistsFormula( Lexer lexer) {
+  private CTLExistsFormula parseExistsFormula(Lexer lexer) {
     lexer.consume(EXISTS);
 
     CTLPathFormula pathFormula = parsePathFormula(lexer);
     return CTLExistsFormula.exists(pathFormula);
   }
 
-  private CTLFormula parseParenthesisFormula( Lexer lexer) {
+  private CTLFormula parseParenthesisFormula(Lexer lexer) {
     lexer.consume(LPAREN);
     CTLFormula inner = parseStateFormula(lexer);
     lexer.consume(RPAREN);
@@ -140,19 +140,19 @@ private CTLFormula parseParenthesisFormula( Lexer lexer) {
     return CTLParenthesisFormula.parenthesis(inner);
   }
 
-  private CTLTrueFormula parseTrueFormula( Lexer lexer) {
+  private CTLTrueFormula parseTrueFormula(Lexer lexer) {
     lexer.consume(TRUE);
 
     return CTLTrueFormula.TRUE();
   }
 
-  private CTLFalseFormula parseFalseFormula( Lexer lexer) {
+  private CTLFalseFormula parseFalseFormula(Lexer lexer) {
     lexer.consume(FALSE);
 
     return CTLFalseFormula.FALSE();
   }
 
-  private CTLIdentifierFormula parseIdentifierFormula( Lexer lexer) {
+  private CTLIdentifierFormula parseIdentifierFormula(Lexer lexer) {
     Token lookahead = lexer.getLookahead();
 
     String identifier = lookahead.getValue();
@@ -161,35 +161,35 @@ private CTLIdentifierFormula parseIdentifierFormula( Lexer lexer) {
     return CTLIdentifierFormula.identifier(identifier);
   }
 
-  private CTLPathFormula parsePathFormula( Lexer lexer) {
+  private CTLPathFormula parsePathFormula(Lexer lexer) {
     lexer.requireNextToken();
 
     Token lookahead = lexer.getLookahead();
     TokenType type = lookahead.getType();
-    if ( type.equals( NEXT ) ) {
-      return parseNextFormula( lexer );
-    } else if ( type.equals( EVENTUALLY ) ) {
-      return parseEventuallyFormula( lexer );
-    } else if ( type.equals( ALWAYS ) ) {
-      return parseAlwaysFormula( lexer );
-    } else if( type.equals( LPAREN )) {
-      return parseParenthesisUntilFormula( lexer );
+    if (type.equals(NEXT)) {
+      return parseNextFormula(lexer);
+    } else if (type.equals(EVENTUALLY)) {
+      return parseEventuallyFormula(lexer);
+    } else if (type.equals(ALWAYS)) {
+      return parseAlwaysFormula(lexer);
+    } else if (type.equals(LPAREN)) {
+      return parseParenthesisUntilFormula(lexer);
     }
 
-    return parseUntilFormula( lexer );
+    return parseUntilFormula(lexer);
   }
 
-  private CTLNextFormula parseNextFormula( Lexer lexer) {
+  private CTLNextFormula parseNextFormula(Lexer lexer) {
     lexer.consume(NEXT);
 
     CTLFormula stateFormula = parseStateFormula(lexer);
     return CTLNextFormula.next(stateFormula);
   }
 
-  private CTLUntilFormula parseUntilFormula( Lexer lexer) {
+  private CTLUntilFormula parseUntilFormula(Lexer lexer) {
     lexer.requireNextToken();
 
-    if(lexer.getLookahead().getType() == LPAREN) {
+    if (lexer.getLookahead().getType() == LPAREN) {
       return parseParenthesisUntilFormula(lexer);
     }
 
@@ -202,14 +202,14 @@ private CTLUntilFormula parseUntilFormula( Lexer lexer) {
     return CTLUntilFormula.until(left, right);
   }
 
-  private CTLUntilFormula parseParenthesisUntilFormula( Lexer lexer ) {
+  private CTLUntilFormula parseParenthesisUntilFormula(Lexer lexer) {
     lexer.consume(LPAREN);
     CTLFormula left = parseStateFormula(lexer);
     CTLFormula right;
 
     lexer.requireNextToken();
 
-    if(lexer.getLookahead().getType() == RPAREN) {
+    if (lexer.getLookahead().getType() == RPAREN) {
       lexer.consume(RPAREN);
       left = CTLParenthesisFormula.parenthesis(left);
 
@@ -224,17 +224,17 @@ private CTLUntilFormula parseParenthesisUntilFormula( Lexer lexer ) {
     return CTLUntilFormula.until(left, right);
   }
 
-  private CTLEventuallyFormula parseEventuallyFormula( Lexer lexer) {
-    lexer.consume( EVENTUALLY );
+  private CTLEventuallyFormula parseEventuallyFormula(Lexer lexer) {
+    lexer.consume(EVENTUALLY);
 
-    CTLFormula stateFormula = parseStateFormula( lexer );
+    CTLFormula stateFormula = parseStateFormula(lexer);
     return CTLEventuallyFormula.eventually(stateFormula);
   }
 
-  private CTLAlwaysFormula parseAlwaysFormula( Lexer lexer) {
-    lexer.consume( ALWAYS );
+  private CTLAlwaysFormula parseAlwaysFormula(Lexer lexer) {
+    lexer.consume(ALWAYS);
 
-    CTLFormula stateFormula = parseStateFormula( lexer );
+    CTLFormula stateFormula = parseStateFormula(lexer);
     return CTLAlwaysFormula.always(stateFormula);
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
index 68fa783..48dfa3a 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/BasicLTLModelChecker.java
@@ -1,5 +1,11 @@
 package me.paultristanwagner.modelchecking.ltl;
 
+import static me.paultristanwagner.modelchecking.ltl.LTLModelCheckingResult.doesNotModel;
+import static me.paultristanwagner.modelchecking.ltl.LTLModelCheckingResult.models;
+import static me.paultristanwagner.modelchecking.ltl.formula.LTLIdentifierFormula.identifier;
+
+import java.util.*;
+import java.util.AbstractMap.SimpleEntry;
 import me.paultristanwagner.modelchecking.automaton.GNBA;
 import me.paultristanwagner.modelchecking.automaton.GNBABuilder;
 import me.paultristanwagner.modelchecking.automaton.NBA;
@@ -8,373 +14,377 @@
 import me.paultristanwagner.modelchecking.ts.TSPersistenceResult;
 import me.paultristanwagner.modelchecking.ts.TransitionSystem;
 
-import java.util.AbstractMap.SimpleEntry;
-import java.util.*;
-
-import static me.paultristanwagner.modelchecking.ltl.LTLModelCheckingResult.doesNotModel;
-import static me.paultristanwagner.modelchecking.ltl.LTLModelCheckingResult.models;
-import static me.paultristanwagner.modelchecking.ltl.formula.LTLIdentifierFormula.identifier;
-
 public class BasicLTLModelChecker implements LTLModelChecker {
 
-    @Override
-    public LTLModelCheckingResult check(TransitionSystem ts, LTLFormula formula) {
-        LTLFormula negation = formula.negate();
+  @Override
+  public LTLModelCheckingResult check(TransitionSystem ts, LTLFormula formula) {
+    LTLFormula negation = formula.negate();
 
-        GNBA gnba = computeGNBA(ts, negation);
+    GNBA gnba = computeGNBA(ts, negation);
 
-        NBA nba = gnba.convertToNBA();
-        TransitionSystem synchronousProduct = ts.reachableSynchronousProduct(nba);
+    NBA nba = gnba.convertToNBA();
+    TransitionSystem synchronousProduct = ts.reachableSynchronousProduct(nba);
 
-        Set<String> persistentStates = new HashSet<>(nba.getStates());
-        nba.getAcceptingStates().forEach(persistentStates::remove);
+    Set<String> persistentStates = new HashSet<>(nba.getStates());
+    nba.getAcceptingStates().forEach(persistentStates::remove);
 
-        TSPersistenceResult result = synchronousProduct.checkPersistence(persistentStates);
-        if (result.isPersistent()) {
-            return models();
-        } else {
-            InfinitePath counterExample = result.getWitness().reduce();
-            return doesNotModel(counterExample);
-        }
+    TSPersistenceResult result = synchronousProduct.checkPersistence(persistentStates);
+    if (result.isPersistent()) {
+      return models();
+    } else {
+      InfinitePath counterExample = result.getWitness().reduce();
+      return doesNotModel(counterExample);
     }
+  }
 
-    private GNBA computeGNBA(TransitionSystem ts, LTLFormula formula) {
-        Set<String> atomicPropositions = new HashSet<>(ts.getAtomicPropositions());
-        Set<LTLFormula> closure = formula.getClosure();
-        Set<Guess> elementarySets = computeElementarySets(atomicPropositions, closure);
-
-        GNBABuilder gnbaBuilder = new GNBABuilder();
-
-        /*
-         * Compute the states and transitions of the GNBA
-         *
-         * We added the following additional transition rules:
-         * (1) always phi in B <=> phi in B and always phi in B'
-         * (2) eventually phi in B <=> phi in B or eventually phi in B'
-         */
-        for (Guess one : elementarySets) {
-            gnbaBuilder.addState(one.toString());
-
-            Set<String> assumedAtomicPropositions = one.assumedAtomicPropositions();
-
-            for (Guess potentialSuccessor : elementarySets) {
-                boolean violates = false;
-                for (LTLFormula ltlFormula : closure) {
-                    if (ltlFormula instanceof LTLNextFormula nextFormula) {
-                        if (one.isAssumed(nextFormula) != potentialSuccessor.isAssumed(nextFormula.getFormula())) {
-                            violates = true;
-                            break;
-                        }
-                    } else if (ltlFormula instanceof LTLUntilFormula untilFormula) {
-                        boolean lhs = one.isAssumed(untilFormula);
-                        boolean rhs = one.isAssumed(untilFormula.getRight()) ||
-                                (one.isAssumed(untilFormula.getLeft()) && potentialSuccessor.isAssumed(untilFormula));
-
-                        if (lhs != rhs) {
-                            violates = true;
-                            break;
-                        }
-                    } else if(ltlFormula instanceof LTLEventuallyFormula eventuallyFormula) {
-                        boolean lhs = one.isAssumed(eventuallyFormula);
-                        boolean rhs = one.isAssumed(eventuallyFormula.getFormula()) ||
-                                potentialSuccessor.isAssumed(eventuallyFormula);
-
-                        if (lhs != rhs) {
-                            violates = true;
-                            break;
-                        }
-                    } else if(ltlFormula instanceof LTLAlwaysFormula alwaysFormula) {
-                        boolean lhs = one.isAssumed(alwaysFormula);
-                        boolean rhs = one.isAssumed(alwaysFormula.getFormula()) &&
-                                potentialSuccessor.isAssumed(alwaysFormula);
-
-                        if (lhs != rhs) {
-                            violates = true;
-                            break;
-                        }
-                    }
-                }
-
-                if (violates) {
-                    continue;
-                }
-                gnbaBuilder.addTransition(one.toString(), assumedAtomicPropositions.toString(), potentialSuccessor.toString());
-            }
-        }
+  private GNBA computeGNBA(TransitionSystem ts, LTLFormula formula) {
+    Set<String> atomicPropositions = new HashSet<>(ts.getAtomicPropositions());
+    Set<LTLFormula> closure = formula.getClosure();
+    Set<Guess> elementarySets = computeElementarySets(atomicPropositions, closure);
+
+    GNBABuilder gnbaBuilder = new GNBABuilder();
+
+    /*
+     * Compute the states and transitions of the GNBA
+     *
+     * We added the following additional transition rules:
+     * (1) always phi in B <=> phi in B and always phi in B'
+     * (2) eventually phi in B <=> phi in B or eventually phi in B'
+     */
+    for (Guess one : elementarySets) {
+      gnbaBuilder.addState(one.toString());
 
-        /*
-         * We add the accepting sets for the GNBA.
-         * The following additional accepting sets were derived
-         * 1. F_{always phi} := {B in Q | always phi in B or phi not in B}
-         * 2. F_{eventually phi} := {B in Q | phi in B or eventually phi not in B}
-         */
+      Set<String> assumedAtomicPropositions = one.assumedAtomicPropositions();
+
+      for (Guess potentialSuccessor : elementarySets) {
+        boolean violates = false;
         for (LTLFormula ltlFormula : closure) {
-            if (ltlFormula instanceof LTLUntilFormula untilFormula) {
-                Set<String> acceptingSet = new HashSet<>();
-
-                for (Guess state : elementarySets) {
-                    if (!state.isAssumed(untilFormula) || state.isAssumed(untilFormula.getRight())) {
-                        acceptingSet.add(state.toString());
-                    }
-                }
-
-                gnbaBuilder.addAcceptingSet(acceptingSet);
-            } else if(ltlFormula instanceof LTLEventuallyFormula eventuallyFormula) {
-                Set<String> acceptingSet = new HashSet<>();
-                for (Guess state : elementarySets) {
-                    if(!state.isAssumed(eventuallyFormula) || state.isAssumed(eventuallyFormula.getFormula())) {
-                        acceptingSet.add(state.toString());
-                    }
-                }
-                gnbaBuilder.addAcceptingSet(acceptingSet);
-            } else if(ltlFormula instanceof LTLAlwaysFormula alwaysFormula) {
-                Set<String> acceptingSet = new HashSet<>();
-                for (Guess state : elementarySets) {
-                    if(state.isAssumed(alwaysFormula) || !state.isAssumed(alwaysFormula.getFormula())) {
-                        acceptingSet.add(state.toString());
-                    }
-                }
-                gnbaBuilder.addAcceptingSet(acceptingSet);
+          if (ltlFormula instanceof LTLNextFormula nextFormula) {
+            if (one.isAssumed(nextFormula)
+                != potentialSuccessor.isAssumed(nextFormula.getFormula())) {
+              violates = true;
+              break;
             }
-        }
-
-        for (Guess elementarySet : elementarySets) {
-            if (elementarySet.isAssumed(formula)) {
-                gnbaBuilder.addInitialState(elementarySet.toString());
+          } else if (ltlFormula instanceof LTLUntilFormula untilFormula) {
+            boolean lhs = one.isAssumed(untilFormula);
+            boolean rhs =
+                one.isAssumed(untilFormula.getRight())
+                    || (one.isAssumed(untilFormula.getLeft())
+                        && potentialSuccessor.isAssumed(untilFormula));
+
+            if (lhs != rhs) {
+              violates = true;
+              break;
+            }
+          } else if (ltlFormula instanceof LTLEventuallyFormula eventuallyFormula) {
+            boolean lhs = one.isAssumed(eventuallyFormula);
+            boolean rhs =
+                one.isAssumed(eventuallyFormula.getFormula())
+                    || potentialSuccessor.isAssumed(eventuallyFormula);
+
+            if (lhs != rhs) {
+              violates = true;
+              break;
+            }
+          } else if (ltlFormula instanceof LTLAlwaysFormula alwaysFormula) {
+            boolean lhs = one.isAssumed(alwaysFormula);
+            boolean rhs =
+                one.isAssumed(alwaysFormula.getFormula())
+                    && potentialSuccessor.isAssumed(alwaysFormula);
+
+            if (lhs != rhs) {
+              violates = true;
+              break;
             }
+          }
         }
 
-       return gnbaBuilder.build();
+        if (violates) {
+          continue;
+        }
+        gnbaBuilder.addTransition(
+            one.toString(), assumedAtomicPropositions.toString(), potentialSuccessor.toString());
+      }
     }
 
-    // we can reduce the closure by removing everything that is directly implied by another formula
-    public Set<LTLFormula> reduceClosure(Set<LTLFormula> closure) {
-        Set<LTLFormula> reduced = new HashSet<>();
-        for (LTLFormula ltlFormula : closure) {
-            if (ltlFormula instanceof LTLTrueFormula || ltlFormula instanceof LTLFalseFormula ||
-                    ltlFormula instanceof LTLNotFormula || ltlFormula instanceof LTLParenthesisFormula) {
-                continue;
-            }
+    /*
+     * We add the accepting sets for the GNBA.
+     * The following additional accepting sets were derived
+     * 1. F_{always phi} := {B in Q | always phi in B or phi not in B}
+     * 2. F_{eventually phi} := {B in Q | phi in B or eventually phi not in B}
+     */
+    for (LTLFormula ltlFormula : closure) {
+      if (ltlFormula instanceof LTLUntilFormula untilFormula) {
+        Set<String> acceptingSet = new HashSet<>();
+
+        for (Guess state : elementarySets) {
+          if (!state.isAssumed(untilFormula) || state.isAssumed(untilFormula.getRight())) {
+            acceptingSet.add(state.toString());
+          }
+        }
 
-            reduced.add(ltlFormula);
+        gnbaBuilder.addAcceptingSet(acceptingSet);
+      } else if (ltlFormula instanceof LTLEventuallyFormula eventuallyFormula) {
+        Set<String> acceptingSet = new HashSet<>();
+        for (Guess state : elementarySets) {
+          if (!state.isAssumed(eventuallyFormula)
+              || state.isAssumed(eventuallyFormula.getFormula())) {
+            acceptingSet.add(state.toString());
+          }
+        }
+        gnbaBuilder.addAcceptingSet(acceptingSet);
+      } else if (ltlFormula instanceof LTLAlwaysFormula alwaysFormula) {
+        Set<String> acceptingSet = new HashSet<>();
+        for (Guess state : elementarySets) {
+          if (state.isAssumed(alwaysFormula) || !state.isAssumed(alwaysFormula.getFormula())) {
+            acceptingSet.add(state.toString());
+          }
         }
+        gnbaBuilder.addAcceptingSet(acceptingSet);
+      }
+    }
 
-        return reduced;
+    for (Guess elementarySet : elementarySets) {
+      if (elementarySet.isAssumed(formula)) {
+        gnbaBuilder.addInitialState(elementarySet.toString());
+      }
     }
 
-    private Set<Guess> computeElementarySets(Set<String> atomicPropositions, Set<LTLFormula> closure) {
-        Set<Guess> elementarySets = new HashSet<>();
+    return gnbaBuilder.build();
+  }
+
+  // we can reduce the closure by removing everything that is directly implied by another formula
+  public Set<LTLFormula> reduceClosure(Set<LTLFormula> closure) {
+    Set<LTLFormula> reduced = new HashSet<>();
+    for (LTLFormula ltlFormula : closure) {
+      if (ltlFormula instanceof LTLTrueFormula
+          || ltlFormula instanceof LTLFalseFormula
+          || ltlFormula instanceof LTLNotFormula
+          || ltlFormula instanceof LTLParenthesisFormula) {
+        continue;
+      }
+
+      reduced.add(ltlFormula);
+    }
 
-        Assignment assignment = new Assignment();
+    return reduced;
+  }
 
-        // add all atomic propositions to the closure, even if they don't occur in the formula
-        for (String atomicProposition : atomicPropositions) {
-            LTLFormula atomicPropositionFormula = identifier(atomicProposition);
-            closure.add(atomicPropositionFormula);
-        }
+  private Set<Guess> computeElementarySets(
+      Set<String> atomicPropositions, Set<LTLFormula> closure) {
+    Set<Guess> elementarySets = new HashSet<>();
 
-        Set<LTLFormula> reduced = reduceClosure(closure);
-
-        while (true) {
-            Optional<LTLFormula> unassigned = reduced.stream().filter(f -> !assignment.assignsFormulaOrNegation(f)).findFirst();
-            if (unassigned.isEmpty()) {
-                Guess guess = assignment.toB();
-                if (guess.isElementary(closure)) {
-                    elementarySets.add(guess);
-                }
-
-                boolean success = assignment.backtrack();
-                if (!success) {
-                    break;
-                }
-            } else {
-                LTLFormula f = unassigned.get();
-                assignment.assign(f, true);
-            }
-        }
+    Assignment assignment = new Assignment();
 
-        return elementarySets;
+    // add all atomic propositions to the closure, even if they don't occur in the formula
+    for (String atomicProposition : atomicPropositions) {
+      LTLFormula atomicPropositionFormula = identifier(atomicProposition);
+      closure.add(atomicPropositionFormula);
     }
 
-    static class Guess {
-        private final Set<LTLFormula> assumedSubformulas;
+    Set<LTLFormula> reduced = reduceClosure(closure);
 
-        Guess(Set<LTLFormula> assumedSubformulas) {
-            this.assumedSubformulas = assumedSubformulas;
+    while (true) {
+      Optional<LTLFormula> unassigned =
+          reduced.stream().filter(f -> !assignment.assignsFormulaOrNegation(f)).findFirst();
+      if (unassigned.isEmpty()) {
+        Guess guess = assignment.toB();
+        if (guess.isElementary(closure)) {
+          elementarySets.add(guess);
         }
 
-        public Set<String> assumedAtomicPropositions() {
-            Set<String> atomicPropositions = new HashSet<>();
-            for (LTLFormula formula : assumedSubformulas) {
-                if (formula instanceof LTLIdentifierFormula identifierFormula) {
-                    atomicPropositions.add(identifierFormula.getIdentifier());
-                }
-            }
+        boolean success = assignment.backtrack();
+        if (!success) {
+          break;
+        }
+      } else {
+        LTLFormula f = unassigned.get();
+        assignment.assign(f, true);
+      }
+    }
 
-            return atomicPropositions;
+    return elementarySets;
+  }
+
+  static class Guess {
+    private final Set<LTLFormula> assumedSubformulas;
+
+    Guess(Set<LTLFormula> assumedSubformulas) {
+      this.assumedSubformulas = assumedSubformulas;
+    }
+
+    public Set<String> assumedAtomicPropositions() {
+      Set<String> atomicPropositions = new HashSet<>();
+      for (LTLFormula formula : assumedSubformulas) {
+        if (formula instanceof LTLIdentifierFormula identifierFormula) {
+          atomicPropositions.add(identifierFormula.getIdentifier());
         }
+      }
 
-        public boolean isAssumed(LTLFormula formula) {
-            if (formula instanceof LTLTrueFormula) {
-                return true;
-            } else if (assumedSubformulas.contains(formula)) {
-                return true;
-            } else if (formula instanceof LTLNotFormula notFormula) {
-                return !isAssumed(notFormula.getFormula());
-            } else if (formula instanceof LTLParenthesisFormula parenthesisFormula) {
-                return isAssumed(parenthesisFormula.getFormula());
-            }
+      return atomicPropositions;
+    }
+
+    public boolean isAssumed(LTLFormula formula) {
+      if (formula instanceof LTLTrueFormula) {
+        return true;
+      } else if (assumedSubformulas.contains(formula)) {
+        return true;
+      } else if (formula instanceof LTLNotFormula notFormula) {
+        return !isAssumed(notFormula.getFormula());
+      } else if (formula instanceof LTLParenthesisFormula parenthesisFormula) {
+        return isAssumed(parenthesisFormula.getFormula());
+      }
+
+      return false;
+    }
+
+    public boolean isElementary(Set<LTLFormula> closure) {
+      return isMaximallyConsistent(closure) && isLocallyConsistent(closure);
+    }
+
+    // we left out the rule for 'not' because by construction, we only have positive literals
+    public boolean isMaximallyConsistent(Set<LTLFormula> closure) {
+      for (LTLFormula formula : closure) {
+        boolean lhs;
+        boolean rhs;
 
+        if (formula instanceof LTLAndFormula andFormula) {
+          lhs = isAssumed(andFormula);
+
+          rhs = true;
+          for (LTLFormula component : andFormula.getComponents()) {
+            rhs &= isAssumed(component);
+          }
+
+          if (lhs != rhs) {
             return false;
-        }
+          }
+        } else if (formula instanceof LTLOrFormula orFormula) {
+          lhs = isAssumed(orFormula);
 
-        public boolean isElementary(Set<LTLFormula> closure) {
-            return isMaximallyConsistent(closure) && isLocallyConsistent(closure);
+          rhs = false;
+          for (LTLFormula component : orFormula.getComponents()) {
+            rhs |= isAssumed(component);
+          }
+
+          if (lhs != rhs) {
+            return false;
+          }
         }
+      }
 
-        // we left out the rule for 'not' because by construction, we only have positive literals
-        public boolean isMaximallyConsistent(Set<LTLFormula> closure) {
-            for (LTLFormula formula : closure) {
-                boolean lhs;
-                boolean rhs;
-
-                if (formula instanceof LTLAndFormula andFormula) {
-                    lhs = isAssumed(andFormula);
-
-                    rhs = true;
-                    for (LTLFormula component : andFormula.getComponents()) {
-                        rhs &= isAssumed(component);
-                    }
-
-                    if (lhs != rhs) {
-                        return false;
-                    }
-                } else if (formula instanceof LTLOrFormula orFormula) {
-                    lhs = isAssumed(orFormula);
-
-                    rhs = false;
-                    for (LTLFormula component : orFormula.getComponents()) {
-                        rhs |= isAssumed(component);
-                    }
-
-                    if (lhs != rhs) {
-                        return false;
-                    }
-                }
-            }
+      return true;
+    }
 
-            return true;
-        }
+    /*
+     * We derived the following additional rules for local consistency:
+     * 1. phi in B => eventually phi in B
+     * 2. always phi in B => phi in B
+     */
+    public boolean isLocallyConsistent(Set<LTLFormula> closure) {
+      for (LTLFormula subformula : closure) {
+        if (subformula instanceof LTLUntilFormula untilFormula) {
+          boolean rightAssumed = isAssumed(untilFormula.getRight());
+          boolean untilAssumed = isAssumed(untilFormula);
+
+          if (rightAssumed && !untilAssumed) {
+            return false;
+          }
 
-        /*
-         * We derived the following additional rules for local consistency:
-         * 1. phi in B => eventually phi in B
-         * 2. always phi in B => phi in B
-         */
-        public boolean isLocallyConsistent(Set<LTLFormula> closure) {
-            for (LTLFormula subformula : closure) {
-                if (subformula instanceof LTLUntilFormula untilFormula) {
-                    boolean rightAssumed = isAssumed(untilFormula.getRight());
-                    boolean untilAssumed = isAssumed(untilFormula);
-
-                    if (rightAssumed && !untilAssumed) {
-                        return false;
-                    }
-
-                    boolean leftAssumed = isAssumed(untilFormula.getLeft());
-
-                    if (untilAssumed && !rightAssumed && !leftAssumed) {
-                        return false;
-                    }
-                } else if(subformula instanceof LTLAlwaysFormula alwaysFormula) {
-                    boolean alwaysAssumed = isAssumed(alwaysFormula);
-                    boolean innerAssumed = isAssumed(alwaysFormula.getFormula());
-
-                    if(alwaysAssumed && !innerAssumed) {
-                        return false;
-                    }
-                } else if(subformula instanceof LTLEventuallyFormula eventuallyFormula) {
-                    boolean eventuallyAssumed = isAssumed(eventuallyFormula);
-                    boolean innerAssumed = isAssumed(eventuallyFormula.getFormula());
-
-                    if(innerAssumed && !eventuallyAssumed) {
-                        return false;
-                    }
-                }
-            }
+          boolean leftAssumed = isAssumed(untilFormula.getLeft());
 
-            return true;
-        }
+          if (untilAssumed && !rightAssumed && !leftAssumed) {
+            return false;
+          }
+        } else if (subformula instanceof LTLAlwaysFormula alwaysFormula) {
+          boolean alwaysAssumed = isAssumed(alwaysFormula);
+          boolean innerAssumed = isAssumed(alwaysFormula.getFormula());
+
+          if (alwaysAssumed && !innerAssumed) {
+            return false;
+          }
+        } else if (subformula instanceof LTLEventuallyFormula eventuallyFormula) {
+          boolean eventuallyAssumed = isAssumed(eventuallyFormula);
+          boolean innerAssumed = isAssumed(eventuallyFormula.getFormula());
 
-        @Override
-        public String toString() {
-            return assumedSubformulas.toString();
+          if (innerAssumed && !eventuallyAssumed) {
+            return false;
+          }
         }
+      }
+
+      return true;
     }
 
-    static class Assignment {
+    @Override
+    public String toString() {
+      return assumedSubformulas.toString();
+    }
+  }
 
-        private final Map<LTLFormula, Boolean> assignments;
-        private final Stack<SimpleEntry<LTLFormula, Boolean>> decisionStack;
+  static class Assignment {
 
-        Assignment() {
-            this.assignments = new HashMap<>();
-            this.decisionStack = new Stack<>();
-        }
+    private final Map<LTLFormula, Boolean> assignments;
+    private final Stack<SimpleEntry<LTLFormula, Boolean>> decisionStack;
 
-        boolean assignsFormulaOrNegation(LTLFormula formula) {
-            return assignments.containsKey(formula) || assignments.containsKey(formula.negate());
-        }
+    Assignment() {
+      this.assignments = new HashMap<>();
+      this.decisionStack = new Stack<>();
+    }
 
-        boolean get(LTLFormula formula) {
-            return assignments.get(formula);
-        }
+    boolean assignsFormulaOrNegation(LTLFormula formula) {
+      return assignments.containsKey(formula) || assignments.containsKey(formula.negate());
+    }
 
-        void assign(LTLFormula formula, boolean value) {
-            assignments.put(formula, value);
-            decisionStack.push(new SimpleEntry<>(formula, false));
-        }
+    boolean get(LTLFormula formula) {
+      return assignments.get(formula);
+    }
 
-        private void reassign(LTLFormula formula, boolean value) {
-            assignments.put(formula, value);
-            decisionStack.push(new SimpleEntry<>(formula, true));
-        }
+    void assign(LTLFormula formula, boolean value) {
+      assignments.put(formula, value);
+      decisionStack.push(new SimpleEntry<>(formula, false));
+    }
 
-        boolean backtrack() {
-            while (!decisionStack.isEmpty()) {
-                SimpleEntry<LTLFormula, Boolean> lastDecision = decisionStack.pop();
-                if (lastDecision.getValue()) {
-                    assignments.remove(lastDecision.getKey());
-                } else {
-                    reassign(lastDecision.getKey(), !get(lastDecision.getKey()));
-                    return true;
-                }
-            }
+    private void reassign(LTLFormula formula, boolean value) {
+      assignments.put(formula, value);
+      decisionStack.push(new SimpleEntry<>(formula, true));
+    }
 
-            return false;
+    boolean backtrack() {
+      while (!decisionStack.isEmpty()) {
+        SimpleEntry<LTLFormula, Boolean> lastDecision = decisionStack.pop();
+        if (lastDecision.getValue()) {
+          assignments.remove(lastDecision.getKey());
+        } else {
+          reassign(lastDecision.getKey(), !get(lastDecision.getKey()));
+          return true;
         }
+      }
 
-        Guess toB() {
-            Set<LTLFormula> assumedSubformulas = new HashSet<>();
-            for (LTLFormula formula : assignments.keySet()) {
-                if (get(formula)) {
-                    assumedSubformulas.add(formula);
-                }
-            }
+      return false;
+    }
 
-            return new Guess(assumedSubformulas);
+    Guess toB() {
+      Set<LTLFormula> assumedSubformulas = new HashSet<>();
+      for (LTLFormula formula : assignments.keySet()) {
+        if (get(formula)) {
+          assumedSubformulas.add(formula);
         }
+      }
 
-        @Override
-        public String toString() {
-            StringBuilder sb = new StringBuilder();
-            for (SimpleEntry<LTLFormula, Boolean> decision : decisionStack) {
-                boolean value = get(decision.getKey());
-                int valueInt = value ? 1 : 0;
-                sb.append(decision.getKey().toString()).append("=").append(valueInt).append("; ");
-            }
+      return new Guess(assumedSubformulas);
+    }
 
-            return sb.toString();
-        }
+    @Override
+    public String toString() {
+      StringBuilder sb = new StringBuilder();
+      for (SimpleEntry<LTLFormula, Boolean> decision : decisionStack) {
+        boolean value = get(decision.getKey());
+        int valueInt = value ? 1 : 0;
+        sb.append(decision.getKey().toString()).append("=").append(valueInt).append("; ");
+      }
+
+      return sb.toString();
     }
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java
index 5f38930..2bdc0fb 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelChecker.java
@@ -3,7 +3,4 @@
 import me.paultristanwagner.modelchecking.ModelChecker;
 import me.paultristanwagner.modelchecking.ltl.formula.LTLFormula;
 
-public interface LTLModelChecker extends ModelChecker<LTLFormula, LTLModelCheckingResult> {
-
-
-}
+public interface LTLModelChecker extends ModelChecker<LTLFormula, LTLModelCheckingResult> {}
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelCheckingResult.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelCheckingResult.java
index 78cc7fd..4c483e3 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelCheckingResult.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/LTLModelCheckingResult.java
@@ -5,22 +5,22 @@
 
 public class LTLModelCheckingResult extends ModelCheckingResult {
 
-    private final InfinitePath counterExample;
+  private final InfinitePath counterExample;
 
-    private LTLModelCheckingResult( boolean result, InfinitePath counterExample ) {
-        super( result );
-        this.counterExample = counterExample;
-    }
+  private LTLModelCheckingResult(boolean result, InfinitePath counterExample) {
+    super(result);
+    this.counterExample = counterExample;
+  }
 
-    public static LTLModelCheckingResult models() {
-        return new LTLModelCheckingResult( true, null );
-    }
+  public static LTLModelCheckingResult models() {
+    return new LTLModelCheckingResult(true, null);
+  }
 
-    public static LTLModelCheckingResult doesNotModel( InfinitePath counterExample ) {
-        return new LTLModelCheckingResult( false, counterExample );
-    }
+  public static LTLModelCheckingResult doesNotModel(InfinitePath counterExample) {
+    return new LTLModelCheckingResult(false, counterExample);
+  }
 
-    public InfinitePath getCounterExample() {
-        return counterExample;
-    }
+  public InfinitePath getCounterExample() {
+    return counterExample;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java
index a54abed..1a6ebb6 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAlwaysFormula.java
@@ -1,47 +1,47 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.ALWAYS_SYMBOL;
-
 public class LTLAlwaysFormula extends LTLFormula {
 
-    private final LTLFormula formula;
-
-    private LTLAlwaysFormula( LTLFormula formula ) {
-        this.formula = formula;
-    }
-
-    public static LTLAlwaysFormula always(LTLFormula formula ) {
-        return new LTLAlwaysFormula( formula );
-    }
-
-    public LTLFormula getFormula() {
-        return formula;
-    }
-
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        subformulas.addAll( formula.getAllSubformulas() );
-        return subformulas;
-    }
-
-    @Override
-    public String toString() {
-        return ALWAYS_SYMBOL + formula;
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLAlwaysFormula alwaysFormula && formula.equals(alwaysFormula.formula);
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(formula);
-    }
+  private final LTLFormula formula;
+
+  private LTLAlwaysFormula(LTLFormula formula) {
+    this.formula = formula;
+  }
+
+  public static LTLAlwaysFormula always(LTLFormula formula) {
+    return new LTLAlwaysFormula(formula);
+  }
+
+  public LTLFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    subformulas.addAll(formula.getAllSubformulas());
+    return subformulas;
+  }
+
+  @Override
+  public String toString() {
+    return ALWAYS_SYMBOL + formula;
+  }
+
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLAlwaysFormula alwaysFormula && formula.equals(alwaysFormula.formula);
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(formula);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java
index d2fe136..422cb60 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLAndFormula.java
@@ -1,65 +1,65 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.AND_SYMBOL;
-
 public class LTLAndFormula extends LTLFormula {
 
-    private final List<LTLFormula> components;
+  private final List<LTLFormula> components;
 
-    private LTLAndFormula(List<LTLFormula> components) {
-        this.components = components;
-    }
+  private LTLAndFormula(List<LTLFormula> components) {
+    this.components = components;
+  }
 
-    public static LTLAndFormula and(LTLFormula... components) {
-        return new LTLAndFormula(Arrays.asList(components));
-    }
+  public static LTLAndFormula and(LTLFormula... components) {
+    return new LTLAndFormula(Arrays.asList(components));
+  }
 
-    public static LTLAndFormula and(List<LTLFormula> components) {
-        return new LTLAndFormula(components);
-    }
+  public static LTLAndFormula and(List<LTLFormula> components) {
+    return new LTLAndFormula(components);
+  }
 
-    public List<LTLFormula> getComponents() {
-        return components;
-    }
+  public List<LTLFormula> getComponents() {
+    return components;
+  }
 
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        for (LTLFormula component : components) {
-            subformulas.addAll( component.getAllSubformulas() );
-        }
-        return subformulas;
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    for (LTLFormula component : components) {
+      subformulas.addAll(component.getAllSubformulas());
     }
+    return subformulas;
+  }
 
-    @Override
-    public String toString() {
-        StringBuilder builder = new StringBuilder();
-        for (int i = 0; i < components.size(); i++) {
-            builder.append(components.get(i).toString());
-
-            if (i < components.size() - 1) {
-                builder.append(" ");
-                builder.append(AND_SYMBOL);
-                builder.append(" ");
-            }
-        }
+  @Override
+  public String toString() {
+    StringBuilder builder = new StringBuilder();
+    for (int i = 0; i < components.size(); i++) {
+      builder.append(components.get(i).toString());
 
-        return builder.toString();
+      if (i < components.size() - 1) {
+        builder.append(" ");
+        builder.append(AND_SYMBOL);
+        builder.append(" ");
+      }
     }
 
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLAndFormula andFormula && components.equals(andFormula.components);
-    }
+    return builder.toString();
+  }
 
-    @Override
-    public int hashCode() {
-        return Objects.hash(components);
-    }
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLAndFormula andFormula && components.equals(andFormula.components);
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(components);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java
index 0271fd0..d9e6719 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLEventuallyFormula.java
@@ -1,47 +1,48 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.EVENTUALLY_SYMBOL;
-
 public class LTLEventuallyFormula extends LTLFormula {
 
-private final LTLFormula formula;
-
-    private LTLEventuallyFormula( LTLFormula formula ) {
-        this.formula = formula;
-    }
-
-    public static LTLEventuallyFormula eventually(LTLFormula formula ) {
-        return new LTLEventuallyFormula( formula );
-    }
-
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        subformulas.addAll( formula.getAllSubformulas() );
-        return subformulas;
-    }
-
-    public LTLFormula getFormula() {
-        return formula;
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLEventuallyFormula eventuallyFormula && formula.equals(eventuallyFormula.formula);
-    }
-
-    @Override
-    public String toString() {
-        return EVENTUALLY_SYMBOL + formula;
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(formula);
-    }
+  private final LTLFormula formula;
+
+  private LTLEventuallyFormula(LTLFormula formula) {
+    this.formula = formula;
+  }
+
+  public static LTLEventuallyFormula eventually(LTLFormula formula) {
+    return new LTLEventuallyFormula(formula);
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    subformulas.addAll(formula.getAllSubformulas());
+    return subformulas;
+  }
+
+  public LTLFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLEventuallyFormula eventuallyFormula
+        && formula.equals(eventuallyFormula.formula);
+  }
+
+  @Override
+  public String toString() {
+    return EVENTUALLY_SYMBOL + formula;
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(formula);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFalseFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFalseFormula.java
index 71cfcb1..74426e3 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFalseFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFalseFormula.java
@@ -6,32 +6,31 @@
 
 public class LTLFalseFormula extends LTLFormula {
 
-    private LTLFalseFormula() {
-    }
-
-    public static LTLFalseFormula FALSE() {
-        return new LTLFalseFormula();
-    }
-
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        return subformulas;
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLFalseFormula;
-    }
-
-    @Override
-    public String toString() {
-        return "false";
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(false);
-    }
+  private LTLFalseFormula() {}
+
+  public static LTLFalseFormula FALSE() {
+    return new LTLFalseFormula();
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    return subformulas;
+  }
+
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLFalseFormula;
+  }
+
+  @Override
+  public String toString() {
+    return "false";
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(false);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFormula.java
index 0fd7b56..af61ee8 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLFormula.java
@@ -1,33 +1,32 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
-import me.paultristanwagner.modelchecking.Formula;
+import static me.paultristanwagner.modelchecking.ltl.formula.LTLNotFormula.not;
 
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
-
-import static me.paultristanwagner.modelchecking.ltl.formula.LTLNotFormula.not;
+import me.paultristanwagner.modelchecking.Formula;
 
 public abstract class LTLFormula extends Formula {
 
-    public abstract List<LTLFormula> getAllSubformulas();
+  public abstract List<LTLFormula> getAllSubformulas();
 
-    public LTLFormula negate() {
-        if (this instanceof LTLNotFormula notFormula) {
-            return notFormula.getFormula();
-        } else {
-            return not(this);
-        }
+  public LTLFormula negate() {
+    if (this instanceof LTLNotFormula notFormula) {
+      return notFormula.getFormula();
+    } else {
+      return not(this);
     }
-
-    public Set<LTLFormula> getClosure() {
-        List<LTLFormula> subformulaList = getAllSubformulas();
-        Set<LTLFormula> subformulaSet = new HashSet<>(subformulaList);
-        Set<LTLFormula> closure = new HashSet<>(subformulaSet);
-        for (LTLFormula formula : subformulaSet) {
-            closure.add(formula.negate());
-        }
-
-        return closure;
+  }
+
+  public Set<LTLFormula> getClosure() {
+    List<LTLFormula> subformulaList = getAllSubformulas();
+    Set<LTLFormula> subformulaSet = new HashSet<>(subformulaList);
+    Set<LTLFormula> closure = new HashSet<>(subformulaSet);
+    for (LTLFormula formula : subformulaSet) {
+      closure.add(formula.negate());
     }
+
+    return closure;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLIdentifierFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLIdentifierFormula.java
index 297877e..dcbe6e1 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLIdentifierFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLIdentifierFormula.java
@@ -6,39 +6,40 @@
 
 public class LTLIdentifierFormula extends LTLFormula {
 
-    private final String identifier;
-
-    private LTLIdentifierFormula( String identifier ) {
-        this.identifier = identifier;
-    }
-
-    public static LTLIdentifierFormula identifier(String identifier ) {
-        return new LTLIdentifierFormula( identifier );
-    }
-
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        return subformulas;
-    }
-
-    public String getIdentifier() {
-        return identifier;
-    }
-
-    @Override
-    public String toString() {
-        return identifier;
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLIdentifierFormula identifierFormula && identifier.equals(identifierFormula.identifier);
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(identifier);
-    }
+  private final String identifier;
+
+  private LTLIdentifierFormula(String identifier) {
+    this.identifier = identifier;
+  }
+
+  public static LTLIdentifierFormula identifier(String identifier) {
+    return new LTLIdentifierFormula(identifier);
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    return subformulas;
+  }
+
+  public String getIdentifier() {
+    return identifier;
+  }
+
+  @Override
+  public String toString() {
+    return identifier;
+  }
+
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLIdentifierFormula identifierFormula
+        && identifier.equals(identifierFormula.identifier);
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(identifier);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java
index f622a98..672e900 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNextFormula.java
@@ -1,47 +1,47 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.NEXT_SYMBOL;
-
 public class LTLNextFormula extends LTLFormula {
 
-    private final LTLFormula formula;
-
-    private LTLNextFormula( LTLFormula formula ) {
-        this.formula = formula;
-    }
-
-    public static LTLNextFormula next(LTLFormula formula ) {
-        return new LTLNextFormula( formula );
-    }
-
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        subformulas.addAll( formula.getAllSubformulas() );
-        return subformulas;
-    }
-
-    public LTLFormula getFormula() {
-        return formula;
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLNextFormula nextFormula && formula.equals(nextFormula.formula);
-    }
-
-    @Override
-    public String toString() {
-        return NEXT_SYMBOL + formula;
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(formula);
-    }
+  private final LTLFormula formula;
+
+  private LTLNextFormula(LTLFormula formula) {
+    this.formula = formula;
+  }
+
+  public static LTLNextFormula next(LTLFormula formula) {
+    return new LTLNextFormula(formula);
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    subformulas.addAll(formula.getAllSubformulas());
+    return subformulas;
+  }
+
+  public LTLFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLNextFormula nextFormula && formula.equals(nextFormula.formula);
+  }
+
+  @Override
+  public String toString() {
+    return NEXT_SYMBOL + formula;
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(formula);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java
index ff6a8e3..66745a4 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLNotFormula.java
@@ -1,11 +1,11 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.NOT_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.NOT_SYMBOL;
-
 public class LTLNotFormula extends LTLFormula {
 
     private final LTLFormula formula;
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java
index db9c62e..0278ce1 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLOrFormula.java
@@ -1,64 +1,64 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.OR_SYMBOL;
-
 public class LTLOrFormula extends LTLFormula {
 
-    private final List<LTLFormula> components;
-
-    private LTLOrFormula(List<LTLFormula> components) {
-        this.components = components;
-    }
+  private final List<LTLFormula> components;
 
-    public static LTLOrFormula or(LTLFormula... components) {
-        return new LTLOrFormula( List.of( components ) );
-    }
+  private LTLOrFormula(List<LTLFormula> components) {
+    this.components = components;
+  }
 
-    public static LTLOrFormula or(List<LTLFormula> components) {
-        return new LTLOrFormula( components );
-    }
+  public static LTLOrFormula or(LTLFormula... components) {
+    return new LTLOrFormula(List.of(components));
+  }
 
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        for (LTLFormula component : components) {
-            subformulas.addAll( component.getAllSubformulas() );
-        }
-        return subformulas;
-    }
+  public static LTLOrFormula or(List<LTLFormula> components) {
+    return new LTLOrFormula(components);
+  }
 
-    public List<LTLFormula> getComponents() {
-        return components;
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    for (LTLFormula component : components) {
+      subformulas.addAll(component.getAllSubformulas());
     }
+    return subformulas;
+  }
 
-    @Override
-    public String toString() {
-        StringBuilder builder = new StringBuilder();
-        for (int i = 0; i < components.size(); i++) {
-            builder.append( components.get( i ).toString() );
+  public List<LTLFormula> getComponents() {
+    return components;
+  }
 
-            if (i < components.size() - 1) {
-                builder.append( " " );
-                builder.append( OR_SYMBOL );
-                builder.append( " " );
-            }
-        }
+  @Override
+  public String toString() {
+    StringBuilder builder = new StringBuilder();
+    for (int i = 0; i < components.size(); i++) {
+      builder.append(components.get(i).toString());
 
-        return builder.toString();
+      if (i < components.size() - 1) {
+        builder.append(" ");
+        builder.append(OR_SYMBOL);
+        builder.append(" ");
+      }
     }
 
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLOrFormula orFormula && components.equals( orFormula.components );
-    }
+    return builder.toString();
+  }
 
-    @Override
-    public int hashCode() {
-        return Objects.hash(components);
-    }
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLOrFormula orFormula && components.equals(orFormula.components);
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(components);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLParenthesisFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLParenthesisFormula.java
index 492b390..bf512b8 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLParenthesisFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLParenthesisFormula.java
@@ -6,44 +6,45 @@
 
 public class LTLParenthesisFormula extends LTLFormula {
 
-    private final LTLFormula formula;
-
-    private LTLParenthesisFormula( LTLFormula formula ) {
-        this.formula = formula;
-    }
-
-    public static LTLParenthesisFormula parenthesis(LTLFormula formula ) {
-        return new LTLParenthesisFormula( formula );
+  private final LTLFormula formula;
+
+  private LTLParenthesisFormula(LTLFormula formula) {
+    this.formula = formula;
+  }
+
+  public static LTLParenthesisFormula parenthesis(LTLFormula formula) {
+    return new LTLParenthesisFormula(formula);
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    subformulas.addAll(formula.getAllSubformulas());
+    return subformulas;
+  }
+
+  public LTLFormula getFormula() {
+    return formula;
+  }
+
+  @Override
+  public String toString() {
+    if (formula instanceof LTLUntilFormula || formula instanceof LTLParenthesisFormula) {
+      return formula.toString();
     }
 
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        subformulas.addAll( formula.getAllSubformulas() );
-        return subformulas;
-    }
-
-    public LTLFormula getFormula() {
-        return formula;
-    }
+    return "(" + formula + ")";
+  }
 
-    @Override
-    public String toString() {
-        if (formula instanceof LTLUntilFormula || formula instanceof LTLParenthesisFormula) {
-            return formula.toString();
-        }
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLParenthesisFormula parenthesisFormula
+        && formula.equals(parenthesisFormula.formula);
+  }
 
-        return "(" + formula + ")";
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLParenthesisFormula parenthesisFormula && formula.equals(parenthesisFormula.formula);
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(formula);
-    }
+  @Override
+  public int hashCode() {
+    return Objects.hash(formula);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLTrueFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLTrueFormula.java
index 3f4bb86..c2dab1f 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLTrueFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLTrueFormula.java
@@ -6,32 +6,31 @@
 
 public class LTLTrueFormula extends LTLFormula {
 
-    private LTLTrueFormula() {
-    }
-
-    public static LTLTrueFormula TRUE() {
-        return new LTLTrueFormula();
-    }
-
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add(this);
-        return subformulas;
-    }
-
-    @Override
-    public String toString() {
-        return "true";
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLTrueFormula;
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(true);
-    }
+  private LTLTrueFormula() {}
+
+  public static LTLTrueFormula TRUE() {
+    return new LTLTrueFormula();
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    return subformulas;
+  }
+
+  @Override
+  public String toString() {
+    return "true";
+  }
+
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLTrueFormula;
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(true);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java
index bb77591..41b0eed 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/formula/LTLUntilFormula.java
@@ -1,54 +1,56 @@
 package me.paultristanwagner.modelchecking.ltl.formula;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.UNTIL_SYMBOL;
+
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Objects;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.UNTIL_SYMBOL;
-
 public class LTLUntilFormula extends LTLFormula {
 
-    private final LTLFormula left;
-    private final LTLFormula right;
-
-    private LTLUntilFormula( LTLFormula left, LTLFormula right ) {
-        this.left = left;
-        this.right = right;
-    }
-
-    public static LTLFormula until(LTLFormula left, LTLFormula right ) {
-        return new LTLUntilFormula( left, right );
-    }
-
-    @Override
-    public List<LTLFormula> getAllSubformulas() {
-        List<LTLFormula> subformulas = new ArrayList<>();
-        subformulas.add( this );
-        subformulas.addAll( left.getAllSubformulas() );
-        subformulas.addAll( right.getAllSubformulas() );
-        return subformulas;
-    }
-
-    public LTLFormula getLeft() {
-        return left;
-    }
-
-    public LTLFormula getRight() {
-        return right;
-    }
-
-    @Override
-    public String toString() {
-        return "(" + left + " " + UNTIL_SYMBOL + " " + right + ")";
-    }
-
-    @Override
-    public boolean equals(Object obj) {
-        return obj instanceof LTLUntilFormula untilFormula && left.equals(untilFormula.left) && right.equals(untilFormula.right);
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(left, right);
-    }
+  private final LTLFormula left;
+  private final LTLFormula right;
+
+  private LTLUntilFormula(LTLFormula left, LTLFormula right) {
+    this.left = left;
+    this.right = right;
+  }
+
+  public static LTLFormula until(LTLFormula left, LTLFormula right) {
+    return new LTLUntilFormula(left, right);
+  }
+
+  @Override
+  public List<LTLFormula> getAllSubformulas() {
+    List<LTLFormula> subformulas = new ArrayList<>();
+    subformulas.add(this);
+    subformulas.addAll(left.getAllSubformulas());
+    subformulas.addAll(right.getAllSubformulas());
+    return subformulas;
+  }
+
+  public LTLFormula getLeft() {
+    return left;
+  }
+
+  public LTLFormula getRight() {
+    return right;
+  }
+
+  @Override
+  public String toString() {
+    return "(" + left + " " + UNTIL_SYMBOL + " " + right + ")";
+  }
+
+  @Override
+  public boolean equals(Object obj) {
+    return obj instanceof LTLUntilFormula untilFormula
+        && left.equals(untilFormula.left)
+        && right.equals(untilFormula.right);
+  }
+
+  @Override
+  public int hashCode() {
+    return Objects.hash(left, right);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java
index 2fff54e..ab107d0 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLLexer.java
@@ -1,33 +1,34 @@
 package me.paultristanwagner.modelchecking.ltl.parse;
 
-import me.paultristanwagner.modelchecking.parse.TokenType;
-import me.paultristanwagner.modelchecking.parse.Lexer;
-
 import static me.paultristanwagner.modelchecking.util.Symbol.*;
 
+import me.paultristanwagner.modelchecking.parse.Lexer;
+import me.paultristanwagner.modelchecking.parse.TokenType;
+
 public class LTLLexer extends Lexer {
 
-    static final TokenType LPAREN = TokenType.of("(", "^\\(");
-    static final TokenType RPAREN = TokenType.of(")", "^\\)");
-    static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)");
-    static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)");
-    static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)");
-    static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)");
-    static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)");
-    static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)");
-    static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)");
-    static final TokenType EVENTUALLY = TokenType.of("eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)");
-    static final TokenType ALWAYS = TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)");
-    static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]");
+  static final TokenType LPAREN = TokenType.of("(", "^\\(");
+  static final TokenType RPAREN = TokenType.of(")", "^\\)");
+  static final TokenType TRUE = TokenType.of("true", "^(true|TRUE)");
+  static final TokenType FALSE = TokenType.of("false", "^(false|FALSE)");
+  static final TokenType NOT = TokenType.of("not", "^(" + NOT_SYMBOL + "|!|not|NOT|~)");
+  static final TokenType AND = TokenType.of("and", "^(" + AND_SYMBOL + "|&|and|AND)");
+  static final TokenType OR = TokenType.of("or", "^(" + OR_SYMBOL + "|\\||or|OR)");
+  static final TokenType NEXT = TokenType.of("next", "^(" + NEXT_SYMBOL + "|next|NEXT|O)");
+  static final TokenType UNTIL = TokenType.of("until", "^(" + UNTIL_SYMBOL + "|until|UNTIL)");
+  static final TokenType EVENTUALLY =
+      TokenType.of(
+          "eventually", "^(" + EVENTUALLY_SYMBOL + "|eventually|EVENTUALLY|diamond|DIAMOND)");
+  static final TokenType ALWAYS =
+      TokenType.of("always", "^(" + ALWAYS_SYMBOL + "|always|ALWAYS|box|BOX)");
+  static final TokenType IDENTIFIER = TokenType.of("identifier", "^[a-z]");
 
-    public LTLLexer(String input) {
-        super(input);
+  public LTLLexer(String input) {
+    super(input);
 
-        registerTokenTypes(
-                LPAREN, RPAREN, TRUE, FALSE, NOT, AND, OR,
-                NEXT, UNTIL, EVENTUALLY, ALWAYS, IDENTIFIER
-        );
+    registerTokenTypes(
+        LPAREN, RPAREN, TRUE, FALSE, NOT, AND, OR, NEXT, UNTIL, EVENTUALLY, ALWAYS, IDENTIFIER);
 
-        this.initialize(input);
-    }
+    this.initialize(input);
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java
index 0dd2590..0ef2284 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ltl/parse/LTLParser.java
@@ -35,158 +35,159 @@
 
 public class LTLParser implements Parser<LTLFormula> {
 
-    // todo: add logical operators for implication and equivalence
-
-    /*
-     * LTL Grammar:
-     *
-     *    <A> ::= <B>
-     *        | <A> OR <B>
-     *    <B> ::= <C>
-     *        | <B> AND <C>
-     *    <C> :: <D>
-     *        | <C> UNTIL <D>
-     *    <D> ::= NOT <D>
-     *        | NEXT <A>
-     *        | ALWAYS <A>
-     *        | EVENTUALLY <A>
-     *        | '(' <A> ')'
-     *        | TRUE
-     *        | FALSE
-     *        | IDENTIFIER
-     *
-     */
-
-    @Override
-    public LTLFormula parse(String input, AtomicInteger index) {
-        LTLLexer lexer = new LTLLexer(input);
-
-        lexer.requireNextToken();
-
-        LTLFormula formula = parseLTLFormula(lexer);
-
-        lexer.requireNoToken();
-
-        return formula;
+  // todo: add logical operators for implication and equivalence
+
+  /*
+   * LTL Grammar:
+   *
+   *    <A> ::= <B>
+   *        | <A> OR <B>
+   *    <B> ::= <C>
+   *        | <B> AND <C>
+   *    <C> :: <D>
+   *        | <C> UNTIL <D>
+   *    <D> ::= NOT <D>
+   *        | NEXT <A>
+   *        | ALWAYS <A>
+   *        | EVENTUALLY <A>
+   *        | '(' <A> ')'
+   *        | TRUE
+   *        | FALSE
+   *        | IDENTIFIER
+   *
+   */
+
+  @Override
+  public LTLFormula parse(String input, AtomicInteger index) {
+    LTLLexer lexer = new LTLLexer(input);
+
+    lexer.requireNextToken();
+
+    LTLFormula formula = parseLTLFormula(lexer);
+
+    lexer.requireNoToken();
+
+    return formula;
+  }
+
+  private LTLFormula parseLTLFormula(LTLLexer lexer) {
+    return A(lexer);
+  }
+
+  private LTLFormula A(LTLLexer lexer) {
+    List<LTLFormula> components = new ArrayList<>();
+    LTLFormula first = B(lexer);
+    components.add(first);
+
+    while (lexer.hasNextToken() && lexer.getLookahead().getType() == LTLLexer.OR) {
+      lexer.consume(OR);
+      components.add(B(lexer));
     }
 
-    private LTLFormula parseLTLFormula(LTLLexer lexer) {
-        return A(lexer);
+    if (components.size() == 1) {
+      return first;
     }
 
-    private LTLFormula A(LTLLexer lexer) {
-        List<LTLFormula> components = new ArrayList<>();
-        LTLFormula first = B(lexer);
-        components.add(first);
+    return or(components);
+  }
 
-        while (lexer.hasNextToken() && lexer.getLookahead().getType() == LTLLexer.OR) {
-            lexer.consume(OR);
-            components.add(B(lexer));
-        }
+  private LTLFormula B(LTLLexer lexer) {
+    List<LTLFormula> components = new ArrayList<>();
+    LTLFormula first = C(lexer);
+    components.add(first);
 
-        if (components.size() == 1) {
-            return first;
-        }
-
-        return or(components);
-    }
-
-    private LTLFormula B(LTLLexer lexer) {
-        List<LTLFormula> components = new ArrayList<>();
-        LTLFormula first = C(lexer);
-        components.add(first);
-
-        while (lexer.hasNextToken() && lexer.getLookahead().getType() == AND) {
-            lexer.consume(AND);
-            components.add(C(lexer));
-        }
-
-        if (components.size() == 1) {
-            return first;
-        }
-
-        return and(components);
+    while (lexer.hasNextToken() && lexer.getLookahead().getType() == AND) {
+      lexer.consume(AND);
+      components.add(C(lexer));
     }
 
-    private LTLFormula C(LTLLexer lexer) {
-        LTLFormula formula = D(lexer);
-
-        while (lexer.hasNextToken() && lexer.getLookahead().getType() == UNTIL) {
-            lexer.consume(UNTIL);
-            LTLFormula second = D(lexer);
-            formula = until(formula, second);
-        }
-
-        return formula;
+    if (components.size() == 1) {
+      return first;
     }
 
-    private LTLFormula D(LTLLexer lexer) {
-        lexer.requireNextToken();
-
-        Token lookahead = lexer.getLookahead();
-        TokenType type = lookahead.getType();
-
-        if (type == NOT) {
-            return parseNot(lexer);
-        } else if (type == NEXT) {
-            return parseNext(lexer);
-        } else if (type == ALWAYS) {
-            return parseAlways(lexer);
-        } else if (type == EVENTUALLY) {
-            return parseEventually(lexer);
-        } else if (type == TRUE) {
-            return parseTrue(lexer);
-        } else if (type == FALSE) {
-            return parseFalse(lexer);
-        } else if (type == LPAREN) {
-            return parseParenthesis(lexer);
-        } else if (type == IDENTIFIER) {
-            return parseIdentifier(lexer);
-        }
-
-        throw new SyntaxError("Unexpected token " + type.getName(), lexer.getInput(), lexer.getTokenStart());
-    }
+    return and(components);
+  }
 
-    private LTLNotFormula parseNot(LTLLexer lexer) {
-        lexer.consume(NOT);
-        return not(D(lexer));
-    }
+  private LTLFormula C(LTLLexer lexer) {
+    LTLFormula formula = D(lexer);
 
-    private LTLNextFormula parseNext(LTLLexer lexer) {
-        lexer.consume(NEXT);
-        return next(A(lexer));
+    while (lexer.hasNextToken() && lexer.getLookahead().getType() == UNTIL) {
+      lexer.consume(UNTIL);
+      LTLFormula second = D(lexer);
+      formula = until(formula, second);
     }
 
-    private LTLAlwaysFormula parseAlways(LTLLexer lexer) {
-        lexer.consume(ALWAYS);
-        return always(A(lexer));
+    return formula;
+  }
+
+  private LTLFormula D(LTLLexer lexer) {
+    lexer.requireNextToken();
+
+    Token lookahead = lexer.getLookahead();
+    TokenType type = lookahead.getType();
+
+    if (type == NOT) {
+      return parseNot(lexer);
+    } else if (type == NEXT) {
+      return parseNext(lexer);
+    } else if (type == ALWAYS) {
+      return parseAlways(lexer);
+    } else if (type == EVENTUALLY) {
+      return parseEventually(lexer);
+    } else if (type == TRUE) {
+      return parseTrue(lexer);
+    } else if (type == FALSE) {
+      return parseFalse(lexer);
+    } else if (type == LPAREN) {
+      return parseParenthesis(lexer);
+    } else if (type == IDENTIFIER) {
+      return parseIdentifier(lexer);
     }
 
-    private LTLEventuallyFormula parseEventually(LTLLexer lexer) {
-        lexer.consume(EVENTUALLY);
-        return eventually(A(lexer));
-    }
-
-    private LTLTrueFormula parseTrue(LTLLexer lexer) {
-        lexer.consume(TRUE);
-        return TRUE();
-    }
-
-    private LTLFalseFormula parseFalse(LTLLexer lexer) {
-        lexer.consume(FALSE);
-        return FALSE();
-    }
-
-    private LTLFormula parseParenthesis(LTLLexer lexer) {
-        lexer.consume(LPAREN);
-        LTLFormula formula = A(lexer);
-        lexer.consume(RPAREN);
-        return parenthesis(formula);
-    }
-
-    private LTLIdentifierFormula parseIdentifier(LTLLexer lexer) {
-        Token token = lexer.getLookahead();
-        lexer.consume(IDENTIFIER);
-        return identifier(token.getValue());
-    }
+    throw new SyntaxError(
+        "Unexpected token " + type.getName(), lexer.getInput(), lexer.getTokenStart());
+  }
+
+  private LTLNotFormula parseNot(LTLLexer lexer) {
+    lexer.consume(NOT);
+    return not(D(lexer));
+  }
+
+  private LTLNextFormula parseNext(LTLLexer lexer) {
+    lexer.consume(NEXT);
+    return next(A(lexer));
+  }
+
+  private LTLAlwaysFormula parseAlways(LTLLexer lexer) {
+    lexer.consume(ALWAYS);
+    return always(A(lexer));
+  }
+
+  private LTLEventuallyFormula parseEventually(LTLLexer lexer) {
+    lexer.consume(EVENTUALLY);
+    return eventually(A(lexer));
+  }
+
+  private LTLTrueFormula parseTrue(LTLLexer lexer) {
+    lexer.consume(TRUE);
+    return TRUE();
+  }
+
+  private LTLFalseFormula parseFalse(LTLLexer lexer) {
+    lexer.consume(FALSE);
+    return FALSE();
+  }
+
+  private LTLFormula parseParenthesis(LTLLexer lexer) {
+    lexer.consume(LPAREN);
+    LTLFormula formula = A(lexer);
+    lexer.consume(RPAREN);
+    return parenthesis(formula);
+  }
+
+  private LTLIdentifierFormula parseIdentifier(LTLLexer lexer) {
+    Token token = lexer.getLookahead();
+    lexer.consume(IDENTIFIER);
+    return identifier(token.getValue());
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/parse/Lexer.java b/src/main/java/me/paultristanwagner/modelchecking/parse/Lexer.java
index f835ed5..c5705f2 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/parse/Lexer.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/parse/Lexer.java
@@ -67,12 +67,19 @@ public Token nextToken() {
   }
 
   public void consume(TokenType token) {
-    if(lookahead == null) {
+    if (lookahead == null) {
       throw new SyntaxError("Expected token '" + token.getName() + "'", input, cursor);
     }
 
     if (lookahead.getType() != token) {
-      throw new SyntaxError("Expected token '" + token.getName() + "' but got token '" + lookahead.getType().getName() + "'", input, cursor - lookahead.getValue().length());
+      throw new SyntaxError(
+          "Expected token '"
+              + token.getName()
+              + "' but got token '"
+              + lookahead.getType().getName()
+              + "'",
+          input,
+          cursor - lookahead.getValue().length());
     }
 
     nextToken();
@@ -95,14 +102,17 @@ public boolean hasNextToken() {
   }
 
   public void requireNextToken() {
-    if(!hasNextToken()) {
+    if (!hasNextToken()) {
       throw new SyntaxError("Unexpected end of input", input, cursor);
     }
   }
 
   public void requireNoToken() {
-    if(hasNextToken()) {
-      throw new SyntaxError("Unexpected token " + lookahead.getType().getName(), input, cursor - lookahead.getValue().length());
+    if (hasNextToken()) {
+      throw new SyntaxError(
+          "Unexpected token " + lookahead.getType().getName(),
+          input,
+          cursor - lookahead.getValue().length());
     }
   }
 
diff --git a/src/main/java/me/paultristanwagner/modelchecking/parse/Parser.java b/src/main/java/me/paultristanwagner/modelchecking/parse/Parser.java
index f051181..5391c58 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/parse/Parser.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/parse/Parser.java
@@ -4,9 +4,9 @@
 
 public interface Parser<T> {
 
-  default T parse( String input ) {
-    return parse( input, new AtomicInteger( 0 ) );
+  default T parse(String input) {
+    return parse(input, new AtomicInteger(0));
   }
-  
-  T parse( String input, AtomicInteger index );
+
+  T parse(String input, AtomicInteger index);
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/parse/SyntaxError.java b/src/main/java/me/paultristanwagner/modelchecking/parse/SyntaxError.java
index 08f0c18..8c50645 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/parse/SyntaxError.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/parse/SyntaxError.java
@@ -4,40 +4,40 @@
 
 public class SyntaxError extends Error {
 
-    private String internalMessage;
-    private final String input;
-    private final int index;
-
-    public SyntaxError(String input, int index) {
-        this.input = input;
-        this.index = index;
-    }
-
-    public SyntaxError(String message, String input, int index) {
-        super(message + " at index " + index);
-        this.internalMessage = message;
-        this.input = input;
-        this.index = index;
-    }
-
-    public void printWithContext() {
-        OUT.println("Syntax Error: " + getMessage());
-        OUT.println(input);
-        for (int i = 0; i < index; i++) {
-            OUT.print(" ");
-        }
-        OUT.println("^");
+  private String internalMessage;
+  private final String input;
+  private final int index;
+
+  public SyntaxError(String input, int index) {
+    this.input = input;
+    this.index = index;
+  }
+
+  public SyntaxError(String message, String input, int index) {
+    super(message + " at index " + index);
+    this.internalMessage = message;
+    this.input = input;
+    this.index = index;
+  }
+
+  public void printWithContext() {
+    OUT.println("Syntax Error: " + getMessage());
+    OUT.println(input);
+    for (int i = 0; i < index; i++) {
+      OUT.print(" ");
     }
+    OUT.println("^");
+  }
 
-    public String getInternalMessage() {
-        return internalMessage;
-    }
+  public String getInternalMessage() {
+    return internalMessage;
+  }
 
-    public String getInput() {
-        return input;
-    }
+  public String getInput() {
+    return input;
+  }
 
-    public int getIndex() {
-        return index;
-    }
+  public int getIndex() {
+    return index;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/parse/Token.java b/src/main/java/me/paultristanwagner/modelchecking/parse/Token.java
index f8c78f6..3cd2672 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/parse/Token.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/parse/Token.java
@@ -1,23 +1,23 @@
 package me.paultristanwagner.modelchecking.parse;
 
 public class Token {
-  
+
   private final TokenType type;
   private final String value;
-  
-  private Token( TokenType type, String value ) {
+
+  private Token(TokenType type, String value) {
     this.type = type;
     this.value = value;
   }
-  
-  public static Token of( TokenType type, String value ) {
-    return new Token( type, value );
+
+  public static Token of(TokenType type, String value) {
+    return new Token(type, value);
   }
-  
+
   public TokenType getType() {
     return type;
   }
-  
+
   public String getValue() {
     return value;
   }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/parse/TokenType.java b/src/main/java/me/paultristanwagner/modelchecking/parse/TokenType.java
index cd10e16..6e02852 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/parse/TokenType.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/parse/TokenType.java
@@ -1,23 +1,23 @@
 package me.paultristanwagner.modelchecking.parse;
 
 public class TokenType {
-  
+
   private final String name;
   private final String regex;
-  
-  private TokenType( String name, String regex) {
+
+  private TokenType(String name, String regex) {
     this.name = name;
     this.regex = regex;
   }
-  
-  public static TokenType of( String name, String regex) {
-    return new TokenType( name, regex );
+
+  public static TokenType of(String name, String regex) {
+    return new TokenType(name, regex);
   }
-  
+
   public String getName() {
     return name;
   }
-  
+
   public String getRegex() {
     return regex;
   }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/InfinitePath.java b/src/main/java/me/paultristanwagner/modelchecking/ts/InfinitePath.java
index ab0a757..84b717c 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ts/InfinitePath.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ts/InfinitePath.java
@@ -1,10 +1,10 @@
 package me.paultristanwagner.modelchecking.ts;
 
+import static me.paultristanwagner.modelchecking.util.Symbol.LOWERCASE_OMEGA;
+
 import java.util.ArrayList;
 import java.util.List;
 
-import static me.paultristanwagner.modelchecking.util.Symbol.LOWERCASE_OMEGA;
-
 public record InfinitePath(List<String> start, List<String> cycle) {
 
     private static final String TUPLE_PREFIX = "(";
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TSPersistenceResult.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TSPersistenceResult.java
index 0fc37c3..a3634f3 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ts/TSPersistenceResult.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TSPersistenceResult.java
@@ -2,27 +2,27 @@
 
 public final class TSPersistenceResult {
 
-    private final boolean isPersistent;
-    private final InfinitePath witness;
+  private final boolean isPersistent;
+  private final InfinitePath witness;
 
-    private TSPersistenceResult(boolean isPersistent, InfinitePath witness) {
-        this.isPersistent = isPersistent;
-        this.witness = witness;
-    }
+  private TSPersistenceResult(boolean isPersistent, InfinitePath witness) {
+    this.isPersistent = isPersistent;
+    this.witness = witness;
+  }
 
-    public static TSPersistenceResult persistent() {
-        return new TSPersistenceResult(true, null);
-    }
+  public static TSPersistenceResult persistent() {
+    return new TSPersistenceResult(true, null);
+  }
 
-    public static TSPersistenceResult notPersistent(InfinitePath witness) {
-        return new TSPersistenceResult(false, witness);
-    }
+  public static TSPersistenceResult notPersistent(InfinitePath witness) {
+    return new TSPersistenceResult(false, witness);
+  }
 
-    public boolean isPersistent() {
-        return isPersistent;
-    }
+  public boolean isPersistent() {
+    return isPersistent;
+  }
 
-    public InfinitePath getWitness() {
-        return witness;
-    }
+  public InfinitePath getWitness() {
+    return witness;
+  }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TSTransition.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TSTransition.java
index 661a34d..faad00c 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ts/TSTransition.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TSTransition.java
@@ -29,7 +29,9 @@ public static class TSTransitionAdapter
 
     @Override
     public JsonElement serialize(
-            TSTransition transition, java.lang.reflect.Type typeOfSrc, JsonSerializationContext context) {
+        TSTransition transition,
+        java.lang.reflect.Type typeOfSrc,
+        JsonSerializationContext context) {
       JsonArray jsonArray = new JsonArray();
       jsonArray.add(transition.getFrom());
       jsonArray.add(transition.getTo());
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java
index 86b58fd..7a3073b 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystem.java
@@ -1,24 +1,24 @@
 package me.paultristanwagner.modelchecking.ts;
 
+import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.notPersistent;
+import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.persistent;
+import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
+
 import com.google.gson.Gson;
 import com.google.gson.GsonBuilder;
+import java.util.*;
+import java.util.AbstractMap.SimpleEntry;
 import me.paultristanwagner.modelchecking.automaton.NBA;
 import me.paultristanwagner.modelchecking.automaton.NBATransition;
 import me.paultristanwagner.modelchecking.ts.TSTransition.TSTransitionAdapter;
 
-import java.util.AbstractMap.SimpleEntry;
-import java.util.*;
-
-import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.notPersistent;
-import static me.paultristanwagner.modelchecking.ts.TSPersistenceResult.persistent;
-import static me.paultristanwagner.modelchecking.util.TupleUtil.stringTuple;
-
 public class TransitionSystem {
 
   private static final Gson GSON;
 
   static {
-    GSON = new GsonBuilder()
+    GSON =
+        new GsonBuilder()
             .registerTypeAdapter(TSTransition.class, new TSTransitionAdapter())
             .setPrettyPrinting()
             .create();
@@ -58,16 +58,16 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
     for (String initialState : initialStates) {
       List<String> label = labelingFunction.get(initialState);
 
-      for(NBATransition nbaTransition : nba.getTransitions()) {
+      for (NBATransition nbaTransition : nba.getTransitions()) {
         String q0 = nbaTransition.getFrom();
-        if(!nba.getInitialStates().contains(q0)) {
+        if (!nba.getInitialStates().contains(q0)) {
           continue;
         }
 
         String q = nbaTransition.getTo();
 
         // todo: match actions and labels more carefully
-        if(!nbaTransition.getAction().equals(label.toString())) {
+        if (!nbaTransition.getAction().equals(label.toString())) {
           continue;
         }
 
@@ -76,7 +76,6 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
         builder.addLabel(resultState, q);
         builder.addInitialState(resultState);
         queue.add(new SimpleEntry<>(initialState, q));
-
       }
     }
 
@@ -90,25 +89,25 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
       String q = state.getValue();
       List<String> sSuccessors = getSuccessors(s);
 
-        for (String sSuccessor : sSuccessors) {
-            List<String> sSuccessorLabel = labelingFunction.get(sSuccessor);
-            String sSuccessorLabelString = sSuccessorLabel.toString();
-            Set<String> qSuccessors = nba.getSuccessors(q, sSuccessorLabelString);
-            for (String qSuccessor : qSuccessors) {
+      for (String sSuccessor : sSuccessors) {
+        List<String> sSuccessorLabel = labelingFunction.get(sSuccessor);
+        String sSuccessorLabelString = sSuccessorLabel.toString();
+        Set<String> qSuccessors = nba.getSuccessors(q, sSuccessorLabelString);
+        for (String qSuccessor : qSuccessors) {
 
-              String from = stringTuple(s, q);
-              String to = stringTuple(sSuccessor, qSuccessor);
+          String from = stringTuple(s, q);
+          String to = stringTuple(sSuccessor, qSuccessor);
 
-              builder.addTransition(from, to);
+          builder.addTransition(from, to);
 
-              SimpleEntry<String, String> successor = new SimpleEntry<>(sSuccessor, qSuccessor);
-              if(!visited.contains(successor)) {
-                queue.add(successor);
-                builder.addState(to);
-                builder.addLabel(to, qSuccessor);
-              }
-            }
+          SimpleEntry<String, String> successor = new SimpleEntry<>(sSuccessor, qSuccessor);
+          if (!visited.contains(successor)) {
+            queue.add(successor);
+            builder.addState(to);
+            builder.addLabel(to, qSuccessor);
+          }
         }
+      }
     }
 
     return builder.build();
@@ -117,13 +116,13 @@ public TransitionSystem reachableSynchronousProduct(NBA nba) {
   private boolean cycleCheck(String s, Set<String> v, Stack<String> xi) {
     xi.push(s);
     v.add(s);
-    while(!xi.isEmpty()) {
+    while (!xi.isEmpty()) {
       String s1 = xi.peek();
       List<String> successors = getSuccessors(s1);
-      if(successors.contains(s)) {
+      if (successors.contains(s)) {
         xi.push(s);
         return true;
-      } else if(!v.containsAll(successors)) {
+      } else if (!v.containsAll(successors)) {
         Set<String> remainingSuccessors = new HashSet<>(successors);
         remainingSuccessors.removeAll(v);
 
@@ -149,7 +148,7 @@ public TSPersistenceResult checkPersistence(Set<String> persistentStates) {
     Stack<String> pi = new Stack<>();
     Stack<String> xi = new Stack<>();
 
-    while(!u.containsAll(initialStates)) {
+    while (!u.containsAll(initialStates)) {
       Set<String> remaining = new HashSet<>(initialStates);
       remaining.removeAll(u);
 
@@ -158,13 +157,13 @@ public TSPersistenceResult checkPersistence(Set<String> persistentStates) {
 
       pi.push(s0);
 
-      while(!pi.isEmpty()) {
+      while (!pi.isEmpty()) {
         String s = pi.peek();
 
         Set<String> remainingSuccessors = new HashSet<>(getSuccessors(s));
         remainingSuccessors.removeAll(u);
 
-        if(!remainingSuccessors.isEmpty()) {
+        if (!remainingSuccessors.isEmpty()) {
           String s1 = remainingSuccessors.stream().findAny().get();
           u.add(s1);
           pi.push(s1);
@@ -174,7 +173,7 @@ public TSPersistenceResult checkPersistence(Set<String> persistentStates) {
 
           boolean notPersistentState = labels.stream().noneMatch(persistentStates::contains);
 
-          if(notPersistentState && cycleCheck(s, v, xi)) {
+          if (notPersistentState && cycleCheck(s, v, xi)) {
             List<String> piList = new ArrayList<>(pi);
             List<String> xiList = new ArrayList<>(xi);
 
@@ -222,6 +221,6 @@ public String toJson() {
   }
 
   public static TransitionSystem fromJson(String string) {
-    return GSON.fromJson( string, TransitionSystem.class );
+    return GSON.fromJson(string, TransitionSystem.class);
   }
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java
index dbd101b..9663586 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/ts/TransitionSystemBuilder.java
@@ -3,13 +3,13 @@
 import java.util.*;
 
 public class TransitionSystemBuilder {
-  
+
   private final List<String> states;
   private final List<TSTransition> transitions;
   private final List<String> initialStates;
   private final List<String> atomicPropositions;
   private final Map<String, List<String>> labelingFunction;
-  
+
   public TransitionSystemBuilder() {
     this.states = new ArrayList<>();
     this.transitions = new ArrayList<>();
@@ -18,65 +18,66 @@ public TransitionSystemBuilder() {
     this.labelingFunction = new HashMap<>();
   }
 
-  public TransitionSystemBuilder addStates( String... states ) {
-    for ( String state : states ) {
-      addState( state );
+  public TransitionSystemBuilder addStates(String... states) {
+    for (String state : states) {
+      addState(state);
     }
 
     return this;
   }
 
-  public TransitionSystemBuilder addState( String state ) {
-    this.states.add( state );
+  public TransitionSystemBuilder addState(String state) {
+    this.states.add(state);
     return this;
   }
-  
-  public TransitionSystemBuilder addTransition( TSTransition transition ) {
-    this.transitions.add( transition );
+
+  public TransitionSystemBuilder addTransition(TSTransition transition) {
+    this.transitions.add(transition);
     return this;
   }
-  
+
   public TransitionSystemBuilder addTransition(String from, String to) {
-    this.transitions.add( TSTransition.of( from, to ) );
+    this.transitions.add(TSTransition.of(from, to));
     return this;
   }
-  
-  public TransitionSystemBuilder addInitialState( String initialState ) {
-    this.initialStates.add( initialState );
+
+  public TransitionSystemBuilder addInitialState(String initialState) {
+    this.initialStates.add(initialState);
     return this;
   }
-  
-  public TransitionSystemBuilder setAtomicPropositions( String... atomicPropositions ) {
-    return setAtomicPropositions( Arrays.asList( atomicPropositions ) );
+
+  public TransitionSystemBuilder setAtomicPropositions(String... atomicPropositions) {
+    return setAtomicPropositions(Arrays.asList(atomicPropositions));
   }
-  
-  public TransitionSystemBuilder setAtomicPropositions( List<String> atomicPropositions ) {
+
+  public TransitionSystemBuilder setAtomicPropositions(List<String> atomicPropositions) {
     this.atomicPropositions.clear();
-    this.atomicPropositions.addAll( atomicPropositions );
+    this.atomicPropositions.addAll(atomicPropositions);
     return this;
   }
-  
-  public TransitionSystemBuilder addAtomicProposition( String atomicProposition ) {
-    this.atomicPropositions.add( atomicProposition );
+
+  public TransitionSystemBuilder addAtomicProposition(String atomicProposition) {
+    this.atomicPropositions.add(atomicProposition);
     return this;
   }
-  
-  public TransitionSystemBuilder addLabel( String state, String atomicProposition ) {
-    List<String> labels = labelingFunction.computeIfAbsent( state, k -> new ArrayList<>() );
-    labels.add( atomicProposition );
-    
+
+  public TransitionSystemBuilder addLabel(String state, String atomicProposition) {
+    List<String> labels = labelingFunction.computeIfAbsent(state, k -> new ArrayList<>());
+    labels.add(atomicProposition);
+
     return this;
   }
-  
+
   public TransitionSystemBuilder addLabels(String state, String... atomicPropositions) {
-    List<String> labels = labelingFunction.computeIfAbsent( state, k -> new ArrayList<>() );
-    labels.addAll( Arrays.asList( atomicPropositions ) );
-    
+    List<String> labels = labelingFunction.computeIfAbsent(state, k -> new ArrayList<>());
+    labels.addAll(Arrays.asList(atomicPropositions));
+
     return this;
   }
-  
+
   public TransitionSystem build() {
-    return new TransitionSystem( states, transitions, initialStates, atomicPropositions, labelingFunction );
+    return new TransitionSystem(
+        states, transitions, initialStates, atomicPropositions, labelingFunction);
   }
 
   public List<String> getInitialStates() {
diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/AnsiColor.java b/src/main/java/me/paultristanwagner/modelchecking/util/AnsiColor.java
index 8c7cf57..ab72cda 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/util/AnsiColor.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/util/AnsiColor.java
@@ -13,7 +13,7 @@ public enum AnsiColor {
 
   private final String code;
 
-  AnsiColor( String code) {
+  AnsiColor(String code) {
     this.code = code;
   }
 
diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java b/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java
index f14580f..f9b4e4d 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/util/Symbol.java
@@ -2,21 +2,21 @@
 
 public class Symbol {
 
-    public static final String NOT_SYMBOL = "¬";
-    public static final String AND_SYMBOL = "∧";
-    public static final String OR_SYMBOL = "∨";
-    public static final String NEXT_SYMBOL = "◯";
-    public static final String UNTIL_SYMBOL = "U";
-    public static final String EVENTUALLY_SYMBOL = "◊";
-    public static final String ALWAYS_SYMBOL = "□";
-    public static final String UNIVERSAL_QUANTIFIER_SYMBOL = "∀";
-    public static final String EXISTENTIAL_QUANTIFIER_SYMBOL = "∃";
+  public static final String NOT_SYMBOL = "¬";
+  public static final String AND_SYMBOL = "∧";
+  public static final String OR_SYMBOL = "∨";
+  public static final String NEXT_SYMBOL = "◯";
+  public static final String UNTIL_SYMBOL = "U";
+  public static final String EVENTUALLY_SYMBOL = "◊";
+  public static final String ALWAYS_SYMBOL = "□";
+  public static final String UNIVERSAL_QUANTIFIER_SYMBOL = "∀";
+  public static final String EXISTENTIAL_QUANTIFIER_SYMBOL = "∃";
 
-    public static final String LOWERCASE_PHI_SYMBOL = "φ";
-    public static final String UPPERCASE_PHI_SYMBOL = "Φ";
+  public static final String LOWERCASE_PHI_SYMBOL = "φ";
+  public static final String UPPERCASE_PHI_SYMBOL = "Φ";
 
-    public static final String LOWERCASE_OMEGA = "ω";
+  public static final String LOWERCASE_OMEGA = "ω";
 
-    public static final String MODELS_SYMBOL = "⊨";
-    public static final String NOT_MODELS_SYMBOL = "⊭";
+  public static final String MODELS_SYMBOL = "⊨";
+  public static final String NOT_MODELS_SYMBOL = "⊭";
 }
diff --git a/src/main/java/me/paultristanwagner/modelchecking/util/TupleUtil.java b/src/main/java/me/paultristanwagner/modelchecking/util/TupleUtil.java
index 346adcb..45a6e36 100644
--- a/src/main/java/me/paultristanwagner/modelchecking/util/TupleUtil.java
+++ b/src/main/java/me/paultristanwagner/modelchecking/util/TupleUtil.java
@@ -2,16 +2,16 @@
 
 public class TupleUtil {
 
-    public static String stringTuple(Object... o) {
-        StringBuilder sb = new StringBuilder();
-        sb.append("(");
-        for (int i = 0; i < o.length; i++) {
-            sb.append(o[i]);
-            if (i < o.length - 1) {
-                sb.append(",");
-            }
-        }
-        sb.append(")");
-        return sb.toString();
+  public static String stringTuple(Object... o) {
+    StringBuilder sb = new StringBuilder();
+    sb.append("(");
+    for (int i = 0; i < o.length; i++) {
+      sb.append(o[i]);
+      if (i < o.length - 1) {
+        sb.append(",");
+      }
     }
+    sb.append(")");
+    return sb.toString();
+  }
 }
diff --git a/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java b/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java
index ca34fdc..4282a87 100644
--- a/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java
+++ b/src/test/java/me/paultristanwagner/modelchecking/GNBATest.java
@@ -1,14 +1,13 @@
 package me.paultristanwagner.modelchecking;
 
+import java.io.IOException;
+import java.io.InputStream;
 import me.paultristanwagner.modelchecking.automaton.GNBA;
 import me.paultristanwagner.modelchecking.automaton.NBA;
 import me.paultristanwagner.modelchecking.automaton.NBAEmptinessResult;
 import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Test;
 
-import java.io.IOException;
-import java.io.InputStream;
-
 public class GNBATest {
 
     @Test
diff --git a/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java b/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java
index 7edb706..cc6e5b9 100644
--- a/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java
+++ b/src/test/java/me/paultristanwagner/modelchecking/SynchronousProductTest.java
@@ -1,29 +1,30 @@
 package me.paultristanwagner.modelchecking;
 
+import java.io.IOException;
+import java.io.InputStream;
 import me.paultristanwagner.modelchecking.automaton.NBA;
 import me.paultristanwagner.modelchecking.ts.TransitionSystem;
 import org.junit.jupiter.api.Assertions;
 import org.junit.jupiter.api.Test;
 
-import java.io.IOException;
-import java.io.InputStream;
-
 public class SynchronousProductTest {
 
-    @Test
-    public void testSynchronousProduct() throws IOException {
-        InputStream tsInputStream = getClass().getClassLoader().getResourceAsStream("ts_message_delivery.json");
-        String tsJson = new String(tsInputStream.readAllBytes());
-        TransitionSystem ts = TransitionSystem.fromJson(tsJson);
+  @Test
+  public void testSynchronousProduct() throws IOException {
+    InputStream tsInputStream =
+        getClass().getClassLoader().getResourceAsStream("ts_message_delivery.json");
+    String tsJson = new String(tsInputStream.readAllBytes());
+    TransitionSystem ts = TransitionSystem.fromJson(tsJson);
 
-        InputStream nbaInputStream = getClass().getClassLoader().getResourceAsStream("nba_never_delivered.json");
-        String nbaJson = new String(nbaInputStream.readAllBytes());
-        NBA nba = NBA.fromJson(nbaJson);
+    InputStream nbaInputStream =
+        getClass().getClassLoader().getResourceAsStream("nba_never_delivered.json");
+    String nbaJson = new String(nbaInputStream.readAllBytes());
+    NBA nba = NBA.fromJson(nbaJson);
 
-        TransitionSystem result = ts.reachableSynchronousProduct(nba);
-        Assertions.assertNotNull(result);
+    TransitionSystem result = ts.reachableSynchronousProduct(nba);
+    Assertions.assertNotNull(result);
 
-        Assertions.assertEquals(10, result.getStates().size());
-        Assertions.assertEquals(1, result.getInitialStates().size());
-    }
+    Assertions.assertEquals(10, result.getStates().size());
+    Assertions.assertEquals(1, result.getInitialStates().size());
+  }
 }