33 files changed, 1604 insertions, 9 deletions

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
index 3e751774..20f1f4a7 100644
--- 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
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..54ba3d09
--- /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..271c9cc0
--- /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..db3a7e73
--- /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
index 70156b02..75154a4c 100644
--- 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
@@ -1 +1,8 @@
 /.Cft2FtTransformation.java._trace
+/.EventMaterializer.java._trace
+/.MaterializedEvent.java._trace
+/.CollectedInputs.java._trace
+/.MaterializedEventCollection.java._trace
+/.FaultTreeBuilder.java._trace
+/.FaultModelBuilder.java._trace
+/.EventCollection.java._trace
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
index ae750806..e87b8865 100644
--- 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
@@ -1,10 +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 void createFaultTree(final ComponentFaultTree componentFaultTree) {
-    throw new UnsupportedOperationException();
+  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..70481341
--- /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,456 @@
+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.transformation.cft2ft.EventCollection;
+import java.util.LinkedHashSet;
+import java.util.Map;
+import java.util.function.Function;
+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 {
+        final Function<EventMaterializer.EventKey<EventDeclaration>, Event> _function = (EventMaterializer.EventKey<EventDeclaration> it) -> {
+          return this.materialize(it.component, it.event);
+        };
+        _xtrycatchfinallyexpression = this.materializationCache.computeIfAbsent(eventKey, _function);
+      } 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 {
+        final Function<EventMaterializer.EventKey<InputEvent>, EventCollection> _function = (EventMaterializer.EventKey<InputEvent> it) -> {
+          return this.materializeConnectedEvents(it.component, it.event);
+        };
+        _xtrycatchfinallyexpression = this.multipleInputCache.computeIfAbsent(inputKey, _function);
+      } 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) {
+        {
+          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
index d26ae359..f705fefe 100644
--- 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
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
index 03d6064f..bab76345 100644
--- 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
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
index 1f6758ac..257bfc56 100644
--- 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
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
index 3569c02f..a1339a18 100644
--- 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
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
index 378550ba..ba19d0fb 100644
--- 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
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
index 0b0e534a..1e8612b2 100644
--- 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
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
index 5e26d4e4..ebe80f2e 100644
--- 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
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
index 8fb7f13f..03bd16f8 100644
--- 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
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
index 8b2d9d97..a63c8e78 100644
--- 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
@@ -3,6 +3,7 @@ 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;
@@ -23,13 +24,18 @@ public class Ecore2CftTransformation {
     this.mappingHandlers = ImmutableList.<MappingHandler>copyOf(ListExtensions.<MappingDefinition, MappingHandler>map(transformationDefinition.getMappingDefinitions(), _function));
   }
   
-  public void createComponentFaultTree() {
-    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);
+  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/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..9fe75a0f
--- /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..3f932890
--- /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 @@
+/.Ft2GalileoTransformation.java._trace
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..e900c62a
--- /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,181 @@
+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) {
+        String _name_1 = event.getName();
+        _builder.append(_name_1);
+        _builder.append(" ");
+        StringConcatenationClient _defineEvent = this.defineEvent(event);
+        _builder.append(_defineEvent);
+        _builder.append(";");
+        _builder.newLineIfNotEmpty();
+      }
+    }
+    return _builder;
+  }
+  
+  protected StringConcatenationClient _defineEvent(final BasicEvent basicEvent) {
+    return this.defineDistribution(basicEvent.getDistribution());
+  }
+  
+  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(" ", "");
+            }
+            String _name = input.getName();
+            _builder.append(_name);
+          }
+        }
+      }
+    };
+    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 StringConcatenationClient 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..57c4608d
--- /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..f5cb52f4
--- /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..5dad0728
--- /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..abd8a501
--- /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..59cc8fe8
--- /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,9 @@
+/.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
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..003d9cc5
--- /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,351 @@
+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 jnr.constants.platform.Signal;
+import org.apache.commons.lang.SystemUtils;
+import org.eclipse.xtend2.lib.StringConcatenation;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.Conversions;
+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.Functions.Function1;
+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 = new Function0<Integer>() {
+    public Integer apply() {
+      int _xifexpression = (int) 0;
+      if (SystemUtils.IS_OS_SOLARIS) {
+        _xifexpression = 0;
+      } else {
+        _xifexpression = 0x80;
+      }
+      return _xifexpression;
+    }
+  }.apply().intValue();
+  
+  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) {
+        int _intValue = Signal.SIGXCPU.intValue();
+        int _plus = (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + _intValue);
+        if (Objects.equal(exitValue, _plus)) {
+          _matched=true;
+        }
+      }
+      if (_matched) {
+        _switchResult = ReliabilityResult.TIMEOUT;
+      }
+    }
+    if (!_matched) {
+      if (Objects.equal(exitValue, StormDftHandler.STORM_MEMOUT)) {
+        _matched=true;
+      }
+      if (!_matched) {
+        int _intValue_1 = Signal.SIGXFSZ.intValue();
+        int _plus_1 = (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + _intValue_1);
+        if (Objects.equal(exitValue, _plus_1)) {
+          _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);
+          final Function1<Signal, Boolean> _function = (Signal it) -> {
+            int _intValue_2 = it.intValue();
+            return Boolean.valueOf((_intValue_2 == signalNumber));
+          };
+          final Signal signal = IterableExtensions.<Signal>findFirst(((Iterable<Signal>)Conversions.doWrapArray(Signal.values())), _function);
+          if ((signal != null)) {
+            throw new StormDftException(((("Storm unexpectedly killed by signal " + signal) + ": ") + 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;
+  }
+}