package de.bmoth.backend.ltl;



import de.bmoth.backend.ltl.transformation.ConvertFinallyGloballyFinallyToGloballyFinally;
import de.bmoth.backend.ltl.transformation.ConvertGloballyFinallyGloballyToFinallyGlobally;
import de.bmoth.backend.ltl.transformation.ConvertNotFinallyToGloballyNot;
import de.bmoth.backend.ltl.transformation.ConvertFinallyFinallyToFinally;
import de.bmoth.backend.ltl.transformation.ConvertGloballyGloballyToGlobally;
import de.bmoth.backend.ltl.transformation.ConvertNotGloballyToFinallyNot;
import de.bmoth.backend.ltl.transformation.ConvertNotNextToNextNot;
import de.bmoth.backend.ltl.transformation.ConvertPhiUntilPhiUntilPsiToPhiUntilPsi;
import de.bmoth.parser.ast.nodes.ltl.LTLFormula;
import de.bmoth.backend.ltl.transformation.*;
import de.bmoth.parser.ast.nodes.ltl.LTLNode;
import de.bmoth.parser.ast.visitors.ASTTransformationVisitor;
import de.bmoth.parser.ast.visitors.AbstractASTTransformation;

import java.util.ArrayList;
import java.util.List;

public class LTLTransformations {
    private static LTLTransformations instance;

    private final List<AbstractASTTransformation> transformationList;

    private LTLTransformations() {
        this.transformationList = new ArrayList<>();
        transformationList.add(new ConvertNotGloballyToFinallyNot());
        transformationList.add(new ConvertNotFinallyToGloballyNot());
        transformationList.add(new ConvertNotNextToNextNot());
        transformationList.add(new ConvertFinallyGloballyFinallyToGloballyFinally());
        transformationList.add(new ConvertGloballyFinallyGloballyToFinallyGlobally());
        transformationList.add(new ConvertGloballyGloballyToGlobally());
        transformationList.add(new ConvertFinallyFinallyToFinally());
        transformationList.add(new ConvertPhiUntilPhiUntilPsiToPhiUntilPsi());
        transformationList.add(new ConvertNextPhiUntilPsiToNextPhiUntilNextPsi());
        transformationList.add(new ConvertFinallyPhiOrPsiToFinallyPhiOrFinallyPsi());
        transformationList.add(new ConvertGloballyPhiAndPsiToGloballyPhiAndGloballyPsi());
        transformationList.add(new ConvertPsiNotBformulaToPsiNegatedBformula());
    }

    public static LTLTransformations getInstance() {
        if (null == instance) {
            instance = new LTLTransformations();
        }
        return instance;
    }

    public static LTLNode transformLTLNode(LTLNode ltlNode) {
        LTLTransformations astTransformationForZ3 = LTLTransformations.getInstance();
        ASTTransformationVisitor visitor = new ASTTransformationVisitor(astTransformationForZ3.transformationList);
        return visitor.transformLTLNode(ltlNode);
    }

}

@@ -29,740 +29,50 @@
 ;%0A%0A%0A
-%0A
 import 
-de.bmoth.backend.ltl.transformation.ConvertFinallyGloballyFinallyToGloballyFinally;%0Aimport de.bmoth.backend.ltl.transformation.ConvertGloballyFinallyGloballyToFinallyGlobally;%0Aimport de.bmoth.backend.ltl.transformation.ConvertNotFinallyToGloballyNot;%0Aimport de.bmoth.backend.ltl.transformation.ConvertFinallyFinallyToFinally;%0Aimport de.bmoth.backend.ltl.transformation.ConvertGloballyGloballyToGlobally;%0Aimport de.bmoth.backend.ltl.transformation.ConvertNotGloballyToFinallyNot;%0Aimport de.bmoth.backend.ltl.transformation.ConvertNotNextToNextNot;%0Aimport de.bmoth.backend.ltl.transformation.ConvertPhiUntilPhiUntilPsiToPhiUntilPsi;%0Aimport de.bmoth.parser.ast.nodes.ltl.LTLFormula;%0Aimport de.bmoth.backend.ltl.transformation.*
+com.google.common.reflect.ClassPath
 ;%0Aim
@@ -241,16 +241,44 @@
 ation;%0A%0A
+import java.io.IOException;%0A
 import j
@@ -324,42 +324,269 @@
 st;%0A
-%0Apublic class LTLTransformations %7B
+import java.util.logging.Level;%0Aimport java.util.logging.Logger;%0A%0Apublic class LTLTransformations %7B%0A    private final ClassLoader loader = Thread.currentThread().getContextClassLoader();%0A    private final Logger logger = Logger.getLogger(getClass().getName());%0A
 %0A   
@@ -786,24 +786,25 @@
 ayList%3C%3E();%0A
+%0A
         tran
@@ -805,200 +805,108 @@
   tr
-ansformationList.add(new ConvertNotGloballyToFinallyNot());%0A        transformationList.add(new ConvertNotFinallyToGloballyNot());%0A        transformationList.add(new ConvertNotNextToNextNot());
+y %7B%0A            for (final ClassPath.ClassInfo info : ClassPath.from(loader).getTopLevelClasses()) %7B
 %0A   
@@ -914,173 +914,156 @@
     
-transformationList.add(new ConvertFinallyGloballyFinallyToGloballyFinally());%0A        transformationList.add(new ConvertGloballyFinallyGloballyToFinallyGlobally
+        if (info.getName().startsWith(%22de.bmoth.backend.ltl.transformation%22)) %7B%0A                    final Class%3C?%3E clazz = info.load
 ()
-)
 ;%0A
+            
     
@@ -1093,539 +1093,266 @@
 add(
-new ConvertGloballyGloballyToGlobally());%0A        transformationList.add(new ConvertFinallyFinallyToFinally());%0A        transformationList.add(new ConvertPhiUntilPhiUntilPsiToPhiUntilPsi());%0A        transformationList.add(new ConvertNextPhiUntilPsiToNextPhiUntilNextPsi());%0A        transformationList.add(new ConvertFinallyPhiOrPsiToFinallyPhiOrFinallyPsi());%0A        transformationList.add(new ConvertGloballyPhiAndPsiToGloballyPhiAndGloballyPsi());%0A        transformationList.add(new ConvertPsiNotBformulaToPsiNegatedBformula());
+(AbstractASTTransformation) clazz.newInstance());%0A                %7D%0A            %7D%0A        %7D catch (IOException %7C InstantiationException %7C IllegalAccessException e) %7B%0A            logger.log(Level.SEVERE, %22Error loading LTL transformation rules%22, e);%0A        %7D
 %0A   
@@ -1352,37 +1352,38 @@
   %7D%0A    %7D%0A%0A    p
-ublic
+rivate
  static LTLTrans

fix broken merge