17 files changed, 1108 insertions, 0 deletions

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
new file mode 100644
index 00000000..a522654c
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/Cft2FtTransformation.xtend
@@ -0,0 +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) {
+                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
+                        }
+                }
+        }
+}
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..6b3ed0d0
--- /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,208 @@
+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
+
+import static extension hu.bme.mit.inf.dslreasoner.faulttree.model.util.CftExtensions.*
+
+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 {
+                        // computeIfAbsent cannot be used recursively, so we must manually cache the event. 
+                        var event = materializationCache.get(eventKey)
+                        if (event === null) {
+                                event = materialize(component, eventDeclaration)
+                                materializationCache.put(eventKey, event)
+                        }
+                        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 {
+                        // computeIfAbsent cannot be used recursively, so we must manually cache the event. 
+                        var eventCollection = multipleInputCache.get(inputKey)
+                        if (eventCollection === null) {
+                                eventCollection = materializeConnectedEvents(component, inputEvent)
+                                multipleInputCache.put(inputKey, eventCollection)
+                        }
+                        eventCollection
+                } finally {
+                        popEventKey(inputKey)
+                }
+        }
+
+        protected def materializeConnectedEvents(Component component, InputEvent inputEvent) {
+                val input = findInput(component, inputEvent)
+                val builder = EventCollection.builder
+                for (connection : input.incomingConnections) {
+                        if (connection.isCurrentlyConnected) {
+                                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/ComponentFaultTreeTrace.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentFaultTreeTrace.xtend
new file mode 100644
index 00000000..10c91fb4
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentFaultTreeTrace.xtend
@@ -0,0 +1,49 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.CftFactory
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentDefinition
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Modality
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.xtend.lib.annotations.Accessors
+
+class ComponentFaultTreeTrace {
+        @Accessors val componentFaultTree = CftFactory.eINSTANCE.createComponentFaultTree
+
+        val nameGenerator = new ComponentNameGenerator
+        val Map<IPatternMatch, ComponentInstanceTrace> componentInstancesMap = newHashMap
+
+        def instantiateComponent(IPatternMatch patternMatch, ComponentDefinition componenDefinition) {
+                instantiateComponent(patternMatch, componenDefinition, Modality.MUST, false)
+        }
+
+        def instantiateComponent(IPatternMatch patternMatch, ComponentDefinition componenDefinition, Modality exists,
+                boolean allowMultiple) {
+                if (componentInstancesMap.containsKey(patternMatch)) {
+                        throw new IllegalArgumentException("Already instantiated component for match: " + patternMatch)
+                }
+                val componentTrace = new ComponentInstanceTrace(componentFaultTree, componenDefinition, nameGenerator,
+                        exists, allowMultiple)
+                componentInstancesMap.put(patternMatch, componentTrace)
+                componentTrace
+        }
+
+        def setTopLevel(ComponentInstanceTrace trace) {
+                if (componentFaultTree.topEvent !== null) {
+                        throw new IllegalArgumentException("Top level component already set")
+                }
+                val outputs = trace.outputs
+                if (outputs.size !== 1) {
+                        throw new IllegalArgumentException("Top level component must have 1 output, got " + outputs.size +
+                                " instead")
+                }
+                if (!trace.appearsExactlyOnce) {
+                        throw new IllegalArgumentException("Top level must appear in the fault tree exactly once")
+                }
+                componentFaultTree.topEvent = outputs.head
+        }
+
+        def lookup(IPatternMatch patternMatch) {
+                componentInstancesMap.get(patternMatch)
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentInstanceTrace.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentInstanceTrace.xtend
new file mode 100644
index 00000000..158ab2e1
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentInstanceTrace.xtend
@@ -0,0 +1,65 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import com.google.common.collect.Maps
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.CftFactory
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentDefinition
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentFaultTree
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.EventDeclaration
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.InputEvent
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Modality
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Output
+import java.util.Map
+
+import static extension hu.bme.mit.inf.dslreasoner.faulttree.model.util.CftExtensions.*
+
+class ComponentInstanceTrace {
+        val componentInstance = CftFactory.eINSTANCE.createComponent
+        val Map<InputEvent, InputTrace> inputEventsMap
+        val Map<EventDeclaration, Output> outputEventsMap
+
+        protected new(ComponentFaultTree faultTree, ComponentDefinition componentDefinition,
+                ComponentNameGenerator nameGenerator, Modality exists, boolean multipleAllowed) {
+                componentInstance.componentDefinition = componentDefinition
+                componentInstance.name = nameGenerator.nextName(componentDefinition)
+                componentInstance.exists = exists
+                componentInstance.multipleAllowed = multipleAllowed
+                inputEventsMap = Maps.newHashMapWithExpectedSize(componentDefinition.inputEvents.size)
+                for (inputEvent : componentDefinition.inputEvents) {
+                        val inputTrace = new InputTrace(componentInstance, inputEvent)
+                        inputEventsMap.put(inputEvent, inputTrace)
+                }
+                outputEventsMap = Maps.newHashMapWithExpectedSize(componentDefinition.outputEvents.size)
+                for (outputEvent : componentDefinition.outputEvents) {
+                        val output = CftFactory.eINSTANCE.createOutput
+                        output.eventDeclaration = outputEvent
+                        componentInstance.outputs += output
+                        outputEventsMap.put(outputEvent, output)
+                }
+                faultTree.components += componentInstance
+        }
+
+        def void assign(EventDeclaration inputEvent, ComponentInstanceTrace sourceComponent, EventDeclaration outputEvent) {
+                assign(inputEvent, sourceComponent, outputEvent, Modality.MUST)
+        }
+
+        def void assign(EventDeclaration inputEvent, ComponentInstanceTrace sourceComponent, EventDeclaration outputEvent,
+                Modality exists) {
+                val inputTrace = inputEventsMap.get(inputEvent)
+                if (inputTrace === null) {
+                        throw new IllegalArgumentException("Unknown input: " + inputEvent)
+                }
+                val output = sourceComponent.outputEventsMap.get(outputEvent)
+                if (output === null) {
+                        throw new IllegalArgumentException("Unknown output: " + outputEvent)
+                }
+                inputTrace.assign(output, exists)
+        }
+
+        protected def getOutputs() {
+                componentInstance.outputs
+        }
+
+        protected def appearsExactlyOnce() {
+                componentInstance.appearsExactlyOnce
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentNameGenerator.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentNameGenerator.xtend
new file mode 100644
index 00000000..71d40a9b
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/ComponentNameGenerator.xtend
@@ -0,0 +1,16 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.ComponentDefinition
+import java.util.Map
+
+class ComponentNameGenerator {
+        static val DEFAULT_NAME = "__unnamed"
+
+        val Map<ComponentDefinition, Integer> instanceCounts = newHashMap
+
+        def nextName(ComponentDefinition componentDefinition) {
+                val instanceCount = instanceCounts.getOrDefault(componentDefinition, 0)
+                instanceCounts.put(componentDefinition, instanceCount + 1)
+                (componentDefinition.name ?: DEFAULT_NAME) + instanceCount
+        }
+}
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
new file mode 100644
index 00000000..062de3df
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/Ecore2CftTransformation.xtend
@@ -0,0 +1,28 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import com.google.common.collect.ImmutableList
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.TransformationDefinition
+import java.util.List
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+
+class Ecore2CftTransformation {
+        val List<MappingHandler> mappingHandlers
+
+        new(TransformationDefinition transformationDefinition, ViatraQueryEngine viatraQueryEngine) {
+                val mappingQueries = new MappingQueries(transformationDefinition, viatraQueryEngine)
+                mappingHandlers = ImmutableList.copyOf(transformationDefinition.mappingDefinitions.map [ mappingDefinition |
+                        new MappingHandler(mappingDefinition, mappingQueries)
+                ])
+        }
+
+        def createComponentFaultTree() {
+                val trace = new ComponentFaultTreeTrace
+                for (handler : mappingHandlers) {
+                        handler.instantiateComponents(trace)
+                }
+                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/ecore2cft/InputTrace.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/InputTrace.xtend
new file mode 100644
index 00000000..b892eff1
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/InputTrace.xtend
@@ -0,0 +1,35 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.CftFactory
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Component
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Connection
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Input
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.InputEvent
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Modality
+import hu.bme.mit.inf.dslreasoner.faulttree.model.cft.Output
+import java.util.Map
+
+import static extension hu.bme.mit.inf.dslreasoner.faulttree.model.util.CftExtensions.*
+
+class InputTrace {
+        val Input input = CftFactory.eINSTANCE.createInput
+        val Map<Output, Connection> connectionsMap = newHashMap
+
+        protected new(Component component, InputEvent inputEvent) {
+                input.inputEvent = inputEvent
+                component.inputs += input
+        }
+
+        def void assign(Output output, Modality exists) {
+                val connection = connectionsMap.get(output)
+                if (connection === null) {
+                        val newConnection = CftFactory.eINSTANCE.createConnection
+                        newConnection.output = output
+                        newConnection.exists = exists
+                        input.incomingConnections += newConnection
+                        connectionsMap.put(output, newConnection)
+                } else if (exists.isMoreConcreteThan(connection.exists)) {
+                        connection.exists = exists
+                }
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/LookupHandler.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/LookupHandler.xtend
new file mode 100644
index 00000000..3a06dcc3
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/LookupHandler.xtend
@@ -0,0 +1,47 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.LookupDefinition
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingDefinition
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+
+class LookupHandler {
+        val int[] argumentIndices
+        val ViatraQueryMatcher<? extends IPatternMatch> lookedUpMatcher
+
+        new(MappingDefinition mappingDefinition, LookupDefinition lookupDefinition,
+                ViatraQueryMatcher<? extends IPatternMatch> lookedUpMatcher) {
+                if (lookupDefinition.eContainer != mappingDefinition) {
+                        throw new IllegalArgumentException("lookupDefinition must be contained in mappingDefinition")
+                }
+                val argumentCount = lookupDefinition.arguments.size
+                if (argumentCount != lookedUpMatcher.parameterNames.length) {
+                        throw new IllegalArgumentException(
+                                "lookupDefinition (name: " + lookupDefinition.mapping?.pattern?.name +
+                                        ") must have as many arguments as lookedUpMatcher (name: " + lookedUpMatcher.patternName + ")")
+                }
+                argumentIndices = newIntArrayOfSize(argumentCount)
+                for (var int i = 0; i < argumentCount; i++) {
+                        val argument = lookupDefinition.arguments.get(i)
+                        val argumentIndex = mappingDefinition.parameters.indexOf(argument)
+                        argumentIndices.set(i, argumentIndex)
+                }
+                this.lookedUpMatcher = lookedUpMatcher
+        }
+
+        def lookupForMatch(ComponentFaultTreeTrace faultTreeTrace, IPatternMatch match) {
+                val lookedUpMatch = createLookedUpMatch(match)
+                faultTreeTrace.lookup(lookedUpMatch)
+        }
+
+        private def createLookedUpMatch(IPatternMatch match) {
+                val lookedUpMatch = lookedUpMatcher.newEmptyMatch
+                val argumentCount = argumentIndices.length
+                for (var int i = 0; i < argumentCount; i++) {
+                        val argumentIndex = argumentIndices.get(i)
+                        var argumentValue = match.get(argumentIndex)
+                        lookedUpMatch.set(i, argumentValue)
+                }
+                lookedUpMatch
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingHandler.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingHandler.xtend
new file mode 100644
index 00000000..643af5c4
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingHandler.xtend
@@ -0,0 +1,91 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import com.google.common.collect.ImmutableMap
+import com.google.common.collect.Maps
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.LookupDefinition
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingDefinition
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.Variable
+import java.util.Map
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+
+class MappingHandler {
+        val ViatraQueryMatcher<? extends IPatternMatch> matcher
+        val MappingDefinition mappingDefinition
+        val Map<LookupDefinition, LookupHandler> lookupHandlers
+
+        new(MappingDefinition mappingDefinition, MappingQueries mappingQueries) {
+                matcher = mappingQueries.getMatcher(mappingDefinition)
+                this.mappingDefinition = mappingDefinition
+                val variables = newHashSet
+                for (assignment : mappingDefinition.assignments) {
+                        variables += assignment.input.component
+                        variables += assignment.output.component
+                }
+                lookupHandlers = ImmutableMap.copyOf(variables.filter(LookupDefinition).toMap([it], [ lookupDefinition |
+                        mappingQueries.createLookupHandler(mappingDefinition, lookupDefinition)
+                ]))
+        }
+
+        def instantiateComponents(ComponentFaultTreeTrace faultTreeTrace) {
+                if (!hasComponentInstace) {
+                        return
+                }
+                matcher.forEachMatch [ match |
+                        val componentTrace = faultTreeTrace.instantiateComponent(match, componentDefinition)
+                        if (isTopLevel) {
+                                faultTreeTrace.topLevel = componentTrace
+                        }
+                ]
+        }
+
+        def instantiateConnections(ComponentFaultTreeTrace faultTreeTrace) {
+                if (!hasConnections) {
+                        return
+                }
+                matcher.forEachMatch [ match |
+                        val lookedUpComponents = lookupComponents(faultTreeTrace, match)
+                        for (assignment : mappingDefinition.assignments) {
+                                val input = assignment.input
+                                val inputComponent = lookedUpComponents.get(input.component)
+                                val output = assignment.output
+                                val outputComponent = lookedUpComponents.get(output.component)
+                                if (inputComponent !== null && outputComponent !== null) {
+                                        inputComponent.assign(input.event, outputComponent, output.event)
+                                }
+                        }
+                ]
+        }
+
+        private def Map<Variable, ComponentInstanceTrace> lookupComponents(ComponentFaultTreeTrace faultTreeTrace,
+                IPatternMatch match) {
+                val lookedUpComponents = Maps.newHashMapWithExpectedSize(lookupHandlers.size + 1)
+                if (hasComponentInstace) {
+                        val componentInstance = faultTreeTrace.lookup(match)
+                        lookedUpComponents.put(mappingDefinition.componentInstance, componentInstance)
+                }
+                for (pair : lookupHandlers.entrySet) {
+                        val componentInstance = pair.value.lookupForMatch(faultTreeTrace, match)
+                        if (componentInstance !== null) {
+                                lookedUpComponents.put(pair.key, componentInstance)
+                        }
+                }
+                lookedUpComponents
+        }
+
+        private def getComponentDefinition() {
+                mappingDefinition.componentInstance?.componentType
+        }
+
+        private def hasComponentInstace() {
+                componentDefinition !== null
+        }
+
+        private def isTopLevel() {
+                mappingDefinition.topLevel
+        }
+
+        private def hasConnections() {
+                !mappingDefinition.assignments.empty
+        }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingQueries.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingQueries.xtend
new file mode 100644
index 00000000..6683b3f8
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/MappingQueries.xtend
@@ -0,0 +1,38 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.ecore2cft
+
+import com.google.common.collect.ImmutableMap
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.LookupDefinition
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.MappingDefinition
+import hu.bme.mit.inf.dslreasoner.faulttree.components.cftLanguage.TransformationDefinition
+import java.util.Map
+import org.eclipse.viatra.query.patternlanguage.emf.specification.SpecificationBuilder
+import org.eclipse.viatra.query.runtime.api.GenericQueryGroup
+import org.eclipse.viatra.query.runtime.api.IPatternMatch
+import org.eclipse.viatra.query.runtime.api.ViatraQueryEngine
+import org.eclipse.viatra.query.runtime.api.ViatraQueryMatcher
+
+class MappingQueries {
+        val Map<MappingDefinition, ViatraQueryMatcher<? extends IPatternMatch>> matchersMap
+
+        new(TransformationDefinition transformationDefinition, ViatraQueryEngine viatraQueryEngine) {
+                val specificationBuilder = new SpecificationBuilder
+                val querySpecificationsMap = transformationDefinition.mappingDefinitions.toMap([it], [
+                        specificationBuilder.getOrCreateSpecification(pattern)
+                ])
+                GenericQueryGroup.of(querySpecificationsMap.values).prepare(viatraQueryEngine)
+                matchersMap = ImmutableMap.copyOf(querySpecificationsMap.mapValues[getMatcher(viatraQueryEngine)])
+        }
+
+        def getMatcher(MappingDefinition mappingDefinition) {
+                val matcher = matchersMap.get(mappingDefinition)
+                if (matcher === null) {
+                        throw new IllegalArgumentException("Unknown mapping definition: " + mappingDefinition)
+                }
+                matcher
+        }
+        
+        def createLookupHandler(MappingDefinition mappingDefinition, LookupDefinition lookupDefinition) {
+                val lookedUpMatcher = getMatcher(lookupDefinition.mapping)
+                new LookupHandler(mappingDefinition, lookupDefinition, lookedUpMatcher)
+        }
+}
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..4a19e2cd
--- /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,57 @@
+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) {
+                // ft-diet (https://moves.rwth-aachen.de/ft-diet/) needs a dormancy factor.
+                '''«defineDistribution(basicEvent.distribution)» dorm=0.0'''
+        }
+
+        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..a250a955
--- /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,182 @@
+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
+
+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)
+
+        static val SIGNAL_EXIT_VALUE_OFFSET = 0x80
+        static val SIGXCPU = 24
+        static val SIGXFSZ = 25
+
+        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 + SIGXCPU:
+                                ReliabilityResult.TIMEOUT
+                        case STORM_MEMOUT,
+                        case SIGNAL_EXIT_VALUE_OFFSET + SIGXFSZ:
+                                ReliabilityResult.MEMOUT
+                        default: {
+                                if (exitValue > SIGNAL_EXIT_VALUE_OFFSET) {
+                                        val signalNumber = exitValue - SIGNAL_EXIT_VALUE_OFFSET
+                                        throw new StormDftException("Storm unexpectedly killed by signal " + signalNumber + ": " + 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)
+        }
+}