45 files changed, 2334 insertions, 14 deletions

diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/META-INF/MANIFEST.MF b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/META-INF/MANIFEST.MF
index 91eeedc5..ce704acf 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/META-INF/MANIFEST.MF
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/META-INF/MANIFEST.MF
@@ -13,4 +13,11 @@ Require-Bundle: com.google.guava,
  org.eclipse.viatra.query.runtime,
  org.eclipse.viatra.query.runtime.rete,
  org.eclipse.viatra.query.runtime.localsearch,
- hu.bme.mit.inf.dslreasoner.faulttree.components
+ hu.bme.mit.inf.dslreasoner.faulttree.components,
+ hu.bme.mit.inf.dslreasoner.logic.model,
+ com.github.jnr.constants;bundle-version="0.9.8",
+ org.apache.commons.lang;bundle-version="2.6.0"
+Export-Package: hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft,
+ hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft,
+ hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo,
+ hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/build.properties b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/build.properties
index 34d2e4d2..d8e2f0e9 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/build.properties
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/build.properties
@@ -1,4 +1,5 @@
-source.. = src/
+source.. = src/,\
+           xtend-gen/
 output.. = bin/
 bin.includes = META-INF/,\
                .
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.xtend
index caaffc3c..a522654c 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.xtend
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.xtend
@@ -1,10 +1,24 @@
 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.FtFactory
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.RandomEvent
 
 class Cft2FtTransformation {
         def createFaultTree(ComponentFaultTree componentFaultTree) {
-                // TODO
-                throw new UnsupportedOperationException()
+                val materializer = new EventMaterializer
+                val topEvent = materializer.getOrMaterialize(componentFaultTree.topEvent)
+                switch (topEvent) {
+                        ConstantEvent:
+                                FtFactory.eINSTANCE.createConstantModel => [
+                                        failed = topEvent.failed
+                                ]
+                        RandomEvent: {
+                                val builder = new FaultTreeBuilder
+                                builder.addTopLevel(topEvent)
+                                builder.faultTree
+                        }
+                }
         }
-}
\ No newline at end of file
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventCollection.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventCollection.xtend
new file mode 100644
index 00000000..102dc57e
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventCollection.xtend
@@ -0,0 +1,90 @@
+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
+
+@Data
+class EventCollection {
+        val int falseEventCount
+        val int trueEventCount
+        val Set<RandomEvent> randomEvents
+
+        def containsFalseEvent() {
+                falseEventCount >= 1
+        }
+
+        def containsTrueEvent() {
+                trueEventCount >= 1
+        }
+
+        def getVariableEventCount() {
+                randomEvents.size
+        }
+
+        def containsRandomEvent() {
+                variableEventCount >= 1
+        }
+
+        def getCount() {
+                falseEventCount + trueEventCount + variableEventCount
+        }
+
+        def isEmpty() {
+                !containsFalseEvent && !containsTrueEvent && !containsRandomEvent
+        }
+
+        def containsExactlyOneRandomEvent() {
+                !containsFalseEvent && !containsTrueEvent && variableEventCount == 1
+        }
+
+        def toSingleRandomEvent() {
+                if (!containsExactlyOneRandomEvent) {
+                        throw new IllegalStateException("Input collection is not a single random event")
+                }
+                randomEvents.head
+        }
+
+        static def builder() {
+                new Builder()
+        }
+
+        static class Builder {
+                var falseEventCount = 0
+                var trueEventCount = 0
+                val randomEventsBuilder = ImmutableSet.<RandomEvent>builder
+
+                private new() {
+                }
+
+                def add(Event event) {
+                        switch (event) {
+                                ConstantEvent:
+                                        if (event.failed) {
+                                                trueEventCount++
+                                        } else {
+                                                falseEventCount++
+                                        }
+                                RandomEvent:
+                                        randomEventsBuilder.add(event)
+                                default:
+                                        throw new IllegalArgumentException("Unknown event: " + event)
+                        }
+                        this
+                }
+
+                def addAll(EventCollection materializedEvens) {
+                        falseEventCount += materializedEvens.falseEventCount
+                        trueEventCount += materializedEvens.trueEventCount
+                        randomEventsBuilder.addAll(materializedEvens.randomEvents)
+                        this
+                }
+
+                def build() {
+                        new EventCollection(falseEventCount, trueEventCount, randomEventsBuilder.build)
+                }
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventMaterializer.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventMaterializer.xtend
new file mode 100644
index 00000000..85396e4d
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventMaterializer.xtend
@@ -0,0 +1,192 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft
+
+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.EventDeclaration
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.GateDefinition
+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.ConstantEvent
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.Event
+import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FtFactory
+import java.util.LinkedHashSet
+import java.util.Map
+import org.eclipse.emf.ecore.util.EcoreUtil
+import org.eclipse.xtend.lib.annotations.Data
+
+class EventMaterializer {
+        extension val FtFactory = FtFactory.eINSTANCE
+
+        val Map<EventKey<EventDeclaration>, Event> materializationCache = newHashMap
+        val Map<EventKey<InputEvent>, EventCollection> multipleInputCache = newHashMap
+        val ConstantEvent falseEvent
+        val ConstantEvent trueEvent
+        val path = new LinkedHashSet<EventKey<? extends EventDeclaration>>
+
+        new() {
+                falseEvent = createConstantEvent => [
+                        failed = false
+                ]
+                trueEvent = createConstantEvent => [
+                        failed = true
+                ]
+        }
+
+        def getOrMaterialize(Output output) {
+                getOrMaterialize(output.component, output.eventDeclaration)
+        }
+
+        def Event getOrMaterialize(Component component, EventDeclaration eventDeclaration) {
+                val eventKey = new EventKey(component, eventDeclaration)
+                pushEventKey(eventKey)
+                try {
+                        materializationCache.computeIfAbsent(eventKey)[materialize(it.component, it.event)]
+                } finally {
+                        popEventKey(eventKey)
+                }
+        }
+
+        protected def materialize(Component component, EventDeclaration eventDeclaration) {
+                val eventName = component.name + "_" + eventDeclaration.name
+                val event = switch (eventDeclaration) {
+                        InputEvent:
+                                return materializeConnectedEvent(component, eventDeclaration)
+                        BasicEventDefinition: {
+                                val basicEvent = createBasicEvent
+                                basicEvent.distribution = EcoreUtil.copy(eventDeclaration.distribution)
+                                basicEvent
+                        }
+                        GateDefinition: {
+                                val inputs = collectInputs(component, eventDeclaration)
+                                val gate = switch (eventDeclaration) {
+                                        AndGateDefinition:
+                                                if (inputs.containsFalseEvent) {
+                                                        return falseEvent
+                                                } else if (inputs.empty) {
+                                                        return trueEvent
+                                                } else if (inputs.containsExactlyOneRandomEvent) {
+                                                        return inputs.toSingleRandomEvent
+                                                } else {
+                                                        createAndGate
+                                                }
+                                        OrGateDefinition:
+                                                if (inputs.containsTrueEvent) {
+                                                        return trueEvent
+                                                } else if (inputs.empty) {
+                                                        return falseEvent
+                                                } else if (inputs.containsExactlyOneRandomEvent) {
+                                                        return inputs.toSingleRandomEvent
+                                                } else {
+                                                        createOrGate
+                                                }
+                                        KOfMGateDefinition: {
+                                                val requiredTrueInputs = inputs.count * eventDeclaration.k / eventDeclaration.m
+                                                val k = requiredTrueInputs - inputs.getTrueEventCount
+                                                val m = inputs.variableEventCount
+                                                if (k == 0) {
+                                                        return trueEvent
+                                                } else if (k > m) {
+                                                        return falseEvent
+                                                } else if (inputs.containsExactlyOneRandomEvent) {
+                                                        return inputs.toSingleRandomEvent
+                                                } else if (k == 1) {
+                                                        createOrGate
+                                                } else if (k == m) {
+                                                        createAndGate
+                                                } else {
+                                                        val kOfMGate = createKOfMGate
+                                                        kOfMGate.k = k
+                                                        kOfMGate
+                                                }
+                                        }
+                                        default:
+                                                throw new IllegalArgumentException("Unknown gate definition: " + eventDeclaration)
+                                }
+                                gate.inputEvents.addAll(inputs.getRandomEvents)
+                                gate
+                        }
+                        default:
+                                throw new IllegalArgumentException("Unknown event declaration: " + eventDeclaration)
+                }
+                event.name = eventName
+                event
+        }
+
+        protected def materializeConnectedEvent(Component component, InputEvent inputEvent) {
+                if (inputEvent.multiple) {
+                        throw new IllegalArgumentException('''Cannot materialize multiple nput «component.name»_«inputEvent.name»''')
+                }
+                val input = findInput(component, inputEvent)
+                val incomingConnections = input.incomingConnections
+                if (incomingConnections.size != 1) {
+                        throw new IllegalArgumentException('''Input «component.name»_«inputEvent.name» has «incomingConnections.size» connections instead of 1''')
+                }
+                val output = incomingConnections.head.output
+                getOrMaterialize(output.component, output.eventDeclaration)
+        }
+
+        protected def collectInputs(Component component, GateDefinition gateDefinition) {
+                val builder = EventCollection.builder
+                for (inputEventDeclaration : gateDefinition.inputEvents) {
+                        switch (inputEventDeclaration) {
+                                InputEvent case inputEventDeclaration.multiple: {
+                                        val materializedEvents = getOrMaterializeConnectedEvents(component, inputEventDeclaration)
+                                        builder.addAll(materializedEvents)
+                                }
+                                default:
+                                        builder.add(getOrMaterialize(component, inputEventDeclaration))
+                        }
+                }
+                builder.build
+        }
+
+        protected def getOrMaterializeConnectedEvents(Component component, InputEvent inputEvent) {
+                val inputKey = new EventKey(component, inputEvent)
+                pushEventKey(inputKey)
+                try {
+                         multipleInputCache.computeIfAbsent(inputKey)[materializeConnectedEvents(it.component, it.event)]
+                } finally {
+                        popEventKey(inputKey)
+                }
+        }
+
+        protected def materializeConnectedEvents(Component component, InputEvent inputEvent) {
+                val input = findInput(component, inputEvent)
+                val builder = EventCollection.builder
+                for (connection : input.incomingConnections) {
+                        val materializedEvent = getOrMaterialize(connection.output)
+                        builder.add(materializedEvent)
+                }
+                builder.build
+        }
+
+        protected def findInput(Component component, InputEvent inputEvent) {
+                val input = component.inputs.findFirst[it.inputEvent == inputEvent]
+                if (input === null) {
+                        throw new IllegalArgumentException('''No input «inputEvent» in component «component»''')
+                }
+                return input
+        }
+
+        private def pushEventKey(EventKey<? extends EventDeclaration> eventKey) {
+                if (!path.add(eventKey)) {
+                        throw new IllegalStateException(
+                        '''Circular dependency [«FOR ancestor : path»«ancestor», «ENDFOR»«eventKey»] detected''')
+                }
+        }
+
+        private def popEventKey(EventKey<? extends EventDeclaration> eventKey) {
+                path.remove(eventKey)
+        }
+
+        @Data
+        protected static class EventKey<T extends EventDeclaration> {
+                val Component component
+                val T event
+
+                override toString() '''«component.name»_«event.name»'''
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/FaultTreeBuilder.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/FaultTreeBuilder.xtend
new file mode 100644
index 00000000..0b0afea6
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/FaultTreeBuilder.xtend
@@ -0,0 +1,39 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.cft2ft
+
+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.xtend.lib.annotations.Accessors
+
+class FaultTreeBuilder {
+        @Accessors
+        val faultTree = FtFactory.eINSTANCE.createFaultTree
+
+        def addTopLevel(RandomEvent event) {
+                if (faultTree.topEvent !== null) {
+                        throw new IllegalStateException("Top event was already set")
+                }
+                add(event)
+                faultTree.topEvent = event
+        }
+
+        protected def void add(RandomEvent event) {
+                if (faultTree.eContainer == faultTree) {
+                        return
+                }
+                if (faultTree.eContainer !== null) {
+                        throw new IllegalStateException("Event is already in a different fault tree")
+                }
+                faultTree.events += event
+                if (event instanceof Gate) {
+                        addAll(event.inputEvents)
+                }
+        }
+
+        protected def addAll(Collection<RandomEvent> events) {
+                for (event : events) {
+                        add(event)
+                }
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.xtend
index 36aac5e1..062de3df 100644
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.xtend
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.xtend
@@ -23,5 +23,6 @@ class Ecore2CftTransformation {
                 for (handler : mappingHandlers) {
                         handler.instantiateConnections(trace)
                 }
+                trace.componentFaultTree
         }
 }
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.xtend
new file mode 100644
index 00000000..732d9fed
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.xtend
@@ -0,0 +1,56 @@
+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 org.eclipse.xtend2.lib.StringConcatenationClient
+
+class Ft2GalileoTransformation {
+        def toGalileo(FaultTree faultTree) '''
+                toplevel «faultTree.topEvent.name»;
+                «FOR event : faultTree.events»
+                        «event.name» «defineEvent(event)»;
+                «ENDFOR»
+        '''
+
+        protected dispatch def defineEvent(BasicEvent basicEvent) {
+                defineDistribution(basicEvent.distribution)
+        }
+
+        protected dispatch def StringConcatenationClient defineDistribution(ConstantDistribution distribution) {
+                '''p=«distribution.p»'''
+        }
+
+        protected dispatch def StringConcatenationClient defineDistribution(ExponentialDistribution distribution) {
+                '''lambda=«distribution.lambda»'''
+        }
+
+        protected dispatch def StringConcatenationClient defineDistribution(Distribution distribution) {
+                throw new IllegalArgumentException("Unknown distribution: " + distribution)
+        }
+
+        protected dispatch def StringConcatenationClient defineEvent(Gate gate) {
+                '''«defineGate(gate)» «FOR input : gate.inputEvents SEPARATOR " "»«input.name»«ENDFOR»'''
+        }
+
+        protected dispatch def StringConcatenationClient defineGate(AndGate gate) '''and'''
+
+        protected dispatch def StringConcatenationClient defineGate(OrGate gate) '''or'''
+
+        protected dispatch def StringConcatenationClient defineGate(KOfMGate gate) '''«gate.k»of«gate.inputEvents.size»'''
+
+        protected dispatch def StringConcatenationClient defineGate(Gate gate) {
+                throw new IllegalArgumentException("Unknown gate: " + gate)
+        }
+
+        protected dispatch def StringConcatenationClient defineEvent(RandomEvent randomEvent) {
+                throw new IllegalArgumentException("Unknown random even: " + randomEvent)
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend
new file mode 100644
index 00000000..19c3d17d
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend
@@ -0,0 +1,51 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
+
+import org.eclipse.xtend.lib.annotations.Data
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
+
+abstract class ReliabilityResult {
+        public static val TIMEOUT = new Unknown("Solver timed out")
+        public static val MEMOUT = new Unknown("Solver out of memory")
+
+        abstract def Solution getOrThrow()
+
+        @Data
+        static final class Solution extends ReliabilityResult {
+                val double lowerBound
+                val double upperBound
+
+                new(double value) {
+                        this(value, value)
+                }
+
+                new(double lowerBound, double upperBound) {
+                        if (lowerBound > upperBound) {
+                                throw new IllegalArgumentException("lowerBound must not be larger than upperBound")
+                        }
+                        this.lowerBound = lowerBound
+                        this.upperBound = upperBound
+                }
+
+                override getOrThrow() {
+                        this
+                }
+        }
+
+        @Data
+        static final class Unknown extends ReliabilityResult {
+                val String message
+                val Throwable cause
+
+                @FinalFieldsConstructor
+                new() {
+                }
+
+                new(String message) {
+                        this(message, null)
+                }
+
+                override getOrThrow() {
+                        throw new RuntimeException(message, cause)
+                }
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend
new file mode 100644
index 00000000..d9059bfc
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend
@@ -0,0 +1,45 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
+
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration
+
+final class StormDftConfiguration extends SolverConfiguration {
+        public static val 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 var approximationHeuristic = ApproximationHeuristic.NONE
+
+        public FtAnalysisObjective objective
+
+        def isApproximationInUse() {
+                approximationHeuristic != ApproximationHeuristic.NONE
+        }
+}
+
+abstract class FtAnalysisObjective {
+        public static val MTTF = new FtAnalysisObjective {
+        }
+
+        private new() {
+        }
+
+        static final class TimeBound extends FtAnalysisObjective {
+                public double timeBound = 0
+        }
+}
+
+enum ApproximationHeuristic {
+        NONE,
+        DEPTH
+// See https://github.com/moves-rwth/storm/issues/35 for additional approximation heuristics.
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend
new file mode 100644
index 00000000..91c6a0d0
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend
@@ -0,0 +1,186 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
+
+import com.google.common.collect.ImmutableList
+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.regex.Pattern
+import jnr.constants.platform.Signal
+import org.apache.commons.lang.SystemUtils
+
+class StormDftException extends RuntimeException {
+        new(String s) {
+                super(s)
+        }
+
+        new(String s, Exception e) {
+                super(s, e)
+        }
+}
+
+class StormDftHandler {
+        static val DOUBLE_REGEX = "[-+]?[0-9]*\\.?[0-9]+([eE][-+]?[0-9]+)?"
+        static val SINGLE_RESULT_GROUP = "single"
+        static val LOWER_BOUND_GROUP = "lower"
+        static val UPPER_BOUND_GROUP = "upper"
+        static val RESULT_REGEX = '''^Result:\s*\[(?:(?<«SINGLE_RESULT_GROUP»>«DOUBLE_REGEX»)|\((?<«LOWER_BOUND_GROUP»>«DOUBLE_REGEX»),\s*(?<«UPPER_BOUND_GROUP»>«DOUBLE_REGEX»)\))\]'''
+        static val RESULT_PATTERN = Pattern.compile(RESULT_REGEX)
+
+        // See http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/jdk7-b147/src/solaris/native/java/lang/UNIXProcess_md.c#l332
+        static val SIGNAL_EXIT_VALUE_OFFSET = if(SystemUtils.IS_OS_SOLARIS) 0 else 0x80
+
+        static val STORM_GENERAL_ERROR = (-1).bitwiseAnd(0xff)
+        static val STORM_TIMEOUT = (-2).bitwiseAnd(0xff)
+        static val STORM_MEMOUT = (-3).bitwiseAnd(0xff)
+
+        def callSolver(String dftFilePath, StormDftConfiguration configuration) {
+                val commandLine = configuration.toCommandLine(dftFilePath)
+                val documentationLevel = configuration.documentationLevel
+                val printOutput = documentationLevel == DocumentationLevel.NORMAL ||
+                        documentationLevel == DocumentationLevel.FULL
+                val processBuilder = new ProcessBuilder().command(commandLine)
+                var Process process = null
+                try {
+                        try {
+                                process = processBuilder.start
+                                process.outputStream.close
+                                val result = readOutput(process.inputStream, printOutput)
+                                val error = readError(process.errorStream, printOutput)
+                                val exitValue = process.waitFor
+                                if (result === null) {
+                                        interpretExitStatus(exitValue, error)
+                                } else {
+                                        result
+                                }
+                        } catch (IOException e) {
+                                throw new StormDftException("Error during input/output handling of the stochastic solver.", e)
+                        }
+                } catch (Exception e) {
+                        if (process !== null) {
+                                process.destroyForcibly.waitFor
+                        }
+                        throw e
+                }
+        }
+
+        private def toCommandLine(extension StormDftConfiguration configuration, String dftFilePath) {
+                extension val optionsBuilder = ImmutableList.builder
+                add(solverPath ?: StormDftConfiguration.DEFAULT_SOLVER_PATH)
+                if (runtimeLimit != SolverConfiguration.Unlimited) {
+                        add("--timeout", runtimeLimit.toString)
+                }
+                add("--precision", precision.toString)
+                if (bisimulation) {
+                        add("--bisimulation")
+                }
+                if (symmetryReduction) {
+                        add("--symmetryreduction")
+                }
+                if (modularization) {
+                        add("--modularisation")
+                }
+                if (!dontCarePropagation) {
+                        add("--disabledc")
+                }
+                if (approximationInUse) {
+                        val heuristicName = switch (approximationHeuristic) {
+                                case DEPTH:
+                                        "depth"
+                                default:
+                                        throw new IllegalArgumentException("Unknown approximation heuristic: " + approximationHeuristic)
+                        }
+                        add("--approximation", approximation.toString, "--approximationheuristic", heuristicName)
+                }
+                add("--dftfile", dftFilePath)
+                switch (objective) {
+                        case FtAnalysisObjective.MTTF:
+                                add("--expectedtime")
+                        FtAnalysisObjective.TimeBound:
+                                add("--timebound")
+                        default:
+                                throw new IllegalArgumentException("Unknown analysis objective: " + objective)
+                }
+                if (documentationLevel == DocumentationLevel.FULL) {
+                        add("--verbose")
+                }
+                build
+        }
+
+        private def readOutput(InputStream inputStream, boolean printOutput) {
+                val bufferedReader = new BufferedReader(new InputStreamReader(inputStream))
+                try {
+                        var String line
+                        while ((line = bufferedReader.readLine) !== null) {
+                                if (printOutput) {
+                                        println(line)
+                                }
+                                val matcher = RESULT_PATTERN.matcher(line)
+                                if (matcher.find) {
+                                        try {
+                                                val single = matcher.group(SINGLE_RESULT_GROUP)
+                                                if (single !== null) {
+                                                        val singleValue = Double.parseDouble(single)
+                                                        return new ReliabilityResult.Solution(singleValue)
+                                                }
+                                                val lower = matcher.group(LOWER_BOUND_GROUP)
+                                                val upper = matcher.group(UPPER_BOUND_GROUP)
+                                                if (lower !== null && upper !== null) {
+                                                        val lowerValue = Double.parseDouble(lower)
+                                                        val upperValue = Double.parseDouble(upper)
+                                                        return new ReliabilityResult.Solution(lowerValue, upperValue)
+                                                }
+                                                throw new StormDftException("Inconsistent stochastic solver output: " + line)
+                                        } catch (NumberFormatException e) {
+                                                throw new StormDftException("Malformatted number from stochastic solver.", e)
+                                        }
+                                }
+                        }
+                } finally {
+                        bufferedReader.close
+                }
+                null
+        }
+
+        private def readError(InputStream inputStream, boolean printOutput) {
+                val bufferedReader = new BufferedReader(new InputStreamReader(inputStream))
+                try {
+                        val lines = newArrayList
+                        var String line
+                        while ((line = bufferedReader.readLine) !== null) {
+                                if (printOutput) {
+                                        System.err.println(line)
+                                }
+                                lines += line
+                        }
+                        lines.join("\n")
+                } finally {
+                        bufferedReader.close
+                }
+        }
+
+        private def interpretExitStatus(int exitValue, String error) {
+                switch (exitValue) {
+                        case STORM_GENERAL_ERROR:
+                                throw new StormDftException("Storm error: " + error)
+                        case STORM_TIMEOUT,
+                        case SIGNAL_EXIT_VALUE_OFFSET + Signal.SIGXCPU.intValue:
+                                ReliabilityResult.TIMEOUT
+                        case STORM_MEMOUT,
+                        case SIGNAL_EXIT_VALUE_OFFSET + Signal.SIGXFSZ.intValue:
+                                ReliabilityResult.MEMOUT
+                        default: {
+                                if (exitValue > SIGNAL_EXIT_VALUE_OFFSET) {
+                                        val signalNumber = exitValue - SIGNAL_EXIT_VALUE_OFFSET
+                                        val signal = Signal.values.findFirst[intValue == signalNumber]
+                                        if (signal !== null) {
+                                                throw new StormDftException("Storm unexpectedly killed by signal " + signal + ": " + error)
+                                        }
+                                }
+                                throw new StormDftException("Storm unexpectedly exit with status " + exitValue + ": " + error)
+                        }
+                }
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend
new file mode 100644
index 00000000..931b9f39
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend
@@ -0,0 +1,43 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
+
+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.workspace.ReasonerWorkspace
+
+class StormDftSolver {
+        static val DFT_FILE_NAME = "ft.dft"
+
+        val ft2Galileo = new Ft2GalileoTransformation
+        val handler = new StormDftHandler
+
+        def solve(ReliabilityModel reliabilityModel, StormDftConfiguration configuration,
+                ReasonerWorkspace reasonerWorkspace) {
+                switch (reliabilityModel) {
+                        FaultTree:
+                                solve(reliabilityModel, configuration, reasonerWorkspace)
+                        ConstantModel: {
+                                val result = if (reliabilityModel.failed) {
+                                                0
+                                        } else {
+                                                switch (objective : configuration.objective) {
+                                                        case FtAnalysisObjective.MTTF: Double.POSITIVE_INFINITY
+                                                        FtAnalysisObjective.TimeBound: 1
+                                                        default: throw new IllegalArgumentException("Unknown objective: " + objective)
+                                                }
+                                        }
+                                new ReliabilityResult.Solution(result)
+                        }
+                        default:
+                                throw new IllegalArgumentException("Unknown reliability model: " + reliabilityModel)
+                }
+        }
+
+        def solve(FaultTree faultTree, StormDftConfiguration configuration, ReasonerWorkspace reasonerWorkspace) {
+                val galileo = ft2Galileo.toGalileo(faultTree)
+                reasonerWorkspace.writeText(DFT_FILE_NAME, galileo)
+                val dftFilePath = reasonerWorkspace.getFile(DFT_FILE_NAME).absolutePath
+                handler.callSolver(dftFilePath, configuration)
+        }
+}
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;
+  }
+}