From d90bedacaafe87e06fddaa05a6ff9b7b796e97e7 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Sat, 16 Feb 2019 00:43:11 +0100 Subject: Two-valued fault tree analyzer WIP --- .../cft2ft/Cft2FtTransformation.xtend | 20 ++- .../transformation/cft2ft/EventCollection.xtend | 90 ++++++++++ .../transformation/cft2ft/EventMaterializer.xtend | 192 +++++++++++++++++++++ .../transformation/cft2ft/FaultTreeBuilder.xtend | 39 +++++ .../ecore2cft/Ecore2CftTransformation.xtend | 1 + .../ft2galileo/Ft2GalileoTransformation.xtend | 56 ++++++ .../transformation/solver/ReliabilityResult.xtend | 51 ++++++ .../solver/StormDftConfiguration.xtend | 45 +++++ .../transformation/solver/StormDftHandler.xtend | 186 ++++++++++++++++++++ .../transformation/solver/StormDftSolver.xtend | 43 +++++ 10 files changed, 720 insertions(+), 3 deletions(-) create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventCollection.xtend create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/EventMaterializer.xtend create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/cft2ft/FaultTreeBuilder.xtend create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/ft2galileo/Ft2GalileoTransformation.xtend create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend (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/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 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.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, Event> materializationCache = newHashMap + val Map, EventCollection> multipleInputCache = newHashMap + val ConstantEvent falseEvent + val ConstantEvent trueEvent + val path = new LinkedHashSet> + + 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 eventKey) { + if (!path.add(eventKey)) { + throw new IllegalStateException( + '''Circular dependency [«FOR ancestor : path»«ancestor», «ENDFOR»«eventKey»] detected''') + } + } + + private def popEventKey(EventKey eventKey) { + path.remove(eventKey) + } + + @Data + protected static class EventKey { + 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 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) + } +} -- cgit v1.2.3-54-g00ecf