6 files changed, 51 insertions, 20 deletions

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
index c9aefe51..6b3ed0d0 100644
--- 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
@@ -17,6 +17,8 @@ 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
 
@@ -169,8 +171,10 @@ class EventMaterializer {
                 val input = findInput(component, inputEvent)
                 val builder = EventCollection.builder
                 for (connection : input.incomingConnections) {
-                        val materializedEvent = getOrMaterialize(connection.output)
-                        builder.add(materializedEvent)
+                        if (connection.isCurrentlyConnected) {
+                                val materializedEvent = getOrMaterialize(connection.output)
+                                builder.add(materializedEvent)
+                        }
                 }
                 builder.build
         }
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
index 7a3e377b..10c91fb4 100644
--- 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
@@ -2,6 +2,7 @@ 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
@@ -13,10 +14,16 @@ class ComponentFaultTreeTrace {
         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)
+                val componentTrace = new ComponentInstanceTrace(componentFaultTree, componenDefinition, nameGenerator,
+                        exists, allowMultiple)
                 componentInstancesMap.put(patternMatch, componentTrace)
                 componentTrace
         }
@@ -30,6 +37,9 @@ class ComponentFaultTreeTrace {
                         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
         }
 
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
index 7353bfe5..158ab2e1 100644
--- 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
@@ -6,18 +6,23 @@ 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) {
+                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)
@@ -34,6 +39,11 @@ class ComponentInstanceTrace {
         }
 
         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)
@@ -42,10 +52,14 @@ class ComponentInstanceTrace {
                 if (output === null) {
                         throw new IllegalArgumentException("Unknown output: " + outputEvent)
                 }
-                inputTrace.assign(output)
+                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/InputTrace.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ecore2cft/InputTrace.xtend
index c529a09b..b892eff1 100644
--- 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
@@ -5,9 +5,12 @@ 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
@@ -17,13 +20,16 @@ class InputTrace {
                 component.inputs += input
         }
 
-        def void assign(Output output) {
+        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/ft2galileo/Ft2GalileoTransformation.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.xtend
index 732d9fed..4a19e2cd 100644
--- 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
@@ -14,14 +14,15 @@ import org.eclipse.xtend2.lib.StringConcatenationClient
 
 class Ft2GalileoTransformation {
         def toGalileo(FaultTree faultTree) '''
-                toplevel «faultTree.topEvent.name»;
+                toplevel "«faultTree.topEvent.name»";
                 «FOR event : faultTree.events»
-                        «event.name» «defineEvent(event)»;
+                        "«event.name»" «defineEvent(event)»;
                 «ENDFOR»
         '''
 
         protected dispatch def defineEvent(BasicEvent basicEvent) {
-                defineDistribution(basicEvent.distribution)
+                // 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) {
@@ -37,7 +38,7 @@ class Ft2GalileoTransformation {
         }
 
         protected dispatch def StringConcatenationClient defineEvent(Gate gate) {
-                '''«defineGate(gate)» «FOR input : gate.inputEvents SEPARATOR " "»«input.name»«ENDFOR»'''
+                '''«defineGate(gate)» «FOR input : gate.inputEvents SEPARATOR " "»"«input.name»"«ENDFOR»'''
         }
 
         protected dispatch def StringConcatenationClient defineGate(AndGate gate) '''and'''
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
index 91c6a0d0..a250a955 100644
--- 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
@@ -8,8 +8,6 @@ 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) {
@@ -29,8 +27,9 @@ class StormDftHandler {
         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 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)
@@ -166,18 +165,15 @@ class StormDftHandler {
                         case STORM_GENERAL_ERROR:
                                 throw new StormDftException("Storm error: " + error)
                         case STORM_TIMEOUT,
-                        case SIGNAL_EXIT_VALUE_OFFSET + Signal.SIGXCPU.intValue:
+                        case SIGNAL_EXIT_VALUE_OFFSET + SIGXCPU:
                                 ReliabilityResult.TIMEOUT
                         case STORM_MEMOUT,
-                        case SIGNAL_EXIT_VALUE_OFFSET + Signal.SIGXFSZ.intValue:
+                        case SIGNAL_EXIT_VALUE_OFFSET + SIGXFSZ:
                                 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 killed by signal " + signalNumber + ": " + error)
                                 }
                                 throw new StormDftException("Storm unexpectedly exit with status " + exitValue + ": " + error)
                         }