From 3f5aaab5025b8eb243f414b1c789085327df04f4 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Wed, 20 Mar 2019 16:09:09 +0100 Subject: Fault tree transformation for partial models WIP --- .../transformation/cft2ft/EventMaterializer.xtend | 8 ++++++-- .../ecore2cft/ComponentFaultTreeTrace.xtend | 12 +++++++++++- .../ecore2cft/ComponentInstanceTrace.xtend | 18 ++++++++++++++++-- .../transformation/ecore2cft/InputTrace.xtend | 8 +++++++- .../ft2galileo/Ft2GalileoTransformation.xtend | 9 +++++---- .../transformation/solver/StormDftHandler.xtend | 16 ++++++---------- 6 files changed, 51 insertions(+), 20 deletions(-) (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit') 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 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 inputEventsMap val Map 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 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) } -- cgit v1.2.3-70-g09d2