Attach index to steps

src/main/java/edu/kit/typicalc/model/Constraint.java

@@ -11,6 +11,7 @@ public class Constraint {
 
     private final Type a;
     private final Type b;
+    private int stepIndex = -1;
 
     /**
      * Creates a new constraint using the two types.
@@ -24,8 +25,6 @@ public class Constraint {
     }
 
     /**
-     * Returns the first type
-     *
      * @return the first type
      */
     public Type getFirstType() {
@@ -33,14 +32,27 @@ public class Constraint {
     }
 
     /**
-     * Returns the second type
-     *
      * @return the second type
      */
     public Type getSecondType() {
         return b;
     }
 
+    /**
+     * Set the number of the step that caused this constraint.
+     * @param index step number
+     */
+    public void setStepIndex(int index) {
+        this.stepIndex = index;
+    }
+
+    /**
+     * @return the step index
+     */
+    public int getStepIndex() {
+        return stepIndex;
+    }
+
     @Override
     public boolean equals(Object o) {
         if (this == o) {

src/main/java/edu/kit/typicalc/model/StepNumberFactory.java

@@ -0,0 +1,38 @@
+package edu.kit.typicalc.model;
+
+import java.util.Objects;
+
+/**
+ * Provides the next step number on demand.
+ */
+public class StepNumberFactory {
+
+    private static final int FIRST_STEP_NUMBER = 0;
+
+    private int nextStepIndex;
+
+    public StepNumberFactory() {
+        this.nextStepIndex = FIRST_STEP_NUMBER;
+    }
+
+    public int nextStepIndex() {
+        return nextStepIndex++;
+    }
+
+    @Override
+    public boolean equals(Object o) {
+        if (this == o) {
+            return true;
+        }
+        if (o == null || getClass() != o.getClass()) {
+            return false;
+        }
+        StepNumberFactory that = (StepNumberFactory) o;
+        return nextStepIndex == that.nextStepIndex;
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(nextStepIndex);
+    }
+}

src/main/java/edu/kit/typicalc/model/Tree.java

@@ -15,6 +15,7 @@ import java.util.*;
 public class Tree implements TermVisitorTree {
 
     private final TypeVariableFactory typeVarFactory;
+    private final StepNumberFactory stepNumberFactory;
     private final StepFactory stepFactory;
 
     private final TypeVariable firstTypeVariable;
@@ -32,7 +33,8 @@ public class Tree implements TermVisitorTree {
      * @param lambdaTerm      the lambda term to generate the tree for
      */
     protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm) {
-        this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE), false);
+        this(typeAssumptions, lambdaTerm, new TypeVariableFactory(TypeVariableKind.TREE), false,
+                new StepNumberFactory());
     }
 
     /**
@@ -46,10 +48,13 @@ public class Tree implements TermVisitorTree {
      * @param lambdaTerm          the lambda term to generate the tree for
      * @param typeVariableFactory the type variable factory to use
      * @param partOfLetTerm       indicates whether the tree is generated for a sub-inference that is part of a let term
+     * @param factory step number factory
      */
     protected Tree(Map<VarTerm, TypeAbstraction> typeAssumptions, LambdaTerm lambdaTerm,
-                   TypeVariableFactory typeVariableFactory, boolean partOfLetTerm) {
+                   TypeVariableFactory typeVariableFactory, boolean partOfLetTerm,
+                   StepNumberFactory factory) {
         this.typeVarFactory = typeVariableFactory;
+        this.stepNumberFactory = factory;
         this.constraints = new ArrayList<>();
 
         // quantified type assumptions have the same effect as let terms
@@ -105,6 +110,7 @@ public class Tree implements TermVisitorTree {
 
     @Override
     public InferenceStep visit(AppTerm appTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
+        int stepNr = stepNumberFactory.nextStepIndex();
         Type leftType = typeVarFactory.nextTypeVariable();
         Type rightType = typeVarFactory.nextTypeVariable();
 
@@ -125,11 +131,12 @@ public class Tree implements TermVisitorTree {
         }
 
         Conclusion conclusion = new Conclusion(typeAssumptions, appTerm, conclusionType);
-        return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint);
+        return stepFactory.createAppStep(leftPremise, rightPremise, conclusion, newConstraint, stepNr);
     }
 
     @Override
     public InferenceStep visit(AbsTerm absTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
+        int stepNr = stepNumberFactory.nextStepIndex();
         Map<VarTerm, TypeAbstraction> extendedTypeAssumptions = new LinkedHashMap<>(typeAssumptions);
         Type assType = typeVarFactory.nextTypeVariable();
         TypeAbstraction assAbs = new TypeAbstraction(assType);
@@ -145,13 +152,14 @@ public class Tree implements TermVisitorTree {
         InferenceStep premise = absTerm.getInner().accept(this, extendedTypeAssumptions, premiseType);
 
         Conclusion conclusion = new Conclusion(typeAssumptions, absTerm, conclusionType);
-        return stepFactory.createAbsStep(premise, conclusion, newConstraint);
+        return stepFactory.createAbsStep(premise, conclusion, newConstraint, stepNr);
     }
 
     @Override
     public InferenceStep visit(LetTerm letTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
+        int stepNr = stepNumberFactory.nextStepIndex();
         TypeInfererLet typeInfererLet = new TypeInfererLet(
-                letTerm.getVariableDefinition(), typeAssumptions, typeVarFactory);
+                letTerm.getVariableDefinition(), typeAssumptions, typeVarFactory, stepNumberFactory);
 
         Type premiseType = typeVarFactory.nextTypeVariable();
         Constraint newConstraint = new Constraint(conclusionType, premiseType);
@@ -185,20 +193,22 @@ public class Tree implements TermVisitorTree {
         }
 
         Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, conclusionType);
-        return stepFactory.createLetStep(conclusion, newConstraint, premise, typeInfererLet);
+        return stepFactory.createLetStep(conclusion, newConstraint, premise, typeInfererLet, stepNr);
     }
 
     @Override
     public InferenceStep visit(ConstTerm constant, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
+        int stepNr = stepNumberFactory.nextStepIndex();
         Constraint newConstraint = new Constraint(conclusionType, constant.getType());
         constraints.add(newConstraint);
 
         Conclusion conclusion = new Conclusion(typeAssumptions, constant, conclusionType);
-        return stepFactory.createConstStep(conclusion, newConstraint);
+        return stepFactory.createConstStep(conclusion, newConstraint, stepNr);
     }
 
     @Override
     public InferenceStep visit(VarTerm varTerm, Map<VarTerm, TypeAbstraction> typeAssumptions, Type conclusionType) {
+        int stepNr = stepNumberFactory.nextStepIndex();
         TypeAbstraction premiseAbs = typeAssumptions.get(varTerm);
         if (premiseAbs == null) {
             throw new IllegalStateException("Cannot create VarStep for VarTerm '"
@@ -210,7 +220,7 @@ public class Tree implements TermVisitorTree {
         constraints.add(newConstraint);
 
         Conclusion conclusion = new Conclusion(typeAssumptions, varTerm, conclusionType);
-        return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint);
+        return stepFactory.createVarStep(premiseAbs, instantiation, conclusion, newConstraint, stepNr);
     }
 
     @Override
@@ -223,11 +233,12 @@ public class Tree implements TermVisitorTree {
         }
         Tree tree = (Tree) o;
         return failedSubInference == tree.failedSubInference && firstTypeVariable.equals(tree.firstTypeVariable)
-                && firstInferenceStep.equals(tree.firstInferenceStep) && constraints.equals(tree.constraints);
+                && firstInferenceStep.equals(tree.firstInferenceStep) && constraints.equals(tree.constraints)
+                && stepNumberFactory.equals(tree.stepNumberFactory);
     }
 
     @Override
     public int hashCode() {
-        return Objects.hash(firstTypeVariable, firstInferenceStep, constraints, failedSubInference);
+        return Objects.hash(firstTypeVariable, firstInferenceStep, constraints, failedSubInference, stepNumberFactory);
     }
 }

src/main/java/edu/kit/typicalc/model/TypeInfererLet.java

@@ -28,10 +28,11 @@ public class TypeInfererLet implements TypeInfererInterface {
      * @param typeAssumptions the type assumptions to consider when generating the tree
      * @param typeVarFactory  the type variable factory that should be used in this inference to guarantee consistency
      *                        with the outer inference
+     * @param factory         the step number factory to pass to the Tree
      */
     protected TypeInfererLet(LambdaTerm lambdaTerm, Map<VarTerm, TypeAbstraction> typeAssumptions,
-                             TypeVariableFactory typeVarFactory) {
+                             TypeVariableFactory typeVarFactory, StepNumberFactory factory) {
-        tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory, true);
+        tree = new Tree(typeAssumptions, lambdaTerm, typeVarFactory, true, factory);
 
         // cancel algorithm if a sub-inference failed
         if (tree.hasFailedSubInference()) {

src/main/java/edu/kit/typicalc/model/step/AbsStep.java

@@ -18,9 +18,10 @@ public abstract class AbsStep extends InferenceStep {
      * @param premise    the premise of this step
      * @param conclusion the conclusion of this step
      * @param constraint the constraint added in this step
+     * @param stepIndex  step number
      */
-    protected AbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
+    protected AbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex) {
-        super(conclusion, constraint);
+        super(conclusion, constraint, stepIndex);
         this.premise = premise;
     }
 

src/main/java/edu/kit/typicalc/model/step/AbsStepDefault.java

@@ -14,9 +14,10 @@ public class AbsStepDefault extends AbsStep {
      * @param premise    the premise of this step
      * @param conclusion the conclusion of this step
      * @param constraint the constraint added in this step
+     * @param stepIndex  step number
      */
-    public AbsStepDefault(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
+    public AbsStepDefault(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex) {
-        super(premise, conclusion, constraint);
+        super(premise, conclusion, constraint, stepIndex);
     }
 
     /**

src/main/java/edu/kit/typicalc/model/step/AbsStepWithLet.java

@@ -14,9 +14,10 @@ public class AbsStepWithLet extends AbsStep {
      * @param premise    the premise of this step
      * @param conclusion the conclusion of this step
      * @param constraint constraint that can be derived from this step
+     * @param stepIndex  step number
      */
-    public AbsStepWithLet(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
+    public AbsStepWithLet(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex) {
-        super(premise, conclusion, constraint);
+        super(premise, conclusion, constraint, stepIndex);
     }
 
     /**

src/main/java/edu/kit/typicalc/model/step/AppStep.java

@@ -16,15 +16,17 @@ public abstract class AppStep extends InferenceStep {
     private final InferenceStep premise2;
 
     /**
-     * Initializes a new AbsStepWithLet with the given values.
+     * Initializes a new AbsStep with the given values.
      *
      * @param premise1   the first premise of this step
      * @param premise2   the second premise of this step
      * @param conclusion the conclusion of this step
      * @param constraint constraint that can be derived from this step
+     * @param stepIndex  step number
      */
-    protected AppStep(InferenceStep premise1, InferenceStep premise2, Conclusion conclusion, Constraint constraint) {
+    protected AppStep(InferenceStep premise1, InferenceStep premise2, Conclusion conclusion, Constraint constraint,
-        super(conclusion, constraint);
+                      int stepIndex) {
+        super(conclusion, constraint, stepIndex);
         this.premise1 = premise1;
         this.premise2 = premise2;
     }

src/main/java/edu/kit/typicalc/model/step/AppStepDefault.java

@@ -9,16 +9,17 @@ import edu.kit.typicalc.model.Constraint;
  */
 public class AppStepDefault extends AppStep {
     /**
-     * Initializes a new AbsStepWithLet with the given values.
+     * Initializes a new AbsStepDefault with the given values.
      *
      * @param premise1   the first premise of this step
      * @param premise2   the second premise of this step
      * @param conclusion the conclusion of this step
      * @param constraint constraint that can be derived from this step
+     * @param stepIndex  step number
      */
     public AppStepDefault(InferenceStep premise1, InferenceStep premise2,
-                          Conclusion conclusion, Constraint constraint) {
+                          Conclusion conclusion, Constraint constraint, int stepIndex) {
-        super(premise1, premise2, conclusion, constraint);
+        super(premise1, premise2, conclusion, constraint, stepIndex);
     }
 
     /**

src/main/java/edu/kit/typicalc/model/step/ConstStep.java

@@ -12,8 +12,9 @@ public abstract class ConstStep extends InferenceStep {
      *
      * @param conclusion the conclusion of this step
      * @param constraint the constraint added in this step
+     * @param stepIndex  step number
      */
-    protected ConstStep(Conclusion conclusion, Constraint constraint) {
+    protected ConstStep(Conclusion conclusion, Constraint constraint, int stepIndex) {
-        super(conclusion, constraint);
+        super(conclusion, constraint, stepIndex);
     }
 }

src/main/java/edu/kit/typicalc/model/step/ConstStepDefault.java

@@ -14,9 +14,10 @@ public class ConstStepDefault extends ConstStep {
      *
      * @param conclusion the conclusion of this step
      * @param constraint the constraint added in this step
+     * @param stepIndex  step number
      */
-    public ConstStepDefault(Conclusion conclusion, Constraint constraint) {
+    public ConstStepDefault(Conclusion conclusion, Constraint constraint, int stepIndex) {
-        super(conclusion, constraint);
+        super(conclusion, constraint, stepIndex);
     }
 
     /**

src/main/java/edu/kit/typicalc/model/step/EmptyStep.java

@@ -19,7 +19,8 @@ public class EmptyStep extends InferenceStep {
     public EmptyStep() {
         super(
                 new Conclusion(Collections.emptyMap(), new VarTerm(""), new NamedType("")),
-                new Constraint(new NamedType(""), new NamedType(""))
+                new Constraint(new NamedType(""), new NamedType("")),
+                -1 // TODO: check if this actually works
         );
     }
 

src/main/java/edu/kit/typicalc/model/step/InferenceStep.java

@@ -17,16 +17,19 @@ import java.util.Objects;
 public abstract class InferenceStep {
     private final Conclusion conclusion;
     private final Constraint constraint;
+    private final int stepIndex;
 
     /**
      * Initializes a new InferenceStep with the given values.
      *
      * @param conclusion the conclusion of this step
      * @param constraint the constraint added in this step
+     * @param stepIndex step number
      */
-    protected InferenceStep(Conclusion conclusion, Constraint constraint) {
+    protected InferenceStep(Conclusion conclusion, Constraint constraint, int stepIndex) {
         this.conclusion = conclusion;
         this.constraint = constraint;
+        this.stepIndex = stepIndex;
     }
 
     /**
@@ -63,11 +66,11 @@ public abstract class InferenceStep {
             return false;
         }
         InferenceStep that = (InferenceStep) o;
-        return conclusion.equals(that.conclusion) && constraint.equals(that.constraint);
+        return conclusion.equals(that.conclusion) && constraint.equals(that.constraint) && stepIndex == that.stepIndex;
     }
 
     @Override
     public int hashCode() {
-        return Objects.hash(conclusion, constraint);
+        return Objects.hash(conclusion, constraint, stepIndex);
     }
 }

src/main/java/edu/kit/typicalc/model/step/LetStep.java

@@ -27,9 +27,11 @@ public abstract class LetStep extends InferenceStep {
      * @param premise     the right premise of this step
      * @param typeInferer the typeInferer that performs the Type Inference for the premise
      *                    that needs its own type Inference.
+     * @param stepIndex   step number
      */
-    protected LetStep(Conclusion conclusion, Constraint constraint, InferenceStep premise, TypeInfererLet typeInferer) {
+    protected LetStep(Conclusion conclusion, Constraint constraint, InferenceStep premise, TypeInfererLet typeInferer,
-        super(conclusion, constraint);
+                      int stepIndex) {
+        super(conclusion, constraint, stepIndex);
         this.premise = premise;
         this.typeInferer = typeInferer;
     }

src/main/java/edu/kit/typicalc/model/step/LetStepDefault.java

@@ -16,10 +16,11 @@ public class LetStepDefault extends LetStep {
      * @param premise     the right premise of this step
      * @param typeInferer the typeInferer that performs the Type Inference for the premise
      *                    that needs its own type Inference.
+     * @param stepIndex   step number
      */
     public LetStepDefault(Conclusion conclusion, Constraint constraint, InferenceStep premise,
-                          TypeInfererLet typeInferer) {
+                          TypeInfererLet typeInferer, int stepIndex) {
-        super(conclusion, constraint, premise, typeInferer);
+        super(conclusion, constraint, premise, typeInferer, stepIndex);
     }
 
     /**

src/main/java/edu/kit/typicalc/model/step/OnlyConclusionStep.java

@@ -19,7 +19,8 @@ public class OnlyConclusionStep extends InferenceStep {
     public OnlyConclusionStep(Conclusion conclusion) {
         super(
                 conclusion,
-                new Constraint(new NamedType(""), new NamedType(""))
+                new Constraint(new NamedType(""), new NamedType("")),
+                -1 // TODO: check whether this is correct
         );
     }
 

src/main/java/edu/kit/typicalc/model/step/StepFactory.java

@@ -18,7 +18,7 @@ public interface StepFactory {
      * @param constraint the constraint that can be derived from this step
      * @return the created AbsStep
      */
-    AbsStep createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint);
+    AbsStep createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint, int stepIndex);
 
     /**
      * Creates an AppStep.
@@ -30,7 +30,7 @@ public interface StepFactory {
      * @return the created AppStep
      */
     AppStep createAppStep(InferenceStep premise1, InferenceStep premise2,
-                          Conclusion conclusion, Constraint constraint);
+                          Conclusion conclusion, Constraint constraint, int stepIndex);
 
     /**
      * Creates an ConstStep.
@@ -39,7 +39,7 @@ public interface StepFactory {
      * @param constraint the constraint that can be derived from this step
      * @return the created ConstStep
      */
-    ConstStep createConstStep(Conclusion conclusion, Constraint constraint);
+    ConstStep createConstStep(Conclusion conclusion, Constraint constraint, int stepIndex);
 
     /**
      * Creates a VarStep.
@@ -51,7 +51,7 @@ public interface StepFactory {
      * @return the created AbsStep
      */
     VarStep createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
-                          Conclusion conclusion, Constraint constraint);
+                          Conclusion conclusion, Constraint constraint, int stepIndex);
 
     /**
      * Creates a LetStep.
@@ -63,5 +63,5 @@ public interface StepFactory {
      * @return the created AppStep
      */
     LetStep createLetStep(Conclusion conclusion, Constraint constraint,
-                          InferenceStep premise, TypeInfererLet typeInferer);
+                          InferenceStep premise, TypeInfererLet typeInferer, int stepIndex);
 }

src/main/java/edu/kit/typicalc/model/step/StepFactoryDefault.java

@@ -11,17 +11,10 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
  */
 public class StepFactoryDefault implements StepFactory {
 
-    /**
-     * Creates an AbsStepDefault.
-     *
-     * @param premise    the premise of this step
-     * @param conclusion the conclusion of this step
-     * @param constraint the constraint that can be derived from this step
-     * @return the created AbsStepDefault
-     */
     @Override
-    public AbsStepDefault createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
+    public AbsStepDefault createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint,
-        return new AbsStepDefault(premise, conclusion, constraint);
+                                        int stepIndex) {
+        return new AbsStepDefault(premise, conclusion, constraint, stepIndex);
     }
 
     /**
@@ -35,8 +28,8 @@ public class StepFactoryDefault implements StepFactory {
      */
     @Override
     public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2,
-                                        Conclusion conclusion, Constraint constraint) {
+                                        Conclusion conclusion, Constraint constraint, int stepIndex) {
-        return new AppStepDefault(premise1, premise2, conclusion, constraint);
+        return new AppStepDefault(premise1, premise2, conclusion, constraint, stepIndex);
     }
 
     /**
@@ -47,8 +40,8 @@ public class StepFactoryDefault implements StepFactory {
      * @return the created ConstStepDefault
      */
     @Override
-    public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) {
+    public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint, int stepIndex) {
-        return new ConstStepDefault(conclusion, constraint);
+        return new ConstStepDefault(conclusion, constraint, stepIndex);
     }
 
     /**
@@ -62,8 +55,8 @@ public class StepFactoryDefault implements StepFactory {
      */
     @Override
     public VarStepDefault createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
-                                        Conclusion conclusion, Constraint constraint) {
+                                        Conclusion conclusion, Constraint constraint, int stepIndex) {
-        return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
+        return new VarStepDefault(typeAbstraction, instantiatedTypeAbs, conclusion, constraint, stepIndex);
     }
 
     /**
@@ -80,7 +73,7 @@ public class StepFactoryDefault implements StepFactory {
      */
     @Override
     public LetStep createLetStep(Conclusion conclusion, Constraint constraint,
-                                 InferenceStep premise, TypeInfererLet typeInferer) {
+                                 InferenceStep premise, TypeInfererLet typeInferer, int stepIndex) {
         throw new UnsupportedOperationException("Not possible to create LetStep when no let is present in the term");
     }
 }

src/main/java/edu/kit/typicalc/model/step/StepFactoryWithLet.java

@@ -11,32 +11,16 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
  */
 public class StepFactoryWithLet implements StepFactory {
 
-    /**
-     * Creates an AbsStepWithLet.
-     *
-     * @param premise    the premise of this step
-     * @param conclusion the conclusion of this step
-     * @param constraint the constraint that can be derived from this step
-     * @return the created AbsStepWithLet
-     */
     @Override
-    public AbsStepWithLet createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint) {
+    public AbsStepWithLet createAbsStep(InferenceStep premise, Conclusion conclusion, Constraint constraint,
-        return new AbsStepWithLet(premise, conclusion, constraint);
+                                        int stepIndex) {
+        return new AbsStepWithLet(premise, conclusion, constraint, stepIndex);
     }
 
-    /**
-     * Creates an AppStepDefault.
-     *
-     * @param premise1   the first premise of this step
-     * @param premise2   the second premise of this step
-     * @param conclusion the conclusion of this step
-     * @param constraint the constraint that can be derived from this step
-     * @return the created AppStepDefault
-     */
     @Override
     public AppStepDefault createAppStep(InferenceStep premise1, InferenceStep premise2,
-                                        Conclusion conclusion, Constraint constraint) {
+                                        Conclusion conclusion, Constraint constraint, int stepIndex) {
-        return new AppStepDefault(premise1, premise2, conclusion, constraint);
+        return new AppStepDefault(premise1, premise2, conclusion, constraint, stepIndex);
     }
 
     /**
@@ -47,8 +31,8 @@ public class StepFactoryWithLet implements StepFactory {
      * @return the created ConstStepDefault
      */
     @Override
-    public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint) {
+    public ConstStepDefault createConstStep(Conclusion conclusion, Constraint constraint, int stepIndex) {
-        return new ConstStepDefault(conclusion, constraint);
+        return new ConstStepDefault(conclusion, constraint, stepIndex);
     }
 
     /**
@@ -62,8 +46,9 @@ public class StepFactoryWithLet implements StepFactory {
      */
     @Override
     public VarStepWithLet createVarStep(TypeAbstraction typeAbstraction, Type instantiatedTypeAbs,
-                                        Conclusion conclusion, Constraint constraint) {
+                                        Conclusion conclusion, Constraint constraint, int stepIndex) {
-        return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint);
+        return new VarStepWithLet(typeAbstraction, instantiatedTypeAbs, conclusion, constraint,
+                stepIndex);
     }
 
     /**
@@ -77,7 +62,7 @@ public class StepFactoryWithLet implements StepFactory {
      */
     @Override
     public LetStepDefault createLetStep(Conclusion conclusion, Constraint constraint,
-                                        InferenceStep premise, TypeInfererLet typeInferer) {
+                                        InferenceStep premise, TypeInfererLet typeInferer, int stepIndex) {
-        return new LetStepDefault(conclusion, constraint, premise, typeInferer);
+        return new LetStepDefault(conclusion, constraint, premise, typeInferer, stepIndex);
     }
 }

src/main/java/edu/kit/typicalc/model/step/VarStep.java

@@ -23,10 +23,11 @@ public abstract class VarStep extends InferenceStep {
      * @param instantiatedTypeAbs      an instantiation of the type abstraction used in this step
      * @param conclusion               the conclusion of this step
      * @param constraint               the constraint added in this step
+     * @param stepIndex step number
      */
     protected VarStep(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
-                      Constraint constraint) {
+                      Constraint constraint, int stepIndex) {
-        super(conclusion, constraint);
+        super(conclusion, constraint, stepIndex);
         this.typeAbstractionInPremise = typeAbstractionInPremise;
         this.instantiatedTypeAbs = instantiatedTypeAbs;
     }

src/main/java/edu/kit/typicalc/model/step/VarStepDefault.java

@@ -17,10 +17,11 @@ public class VarStepDefault extends VarStep {
      * @param instantiatedTypeAbs      an instantiation of the type abstraction used in this step
      * @param conclusion               the conclusion of this step
      * @param constraint               the constraint added in this step
+     * @param stepIndex step number
      */
     public VarStepDefault(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
-                          Constraint constraint) {
+                          Constraint constraint, int stepIndex) {
-        super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint);
+        super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint, stepIndex);
     }
 
     /**

src/main/java/edu/kit/typicalc/model/step/VarStepWithLet.java

@@ -18,10 +18,11 @@ public class VarStepWithLet extends VarStep {
      * @param instantiatedTypeAbs      an instantiation of the type abstraction used in this step
      * @param conclusion               the conclusion of this step
      * @param constraint               the constraint added in this step
+     * @param stepIndex step number
      */
     public VarStepWithLet(TypeAbstraction typeAbstractionInPremise, Type instantiatedTypeAbs, Conclusion conclusion,
-                          Constraint constraint) {
+                          Constraint constraint, int stepIndex) {
-        super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint);
+        super(typeAbstractionInPremise, instantiatedTypeAbs, conclusion, constraint, stepIndex);
     }
 
     /**

src/test/java/edu/kit/typicalc/model/ConstraintTest.java

@@ -15,7 +15,7 @@ class ConstraintTest {
 
     @Test
     void equalsTest() {
-        EqualsVerifier.forClass(Constraint.class).usingGetClass().verify();
+        EqualsVerifier.forClass(Constraint.class).usingGetClass().withIgnoredFields("stepIndex").verify();
     }
 
     @Test

src/test/java/edu/kit/typicalc/model/ModelImplTest.java

@@ -51,10 +51,12 @@ class ModelImplTest {
                                         x, new TypeAbstraction(NamedType.INT),
                                         y, new TypeAbstraction(a2)),
                                         x, a3),
-                                new Constraint(a3, NamedType.INT)
+                                new Constraint(a3, NamedType.INT),
+                                1
                         ),
                         new Conclusion(Map.of(x, new TypeAbstraction(NamedType.INT)), term, a1),
-                        new Constraint(a1, new FunctionType(a2, a3))
+                        new Constraint(a1, new FunctionType(a2, a3)),
+                        0
                 ), typeInference.getFirstInferenceStep()
         );
     }

src/test/java/edu/kit/typicalc/model/TreeTest.java

@@ -42,7 +42,7 @@ class TreeTest {
             factory.nextTypeVariable();
             factoryRef.nextTypeVariable();
         }
-        Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR, factory, false);
+        Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR, factory, false, new StepNumberFactory());
         assertEquals(tree.getFirstTypeVariable(), factoryRef.nextTypeVariable());
     }
 
@@ -63,15 +63,15 @@ class TreeTest {
 
         Conclusion varLeftConclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, variable2);
         Constraint varLeftConstraint = new Constraint(variable2, TYPE);
-        InferenceStep varLeftStep = new VarStepDefault(TYPE_ABS, TYPE, varLeftConclusion, varLeftConstraint);
+        InferenceStep varLeftStep = new VarStepDefault(TYPE_ABS, TYPE, varLeftConclusion, varLeftConstraint, 1);
 
         Conclusion varRightConclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, variable3);
         Constraint varRightConstraint = new Constraint(variable3, TYPE);
-        InferenceStep varRightStep = new VarStepDefault(TYPE_ABS, TYPE, varRightConclusion, varRightConstraint);
+        InferenceStep varRightStep = new VarStepDefault(TYPE_ABS, TYPE, varRightConclusion, varRightConstraint, 2);
 
         Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, APP, tree.getFirstTypeVariable());
         Constraint appConstraint = new Constraint(variable2, new FunctionType(variable3, tree.getFirstTypeVariable()));
-        InferenceStep expectedStep = new AppStepDefault(varLeftStep, varRightStep, conclusion, appConstraint);
+        InferenceStep expectedStep = new AppStepDefault(varLeftStep, varRightStep, conclusion, appConstraint, 0);
 
         assertEquals(expectedStep, tree.getFirstInferenceStep());
 
@@ -94,11 +94,11 @@ class TreeTest {
         Conclusion varConclusion = new Conclusion(varTypeAss, VAR, variable3);
         Constraint varConstraint = new Constraint(variable2, variable3);
         InferenceStep varStep = new VarStepDefault(new TypeAbstraction(variable2), variable2, varConclusion,
-                varConstraint);
+                varConstraint, 1);
 
         Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, ABS, tree.getFirstTypeVariable());
         Constraint absConstraint = new Constraint(tree.getFirstTypeVariable(), new FunctionType(variable2, variable3));
-        InferenceStep expectedStep = new AbsStepDefault(varStep, conclusion, absConstraint);
+        InferenceStep expectedStep = new AbsStepDefault(varStep, conclusion, absConstraint, 0);
 
         assertEquals(expectedStep, tree.getFirstInferenceStep());
 
@@ -113,7 +113,7 @@ class TreeTest {
         Tree tree = new Tree(TYPE_ASSUMPTIONS, CONST);
         Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, CONST, tree.getFirstTypeVariable());
         Constraint constraint = new Constraint(NamedType.INT, tree.getFirstTypeVariable());
-        InferenceStep expectedStep = new ConstStepDefault(conclusion, constraint);
+        InferenceStep expectedStep = new ConstStepDefault(conclusion, constraint, 0);
         assertEquals(expectedStep, tree.getFirstInferenceStep());
         assertEquals(Collections.singletonList(constraint), tree.getConstraints());
     }
@@ -123,7 +123,7 @@ class TreeTest {
         Tree tree = new Tree(TYPE_ASSUMPTIONS, VAR);
         Conclusion conclusion = new Conclusion(TYPE_ASSUMPTIONS, VAR, tree.getFirstTypeVariable());
         Constraint constraint = new Constraint(TYPE, tree.getFirstTypeVariable());
-        InferenceStep expectedStep = new VarStepDefault(TYPE_ABS, TYPE, conclusion, constraint);
+        InferenceStep expectedStep = new VarStepDefault(TYPE_ABS, TYPE, conclusion, constraint, 0);
         assertEquals(expectedStep, tree.getFirstInferenceStep());
         assertEquals(Collections.singletonList(constraint), tree.getConstraints());
     }
@@ -144,8 +144,11 @@ class TreeTest {
         Tree tree = new Tree(typeAssumptions, letTerm);
 
         TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE);
+        StepNumberFactory nrFactory = new StepNumberFactory();
         refFac.nextTypeVariable();
-        TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac);
+        nrFactory.nextStepIndex();
+        TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac, nrFactory);
+        nrFactory.nextStepIndex();
 
 
         Map<VarTerm, TypeAbstraction> varRightTypeAss = new LinkedHashMap<>(typeAssumptions);
@@ -153,11 +156,11 @@ class TreeTest {
         Conclusion varRightConclusion = new Conclusion(varRightTypeAss, f, variable3);
         Constraint varRightConstraint = new Constraint(variable3, generated1);
         InferenceStep varRightStep = new VarStepWithLet(generated1Abs, generated1,
-                varRightConclusion, varRightConstraint);
+                varRightConclusion, varRightConstraint, 2);
 
         Conclusion conclusion = new Conclusion(typeAssumptions, letTerm, tree.getFirstTypeVariable());
         Constraint letConstraint = new Constraint(tree.getFirstTypeVariable(), variable3);
-        InferenceStep expectedStep = new LetStepDefault(conclusion, letConstraint, varRightStep, typeInfererLet);
+        InferenceStep expectedStep = new LetStepDefault(conclusion, letConstraint, varRightStep, typeInfererLet, 0);
 
         assertEquals(expectedStep, tree.getFirstInferenceStep());
 

src/test/java/edu/kit/typicalc/model/TypeInfererLetTest.java

@@ -28,12 +28,12 @@ class TypeInfererLetTest {
 
         TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE);
         refFac.nextTypeVariable();
-        TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac);
+        TypeInfererLet typeInfererLet = new TypeInfererLet(x, typeAssumptions, refFac, new StepNumberFactory());
 
         Conclusion varLeftConclusion = new Conclusion(typeAssumptions, x, variable2);
         Constraint varLeftConstraint = new Constraint(variable2, generated1);
         InferenceStep varLeftStep = new VarStepWithLet(generated1Abs, generated1,
-                varLeftConclusion, varLeftConstraint);
+                varLeftConclusion, varLeftConstraint, 0);
 
         assertEquals(varLeftStep, typeInfererLet.getFirstInferenceStep());
         assertTrue(typeInfererLet.getType().isPresent());

src/test/java/edu/kit/typicalc/model/TypeInfererTest.java

@@ -68,9 +68,14 @@ class TypeInfererTest {
         TypeInferer typeInferer = new TypeInferer(let, givenTypeAssumptions);
 
         TypeVariableFactory refFac = new TypeVariableFactory(TypeVariableKind.TREE);
+        StepNumberFactory nrFactory = new StepNumberFactory();
         refFac.nextTypeVariable();
-        TypeInfererLet expectedTypeInfererLet = new TypeInfererLet(lxlyx, givenTypeAssumptions, refFac);
+        nrFactory.nextStepIndex();
-
+        TypeInfererLet expectedTypeInfererLet = new TypeInfererLet(lxlyx, givenTypeAssumptions, refFac,
+                nrFactory);
+        for (int i = 4; i <= 12; i++) {
+            nrFactory.nextStepIndex();
+        }
         TypeAbstraction resultingAbs = new TypeAbstraction(new FunctionType(a3, new FunctionType(a5, a3)),
                 new HashSet<>(Arrays.asList(a3, a5)));
         Map<VarTerm, TypeAbstraction> typeAssumptionsRight = new LinkedHashMap<>(givenTypeAssumptions);
@@ -80,48 +85,49 @@ class TypeInfererTest {
         Conclusion varStepKLeftConc = new Conclusion(typeAssumptionsRight, k, a10);
         Constraint varStepKLeftConst = new Constraint(a10, varStepKLeftInst);
         InferenceStep varStepKLeft = new VarStepWithLet(resultingAbs, varStepKLeftInst,
-                varStepKLeftConc, varStepKLeftConst);
+                varStepKLeftConc, varStepKLeftConst, 6);
 
         Conclusion varStepAConc = new Conclusion(typeAssumptionsRight, a, a11);
         Constraint varStepAConst = new Constraint(a11, intT);
-        InferenceStep varStepA = new VarStepWithLet(intAbs, intT, varStepAConc, varStepAConst);
+        InferenceStep varStepA = new VarStepWithLet(intAbs, intT, varStepAConc, varStepAConst, 7);
 
         Conclusion appStepKAConc = new Conclusion(typeAssumptionsRight, ka, a8);
         Constraint appStepKAConst = new Constraint(a10, new FunctionType(a11, a8));
-        InferenceStep appStepKA = new AppStepDefault(varStepKLeft, varStepA, appStepKAConc, appStepKAConst);
+        InferenceStep appStepKA = new AppStepDefault(varStepKLeft, varStepA, appStepKAConc, appStepKAConst, 5);
 
         Type varStepKRightInst = new FunctionType(a18, new FunctionType(a19, a18));
         Conclusion varStepKRightConc = new Conclusion(typeAssumptionsRight, k, a16);
         Constraint varStepKRightConst = new Constraint(a16, varStepKRightInst);
         InferenceStep varStepKRight = new VarStepWithLet(resultingAbs, varStepKRightInst,
-                varStepKRightConc, varStepKRightConst);
+                varStepKRightConc, varStepKRightConst, 10);
 
         Conclusion varStepBConc = new Conclusion(typeAssumptionsRight, b, a17);
         Constraint varStepBConst = new Constraint(a17, boolT);
-        InferenceStep varStepB = new VarStepWithLet(boolAbs, boolT, varStepBConc, varStepBConst);
+        InferenceStep varStepB = new VarStepWithLet(boolAbs, boolT, varStepBConc, varStepBConst, 11);
 
         Conclusion appStepKBConc = new Conclusion(typeAssumptionsRight, kb, a14);
         Constraint appStepKBConst = new Constraint(a16, new FunctionType(a17, a14));
-        InferenceStep appStepKB = new AppStepDefault(varStepKRight, varStepB, appStepKBConc, appStepKBConst);
+        InferenceStep appStepKB = new AppStepDefault(varStepKRight, varStepB, appStepKBConc, appStepKBConst, 9);
 
         Conclusion varStepCConc = new Conclusion(typeAssumptionsRight, c, a15);
         Constraint varStepCConst = new Constraint(a15, charT);
-        InferenceStep varStepC = new VarStepWithLet(charAbs, charT, varStepCConc, varStepCConst);
+        InferenceStep varStepC = new VarStepWithLet(charAbs, charT, varStepCConc, varStepCConst, 12);
 
         Conclusion appStepKBCConc = new Conclusion(typeAssumptionsRight, kbc, a9);
         Constraint appStepKBCConst = new Constraint(a14, new FunctionType(a15, a9));
-        InferenceStep appStepKBC = new AppStepDefault(appStepKB, varStepC, appStepKBCConc, appStepKBCConst);
+        InferenceStep appStepKBC = new AppStepDefault(appStepKB, varStepC, appStepKBCConc, appStepKBCConst, 8);
 
         Conclusion appStepKAKBCConc = new Conclusion(typeAssumptionsRight, kakbc, a7);
         Constraint appStepKAKBCConst = new Constraint(a8, new FunctionType(a9, a7));
-        InferenceStep appStepKAKBC = new AppStepDefault(appStepKA, appStepKBC, appStepKAKBCConc, appStepKAKBCConst);
+        InferenceStep appStepKAKBC = new AppStepDefault(appStepKA, appStepKBC, appStepKAKBCConc, appStepKAKBCConst, 4);
 
         Conclusion letConc = new Conclusion(givenTypeAssumptions, let, a1);
         Constraint letConst = new Constraint(a1, a7);
         InferenceStep expectedFirstInferenceStep
-                = new LetStepDefault(letConc, letConst, appStepKAKBC, expectedTypeInfererLet);
+                = new LetStepDefault(letConc, letConst, appStepKAKBC, expectedTypeInfererLet, 0);
 
-        assertEquals(expectedFirstInferenceStep, typeInferer.getFirstInferenceStep());
+        InferenceStep actual = typeInferer.getFirstInferenceStep();
+        assertEquals(expectedFirstInferenceStep, actual);
 
         List<Constraint> expectedConstraints = new ArrayList<>();
         expectedConstraints.add(letConst);

src/test/java/edu/kit/typicalc/model/step/AbsStepDefaultTest.java

@@ -33,25 +33,23 @@ class AbsStepDefaultTest {
         NamedType type1 = new NamedType("a");
         NamedType type2 = new NamedType("b");
         constraint = new Constraint(type1, type2);
-        premise = new ConstStepDefault(conclusion, constraint);
+        premise = new ConstStepDefault(conclusion, constraint, 0);
     }
     @Test
     void equalsTest() {
-        AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint);
+        AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint, 0);
-        AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint);
+        AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint, 0);
-        AbsStepDefault step3 = new AbsStepDefault(premise, conclusion, null);
 
         assertEquals(step1, step1);
         assertEquals(step1, step2);
         assertNotEquals(new EmptyStep(), step1);
         assertNotEquals(null, step1);
-        assertNotEquals(step1, step3);
 
     }
     @Test
     void hashCodeTest() {
-        AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint);
+        AbsStepDefault step1 = new AbsStepDefault(premise, conclusion, constraint, 0);
-        AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint);
+        AbsStepDefault step2 = new AbsStepDefault(premise, conclusion, constraint, 0);
 
         assertEquals(step1.hashCode(), step2.hashCode());
     }
@@ -59,7 +57,7 @@ class AbsStepDefaultTest {
     @Test
     void acceptTest() {
         TestStepVisitor testStepVisitor = new TestStepVisitor();
-        AbsStepDefault step = new AbsStepDefault(premise, conclusion, constraint);
+        AbsStepDefault step = new AbsStepDefault(premise, conclusion, constraint, 0);
         step.accept(testStepVisitor);
         assertEquals("AbsDef", testStepVisitor.visited);
     }

src/test/java/edu/kit/typicalc/model/step/AbsStepWithLetTest.java

@@ -33,26 +33,24 @@ class AbsStepWithLetTest {
         NamedType type1 = new NamedType("a");
         NamedType type2 = new NamedType("b");
         constraint = new Constraint(type1, type2);
-        premise = new ConstStepDefault(conclusion, constraint);
+        premise = new ConstStepDefault(conclusion, constraint, 0);
     }
 
     @Test
     void equalsTest() {
-        AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint);
+        AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint, 0);
-        AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint);
+        AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint, 0);
-        AbsStepWithLet step3 = new AbsStepWithLet(premise, conclusion, null);
 
         assertEquals(step1, step1);
         assertEquals(step1, step2);
         assertNotEquals(new EmptyStep(), step1);
         assertNotEquals(null, step1);
-        assertNotEquals(step1, step3);
 
     }
     @Test
     void hashCodeTest() {
-        AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint);
+        AbsStepWithLet step1 = new AbsStepWithLet(premise, conclusion, constraint, 0);
-        AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint);
+        AbsStepWithLet step2 = new AbsStepWithLet(premise, conclusion, constraint, 0);
 
         assertEquals(step1.hashCode(), step2.hashCode());
     }
@@ -60,7 +58,7 @@ class AbsStepWithLetTest {
     @Test
     void acceptTest() {
         TestStepVisitor testStepVisitor = new TestStepVisitor();
-        AbsStepWithLet step = new AbsStepWithLet(premise, conclusion, constraint);
+        AbsStepWithLet step = new AbsStepWithLet(premise, conclusion, constraint, 0);
         step.accept(testStepVisitor);
         assertEquals("AbsLet", testStepVisitor.visited);
     }

src/test/java/edu/kit/typicalc/model/step/AppStepDefaultTest.java

@@ -35,32 +35,26 @@ class AppStepDefaultTest {
         NamedType type1 = new NamedType("a");
         NamedType type2 = new NamedType("b");
         constraint = new Constraint(type1, type2);
-        premise1 = new ConstStepDefault(conclusion, constraint);
+        premise1 = new ConstStepDefault(conclusion, constraint, 0);
-        premise2 = new ConstStepDefault(conclusion, constraint);
+        premise2 = new ConstStepDefault(conclusion, constraint, 0);
     }
 
     @Test
     void equalsTest() {
-        AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint);
+        AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0);
-        AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint);
+        AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0);
-        AppStepDefault step3 = new AppStepDefault(premise1, premise2, conclusion, null);
-        AppStepDefault step4 = new AppStepDefault(premise1, null, conclusion, constraint);
-        AppStepDefault step5 = new AppStepDefault(null, premise2, conclusion, constraint);
 
         assertEquals(step1, step1);
         assertEquals(step1, step2);
         assertNotEquals(new EmptyStep(), step1);
         assertNotEquals(null, step1);
-        assertNotEquals(step1, step3);
-        assertNotEquals(step1, step4);
-        assertNotEquals(step1, step5);
 
     }
 
     @Test
     void hashCodeTest() {
-        AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint);
+        AppStepDefault step1 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0);
-        AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint);
+        AppStepDefault step2 = new AppStepDefault(premise1, premise2, conclusion, constraint, 0);
 
         assertEquals(step1.hashCode(), step2.hashCode());
     }
@@ -68,7 +62,7 @@ class AppStepDefaultTest {
     @Test
     void acceptTest() {
         TestStepVisitor testStepVisitor = new TestStepVisitor();
-        AppStepDefault step = new AppStepDefault(premise1, premise2, conclusion, constraint);
+        AppStepDefault step = new AppStepDefault(premise1, premise2, conclusion, constraint, 0);
         step.accept(testStepVisitor);
         assertEquals("AppDef", testStepVisitor.visited);
     }

src/test/java/edu/kit/typicalc/model/step/ConstStepDefaultTest.java

@@ -37,21 +37,19 @@ class ConstStepDefaultTest {
 
     @Test
     void equalsTest() {
-        ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint);
+        ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint, 0);
-        ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint);
+        ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint, 0);
-        ConstStepDefault step3 = new ConstStepDefault(conclusion, null);
 
         assertEquals(step1, step1);
         assertEquals(step1, step2);
         assertNotEquals(step1, new EmptyStep());
-        assertNotEquals(step1, step3);
 
     }
 
     @Test
     void hashCodeTest() {
-        ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint);
+        ConstStepDefault step1 = new ConstStepDefault(conclusion, constraint, 0);
-        ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint);
+        ConstStepDefault step2 = new ConstStepDefault(conclusion, constraint, 0);
 
         assertEquals(step1.hashCode(), step2.hashCode());
     }
@@ -59,7 +57,7 @@ class ConstStepDefaultTest {
     @Test
     void acceptTest() {
         TestStepVisitor testStepVisitor = new TestStepVisitor();
-        ConstStepDefault step = new ConstStepDefault(conclusion, constraint);
+        ConstStepDefault step = new ConstStepDefault(conclusion, constraint, 0);
         step.accept(testStepVisitor);
         assertEquals("ConstDef", testStepVisitor.visited);
     }

src/test/java/edu/kit/typicalc/model/step/LetStepDefaultTest.java

@@ -2,6 +2,7 @@ package edu.kit.typicalc.model.step;
 
 import edu.kit.typicalc.model.Conclusion;
 import edu.kit.typicalc.model.Constraint;
+import edu.kit.typicalc.model.StepNumberFactory;
 import edu.kit.typicalc.model.term.IntegerTerm;
 import edu.kit.typicalc.model.term.VarTerm;
 import edu.kit.typicalc.model.type.NamedType;
@@ -34,30 +35,23 @@ class LetStepDefaultTest {
         NamedType type1 = new NamedType("a");
         NamedType type2 = new NamedType("b");
         constraint = new Constraint(type1, type2);
-        premise = new ConstStepDefault(conclusion, constraint);
+        premise = new ConstStepDefault(conclusion, constraint, 0);
-        typeInferer = new TestTypeInfererLet(integerTerm, map, new TestTypeVariableFactory());
+        typeInferer = new TestTypeInfererLet(integerTerm, map, new TestTypeVariableFactory(), new StepNumberFactory());
     }
     @Test
     void equalsTest() {
-        LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer);
+        LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0);
-        LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer);
+        LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0);
-        LetStepDefault step3 = new LetStepDefault(conclusion, null, premise, typeInferer);
-        LetStepDefault step4 = new LetStepDefault(conclusion, constraint, null, typeInferer);
-        LetStepDefault step5 = new LetStepDefault(conclusion, constraint, premise, null);
 
         assertEquals(step1, step1);
         assertEquals(step1, step2);
         assertNotEquals(new EmptyStep(), step1);
-        assertNotEquals(null, step1);
-        assertNotEquals(step1, step3);
-        assertNotEquals(step1, step4);
-        assertNotEquals(step1, step5);
 
     }
     @Test
     void hashCodeTest() {
-        LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer);
+        LetStepDefault step1 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0);
-        LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer);
+        LetStepDefault step2 = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0);
 
         assertEquals(step1.hashCode(), step2.hashCode());
     }
@@ -65,7 +59,7 @@ class LetStepDefaultTest {
     @Test
     void acceptTest() {
         TestStepVisitor testStepVisitor = new TestStepVisitor();
-        LetStepDefault step = new LetStepDefault(conclusion, constraint, premise, typeInferer);
+        LetStepDefault step = new LetStepDefault(conclusion, constraint, premise, typeInferer, 0);
         step.accept(testStepVisitor);
         assertEquals("LetDef", testStepVisitor.visited);
     }

src/test/java/edu/kit/typicalc/model/step/StepFactoryDefaultTest.java

@@ -34,13 +34,13 @@ class StepFactoryDefaultTest {
         NamedType type1 = new NamedType("a");
         NamedType type2 = new NamedType("b");
         constraint = new Constraint(type1, type2);
-        premise = new ConstStepDefault(conclusion, constraint);
+        premise = new ConstStepDefault(conclusion, constraint, 0);
     }
 
     @Test
     void createAbsStepTest() {
         StepFactoryDefault factory = new StepFactoryDefault();
-        AbsStepDefault step = factory.createAbsStep(premise, conclusion, constraint);
+        AbsStepDefault step = factory.createAbsStep(premise, conclusion, constraint, 0);
         assertEquals(premise, step.getPremise());
         assertEquals(conclusion, step.getConclusion());
         assertEquals(constraint, step.getConstraint());
@@ -49,7 +49,7 @@ class StepFactoryDefaultTest {
     @Test
     void createAppStepTest() {
         StepFactoryDefault factory = new StepFactoryDefault();
-        AppStepDefault step = factory.createAppStep(premise, premise,  conclusion, constraint);
+        AppStepDefault step = factory.createAppStep(premise, premise,  conclusion, constraint, 0);
         assertEquals(premise, step.getPremise1());
         assertEquals(premise, step.getPremise2());
         assertEquals(conclusion, step.getConclusion());
@@ -59,7 +59,7 @@ class StepFactoryDefaultTest {
     @Test
     void createConstStepTest() {
         StepFactoryDefault factory = new StepFactoryDefault();
-        ConstStepDefault step = factory.createConstStep(conclusion, constraint);
+        ConstStepDefault step = factory.createConstStep(conclusion, constraint, 0);
         assertEquals(conclusion, step.getConclusion());
         assertEquals(constraint, step.getConstraint());
     }
@@ -67,23 +67,11 @@ class StepFactoryDefaultTest {
     @Test
     void createVarStepTest() {
         StepFactoryDefault factory = new StepFactoryDefault();
-        VarStepDefault step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint);
+        VarStepDefault step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint, 0);
         assertEquals(typeAbstraction, step.getTypeAbsInPremise());
         assertEquals(namedType, step.getInstantiatedTypeAbs());
         assertEquals(conclusion, step.getConclusion());
         assertEquals(constraint, step.getConstraint());
     }
 
-    @Test
-    void createLetStepTest() {
-        StepFactoryDefault factory = new StepFactoryDefault();
-        boolean thrown = false;
-        try {
-            LetStep step = factory.createLetStep(conclusion, constraint, premise, null);
-        } catch (UnsupportedOperationException e) {
-            thrown = true;
-        }
-        assertTrue(thrown);
-    }
-
 }

src/test/java/edu/kit/typicalc/model/step/StepFactoryWithLetTest.java

@@ -35,13 +35,13 @@ class StepFactoryWithLetTest {
         NamedType type1 = new NamedType("a");
         NamedType type2 = new NamedType("b");
         constraint = new Constraint(type1, type2);
-        premise = new ConstStepDefault(conclusion, constraint);
+        premise = new ConstStepDefault(conclusion, constraint, 0);
     }
 
     @Test
     void createAbsStepTest() {
         StepFactoryWithLet factory = new StepFactoryWithLet();
-        AbsStepWithLet step = factory.createAbsStep(premise, conclusion, constraint);
+        AbsStepWithLet step = factory.createAbsStep(premise, conclusion, constraint, 0);
         assertEquals(premise, step.getPremise());
         assertEquals(conclusion, step.getConclusion());
         assertEquals(constraint, step.getConstraint());
@@ -50,7 +50,7 @@ class StepFactoryWithLetTest {
     @Test
     void createAppStepTest() {
         StepFactoryWithLet factory = new StepFactoryWithLet();
-        AppStepDefault step = factory.createAppStep(premise, premise, conclusion, constraint);
+        AppStepDefault step = factory.createAppStep(premise, premise, conclusion, constraint, 0);
         assertEquals(premise, step.getPremise1());
         assertEquals(premise, step.getPremise2());
         assertEquals(conclusion, step.getConclusion());
@@ -60,7 +60,7 @@ class StepFactoryWithLetTest {
     @Test
     void createConstStepTest() {
         StepFactoryWithLet factory = new StepFactoryWithLet();
-        ConstStepDefault step = factory.createConstStep(conclusion, constraint);
+        ConstStepDefault step = factory.createConstStep(conclusion, constraint, 0);
         assertEquals(conclusion, step.getConclusion());
         assertEquals(constraint, step.getConstraint());
     }
@@ -68,20 +68,10 @@ class StepFactoryWithLetTest {
     @Test
     void createVarStepTest() {
         StepFactoryWithLet factory = new StepFactoryWithLet();
-        VarStepWithLet step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint);
+        VarStepWithLet step = factory.createVarStep(typeAbstraction, namedType, conclusion, constraint, 0);
         assertEquals(typeAbstraction, step.getTypeAbsInPremise());
         assertEquals(namedType, step.getInstantiatedTypeAbs());
         assertEquals(conclusion, step.getConclusion());
         assertEquals(constraint, step.getConstraint());
     }
-
-    @Test
-    void createLetStepTest() {
-        StepFactoryWithLet factory = new StepFactoryWithLet();
-        LetStep step = factory.createLetStep(conclusion, constraint, premise, null);
-        assertEquals(premise, step.getPremise());
-        assertNull(step.getTypeInferer());
-        assertEquals(conclusion, step.getConclusion());
-        assertEquals(constraint, step.getConstraint());
-    }
 }

src/test/java/edu/kit/typicalc/model/step/TestTypeInfererLet.java

@@ -1,5 +1,6 @@
 package edu.kit.typicalc.model.step;
 
+import edu.kit.typicalc.model.StepNumberFactory;
 import edu.kit.typicalc.model.TypeInfererLet;
 import edu.kit.typicalc.model.TypeVariableFactory;
 import edu.kit.typicalc.model.term.LambdaTerm;
@@ -9,7 +10,8 @@ import edu.kit.typicalc.model.type.TypeAbstraction;
 import java.util.Map;
 
 public class TestTypeInfererLet extends TypeInfererLet {
-    public TestTypeInfererLet(LambdaTerm term, Map<VarTerm, TypeAbstraction> map, TypeVariableFactory factory) {
+    public TestTypeInfererLet(LambdaTerm term, Map<VarTerm, TypeAbstraction> map, TypeVariableFactory factory,
-        super(term, map, factory);
+                              StepNumberFactory factory2) {
+        super(term, map, factory, factory2);
     }
 }

src/test/java/edu/kit/typicalc/model/step/VarStepDefaultTest.java

@@ -16,7 +16,6 @@ import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertNotEquals;
 
 class VarStepDefaultTest {
-    static InferenceStep premise = null;
     static Conclusion conclusion = null;
     static Constraint constraint = null;
     static NamedType namedType = null;
@@ -38,26 +37,20 @@ class VarStepDefaultTest {
 
     @Test
     void equalsTest() {
-        VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint);
+        VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0);
-        VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint);
+        VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0);
-        VarStepDefault step3 = new VarStepDefault(typeAbstraction, namedType, conclusion, null);
-        VarStepDefault step4 = new VarStepDefault(null, namedType, conclusion, constraint);
-        VarStepDefault step5 = new VarStepDefault(typeAbstraction, null, conclusion, constraint);
 
         assertEquals(step1, step1);
         assertEquals(step1, step2);
         assertNotEquals(new EmptyStep(), step1);
         assertNotEquals(null, step1);
-        assertNotEquals(step1, step3);
-        assertNotEquals(step1, step4);
-        assertNotEquals(step1, step5);
 
     }
 
     @Test
     void hashCodeTest() {
-        VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint);
+        VarStepDefault step1 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0);
-        VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint);
+        VarStepDefault step2 = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0);
 
         assertEquals(step1.hashCode(), step2.hashCode());
     }
@@ -65,7 +58,7 @@ class VarStepDefaultTest {
     @Test
     void acceptTest() {
         TestStepVisitor testStepVisitor = new TestStepVisitor();
-        VarStepDefault step = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint);
+        VarStepDefault step = new VarStepDefault(typeAbstraction, namedType, conclusion, constraint, 0);
         step.accept(testStepVisitor);
         assertEquals("VarDef", testStepVisitor.visited);
     }

src/test/java/edu/kit/typicalc/model/step/VarStepWithLetTest.java

@@ -16,7 +16,6 @@ import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertNotEquals;
 
 class VarStepWithLetTest {
-    static InferenceStep premise = null;
     static Conclusion conclusion = null;
     static Constraint constraint = null;
     static NamedType namedType = null;
@@ -34,35 +33,11 @@ class VarStepWithLetTest {
         NamedType type2 = new NamedType("b");
         constraint = new Constraint(type1, type2);
     }
-    @Test
-    void equalsTest() {
-        VarStepWithLet step1 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint);
-        VarStepWithLet step2 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint);
-        VarStepWithLet step3 = new VarStepWithLet(typeAbstraction, namedType, conclusion, null);
-        VarStepWithLet step4 = new VarStepWithLet(null, namedType, conclusion, constraint);
-        VarStepWithLet step5 = new VarStepWithLet(typeAbstraction, null, conclusion, constraint);
-
-        assertEquals(step1, step1);
-        assertEquals(step1, step2);
-        assertNotEquals(new EmptyStep(), step1);
-        assertNotEquals(null, step1);
-        assertNotEquals(step1, step3);
-        assertNotEquals(step1, step4);
-        assertNotEquals(step1, step5);
-
-    }
-    @Test
-    void hashCodeTest() {
-        VarStepWithLet step1 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint);
-        VarStepWithLet step2 = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint);
-
-        assertEquals(step1.hashCode(), step2.hashCode());
-    }
 
     @Test
     void acceptTest() {
         TestStepVisitor testStepVisitor = new TestStepVisitor();
-        VarStepWithLet step = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint);
+        VarStepWithLet step = new VarStepWithLet(typeAbstraction, namedType, conclusion, constraint, 0);
         step.accept(testStepVisitor);
         assertEquals("VarLet", testStepVisitor.visited);
     }