4 files changed, 325 insertions, 0 deletions

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)
+        }
+}