42 files changed, 2210 insertions, 0 deletions

diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/.gitignore
new file mode 100644
index 00000000..49df59a2
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/.gitignore
@@ -0,0 +1,8 @@
+/.CftTransformation.java._trace
+/.ComponentFaultTreeTrace.java._trace
+/.ComponentInstanceTrace.java._trace
+/.InputTrace.java._trace
+/.MappingHandler.java._trace
+/.ComponentInstantiationHandler.java._trace
+/.MappingQueries.java._trace
+/.LookupHandler.java._trace
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.Cft2FtTransformation.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.Cft2FtTransformation.xtendbin
new file mode 100644
index 00000000..dfae40e9
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.Cft2FtTransformation.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventCollection.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventCollection.xtendbin
new file mode 100644
index 00000000..0aaf712d
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventCollection.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventMaterializer.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventMaterializer.xtendbin
new file mode 100644
index 00000000..e51f73a6
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.EventMaterializer.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.FaultTreeBuilder.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.FaultTreeBuilder.xtendbin
new file mode 100644
index 00000000..89e003dc
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.FaultTreeBuilder.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.gitignore
new file mode 100644
index 00000000..058cff19
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/.gitignore
@@ -0,0 +1,16 @@
+/.Cft2FtTransformation.java._trace
+/.EventMaterializer.java._trace
+/.MaterializedEvent.java._trace
+/.CollectedInputs.java._trace
+/.MaterializedEventCollection.java._trace
+/.FaultTreeBuilder.java._trace
+/.FaultModelBuilder.java._trace
+/.EventCollection.java._trace
+/.Cft2FtTransformation.xtendbin
+/.EventCollection.xtendbin
+/.EventMaterializer.xtendbin
+/.FaultTreeBuilder.xtendbin
+/Cft2FtTransformation.java
+/EventCollection.java
+/EventMaterializer.java
+/FaultTreeBuilder.java
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.java
new file mode 100644
index 00000000..e87b8865
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.java
@@ -0,0 +1,49 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft;
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentFaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantModel;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Event;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FtFactory;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.RandomEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ReliabilityModel;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft.EventMaterializer;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft.FaultTreeBuilder;
+import org.eclipse.xtext.xbase.lib.ObjectExtensions;
+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
+
+@SuppressWarnings("all")
+public class Cft2FtTransformation {
+  public ReliabilityModel createFaultTree(final ComponentFaultTree componentFaultTree) {
+    ReliabilityModel _xblockexpression = null;
+    {
+      final EventMaterializer materializer = new EventMaterializer();
+      final Event topEvent = materializer.getOrMaterialize(componentFaultTree.getTopEvent());
+      ReliabilityModel _switchResult = null;
+      boolean _matched = false;
+      if (topEvent instanceof ConstantEvent) {
+        _matched=true;
+        ConstantModel _createConstantModel = FtFactory.eINSTANCE.createConstantModel();
+        final Procedure1<ConstantModel> _function = (ConstantModel it) -> {
+          it.setFailed(((ConstantEvent)topEvent).isFailed());
+        };
+        _switchResult = ObjectExtensions.<ConstantModel>operator_doubleArrow(_createConstantModel, _function);
+      }
+      if (!_matched) {
+        if (topEvent instanceof RandomEvent) {
+          _matched=true;
+          FaultTree _xblockexpression_1 = null;
+          {
+            final FaultTreeBuilder builder = new FaultTreeBuilder();
+            builder.addTopLevel(((RandomEvent)topEvent));
+            _xblockexpression_1 = builder.getFaultTree();
+          }
+          _switchResult = _xblockexpression_1;
+        }
+      }
+      _xblockexpression = _switchResult;
+    }
+    return _xblockexpression;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventCollection.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventCollection.java
new file mode 100644
index 00000000..dceef9f8
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventCollection.java
@@ -0,0 +1,188 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft;
+
+import com.google.common.collect.ImmutableSet;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Event;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.RandomEvent;
+import java.util.Set;
+import org.eclipse.xtend.lib.annotations.Data;
+import org.eclipse.xtext.xbase.lib.IterableExtensions;
+import org.eclipse.xtext.xbase.lib.Pure;
+import org.eclipse.xtext.xbase.lib.util.ToStringBuilder;
+
+@Data
+@SuppressWarnings("all")
+public class EventCollection {
+  public static class Builder {
+    private int falseEventCount = 0;
+    
+    private int trueEventCount = 0;
+    
+    private final ImmutableSet.Builder<RandomEvent> randomEventsBuilder = ImmutableSet.<RandomEvent>builder();
+    
+    private Builder() {
+    }
+    
+    public EventCollection.Builder add(final Event event) {
+      EventCollection.Builder _xblockexpression = null;
+      {
+        boolean _matched = false;
+        if (event instanceof ConstantEvent) {
+          _matched=true;
+          boolean _isFailed = ((ConstantEvent)event).isFailed();
+          if (_isFailed) {
+            this.trueEventCount++;
+          } else {
+            this.falseEventCount++;
+          }
+        }
+        if (!_matched) {
+          if (event instanceof RandomEvent) {
+            _matched=true;
+            this.randomEventsBuilder.add(((RandomEvent)event));
+          }
+        }
+        if (!_matched) {
+          throw new IllegalArgumentException(("Unknown event: " + event));
+        }
+        _xblockexpression = this;
+      }
+      return _xblockexpression;
+    }
+    
+    public EventCollection.Builder addAll(final EventCollection materializedEvens) {
+      EventCollection.Builder _xblockexpression = null;
+      {
+        int _falseEventCount = this.falseEventCount;
+        this.falseEventCount = (_falseEventCount + materializedEvens.falseEventCount);
+        int _trueEventCount = this.trueEventCount;
+        this.trueEventCount = (_trueEventCount + materializedEvens.trueEventCount);
+        this.randomEventsBuilder.addAll(materializedEvens.randomEvents);
+        _xblockexpression = this;
+      }
+      return _xblockexpression;
+    }
+    
+    public EventCollection build() {
+      ImmutableSet<RandomEvent> _build = this.randomEventsBuilder.build();
+      return new EventCollection(this.falseEventCount, this.trueEventCount, _build);
+    }
+  }
+  
+  private final int falseEventCount;
+  
+  private final int trueEventCount;
+  
+  private final Set<RandomEvent> randomEvents;
+  
+  public boolean containsFalseEvent() {
+    return (this.falseEventCount >= 1);
+  }
+  
+  public boolean containsTrueEvent() {
+    return (this.trueEventCount >= 1);
+  }
+  
+  public int getVariableEventCount() {
+    return this.randomEvents.size();
+  }
+  
+  public boolean containsRandomEvent() {
+    int _variableEventCount = this.getVariableEventCount();
+    return (_variableEventCount >= 1);
+  }
+  
+  public int getCount() {
+    int _variableEventCount = this.getVariableEventCount();
+    return ((this.falseEventCount + this.trueEventCount) + _variableEventCount);
+  }
+  
+  public boolean isEmpty() {
+    return (((!this.containsFalseEvent()) && (!this.containsTrueEvent())) && (!this.containsRandomEvent()));
+  }
+  
+  public boolean containsExactlyOneRandomEvent() {
+    return (((!this.containsFalseEvent()) && (!this.containsTrueEvent())) && (this.getVariableEventCount() == 1));
+  }
+  
+  public RandomEvent toSingleRandomEvent() {
+    RandomEvent _xblockexpression = null;
+    {
+      boolean _containsExactlyOneRandomEvent = this.containsExactlyOneRandomEvent();
+      boolean _not = (!_containsExactlyOneRandomEvent);
+      if (_not) {
+        throw new IllegalStateException("Input collection is not a single random event");
+      }
+      _xblockexpression = IterableExtensions.<RandomEvent>head(this.randomEvents);
+    }
+    return _xblockexpression;
+  }
+  
+  public static EventCollection.Builder builder() {
+    return new EventCollection.Builder();
+  }
+  
+  public EventCollection(final int falseEventCount, final int trueEventCount, final Set<RandomEvent> randomEvents) {
+    super();
+    this.falseEventCount = falseEventCount;
+    this.trueEventCount = trueEventCount;
+    this.randomEvents = randomEvents;
+  }
+  
+  @Override
+  @Pure
+  public int hashCode() {
+    final int prime = 31;
+    int result = 1;
+    result = prime * result + this.falseEventCount;
+    result = prime * result + this.trueEventCount;
+    return prime * result + ((this.randomEvents== null) ? 0 : this.randomEvents.hashCode());
+  }
+  
+  @Override
+  @Pure
+  public boolean equals(final Object obj) {
+    if (this == obj)
+      return true;
+    if (obj == null)
+      return false;
+    if (getClass() != obj.getClass())
+      return false;
+    EventCollection other = (EventCollection) obj;
+    if (other.falseEventCount != this.falseEventCount)
+      return false;
+    if (other.trueEventCount != this.trueEventCount)
+      return false;
+    if (this.randomEvents == null) {
+      if (other.randomEvents != null)
+        return false;
+    } else if (!this.randomEvents.equals(other.randomEvents))
+      return false;
+    return true;
+  }
+  
+  @Override
+  @Pure
+  public String toString() {
+    ToStringBuilder b = new ToStringBuilder(this);
+    b.add("falseEventCount", this.falseEventCount);
+    b.add("trueEventCount", this.trueEventCount);
+    b.add("randomEvents", this.randomEvents);
+    return b.toString();
+  }
+  
+  @Pure
+  public int getFalseEventCount() {
+    return this.falseEventCount;
+  }
+  
+  @Pure
+  public int getTrueEventCount() {
+    return this.trueEventCount;
+  }
+  
+  @Pure
+  public Set<RandomEvent> getRandomEvents() {
+    return this.randomEvents;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventMaterializer.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventMaterializer.java
new file mode 100644
index 00000000..98a82b7d
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventMaterializer.java
@@ -0,0 +1,469 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft;
+
+import com.google.common.base.Objects;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.AndGateDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.BasicEventDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Component;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Connection;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.EventDeclaration;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.GateDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Input;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.InputEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.KOfMGateDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.OrGateDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Output;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.AndGate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.BasicEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Distribution;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Event;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FtFactory;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Gate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.KOfMGate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.OrGate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.RandomEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.util.CftExtensions;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft.EventCollection;
+import java.util.LinkedHashSet;
+import java.util.Map;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.util.EcoreUtil;
+import org.eclipse.xtend.lib.annotations.Data;
+import org.eclipse.xtend2.lib.StringConcatenation;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.Extension;
+import org.eclipse.xtext.xbase.lib.Functions.Function1;
+import org.eclipse.xtext.xbase.lib.IterableExtensions;
+import org.eclipse.xtext.xbase.lib.ObjectExtensions;
+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
+import org.eclipse.xtext.xbase.lib.Pure;
+
+@SuppressWarnings("all")
+public class EventMaterializer {
+  @Data
+  protected static class EventKey<T extends EventDeclaration> {
+    private final Component component;
+    
+    private final T event;
+    
+    @Override
+    public String toString() {
+      StringConcatenation _builder = new StringConcatenation();
+      String _name = this.component.getName();
+      _builder.append(_name);
+      _builder.append("_");
+      String _name_1 = this.event.getName();
+      _builder.append(_name_1);
+      return _builder.toString();
+    }
+    
+    public EventKey(final Component component, final T event) {
+      super();
+      this.component = component;
+      this.event = event;
+    }
+    
+    @Override
+    @Pure
+    public int hashCode() {
+      final int prime = 31;
+      int result = 1;
+      result = prime * result + ((this.component== null) ? 0 : this.component.hashCode());
+      return prime * result + ((this.event== null) ? 0 : this.event.hashCode());
+    }
+    
+    @Override
+    @Pure
+    public boolean equals(final Object obj) {
+      if (this == obj)
+        return true;
+      if (obj == null)
+        return false;
+      if (getClass() != obj.getClass())
+        return false;
+      EventMaterializer.EventKey<?> other = (EventMaterializer.EventKey<?>) obj;
+      if (this.component == null) {
+        if (other.component != null)
+          return false;
+      } else if (!this.component.equals(other.component))
+        return false;
+      if (this.event == null) {
+        if (other.event != null)
+          return false;
+      } else if (!this.event.equals(other.event))
+        return false;
+      return true;
+    }
+    
+    @Pure
+    public Component getComponent() {
+      return this.component;
+    }
+    
+    @Pure
+    public T getEvent() {
+      return this.event;
+    }
+  }
+  
+  @Extension
+  private final FtFactory _ftFactory = FtFactory.eINSTANCE;
+  
+  private final Map<EventMaterializer.EventKey<EventDeclaration>, Event> materializationCache = CollectionLiterals.<EventMaterializer.EventKey<EventDeclaration>, Event>newHashMap();
+  
+  private final Map<EventMaterializer.EventKey<InputEvent>, EventCollection> multipleInputCache = CollectionLiterals.<EventMaterializer.EventKey<InputEvent>, EventCollection>newHashMap();
+  
+  private final ConstantEvent falseEvent;
+  
+  private final ConstantEvent trueEvent;
+  
+  private final LinkedHashSet<EventMaterializer.EventKey<? extends EventDeclaration>> path = new LinkedHashSet<EventMaterializer.EventKey<? extends EventDeclaration>>();
+  
+  public EventMaterializer() {
+    ConstantEvent _createConstantEvent = this._ftFactory.createConstantEvent();
+    final Procedure1<ConstantEvent> _function = (ConstantEvent it) -> {
+      it.setFailed(false);
+    };
+    ConstantEvent _doubleArrow = ObjectExtensions.<ConstantEvent>operator_doubleArrow(_createConstantEvent, _function);
+    this.falseEvent = _doubleArrow;
+    ConstantEvent _createConstantEvent_1 = this._ftFactory.createConstantEvent();
+    final Procedure1<ConstantEvent> _function_1 = (ConstantEvent it) -> {
+      it.setFailed(true);
+    };
+    ConstantEvent _doubleArrow_1 = ObjectExtensions.<ConstantEvent>operator_doubleArrow(_createConstantEvent_1, _function_1);
+    this.trueEvent = _doubleArrow_1;
+  }
+  
+  public Event getOrMaterialize(final Output output) {
+    return this.getOrMaterialize(output.getComponent(), output.getEventDeclaration());
+  }
+  
+  public Event getOrMaterialize(final Component component, final EventDeclaration eventDeclaration) {
+    Event _xblockexpression = null;
+    {
+      final EventMaterializer.EventKey<EventDeclaration> eventKey = new EventMaterializer.EventKey<EventDeclaration>(component, eventDeclaration);
+      this.pushEventKey(eventKey);
+      Event _xtrycatchfinallyexpression = null;
+      try {
+        Event _xblockexpression_1 = null;
+        {
+          Event event = this.materializationCache.get(eventKey);
+          if ((event == null)) {
+            event = this.materialize(component, eventDeclaration);
+            this.materializationCache.put(eventKey, event);
+          }
+          _xblockexpression_1 = event;
+        }
+        _xtrycatchfinallyexpression = _xblockexpression_1;
+      } finally {
+        this.popEventKey(eventKey);
+      }
+      _xblockexpression = _xtrycatchfinallyexpression;
+    }
+    return _xblockexpression;
+  }
+  
+  protected Event materialize(final Component component, final EventDeclaration eventDeclaration) {
+    RandomEvent _xblockexpression = null;
+    {
+      String _name = component.getName();
+      String _plus = (_name + "_");
+      String _name_1 = eventDeclaration.getName();
+      final String eventName = (_plus + _name_1);
+      RandomEvent _switchResult = null;
+      boolean _matched = false;
+      if (eventDeclaration instanceof InputEvent) {
+        _matched=true;
+        return this.materializeConnectedEvent(component, ((InputEvent)eventDeclaration));
+      }
+      if (!_matched) {
+        if (eventDeclaration instanceof BasicEventDefinition) {
+          _matched=true;
+          BasicEvent _xblockexpression_1 = null;
+          {
+            final BasicEvent basicEvent = this._ftFactory.createBasicEvent();
+            basicEvent.setDistribution(EcoreUtil.<Distribution>copy(((BasicEventDefinition)eventDeclaration).getDistribution()));
+            _xblockexpression_1 = basicEvent;
+          }
+          _switchResult = _xblockexpression_1;
+        }
+      }
+      if (!_matched) {
+        if (eventDeclaration instanceof GateDefinition) {
+          _matched=true;
+          Gate _xblockexpression_1 = null;
+          {
+            final EventCollection inputs = this.collectInputs(component, ((GateDefinition)eventDeclaration));
+            Gate _switchResult_1 = null;
+            boolean _matched_1 = false;
+            if (eventDeclaration instanceof AndGateDefinition) {
+              _matched_1=true;
+              AndGate _xifexpression = null;
+              boolean _containsFalseEvent = inputs.containsFalseEvent();
+              if (_containsFalseEvent) {
+                return this.falseEvent;
+              } else {
+                AndGate _xifexpression_1 = null;
+                boolean _isEmpty = inputs.isEmpty();
+                if (_isEmpty) {
+                  return this.trueEvent;
+                } else {
+                  AndGate _xifexpression_2 = null;
+                  boolean _containsExactlyOneRandomEvent = inputs.containsExactlyOneRandomEvent();
+                  if (_containsExactlyOneRandomEvent) {
+                    return inputs.toSingleRandomEvent();
+                  } else {
+                    _xifexpression_2 = this._ftFactory.createAndGate();
+                  }
+                  _xifexpression_1 = _xifexpression_2;
+                }
+                _xifexpression = _xifexpression_1;
+              }
+              _switchResult_1 = _xifexpression;
+            }
+            if (!_matched_1) {
+              if (eventDeclaration instanceof OrGateDefinition) {
+                _matched_1=true;
+                OrGate _xifexpression = null;
+                boolean _containsTrueEvent = inputs.containsTrueEvent();
+                if (_containsTrueEvent) {
+                  return this.trueEvent;
+                } else {
+                  OrGate _xifexpression_1 = null;
+                  boolean _isEmpty = inputs.isEmpty();
+                  if (_isEmpty) {
+                    return this.falseEvent;
+                  } else {
+                    OrGate _xifexpression_2 = null;
+                    boolean _containsExactlyOneRandomEvent = inputs.containsExactlyOneRandomEvent();
+                    if (_containsExactlyOneRandomEvent) {
+                      return inputs.toSingleRandomEvent();
+                    } else {
+                      _xifexpression_2 = this._ftFactory.createOrGate();
+                    }
+                    _xifexpression_1 = _xifexpression_2;
+                  }
+                  _xifexpression = _xifexpression_1;
+                }
+                _switchResult_1 = _xifexpression;
+              }
+            }
+            if (!_matched_1) {
+              if (eventDeclaration instanceof KOfMGateDefinition) {
+                _matched_1=true;
+                Gate _xblockexpression_2 = null;
+                {
+                  int _count = inputs.getCount();
+                  int _k = ((KOfMGateDefinition)eventDeclaration).getK();
+                  int _multiply = (_count * _k);
+                  int _m = ((KOfMGateDefinition)eventDeclaration).getM();
+                  final int requiredTrueInputs = (_multiply / _m);
+                  int _trueEventCount = inputs.getTrueEventCount();
+                  final int k = (requiredTrueInputs - _trueEventCount);
+                  final int m = inputs.getVariableEventCount();
+                  Gate _xifexpression = null;
+                  if ((k == 0)) {
+                    return this.trueEvent;
+                  } else {
+                    Gate _xifexpression_1 = null;
+                    if ((k > m)) {
+                      return this.falseEvent;
+                    } else {
+                      Gate _xifexpression_2 = null;
+                      boolean _containsExactlyOneRandomEvent = inputs.containsExactlyOneRandomEvent();
+                      if (_containsExactlyOneRandomEvent) {
+                        return inputs.toSingleRandomEvent();
+                      } else {
+                        Gate _xifexpression_3 = null;
+                        if ((k == 1)) {
+                          _xifexpression_3 = this._ftFactory.createOrGate();
+                        } else {
+                          Gate _xifexpression_4 = null;
+                          if ((k == m)) {
+                            _xifexpression_4 = this._ftFactory.createAndGate();
+                          } else {
+                            KOfMGate _xblockexpression_3 = null;
+                            {
+                              final KOfMGate kOfMGate = this._ftFactory.createKOfMGate();
+                              kOfMGate.setK(k);
+                              _xblockexpression_3 = kOfMGate;
+                            }
+                            _xifexpression_4 = _xblockexpression_3;
+                          }
+                          _xifexpression_3 = _xifexpression_4;
+                        }
+                        _xifexpression_2 = _xifexpression_3;
+                      }
+                      _xifexpression_1 = _xifexpression_2;
+                    }
+                    _xifexpression = _xifexpression_1;
+                  }
+                  _xblockexpression_2 = _xifexpression;
+                }
+                _switchResult_1 = _xblockexpression_2;
+              }
+            }
+            if (!_matched_1) {
+              throw new IllegalArgumentException(("Unknown gate definition: " + eventDeclaration));
+            }
+            final Gate gate = _switchResult_1;
+            gate.getInputEvents().addAll(inputs.getRandomEvents());
+            _xblockexpression_1 = gate;
+          }
+          _switchResult = _xblockexpression_1;
+        }
+      }
+      if (!_matched) {
+        throw new IllegalArgumentException(("Unknown event declaration: " + eventDeclaration));
+      }
+      final RandomEvent event = _switchResult;
+      event.setName(eventName);
+      _xblockexpression = event;
+    }
+    return _xblockexpression;
+  }
+  
+  protected Event materializeConnectedEvent(final Component component, final InputEvent inputEvent) {
+    Event _xblockexpression = null;
+    {
+      boolean _isMultiple = inputEvent.isMultiple();
+      if (_isMultiple) {
+        StringConcatenation _builder = new StringConcatenation();
+        _builder.append("Cannot materialize multiple nput ");
+        String _name = component.getName();
+        _builder.append(_name);
+        _builder.append("_");
+        String _name_1 = inputEvent.getName();
+        _builder.append(_name_1);
+        throw new IllegalArgumentException(_builder.toString());
+      }
+      final Input input = this.findInput(component, inputEvent);
+      final EList<Connection> incomingConnections = input.getIncomingConnections();
+      int _size = incomingConnections.size();
+      boolean _notEquals = (_size != 1);
+      if (_notEquals) {
+        StringConcatenation _builder_1 = new StringConcatenation();
+        _builder_1.append("Input ");
+        String _name_2 = component.getName();
+        _builder_1.append(_name_2);
+        _builder_1.append("_");
+        String _name_3 = inputEvent.getName();
+        _builder_1.append(_name_3);
+        _builder_1.append(" has ");
+        int _size_1 = incomingConnections.size();
+        _builder_1.append(_size_1);
+        _builder_1.append(" connections instead of 1");
+        throw new IllegalArgumentException(_builder_1.toString());
+      }
+      final Output output = IterableExtensions.<Connection>head(incomingConnections).getOutput();
+      _xblockexpression = this.getOrMaterialize(output.getComponent(), output.getEventDeclaration());
+    }
+    return _xblockexpression;
+  }
+  
+  protected EventCollection collectInputs(final Component component, final GateDefinition gateDefinition) {
+    EventCollection _xblockexpression = null;
+    {
+      final EventCollection.Builder builder = EventCollection.builder();
+      EList<EventDeclaration> _inputEvents = gateDefinition.getInputEvents();
+      for (final EventDeclaration inputEventDeclaration : _inputEvents) {
+        boolean _matched = false;
+        if (inputEventDeclaration instanceof InputEvent) {
+          boolean _isMultiple = ((InputEvent)inputEventDeclaration).isMultiple();
+          if (_isMultiple) {
+            _matched=true;
+            final EventCollection materializedEvents = this.getOrMaterializeConnectedEvents(component, ((InputEvent)inputEventDeclaration));
+            builder.addAll(materializedEvents);
+          }
+        }
+        if (!_matched) {
+          builder.add(this.getOrMaterialize(component, inputEventDeclaration));
+        }
+      }
+      _xblockexpression = builder.build();
+    }
+    return _xblockexpression;
+  }
+  
+  protected EventCollection getOrMaterializeConnectedEvents(final Component component, final InputEvent inputEvent) {
+    EventCollection _xblockexpression = null;
+    {
+      final EventMaterializer.EventKey<InputEvent> inputKey = new EventMaterializer.EventKey<InputEvent>(component, inputEvent);
+      this.pushEventKey(inputKey);
+      EventCollection _xtrycatchfinallyexpression = null;
+      try {
+        EventCollection _xblockexpression_1 = null;
+        {
+          EventCollection eventCollection = this.multipleInputCache.get(inputKey);
+          if ((eventCollection == null)) {
+            eventCollection = this.materializeConnectedEvents(component, inputEvent);
+            this.multipleInputCache.put(inputKey, eventCollection);
+          }
+          _xblockexpression_1 = eventCollection;
+        }
+        _xtrycatchfinallyexpression = _xblockexpression_1;
+      } finally {
+        this.popEventKey(inputKey);
+      }
+      _xblockexpression = _xtrycatchfinallyexpression;
+    }
+    return _xblockexpression;
+  }
+  
+  protected EventCollection materializeConnectedEvents(final Component component, final InputEvent inputEvent) {
+    EventCollection _xblockexpression = null;
+    {
+      final Input input = this.findInput(component, inputEvent);
+      final EventCollection.Builder builder = EventCollection.builder();
+      EList<Connection> _incomingConnections = input.getIncomingConnections();
+      for (final Connection connection : _incomingConnections) {
+        boolean _isCurrentlyConnected = CftExtensions.isCurrentlyConnected(connection);
+        if (_isCurrentlyConnected) {
+          final Event materializedEvent = this.getOrMaterialize(connection.getOutput());
+          builder.add(materializedEvent);
+        }
+      }
+      _xblockexpression = builder.build();
+    }
+    return _xblockexpression;
+  }
+  
+  protected Input findInput(final Component component, final InputEvent inputEvent) {
+    final Function1<Input, Boolean> _function = (Input it) -> {
+      InputEvent _inputEvent = it.getInputEvent();
+      return Boolean.valueOf(Objects.equal(_inputEvent, inputEvent));
+    };
+    final Input input = IterableExtensions.<Input>findFirst(component.getInputs(), _function);
+    if ((input == null)) {
+      StringConcatenation _builder = new StringConcatenation();
+      _builder.append("No input ");
+      _builder.append(inputEvent);
+      _builder.append(" in component ");
+      _builder.append(component);
+      throw new IllegalArgumentException(_builder.toString());
+    }
+    return input;
+  }
+  
+  private void pushEventKey(final EventMaterializer.EventKey<? extends EventDeclaration> eventKey) {
+    boolean _add = this.path.add(eventKey);
+    boolean _not = (!_add);
+    if (_not) {
+      StringConcatenation _builder = new StringConcatenation();
+      _builder.append("Circular dependency [");
+      {
+        for(final EventMaterializer.EventKey<? extends EventDeclaration> ancestor : this.path) {
+          _builder.append(ancestor);
+          _builder.append(", ");
+        }
+      }
+      _builder.append(eventKey);
+      _builder.append("] detected");
+      throw new IllegalStateException(_builder.toString());
+    }
+  }
+  
+  private boolean popEventKey(final EventMaterializer.EventKey<? extends EventDeclaration> eventKey) {
+    return this.path.remove(eventKey);
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/FaultTreeBuilder.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/FaultTreeBuilder.java
new file mode 100644
index 00000000..9b2dfd76
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/FaultTreeBuilder.java
@@ -0,0 +1,57 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft;
+
+import com.google.common.base.Objects;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FtFactory;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Gate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.RandomEvent;
+import java.util.Collection;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.xtend.lib.annotations.Accessors;
+import org.eclipse.xtext.xbase.lib.Pure;
+
+@SuppressWarnings("all")
+public class FaultTreeBuilder {
+  @Accessors
+  private final FaultTree faultTree = FtFactory.eINSTANCE.createFaultTree();
+  
+  public void addTopLevel(final RandomEvent event) {
+    RandomEvent _topEvent = this.faultTree.getTopEvent();
+    boolean _tripleNotEquals = (_topEvent != null);
+    if (_tripleNotEquals) {
+      throw new IllegalStateException("Top event was already set");
+    }
+    this.add(event);
+    this.faultTree.setTopEvent(event);
+  }
+  
+  protected void add(final RandomEvent event) {
+    EObject _eContainer = this.faultTree.eContainer();
+    boolean _equals = Objects.equal(_eContainer, this.faultTree);
+    if (_equals) {
+      return;
+    }
+    EObject _eContainer_1 = this.faultTree.eContainer();
+    boolean _tripleNotEquals = (_eContainer_1 != null);
+    if (_tripleNotEquals) {
+      throw new IllegalStateException("Event is already in a different fault tree");
+    }
+    EList<RandomEvent> _events = this.faultTree.getEvents();
+    _events.add(event);
+    if ((event instanceof Gate)) {
+      this.addAll(((Gate)event).getInputEvents());
+    }
+  }
+  
+  protected void addAll(final Collection<RandomEvent> events) {
+    for (final RandomEvent event : events) {
+      this.add(event);
+    }
+  }
+  
+  @Pure
+  public FaultTree getFaultTree() {
+    return this.faultTree;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentFaultTreeTrace.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentFaultTreeTrace.xtendbin
new file mode 100644
index 00000000..028440a8
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentFaultTreeTrace.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentInstanceTrace.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentInstanceTrace.xtendbin
new file mode 100644
index 00000000..d542ba2d
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentInstanceTrace.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentNameGenerator.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentNameGenerator.xtendbin
new file mode 100644
index 00000000..949da0cd
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.ComponentNameGenerator.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.Ecore2CftTransformation.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.Ecore2CftTransformation.xtendbin
new file mode 100644
index 00000000..82c045e2
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.Ecore2CftTransformation.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.InputTrace.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.InputTrace.xtendbin
new file mode 100644
index 00000000..ffd70c04
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.InputTrace.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.LookupHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.LookupHandler.xtendbin
new file mode 100644
index 00000000..418c71d4
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.LookupHandler.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingHandler.xtendbin
new file mode 100644
index 00000000..86c0d704
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingHandler.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingQueries.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingQueries.xtendbin
new file mode 100644
index 00000000..c9dda5c4
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.MappingQueries.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.gitignore
new file mode 100644
index 00000000..377aa872
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/.gitignore
@@ -0,0 +1,25 @@
+/.ComponentFaultTreeTrace.java._trace
+/.ComponentInstanceTrace.java._trace
+/.InputTrace.java._trace
+/.LookupHandler.java._trace
+/.MappingHandler.java._trace
+/.MappingQueries.java._trace
+/.CftTransformation.java._trace
+/.Ecore2CftTransformation.java._trace
+/.ComponentNameGenerator.java._trace
+/.ComponentFaultTreeTrace.xtendbin
+/.ComponentInstanceTrace.xtendbin
+/.ComponentNameGenerator.xtendbin
+/.Ecore2CftTransformation.xtendbin
+/.InputTrace.xtendbin
+/.LookupHandler.xtendbin
+/.MappingHandler.xtendbin
+/.MappingQueries.xtendbin
+/ComponentFaultTreeTrace.java
+/ComponentInstanceTrace.java
+/ComponentNameGenerator.java
+/Ecore2CftTransformation.java
+/InputTrace.java
+/LookupHandler.java
+/MappingHandler.java
+/MappingQueries.java
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentFaultTreeTrace.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentFaultTreeTrace.java
new file mode 100644
index 00000000..ddcf9036
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentFaultTreeTrace.java
@@ -0,0 +1,77 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.CftFactory;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentFaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Modality;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Output;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentInstanceTrace;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentNameGenerator;
+import java.util.Map;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.viatra.query.runtime.api.IPatternMatch;
+import org.eclipse.xtend.lib.annotations.Accessors;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.IterableExtensions;
+import org.eclipse.xtext.xbase.lib.Pure;
+
+@SuppressWarnings("all")
+public class ComponentFaultTreeTrace {
+  @Accessors
+  private final ComponentFaultTree componentFaultTree = CftFactory.eINSTANCE.createComponentFaultTree();
+  
+  private final ComponentNameGenerator nameGenerator = new ComponentNameGenerator();
+  
+  private final Map<IPatternMatch, ComponentInstanceTrace> componentInstancesMap = CollectionLiterals.<IPatternMatch, ComponentInstanceTrace>newHashMap();
+  
+  public ComponentInstanceTrace instantiateComponent(final IPatternMatch patternMatch, final ComponentDefinition componenDefinition) {
+    return this.instantiateComponent(patternMatch, componenDefinition, Modality.MUST, false);
+  }
+  
+  public ComponentInstanceTrace instantiateComponent(final IPatternMatch patternMatch, final ComponentDefinition componenDefinition, final Modality exists, final boolean allowMultiple) {
+    ComponentInstanceTrace _xblockexpression = null;
+    {
+      boolean _containsKey = this.componentInstancesMap.containsKey(patternMatch);
+      if (_containsKey) {
+        throw new IllegalArgumentException(("Already instantiated component for match: " + patternMatch));
+      }
+      final ComponentInstanceTrace componentTrace = new ComponentInstanceTrace(this.componentFaultTree, componenDefinition, this.nameGenerator, exists, allowMultiple);
+      this.componentInstancesMap.put(patternMatch, componentTrace);
+      _xblockexpression = componentTrace;
+    }
+    return _xblockexpression;
+  }
+  
+  public void setTopLevel(final ComponentInstanceTrace trace) {
+    Output _topEvent = this.componentFaultTree.getTopEvent();
+    boolean _tripleNotEquals = (_topEvent != null);
+    if (_tripleNotEquals) {
+      throw new IllegalArgumentException("Top level component already set");
+    }
+    final EList<Output> outputs = trace.getOutputs();
+    int _size = outputs.size();
+    boolean _tripleNotEquals_1 = (_size != 1);
+    if (_tripleNotEquals_1) {
+      int _size_1 = outputs.size();
+      String _plus = ("Top level component must have 1 output, got " + Integer.valueOf(_size_1));
+      String _plus_1 = (_plus + 
+        " instead");
+      throw new IllegalArgumentException(_plus_1);
+    }
+    boolean _appearsExactlyOnce = trace.appearsExactlyOnce();
+    boolean _not = (!_appearsExactlyOnce);
+    if (_not) {
+      throw new IllegalArgumentException("Top level must appear in the fault tree exactly once");
+    }
+    this.componentFaultTree.setTopEvent(IterableExtensions.<Output>head(outputs));
+  }
+  
+  public ComponentInstanceTrace lookup(final IPatternMatch patternMatch) {
+    return this.componentInstancesMap.get(patternMatch);
+  }
+  
+  @Pure
+  public ComponentFaultTree getComponentFaultTree() {
+    return this.componentFaultTree;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentInstanceTrace.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentInstanceTrace.java
new file mode 100644
index 00000000..4034bdf3
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentInstanceTrace.java
@@ -0,0 +1,77 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import com.google.common.collect.Maps;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.CftFactory;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Component;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentFaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.EventDeclaration;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.InputEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Modality;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Output;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.util.CftExtensions;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentNameGenerator;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.InputTrace;
+import java.util.Map;
+import org.eclipse.emf.common.util.EList;
+
+@SuppressWarnings("all")
+public class ComponentInstanceTrace {
+  private final Component componentInstance = CftFactory.eINSTANCE.createComponent();
+  
+  private final Map<InputEvent, InputTrace> inputEventsMap;
+  
+  private final Map<EventDeclaration, Output> outputEventsMap;
+  
+  protected ComponentInstanceTrace(final ComponentFaultTree faultTree, final ComponentDefinition componentDefinition, final ComponentNameGenerator nameGenerator, final Modality exists, final boolean multipleAllowed) {
+    this.componentInstance.setComponentDefinition(componentDefinition);
+    this.componentInstance.setName(nameGenerator.nextName(componentDefinition));
+    this.componentInstance.setExists(exists);
+    this.componentInstance.setMultipleAllowed(multipleAllowed);
+    this.inputEventsMap = Maps.<InputEvent, InputTrace>newHashMapWithExpectedSize(componentDefinition.getInputEvents().size());
+    EList<InputEvent> _inputEvents = componentDefinition.getInputEvents();
+    for (final InputEvent inputEvent : _inputEvents) {
+      {
+        final InputTrace inputTrace = new InputTrace(this.componentInstance, inputEvent);
+        this.inputEventsMap.put(inputEvent, inputTrace);
+      }
+    }
+    this.outputEventsMap = Maps.<EventDeclaration, Output>newHashMapWithExpectedSize(componentDefinition.getOutputEvents().size());
+    EList<EventDeclaration> _outputEvents = componentDefinition.getOutputEvents();
+    for (final EventDeclaration outputEvent : _outputEvents) {
+      {
+        final Output output = CftFactory.eINSTANCE.createOutput();
+        output.setEventDeclaration(outputEvent);
+        EList<Output> _outputs = this.componentInstance.getOutputs();
+        _outputs.add(output);
+        this.outputEventsMap.put(outputEvent, output);
+      }
+    }
+    EList<Component> _components = faultTree.getComponents();
+    _components.add(this.componentInstance);
+  }
+  
+  public void assign(final EventDeclaration inputEvent, final ComponentInstanceTrace sourceComponent, final EventDeclaration outputEvent) {
+    this.assign(inputEvent, sourceComponent, outputEvent, Modality.MUST);
+  }
+  
+  public void assign(final EventDeclaration inputEvent, final ComponentInstanceTrace sourceComponent, final EventDeclaration outputEvent, final Modality exists) {
+    final InputTrace inputTrace = this.inputEventsMap.get(inputEvent);
+    if ((inputTrace == null)) {
+      throw new IllegalArgumentException(("Unknown input: " + inputEvent));
+    }
+    final Output output = sourceComponent.outputEventsMap.get(outputEvent);
+    if ((output == null)) {
+      throw new IllegalArgumentException(("Unknown output: " + outputEvent));
+    }
+    inputTrace.assign(output, exists);
+  }
+  
+  protected EList<Output> getOutputs() {
+    return this.componentInstance.getOutputs();
+  }
+  
+  protected boolean appearsExactlyOnce() {
+    return CftExtensions.appearsExactlyOnce(this.componentInstance);
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentNameGenerator.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentNameGenerator.java
new file mode 100644
index 00000000..e7dca003
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentNameGenerator.java
@@ -0,0 +1,29 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentDefinition;
+import java.util.Map;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+
+@SuppressWarnings("all")
+public class ComponentNameGenerator {
+  private static final String DEFAULT_NAME = "__unnamed";
+  
+  private final Map<ComponentDefinition, Integer> instanceCounts = CollectionLiterals.<ComponentDefinition, Integer>newHashMap();
+  
+  public String nextName(final ComponentDefinition componentDefinition) {
+    String _xblockexpression = null;
+    {
+      final Integer instanceCount = this.instanceCounts.getOrDefault(componentDefinition, Integer.valueOf(0));
+      this.instanceCounts.put(componentDefinition, Integer.valueOf(((instanceCount).intValue() + 1)));
+      String _elvis = null;
+      String _name = componentDefinition.getName();
+      if (_name != null) {
+        _elvis = _name;
+      } else {
+        _elvis = ComponentNameGenerator.DEFAULT_NAME;
+      }
+      _xblockexpression = (_elvis + instanceCount);
+    }
+    return _xblockexpression;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.java
new file mode 100644
index 00000000..a63c8e78
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.java
@@ -0,0 +1,41 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import com.google.common.collect.ImmutableList;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.TransformationDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentFaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentFaultTreeTrace;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.MappingHandler;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.MappingQueries;
+import java.util.List;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
+import org.eclipse.xtext.xbase.lib.Functions.Function1;
+import org.eclipse.xtext.xbase.lib.ListExtensions;
+
+@SuppressWarnings("all")
+public class Ecore2CftTransformation {
+  private final List<MappingHandler> mappingHandlers;
+  
+  public Ecore2CftTransformation(final TransformationDefinition transformationDefinition, final ViatraQueryEngine viatraQueryEngine) {
+    final MappingQueries mappingQueries = new MappingQueries(transformationDefinition, viatraQueryEngine);
+    final Function1<MappingDefinition, MappingHandler> _function = (MappingDefinition mappingDefinition) -> {
+      return new MappingHandler(mappingDefinition, mappingQueries);
+    };
+    this.mappingHandlers = ImmutableList.<MappingHandler>copyOf(ListExtensions.<MappingDefinition, MappingHandler>map(transformationDefinition.getMappingDefinitions(), _function));
+  }
+  
+  public ComponentFaultTree createComponentFaultTree() {
+    ComponentFaultTree _xblockexpression = null;
+    {
+      final ComponentFaultTreeTrace trace = new ComponentFaultTreeTrace();
+      for (final MappingHandler handler : this.mappingHandlers) {
+        handler.instantiateComponents(trace);
+      }
+      for (final MappingHandler handler_1 : this.mappingHandlers) {
+        handler_1.instantiateConnections(trace);
+      }
+      _xblockexpression = trace.getComponentFaultTree();
+    }
+    return _xblockexpression;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/InputTrace.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/InputTrace.java
new file mode 100644
index 00000000..2b30566f
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/InputTrace.java
@@ -0,0 +1,43 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.CftFactory;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Component;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Connection;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Input;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.InputEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Modality;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Output;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.util.CftExtensions;
+import java.util.Map;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+
+@SuppressWarnings("all")
+public class InputTrace {
+  private final Input input = CftFactory.eINSTANCE.createInput();
+  
+  private final Map<Output, Connection> connectionsMap = CollectionLiterals.<Output, Connection>newHashMap();
+  
+  protected InputTrace(final Component component, final InputEvent inputEvent) {
+    this.input.setInputEvent(inputEvent);
+    EList<Input> _inputs = component.getInputs();
+    _inputs.add(this.input);
+  }
+  
+  public void assign(final Output output, final Modality exists) {
+    final Connection connection = this.connectionsMap.get(output);
+    if ((connection == null)) {
+      final Connection newConnection = CftFactory.eINSTANCE.createConnection();
+      newConnection.setOutput(output);
+      newConnection.setExists(exists);
+      EList<Connection> _incomingConnections = this.input.getIncomingConnections();
+      _incomingConnections.add(newConnection);
+      this.connectionsMap.put(output, newConnection);
+    } else {
+      boolean _isMoreConcreteThan = CftExtensions.isMoreConcreteThan(exists, connection.getExists());
+      if (_isMoreConcreteThan) {
+        connection.setExists(exists);
+      }
+    }
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/LookupHandler.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/LookupHandler.java
new file mode 100644
index 00000000..e155aac8
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/LookupHandler.java
@@ -0,0 +1,84 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import com.google.common.base.Objects;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.LookupDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingParameter;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentFaultTreeTrace;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentInstanceTrace;
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.viatra.query.patternlanguage.emf.vql.Pattern;
+import org.eclipse.viatra.query.runtime.api.IPatternMatch;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
+import org.eclipse.xtext.xbase.lib.Conversions;
+
+@SuppressWarnings("all")
+public class LookupHandler {
+  private final int[] argumentIndices;
+  
+  private final ViatraQueryMatcher<? extends IPatternMatch> lookedUpMatcher;
+  
+  public LookupHandler(final MappingDefinition mappingDefinition, final LookupDefinition lookupDefinition, final ViatraQueryMatcher<? extends IPatternMatch> lookedUpMatcher) {
+    EObject _eContainer = lookupDefinition.eContainer();
+    boolean _notEquals = (!Objects.equal(_eContainer, mappingDefinition));
+    if (_notEquals) {
+      throw new IllegalArgumentException("lookupDefinition must be contained in mappingDefinition");
+    }
+    final int argumentCount = lookupDefinition.getArguments().size();
+    int _length = ((Object[])Conversions.unwrapArray(lookedUpMatcher.getParameterNames(), Object.class)).length;
+    boolean _notEquals_1 = (argumentCount != _length);
+    if (_notEquals_1) {
+      MappingDefinition _mapping = lookupDefinition.getMapping();
+      Pattern _pattern = null;
+      if (_mapping!=null) {
+        _pattern=_mapping.getPattern();
+      }
+      String _name = null;
+      if (_pattern!=null) {
+        _name=_pattern.getName();
+      }
+      String _plus = ("lookupDefinition (name: " + _name);
+      String _plus_1 = (_plus + 
+        ") must have as many arguments as lookedUpMatcher (name: ");
+      String _patternName = lookedUpMatcher.getPatternName();
+      String _plus_2 = (_plus_1 + _patternName);
+      String _plus_3 = (_plus_2 + ")");
+      throw new IllegalArgumentException(_plus_3);
+    }
+    this.argumentIndices = new int[argumentCount];
+    for (int i = 0; (i < argumentCount); i++) {
+      {
+        final MappingParameter argument = lookupDefinition.getArguments().get(i);
+        final int argumentIndex = mappingDefinition.getParameters().indexOf(argument);
+        this.argumentIndices[i] = argumentIndex;
+      }
+    }
+    this.lookedUpMatcher = lookedUpMatcher;
+  }
+  
+  public ComponentInstanceTrace lookupForMatch(final ComponentFaultTreeTrace faultTreeTrace, final IPatternMatch match) {
+    ComponentInstanceTrace _xblockexpression = null;
+    {
+      final IPatternMatch lookedUpMatch = this.createLookedUpMatch(match);
+      _xblockexpression = faultTreeTrace.lookup(lookedUpMatch);
+    }
+    return _xblockexpression;
+  }
+  
+  private IPatternMatch createLookedUpMatch(final IPatternMatch match) {
+    IPatternMatch _xblockexpression = null;
+    {
+      final IPatternMatch lookedUpMatch = this.lookedUpMatcher.newEmptyMatch();
+      final int argumentCount = this.argumentIndices.length;
+      for (int i = 0; (i < argumentCount); i++) {
+        {
+          final int argumentIndex = this.argumentIndices[i];
+          Object argumentValue = match.get(argumentIndex);
+          lookedUpMatch.set(i, argumentValue);
+        }
+      }
+      _xblockexpression = lookedUpMatch;
+    }
+    return _xblockexpression;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingHandler.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingHandler.java
new file mode 100644
index 00000000..41703289
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingHandler.java
@@ -0,0 +1,146 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import com.google.common.collect.ImmutableMap;
+import com.google.common.collect.Iterables;
+import com.google.common.collect.Maps;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.Assignment;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.ComponentInstance;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.EventReference;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.LookupDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.Variable;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentFaultTreeTrace;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.ComponentInstanceTrace;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.LookupHandler;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.MappingQueries;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.Map;
+import java.util.Set;
+import java.util.function.Consumer;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.viatra.query.runtime.api.IPatternMatch;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.Functions.Function1;
+import org.eclipse.xtext.xbase.lib.IterableExtensions;
+
+@SuppressWarnings("all")
+public class MappingHandler {
+  private final ViatraQueryMatcher<? extends IPatternMatch> matcher;
+  
+  private final MappingDefinition mappingDefinition;
+  
+  private final Map<LookupDefinition, LookupHandler> lookupHandlers;
+  
+  public MappingHandler(final MappingDefinition mappingDefinition, final MappingQueries mappingQueries) {
+    this.matcher = mappingQueries.getMatcher(mappingDefinition);
+    this.mappingDefinition = mappingDefinition;
+    final HashSet<Variable> variables = CollectionLiterals.<Variable>newHashSet();
+    EList<Assignment> _assignments = mappingDefinition.getAssignments();
+    for (final Assignment assignment : _assignments) {
+      {
+        Variable _component = assignment.getInput().getComponent();
+        variables.add(_component);
+        Variable _component_1 = assignment.getOutput().getComponent();
+        variables.add(_component_1);
+      }
+    }
+    final Function1<LookupDefinition, LookupDefinition> _function = (LookupDefinition it) -> {
+      return it;
+    };
+    final Function1<LookupDefinition, LookupHandler> _function_1 = (LookupDefinition lookupDefinition) -> {
+      return mappingQueries.createLookupHandler(mappingDefinition, lookupDefinition);
+    };
+    this.lookupHandlers = ImmutableMap.<LookupDefinition, LookupHandler>copyOf(IterableExtensions.<LookupDefinition, LookupDefinition, LookupHandler>toMap(Iterables.<LookupDefinition>filter(variables, LookupDefinition.class), _function, _function_1));
+  }
+  
+  public void instantiateComponents(final ComponentFaultTreeTrace faultTreeTrace) {
+    boolean _hasComponentInstace = this.hasComponentInstace();
+    boolean _not = (!_hasComponentInstace);
+    if (_not) {
+      return;
+    }
+    final Consumer<IPatternMatch> _function = (IPatternMatch match) -> {
+      final ComponentInstanceTrace componentTrace = faultTreeTrace.instantiateComponent(match, this.getComponentDefinition());
+      boolean _isTopLevel = this.isTopLevel();
+      if (_isTopLevel) {
+        faultTreeTrace.setTopLevel(componentTrace);
+      }
+    };
+    this.matcher.forEachMatch(_function);
+  }
+  
+  public void instantiateConnections(final ComponentFaultTreeTrace faultTreeTrace) {
+    boolean _hasConnections = this.hasConnections();
+    boolean _not = (!_hasConnections);
+    if (_not) {
+      return;
+    }
+    final Consumer<IPatternMatch> _function = (IPatternMatch match) -> {
+      final Map<Variable, ComponentInstanceTrace> lookedUpComponents = this.lookupComponents(faultTreeTrace, match);
+      EList<Assignment> _assignments = this.mappingDefinition.getAssignments();
+      for (final Assignment assignment : _assignments) {
+        {
+          final EventReference input = assignment.getInput();
+          final ComponentInstanceTrace inputComponent = lookedUpComponents.get(input.getComponent());
+          final EventReference output = assignment.getOutput();
+          final ComponentInstanceTrace outputComponent = lookedUpComponents.get(output.getComponent());
+          if (((inputComponent != null) && (outputComponent != null))) {
+            inputComponent.assign(input.getEvent(), outputComponent, output.getEvent());
+          }
+        }
+      }
+    };
+    this.matcher.forEachMatch(_function);
+  }
+  
+  private Map<Variable, ComponentInstanceTrace> lookupComponents(final ComponentFaultTreeTrace faultTreeTrace, final IPatternMatch match) {
+    HashMap<Variable, ComponentInstanceTrace> _xblockexpression = null;
+    {
+      int _size = this.lookupHandlers.size();
+      int _plus = (_size + 1);
+      final HashMap<Variable, ComponentInstanceTrace> lookedUpComponents = Maps.<Variable, ComponentInstanceTrace>newHashMapWithExpectedSize(_plus);
+      boolean _hasComponentInstace = this.hasComponentInstace();
+      if (_hasComponentInstace) {
+        final ComponentInstanceTrace componentInstance = faultTreeTrace.lookup(match);
+        lookedUpComponents.put(this.mappingDefinition.getComponentInstance(), componentInstance);
+      }
+      Set<Map.Entry<LookupDefinition, LookupHandler>> _entrySet = this.lookupHandlers.entrySet();
+      for (final Map.Entry<LookupDefinition, LookupHandler> pair : _entrySet) {
+        {
+          final ComponentInstanceTrace componentInstance_1 = pair.getValue().lookupForMatch(faultTreeTrace, match);
+          if ((componentInstance_1 != null)) {
+            lookedUpComponents.put(pair.getKey(), componentInstance_1);
+          }
+        }
+      }
+      _xblockexpression = lookedUpComponents;
+    }
+    return _xblockexpression;
+  }
+  
+  private ComponentDefinition getComponentDefinition() {
+    ComponentInstance _componentInstance = this.mappingDefinition.getComponentInstance();
+    ComponentDefinition _componentType = null;
+    if (_componentInstance!=null) {
+      _componentType=_componentInstance.getComponentType();
+    }
+    return _componentType;
+  }
+  
+  private boolean hasComponentInstace() {
+    ComponentDefinition _componentDefinition = this.getComponentDefinition();
+    return (_componentDefinition != null);
+  }
+  
+  private boolean isTopLevel() {
+    return this.mappingDefinition.isTopLevel();
+  }
+  
+  private boolean hasConnections() {
+    boolean _isEmpty = this.mappingDefinition.getAssignments().isEmpty();
+    return (!_isEmpty);
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingQueries.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingQueries.java
new file mode 100644
index 00000000..6147807e
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingQueries.java
@@ -0,0 +1,60 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft;
+
+import com.google.common.collect.ImmutableMap;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.LookupDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.TransformationDefinition;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft.LookupHandler;
+import java.util.Map;
+import org.eclipse.viatra.query.patternlanguage.emf.specification.SpecificationBuilder;
+import org.eclipse.viatra.query.runtime.api.GenericQueryGroup;
+import org.eclipse.viatra.query.runtime.api.IPatternMatch;
+import org.eclipse.viatra.query.runtime.api.IQuerySpecification;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine;
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher;
+import org.eclipse.xtext.xbase.lib.Conversions;
+import org.eclipse.xtext.xbase.lib.Functions.Function1;
+import org.eclipse.xtext.xbase.lib.IterableExtensions;
+import org.eclipse.xtext.xbase.lib.MapExtensions;
+
+@SuppressWarnings("all")
+public class MappingQueries {
+  private final Map<MappingDefinition, ViatraQueryMatcher<? extends IPatternMatch>> matchersMap;
+  
+  public MappingQueries(final TransformationDefinition transformationDefinition, final ViatraQueryEngine viatraQueryEngine) {
+    final SpecificationBuilder specificationBuilder = new SpecificationBuilder();
+    final Function1<MappingDefinition, MappingDefinition> _function = (MappingDefinition it) -> {
+      return it;
+    };
+    final Function1<MappingDefinition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> _function_1 = (MappingDefinition it) -> {
+      return specificationBuilder.getOrCreateSpecification(it.getPattern());
+    };
+    final Map<MappingDefinition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>> querySpecificationsMap = IterableExtensions.<MappingDefinition, MappingDefinition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>>toMap(transformationDefinition.getMappingDefinitions(), _function, _function_1);
+    GenericQueryGroup.of(((IQuerySpecification<?>[])Conversions.unwrapArray(querySpecificationsMap.values(), IQuerySpecification.class))).prepare(viatraQueryEngine);
+    final Function1<IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>, ViatraQueryMatcher<? extends IPatternMatch>> _function_2 = (IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>> it) -> {
+      return it.getMatcher(viatraQueryEngine);
+    };
+    this.matchersMap = ImmutableMap.<MappingDefinition, ViatraQueryMatcher<? extends IPatternMatch>>copyOf(MapExtensions.<MappingDefinition, IQuerySpecification<? extends ViatraQueryMatcher<? extends IPatternMatch>>, ViatraQueryMatcher<? extends IPatternMatch>>mapValues(querySpecificationsMap, _function_2));
+  }
+  
+  public ViatraQueryMatcher<? extends IPatternMatch> getMatcher(final MappingDefinition mappingDefinition) {
+    ViatraQueryMatcher<? extends IPatternMatch> _xblockexpression = null;
+    {
+      final ViatraQueryMatcher<? extends IPatternMatch> matcher = this.matchersMap.get(mappingDefinition);
+      if ((matcher == null)) {
+        throw new IllegalArgumentException(("Unknown mapping definition: " + mappingDefinition));
+      }
+      _xblockexpression = matcher;
+    }
+    return _xblockexpression;
+  }
+  
+  public LookupHandler createLookupHandler(final MappingDefinition mappingDefinition, final LookupDefinition lookupDefinition) {
+    LookupHandler _xblockexpression = null;
+    {
+      final ViatraQueryMatcher<? extends IPatternMatch> lookedUpMatcher = this.getMatcher(lookupDefinition.getMapping());
+      _xblockexpression = new LookupHandler(mappingDefinition, lookupDefinition, lookedUpMatcher);
+    }
+    return _xblockexpression;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.Ft2GalileoTransformation.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.Ft2GalileoTransformation.xtendbin
new file mode 100644
index 00000000..0956e6e0
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.Ft2GalileoTransformation.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.gitignore
new file mode 100644
index 00000000..f4610b04
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/.gitignore
@@ -0,0 +1,3 @@
+/.Ft2GalileoTransformation.java._trace
+/.Ft2GalileoTransformation.xtendbin
+/Ft2GalileoTransformation.java
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.java
new file mode 100644
index 00000000..8748825d
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.java
@@ -0,0 +1,188 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo;
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.AndGate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.BasicEvent;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantDistribution;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Distribution;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ExponentialDistribution;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Gate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.KOfMGate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.OrGate;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.RandomEvent;
+import java.util.Arrays;
+import org.eclipse.emf.common.util.EList;
+import org.eclipse.xtend2.lib.StringConcatenation;
+import org.eclipse.xtend2.lib.StringConcatenationClient;
+
+@SuppressWarnings("all")
+public class Ft2GalileoTransformation {
+  public CharSequence toGalileo(final FaultTree faultTree) {
+    StringConcatenation _builder = new StringConcatenation();
+    _builder.append("toplevel \"");
+    String _name = faultTree.getTopEvent().getName();
+    _builder.append(_name);
+    _builder.append("\";");
+    _builder.newLineIfNotEmpty();
+    {
+      EList<RandomEvent> _events = faultTree.getEvents();
+      for(final RandomEvent event : _events) {
+        _builder.append("\"");
+        String _name_1 = event.getName();
+        _builder.append(_name_1);
+        _builder.append("\" ");
+        Object _defineEvent = this.defineEvent(event);
+        _builder.append(_defineEvent);
+        _builder.append(";");
+        _builder.newLineIfNotEmpty();
+      }
+    }
+    return _builder;
+  }
+  
+  protected Object _defineEvent(final BasicEvent basicEvent) {
+    StringConcatenation _builder = new StringConcatenation();
+    StringConcatenationClient _defineDistribution = this.defineDistribution(basicEvent.getDistribution());
+    _builder.append(_defineDistribution);
+    _builder.append(" dorm=0.0");
+    return _builder;
+  }
+  
+  protected StringConcatenationClient _defineDistribution(final ConstantDistribution distribution) {
+    StringConcatenationClient _client = new StringConcatenationClient() {
+      @Override
+      protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) {
+        _builder.append("p=");
+        double _p = distribution.getP();
+        _builder.append(_p);
+      }
+    };
+    return _client;
+  }
+  
+  protected StringConcatenationClient _defineDistribution(final ExponentialDistribution distribution) {
+    StringConcatenationClient _client = new StringConcatenationClient() {
+      @Override
+      protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) {
+        _builder.append("lambda=");
+        double _lambda = distribution.getLambda();
+        _builder.append(_lambda);
+      }
+    };
+    return _client;
+  }
+  
+  protected StringConcatenationClient _defineDistribution(final Distribution distribution) {
+    throw new IllegalArgumentException(("Unknown distribution: " + distribution));
+  }
+  
+  protected StringConcatenationClient _defineEvent(final Gate gate) {
+    StringConcatenationClient _client = new StringConcatenationClient() {
+      @Override
+      protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) {
+        StringConcatenationClient _defineGate = Ft2GalileoTransformation.this.defineGate(gate);
+        _builder.append(_defineGate);
+        _builder.append(" ");
+        {
+          EList<RandomEvent> _inputEvents = gate.getInputEvents();
+          boolean _hasElements = false;
+          for(final RandomEvent input : _inputEvents) {
+            if (!_hasElements) {
+              _hasElements = true;
+            } else {
+              _builder.appendImmediate(" ", "");
+            }
+            _builder.append("\"");
+            String _name = input.getName();
+            _builder.append(_name);
+            _builder.append("\"");
+          }
+        }
+      }
+    };
+    return _client;
+  }
+  
+  protected StringConcatenationClient _defineGate(final AndGate gate) {
+    StringConcatenationClient _client = new StringConcatenationClient() {
+      @Override
+      protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) {
+        _builder.append("and");
+      }
+    };
+    return _client;
+  }
+  
+  protected StringConcatenationClient _defineGate(final OrGate gate) {
+    StringConcatenationClient _client = new StringConcatenationClient() {
+      @Override
+      protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) {
+        _builder.append("or");
+      }
+    };
+    return _client;
+  }
+  
+  protected StringConcatenationClient _defineGate(final KOfMGate gate) {
+    StringConcatenationClient _client = new StringConcatenationClient() {
+      @Override
+      protected void appendTo(StringConcatenationClient.TargetStringConcatenation _builder) {
+        int _k = gate.getK();
+        _builder.append(_k);
+        _builder.append("of");
+        int _size = gate.getInputEvents().size();
+        _builder.append(_size);
+      }
+    };
+    return _client;
+  }
+  
+  protected StringConcatenationClient _defineGate(final Gate gate) {
+    throw new IllegalArgumentException(("Unknown gate: " + gate));
+  }
+  
+  protected StringConcatenationClient _defineEvent(final RandomEvent randomEvent) {
+    throw new IllegalArgumentException(("Unknown random even: " + randomEvent));
+  }
+  
+  protected Object defineEvent(final RandomEvent basicEvent) {
+    if (basicEvent instanceof BasicEvent) {
+      return _defineEvent((BasicEvent)basicEvent);
+    } else if (basicEvent instanceof Gate) {
+      return _defineEvent((Gate)basicEvent);
+    } else if (basicEvent != null) {
+      return _defineEvent(basicEvent);
+    } else {
+      throw new IllegalArgumentException("Unhandled parameter types: " +
+        Arrays.<Object>asList(basicEvent).toString());
+    }
+  }
+  
+  protected StringConcatenationClient defineDistribution(final Distribution distribution) {
+    if (distribution instanceof ConstantDistribution) {
+      return _defineDistribution((ConstantDistribution)distribution);
+    } else if (distribution instanceof ExponentialDistribution) {
+      return _defineDistribution((ExponentialDistribution)distribution);
+    } else if (distribution != null) {
+      return _defineDistribution(distribution);
+    } else {
+      throw new IllegalArgumentException("Unhandled parameter types: " +
+        Arrays.<Object>asList(distribution).toString());
+    }
+  }
+  
+  protected StringConcatenationClient defineGate(final Gate gate) {
+    if (gate instanceof AndGate) {
+      return _defineGate((AndGate)gate);
+    } else if (gate instanceof KOfMGate) {
+      return _defineGate((KOfMGate)gate);
+    } else if (gate instanceof OrGate) {
+      return _defineGate((OrGate)gate);
+    } else if (gate != null) {
+      return _defineGate(gate);
+    } else {
+      throw new IllegalArgumentException("Unhandled parameter types: " +
+        Arrays.<Object>asList(gate).toString());
+    }
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin
new file mode 100644
index 00000000..cdaacb58
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin
new file mode 100644
index 00000000..6e1908aa
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin
new file mode 100644
index 00000000..5772b0e7
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin
new file mode 100644
index 00000000..e1c1a8c7
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore
new file mode 100644
index 00000000..8a74c101
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore
@@ -0,0 +1,20 @@
+/.StormDftSolver.java._trace
+/.StormDftConfiguration.java._trace
+/.StormDftMttfConfiguration.java._trace
+/.FtAnalysisObjective.java._trace
+/.ApproximationHeuristic.java._trace
+/.StormDftHandler.java._trace
+/.StormDftException.java._trace
+/.ReliabilityModelSolution.java._trace
+/.ReliabilityResult.java._trace
+/.ReliabilityResult.xtendbin
+/.StormDftConfiguration.xtendbin
+/.StormDftHandler.xtendbin
+/.StormDftSolver.xtendbin
+/ApproximationHeuristic.java
+/FtAnalysisObjective.java
+/ReliabilityResult.java
+/StormDftConfiguration.java
+/StormDftException.java
+/StormDftHandler.java
+/StormDftSolver.java
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java
new file mode 100644
index 00000000..822d4f36
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java
@@ -0,0 +1,8 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+@SuppressWarnings("all")
+public enum ApproximationHeuristic {
+  NONE,
+  
+  DEPTH;
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java
new file mode 100644
index 00000000..528ada42
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java
@@ -0,0 +1,14 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+@SuppressWarnings("all")
+public abstract class FtAnalysisObjective {
+  public static final class TimeBound extends FtAnalysisObjective {
+    public double timeBound = 0;
+  }
+  
+  public static final FtAnalysisObjective MTTF = new FtAnalysisObjective() {
+  };
+  
+  private FtAnalysisObjective() {
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java
new file mode 100644
index 00000000..c8c8b000
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java
@@ -0,0 +1,156 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import org.eclipse.xtend.lib.annotations.Data;
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor;
+import org.eclipse.xtext.xbase.lib.Pure;
+import org.eclipse.xtext.xbase.lib.util.ToStringBuilder;
+
+@SuppressWarnings("all")
+public abstract class ReliabilityResult {
+  @Data
+  public static final class Solution extends ReliabilityResult {
+    private final double lowerBound;
+    
+    private final double upperBound;
+    
+    public Solution(final double value) {
+      this(value, value);
+    }
+    
+    public Solution(final double lowerBound, final double upperBound) {
+      if ((lowerBound > upperBound)) {
+        throw new IllegalArgumentException("lowerBound must not be larger than upperBound");
+      }
+      this.lowerBound = lowerBound;
+      this.upperBound = upperBound;
+    }
+    
+    @Override
+    public ReliabilityResult.Solution getOrThrow() {
+      return this;
+    }
+    
+    @Override
+    @Pure
+    public int hashCode() {
+      final int prime = 31;
+      int result = 1;
+      result = prime * result + (int) (Double.doubleToLongBits(this.lowerBound) ^ (Double.doubleToLongBits(this.lowerBound) >>> 32));
+      return prime * result + (int) (Double.doubleToLongBits(this.upperBound) ^ (Double.doubleToLongBits(this.upperBound) >>> 32));
+    }
+    
+    @Override
+    @Pure
+    public boolean equals(final Object obj) {
+      if (this == obj)
+        return true;
+      if (obj == null)
+        return false;
+      if (getClass() != obj.getClass())
+        return false;
+      ReliabilityResult.Solution other = (ReliabilityResult.Solution) obj;
+      if (Double.doubleToLongBits(other.lowerBound) != Double.doubleToLongBits(this.lowerBound))
+        return false; 
+      if (Double.doubleToLongBits(other.upperBound) != Double.doubleToLongBits(this.upperBound))
+        return false; 
+      return true;
+    }
+    
+    @Override
+    @Pure
+    public String toString() {
+      return new ToStringBuilder(this)
+        .addAllFields()
+        .toString();
+    }
+    
+    @Pure
+    public double getLowerBound() {
+      return this.lowerBound;
+    }
+    
+    @Pure
+    public double getUpperBound() {
+      return this.upperBound;
+    }
+  }
+  
+  @Data
+  public static final class Unknown extends ReliabilityResult {
+    private final String message;
+    
+    private final Throwable cause;
+    
+    @FinalFieldsConstructor
+    public Unknown(final String message, final Throwable cause) {
+      super();
+      this.message = message;
+      this.cause = cause;
+    }
+    
+    public Unknown(final String message) {
+      this(message, null);
+    }
+    
+    @Override
+    public ReliabilityResult.Solution getOrThrow() {
+      throw new RuntimeException(this.message, this.cause);
+    }
+    
+    @Override
+    @Pure
+    public int hashCode() {
+      final int prime = 31;
+      int result = 1;
+      result = prime * result + ((this.message== null) ? 0 : this.message.hashCode());
+      return prime * result + ((this.cause== null) ? 0 : this.cause.hashCode());
+    }
+    
+    @Override
+    @Pure
+    public boolean equals(final Object obj) {
+      if (this == obj)
+        return true;
+      if (obj == null)
+        return false;
+      if (getClass() != obj.getClass())
+        return false;
+      ReliabilityResult.Unknown other = (ReliabilityResult.Unknown) obj;
+      if (this.message == null) {
+        if (other.message != null)
+          return false;
+      } else if (!this.message.equals(other.message))
+        return false;
+      if (this.cause == null) {
+        if (other.cause != null)
+          return false;
+      } else if (!this.cause.equals(other.cause))
+        return false;
+      return true;
+    }
+    
+    @Override
+    @Pure
+    public String toString() {
+      return new ToStringBuilder(this)
+        .addAllFields()
+        .toString();
+    }
+    
+    @Pure
+    public String getMessage() {
+      return this.message;
+    }
+    
+    @Pure
+    public Throwable getCause() {
+      return this.cause;
+    }
+  }
+  
+  public static final ReliabilityResult.Unknown TIMEOUT = new ReliabilityResult.Unknown("Solver timed out");
+  
+  public static final ReliabilityResult.Unknown MEMOUT = new ReliabilityResult.Unknown("Solver out of memory");
+  
+  public abstract ReliabilityResult.Solution getOrThrow();
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java
new file mode 100644
index 00000000..e1bb3625
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java
@@ -0,0 +1,31 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import com.google.common.base.Objects;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration;
+
+@SuppressWarnings("all")
+public final class StormDftConfiguration extends SolverConfiguration {
+  public static final String DEFAULT_SOLVER_PATH = "storm-dft";
+  
+  public double precision = 1e-6;
+  
+  public boolean bisimulation = true;
+  
+  public boolean symmetryReduction = true;
+  
+  public boolean modularization = true;
+  
+  public boolean dontCarePropagation = true;
+  
+  public double approximation = 0;
+  
+  public ApproximationHeuristic approximationHeuristic = ApproximationHeuristic.NONE;
+  
+  public FtAnalysisObjective objective;
+  
+  public boolean isApproximationInUse() {
+    return (!Objects.equal(this.approximationHeuristic, ApproximationHeuristic.NONE));
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java
new file mode 100644
index 00000000..955c9ed1
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java
@@ -0,0 +1,12 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+@SuppressWarnings("all")
+public class StormDftException extends RuntimeException {
+  public StormDftException(final String s) {
+    super(s);
+  }
+  
+  public StormDftException(final String s, final Exception e) {
+    super(s, e);
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java
new file mode 100644
index 00000000..46127425
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java
@@ -0,0 +1,330 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import com.google.common.base.Objects;
+import com.google.common.collect.ImmutableList;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftException;
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration;
+import java.io.BufferedReader;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.InputStreamReader;
+import java.util.ArrayList;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import org.eclipse.xtend2.lib.StringConcatenation;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.Exceptions;
+import org.eclipse.xtext.xbase.lib.Extension;
+import org.eclipse.xtext.xbase.lib.Functions.Function0;
+import org.eclipse.xtext.xbase.lib.InputOutput;
+import org.eclipse.xtext.xbase.lib.IterableExtensions;
+
+@SuppressWarnings("all")
+public class StormDftHandler {
+  private static final String DOUBLE_REGEX = "[-+]?[0-9]*\\.?[0-9]+([eE][-+]?[0-9]+)?";
+  
+  private static final String SINGLE_RESULT_GROUP = "single";
+  
+  private static final String LOWER_BOUND_GROUP = "lower";
+  
+  private static final String UPPER_BOUND_GROUP = "upper";
+  
+  private static final String RESULT_REGEX = new Function0<String>() {
+    public String apply() {
+      StringConcatenation _builder = new StringConcatenation();
+      _builder.append("^Result:\\s*\\[(?:(?<");
+      _builder.append(StormDftHandler.SINGLE_RESULT_GROUP);
+      _builder.append(">");
+      _builder.append(StormDftHandler.DOUBLE_REGEX);
+      _builder.append(")|\\((?<");
+      _builder.append(StormDftHandler.LOWER_BOUND_GROUP);
+      _builder.append(">");
+      _builder.append(StormDftHandler.DOUBLE_REGEX);
+      _builder.append("),\\s*(?<");
+      _builder.append(StormDftHandler.UPPER_BOUND_GROUP);
+      _builder.append(">");
+      _builder.append(StormDftHandler.DOUBLE_REGEX);
+      _builder.append(")\\))\\]");
+      return _builder.toString();
+    }
+  }.apply();
+  
+  private static final Pattern RESULT_PATTERN = Pattern.compile(StormDftHandler.RESULT_REGEX);
+  
+  private static final int SIGNAL_EXIT_VALUE_OFFSET = 0x80;
+  
+  private static final int SIGXCPU = 24;
+  
+  private static final int SIGXFSZ = 25;
+  
+  private static final int STORM_GENERAL_ERROR = ((-1) & 0xff);
+  
+  private static final int STORM_TIMEOUT = ((-2) & 0xff);
+  
+  private static final int STORM_MEMOUT = ((-3) & 0xff);
+  
+  public ReliabilityResult callSolver(final String dftFilePath, final StormDftConfiguration configuration) {
+    try {
+      ReliabilityResult _xblockexpression = null;
+      {
+        final ImmutableList<String> commandLine = this.toCommandLine(configuration, dftFilePath);
+        final DocumentationLevel documentationLevel = configuration.documentationLevel;
+        final boolean printOutput = (Objects.equal(documentationLevel, DocumentationLevel.NORMAL) || 
+          Objects.equal(documentationLevel, DocumentationLevel.FULL));
+        final ProcessBuilder processBuilder = new ProcessBuilder().command(commandLine);
+        Process process = null;
+        ReliabilityResult _xtrycatchfinallyexpression = null;
+        try {
+          ReliabilityResult _xtrycatchfinallyexpression_1 = null;
+          try {
+            ReliabilityResult _xblockexpression_1 = null;
+            {
+              process = processBuilder.start();
+              process.getOutputStream().close();
+              final ReliabilityResult.Solution result = this.readOutput(process.getInputStream(), printOutput);
+              final String error = this.readError(process.getErrorStream(), printOutput);
+              final int exitValue = process.waitFor();
+              ReliabilityResult _xifexpression = null;
+              if ((result == null)) {
+                _xifexpression = this.interpretExitStatus(exitValue, error);
+              } else {
+                _xifexpression = result;
+              }
+              _xblockexpression_1 = _xifexpression;
+            }
+            _xtrycatchfinallyexpression_1 = _xblockexpression_1;
+          } catch (final Throwable _t) {
+            if (_t instanceof IOException) {
+              final IOException e = (IOException)_t;
+              throw new StormDftException("Error during input/output handling of the stochastic solver.", e);
+            } else {
+              throw Exceptions.sneakyThrow(_t);
+            }
+          }
+          _xtrycatchfinallyexpression = _xtrycatchfinallyexpression_1;
+        } catch (final Throwable _t_1) {
+          if (_t_1 instanceof Exception) {
+            final Exception e_1 = (Exception)_t_1;
+            if ((process != null)) {
+              process.destroyForcibly().waitFor();
+            }
+            throw e_1;
+          } else {
+            throw Exceptions.sneakyThrow(_t_1);
+          }
+        }
+        _xblockexpression = _xtrycatchfinallyexpression;
+      }
+      return _xblockexpression;
+    } catch (Throwable _e) {
+      throw Exceptions.sneakyThrow(_e);
+    }
+  }
+  
+  private ImmutableList<String> toCommandLine(@Extension final StormDftConfiguration configuration, final String dftFilePath) {
+    ImmutableList<String> _xblockexpression = null;
+    {
+      @Extension
+      final ImmutableList.Builder<String> optionsBuilder = ImmutableList.<String>builder();
+      String _elvis = null;
+      if (configuration.solverPath != null) {
+        _elvis = configuration.solverPath;
+      } else {
+        _elvis = StormDftConfiguration.DEFAULT_SOLVER_PATH;
+      }
+      optionsBuilder.add(_elvis);
+      if ((configuration.runtimeLimit != SolverConfiguration.Unlimited)) {
+        optionsBuilder.add("--timeout", Integer.valueOf(configuration.runtimeLimit).toString());
+      }
+      optionsBuilder.add("--precision", Double.valueOf(configuration.precision).toString());
+      if (configuration.bisimulation) {
+        optionsBuilder.add("--bisimulation");
+      }
+      if (configuration.symmetryReduction) {
+        optionsBuilder.add("--symmetryreduction");
+      }
+      if (configuration.modularization) {
+        optionsBuilder.add("--modularisation");
+      }
+      if ((!configuration.dontCarePropagation)) {
+        optionsBuilder.add("--disabledc");
+      }
+      boolean _isApproximationInUse = configuration.isApproximationInUse();
+      if (_isApproximationInUse) {
+        String _switchResult = null;
+        final ApproximationHeuristic approximationHeuristic = configuration.approximationHeuristic;
+        if (approximationHeuristic != null) {
+          switch (approximationHeuristic) {
+            case DEPTH:
+              _switchResult = "depth";
+              break;
+            default:
+              throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic));
+          }
+        } else {
+          throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic));
+        }
+        final String heuristicName = _switchResult;
+        optionsBuilder.add("--approximation", Double.valueOf(configuration.approximation).toString(), "--approximationheuristic", heuristicName);
+      }
+      optionsBuilder.add("--dftfile", dftFilePath);
+      final FtAnalysisObjective objective = configuration.objective;
+      boolean _matched = false;
+      if (Objects.equal(objective, FtAnalysisObjective.MTTF)) {
+        _matched=true;
+        optionsBuilder.add("--expectedtime");
+      }
+      if (!_matched) {
+        if (objective instanceof FtAnalysisObjective.TimeBound) {
+          _matched=true;
+          optionsBuilder.add("--timebound");
+        }
+      }
+      if (!_matched) {
+        throw new IllegalArgumentException(("Unknown analysis objective: " + configuration.objective));
+      }
+      boolean _equals = Objects.equal(configuration.documentationLevel, DocumentationLevel.FULL);
+      if (_equals) {
+        optionsBuilder.add("--verbose");
+      }
+      _xblockexpression = optionsBuilder.build();
+    }
+    return _xblockexpression;
+  }
+  
+  private ReliabilityResult.Solution readOutput(final InputStream inputStream, final boolean printOutput) {
+    try {
+      Object _xblockexpression = null;
+      {
+        InputStreamReader _inputStreamReader = new InputStreamReader(inputStream);
+        final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader);
+        try {
+          String line = null;
+          while (((line = bufferedReader.readLine()) != null)) {
+            {
+              if (printOutput) {
+                InputOutput.<String>println(line);
+              }
+              final Matcher matcher = StormDftHandler.RESULT_PATTERN.matcher(line);
+              boolean _find = matcher.find();
+              if (_find) {
+                try {
+                  final String single = matcher.group(StormDftHandler.SINGLE_RESULT_GROUP);
+                  if ((single != null)) {
+                    final double singleValue = Double.parseDouble(single);
+                    return new ReliabilityResult.Solution(singleValue);
+                  }
+                  final String lower = matcher.group(StormDftHandler.LOWER_BOUND_GROUP);
+                  final String upper = matcher.group(StormDftHandler.UPPER_BOUND_GROUP);
+                  if (((lower != null) && (upper != null))) {
+                    final double lowerValue = Double.parseDouble(lower);
+                    final double upperValue = Double.parseDouble(upper);
+                    return new ReliabilityResult.Solution(lowerValue, upperValue);
+                  }
+                  throw new StormDftException(("Inconsistent stochastic solver output: " + line));
+                } catch (final Throwable _t) {
+                  if (_t instanceof NumberFormatException) {
+                    final NumberFormatException e = (NumberFormatException)_t;
+                    throw new StormDftException("Malformatted number from stochastic solver.", e);
+                  } else {
+                    throw Exceptions.sneakyThrow(_t);
+                  }
+                }
+              }
+            }
+          }
+        } finally {
+          bufferedReader.close();
+        }
+        _xblockexpression = null;
+      }
+      return ((ReliabilityResult.Solution)_xblockexpression);
+    } catch (Throwable _e) {
+      throw Exceptions.sneakyThrow(_e);
+    }
+  }
+  
+  private String readError(final InputStream inputStream, final boolean printOutput) {
+    try {
+      String _xblockexpression = null;
+      {
+        InputStreamReader _inputStreamReader = new InputStreamReader(inputStream);
+        final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader);
+        String _xtrycatchfinallyexpression = null;
+        try {
+          String _xblockexpression_1 = null;
+          {
+            final ArrayList<String> lines = CollectionLiterals.<String>newArrayList();
+            String line = null;
+            while (((line = bufferedReader.readLine()) != null)) {
+              {
+                if (printOutput) {
+                  System.err.println(line);
+                }
+                lines.add(line);
+              }
+            }
+            _xblockexpression_1 = IterableExtensions.join(lines, "\n");
+          }
+          _xtrycatchfinallyexpression = _xblockexpression_1;
+        } finally {
+          bufferedReader.close();
+        }
+        _xblockexpression = _xtrycatchfinallyexpression;
+      }
+      return _xblockexpression;
+    } catch (Throwable _e) {
+      throw Exceptions.sneakyThrow(_e);
+    }
+  }
+  
+  private ReliabilityResult.Unknown interpretExitStatus(final int exitValue, final String error) {
+    ReliabilityResult.Unknown _switchResult = null;
+    boolean _matched = false;
+    if (Objects.equal(exitValue, StormDftHandler.STORM_GENERAL_ERROR)) {
+      _matched=true;
+      throw new StormDftException(("Storm error: " + error));
+    }
+    if (!_matched) {
+      if (Objects.equal(exitValue, StormDftHandler.STORM_TIMEOUT)) {
+        _matched=true;
+      }
+      if (!_matched) {
+        if (Objects.equal(exitValue, (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + StormDftHandler.SIGXCPU))) {
+          _matched=true;
+        }
+      }
+      if (_matched) {
+        _switchResult = ReliabilityResult.TIMEOUT;
+      }
+    }
+    if (!_matched) {
+      if (Objects.equal(exitValue, StormDftHandler.STORM_MEMOUT)) {
+        _matched=true;
+      }
+      if (!_matched) {
+        if (Objects.equal(exitValue, (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + StormDftHandler.SIGXFSZ))) {
+          _matched=true;
+        }
+      }
+      if (_matched) {
+        _switchResult = ReliabilityResult.MEMOUT;
+      }
+    }
+    if (!_matched) {
+      {
+        if ((exitValue > StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET)) {
+          final int signalNumber = (exitValue - StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET);
+          throw new StormDftException(((("Storm unexpectedly killed by signal " + Integer.valueOf(signalNumber)) + ": ") + error));
+        }
+        throw new StormDftException(((("Storm unexpectedly exit with status " + Integer.valueOf(exitValue)) + ": ") + error));
+      }
+    }
+    return _switchResult;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java
new file mode 100644
index 00000000..491e7fc1
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java
@@ -0,0 +1,79 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import com.google.common.base.Objects;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantModel;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree;
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ReliabilityModel;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo.Ft2GalileoTransformation;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftHandler;
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
+
+@SuppressWarnings("all")
+public class StormDftSolver {
+  private static final String DFT_FILE_NAME = "ft.dft";
+  
+  private final Ft2GalileoTransformation ft2Galileo = new Ft2GalileoTransformation();
+  
+  private final StormDftHandler handler = new StormDftHandler();
+  
+  public ReliabilityResult solve(final ReliabilityModel reliabilityModel, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) {
+    ReliabilityResult _switchResult = null;
+    boolean _matched = false;
+    if (reliabilityModel instanceof FaultTree) {
+      _matched=true;
+      _switchResult = this.solve(((FaultTree)reliabilityModel), configuration, reasonerWorkspace);
+    }
+    if (!_matched) {
+      if (reliabilityModel instanceof ConstantModel) {
+        _matched=true;
+        ReliabilityResult.Solution _xblockexpression = null;
+        {
+          double _xifexpression = (double) 0;
+          boolean _isFailed = ((ConstantModel)reliabilityModel).isFailed();
+          if (_isFailed) {
+            _xifexpression = 0;
+          } else {
+            double _switchResult_1 = (double) 0;
+            final FtAnalysisObjective objective = configuration.objective;
+            boolean _matched_1 = false;
+            if (Objects.equal(objective, FtAnalysisObjective.MTTF)) {
+              _matched_1=true;
+              _switchResult_1 = Double.POSITIVE_INFINITY;
+            }
+            if (!_matched_1) {
+              if (objective instanceof FtAnalysisObjective.TimeBound) {
+                _matched_1=true;
+                _switchResult_1 = 1;
+              }
+            }
+            if (!_matched_1) {
+              throw new IllegalArgumentException(("Unknown objective: " + objective));
+            }
+            _xifexpression = _switchResult_1;
+          }
+          final double result = _xifexpression;
+          _xblockexpression = new ReliabilityResult.Solution(result);
+        }
+        _switchResult = _xblockexpression;
+      }
+    }
+    if (!_matched) {
+      throw new IllegalArgumentException(("Unknown reliability model: " + reliabilityModel));
+    }
+    return _switchResult;
+  }
+  
+  public ReliabilityResult solve(final FaultTree faultTree, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) {
+    ReliabilityResult _xblockexpression = null;
+    {
+      final CharSequence galileo = this.ft2Galileo.toGalileo(faultTree);
+      reasonerWorkspace.writeText(StormDftSolver.DFT_FILE_NAME, galileo);
+      final String dftFilePath = reasonerWorkspace.getFile(StormDftSolver.DFT_FILE_NAME).getAbsolutePath();
+      _xblockexpression = this.handler.callSolver(dftFilePath, configuration);
+    }
+    return _xblockexpression;
+  }
+}