12 files changed, 660 insertions, 0 deletions

diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin
new file mode 100644
index 00000000..57c4608d
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin
new file mode 100644
index 00000000..f5cb52f4
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin
new file mode 100644
index 00000000..5dad0728
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin
new file mode 100644
index 00000000..abd8a501
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore
new file mode 100644
index 00000000..59cc8fe8
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore
@@ -0,0 +1,9 @@
+/.StormDftSolver.java._trace
+/.StormDftConfiguration.java._trace
+/.StormDftMttfConfiguration.java._trace
+/.FtAnalysisObjective.java._trace
+/.ApproximationHeuristic.java._trace
+/.StormDftHandler.java._trace
+/.StormDftException.java._trace
+/.ReliabilityModelSolution.java._trace
+/.ReliabilityResult.java._trace
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java
new file mode 100644
index 00000000..822d4f36
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java
@@ -0,0 +1,8 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+@SuppressWarnings("all")
+public enum ApproximationHeuristic {
+  NONE,
+  
+  DEPTH;
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java
new file mode 100644
index 00000000..528ada42
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java
@@ -0,0 +1,14 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+@SuppressWarnings("all")
+public abstract class FtAnalysisObjective {
+  public static final class TimeBound extends FtAnalysisObjective {
+    public double timeBound = 0;
+  }
+  
+  public static final FtAnalysisObjective MTTF = new FtAnalysisObjective() {
+  };
+  
+  private FtAnalysisObjective() {
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java
new file mode 100644
index 00000000..c8c8b000
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java
@@ -0,0 +1,156 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import org.eclipse.xtend.lib.annotations.Data;
+import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor;
+import org.eclipse.xtext.xbase.lib.Pure;
+import org.eclipse.xtext.xbase.lib.util.ToStringBuilder;
+
+@SuppressWarnings("all")
+public abstract class ReliabilityResult {
+  @Data
+  public static final class Solution extends ReliabilityResult {
+    private final double lowerBound;
+    
+    private final double upperBound;
+    
+    public Solution(final double value) {
+      this(value, value);
+    }
+    
+    public Solution(final double lowerBound, final double upperBound) {
+      if ((lowerBound > upperBound)) {
+        throw new IllegalArgumentException("lowerBound must not be larger than upperBound");
+      }
+      this.lowerBound = lowerBound;
+      this.upperBound = upperBound;
+    }
+    
+    @Override
+    public ReliabilityResult.Solution getOrThrow() {
+      return this;
+    }
+    
+    @Override
+    @Pure
+    public int hashCode() {
+      final int prime = 31;
+      int result = 1;
+      result = prime * result + (int) (Double.doubleToLongBits(this.lowerBound) ^ (Double.doubleToLongBits(this.lowerBound) >>> 32));
+      return prime * result + (int) (Double.doubleToLongBits(this.upperBound) ^ (Double.doubleToLongBits(this.upperBound) >>> 32));
+    }
+    
+    @Override
+    @Pure
+    public boolean equals(final Object obj) {
+      if (this == obj)
+        return true;
+      if (obj == null)
+        return false;
+      if (getClass() != obj.getClass())
+        return false;
+      ReliabilityResult.Solution other = (ReliabilityResult.Solution) obj;
+      if (Double.doubleToLongBits(other.lowerBound) != Double.doubleToLongBits(this.lowerBound))
+        return false; 
+      if (Double.doubleToLongBits(other.upperBound) != Double.doubleToLongBits(this.upperBound))
+        return false; 
+      return true;
+    }
+    
+    @Override
+    @Pure
+    public String toString() {
+      return new ToStringBuilder(this)
+        .addAllFields()
+        .toString();
+    }
+    
+    @Pure
+    public double getLowerBound() {
+      return this.lowerBound;
+    }
+    
+    @Pure
+    public double getUpperBound() {
+      return this.upperBound;
+    }
+  }
+  
+  @Data
+  public static final class Unknown extends ReliabilityResult {
+    private final String message;
+    
+    private final Throwable cause;
+    
+    @FinalFieldsConstructor
+    public Unknown(final String message, final Throwable cause) {
+      super();
+      this.message = message;
+      this.cause = cause;
+    }
+    
+    public Unknown(final String message) {
+      this(message, null);
+    }
+    
+    @Override
+    public ReliabilityResult.Solution getOrThrow() {
+      throw new RuntimeException(this.message, this.cause);
+    }
+    
+    @Override
+    @Pure
+    public int hashCode() {
+      final int prime = 31;
+      int result = 1;
+      result = prime * result + ((this.message== null) ? 0 : this.message.hashCode());
+      return prime * result + ((this.cause== null) ? 0 : this.cause.hashCode());
+    }
+    
+    @Override
+    @Pure
+    public boolean equals(final Object obj) {
+      if (this == obj)
+        return true;
+      if (obj == null)
+        return false;
+      if (getClass() != obj.getClass())
+        return false;
+      ReliabilityResult.Unknown other = (ReliabilityResult.Unknown) obj;
+      if (this.message == null) {
+        if (other.message != null)
+          return false;
+      } else if (!this.message.equals(other.message))
+        return false;
+      if (this.cause == null) {
+        if (other.cause != null)
+          return false;
+      } else if (!this.cause.equals(other.cause))
+        return false;
+      return true;
+    }
+    
+    @Override
+    @Pure
+    public String toString() {
+      return new ToStringBuilder(this)
+        .addAllFields()
+        .toString();
+    }
+    
+    @Pure
+    public String getMessage() {
+      return this.message;
+    }
+    
+    @Pure
+    public Throwable getCause() {
+      return this.cause;
+    }
+  }
+  
+  public static final ReliabilityResult.Unknown TIMEOUT = new ReliabilityResult.Unknown("Solver timed out");
+  
+  public static final ReliabilityResult.Unknown MEMOUT = new ReliabilityResult.Unknown("Solver out of memory");
+  
+  public abstract ReliabilityResult.Solution getOrThrow();
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java
new file mode 100644
index 00000000..e1bb3625
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java
@@ -0,0 +1,31 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import com.google.common.base.Objects;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
+import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration;
+
+@SuppressWarnings("all")
+public final class StormDftConfiguration extends SolverConfiguration {
+  public static final String 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 ApproximationHeuristic approximationHeuristic = ApproximationHeuristic.NONE;
+  
+  public FtAnalysisObjective objective;
+  
+  public boolean isApproximationInUse() {
+    return (!Objects.equal(this.approximationHeuristic, ApproximationHeuristic.NONE));
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java
new file mode 100644
index 00000000..955c9ed1
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java
@@ -0,0 +1,12 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+@SuppressWarnings("all")
+public class StormDftException extends RuntimeException {
+  public StormDftException(final String s) {
+    super(s);
+  }
+  
+  public StormDftException(final String s, final Exception e) {
+    super(s, e);
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java
new file mode 100644
index 00000000..003d9cc5
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java
@@ -0,0 +1,351 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import com.google.common.base.Objects;
+import com.google.common.collect.ImmutableList;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftException;
+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.ArrayList;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+import jnr.constants.platform.Signal;
+import org.apache.commons.lang.SystemUtils;
+import org.eclipse.xtend2.lib.StringConcatenation;
+import org.eclipse.xtext.xbase.lib.CollectionLiterals;
+import org.eclipse.xtext.xbase.lib.Conversions;
+import org.eclipse.xtext.xbase.lib.Exceptions;
+import org.eclipse.xtext.xbase.lib.Extension;
+import org.eclipse.xtext.xbase.lib.Functions.Function0;
+import org.eclipse.xtext.xbase.lib.Functions.Function1;
+import org.eclipse.xtext.xbase.lib.InputOutput;
+import org.eclipse.xtext.xbase.lib.IterableExtensions;
+
+@SuppressWarnings("all")
+public class StormDftHandler {
+  private static final String DOUBLE_REGEX = "[-+]?[0-9]*\\.?[0-9]+([eE][-+]?[0-9]+)?";
+  
+  private static final String SINGLE_RESULT_GROUP = "single";
+  
+  private static final String LOWER_BOUND_GROUP = "lower";
+  
+  private static final String UPPER_BOUND_GROUP = "upper";
+  
+  private static final String RESULT_REGEX = new Function0<String>() {
+    public String apply() {
+      StringConcatenation _builder = new StringConcatenation();
+      _builder.append("^Result:\\s*\\[(?:(?<");
+      _builder.append(StormDftHandler.SINGLE_RESULT_GROUP);
+      _builder.append(">");
+      _builder.append(StormDftHandler.DOUBLE_REGEX);
+      _builder.append(")|\\((?<");
+      _builder.append(StormDftHandler.LOWER_BOUND_GROUP);
+      _builder.append(">");
+      _builder.append(StormDftHandler.DOUBLE_REGEX);
+      _builder.append("),\\s*(?<");
+      _builder.append(StormDftHandler.UPPER_BOUND_GROUP);
+      _builder.append(">");
+      _builder.append(StormDftHandler.DOUBLE_REGEX);
+      _builder.append(")\\))\\]");
+      return _builder.toString();
+    }
+  }.apply();
+  
+  private static final Pattern RESULT_PATTERN = Pattern.compile(StormDftHandler.RESULT_REGEX);
+  
+  private static final int SIGNAL_EXIT_VALUE_OFFSET = new Function0<Integer>() {
+    public Integer apply() {
+      int _xifexpression = (int) 0;
+      if (SystemUtils.IS_OS_SOLARIS) {
+        _xifexpression = 0;
+      } else {
+        _xifexpression = 0x80;
+      }
+      return _xifexpression;
+    }
+  }.apply().intValue();
+  
+  private static final int STORM_GENERAL_ERROR = ((-1) & 0xff);
+  
+  private static final int STORM_TIMEOUT = ((-2) & 0xff);
+  
+  private static final int STORM_MEMOUT = ((-3) & 0xff);
+  
+  public ReliabilityResult callSolver(final String dftFilePath, final StormDftConfiguration configuration) {
+    try {
+      ReliabilityResult _xblockexpression = null;
+      {
+        final ImmutableList<String> commandLine = this.toCommandLine(configuration, dftFilePath);
+        final DocumentationLevel documentationLevel = configuration.documentationLevel;
+        final boolean printOutput = (Objects.equal(documentationLevel, DocumentationLevel.NORMAL) || 
+          Objects.equal(documentationLevel, DocumentationLevel.FULL));
+        final ProcessBuilder processBuilder = new ProcessBuilder().command(commandLine);
+        Process process = null;
+        ReliabilityResult _xtrycatchfinallyexpression = null;
+        try {
+          ReliabilityResult _xtrycatchfinallyexpression_1 = null;
+          try {
+            ReliabilityResult _xblockexpression_1 = null;
+            {
+              process = processBuilder.start();
+              process.getOutputStream().close();
+              final ReliabilityResult.Solution result = this.readOutput(process.getInputStream(), printOutput);
+              final String error = this.readError(process.getErrorStream(), printOutput);
+              final int exitValue = process.waitFor();
+              ReliabilityResult _xifexpression = null;
+              if ((result == null)) {
+                _xifexpression = this.interpretExitStatus(exitValue, error);
+              } else {
+                _xifexpression = result;
+              }
+              _xblockexpression_1 = _xifexpression;
+            }
+            _xtrycatchfinallyexpression_1 = _xblockexpression_1;
+          } catch (final Throwable _t) {
+            if (_t instanceof IOException) {
+              final IOException e = (IOException)_t;
+              throw new StormDftException("Error during input/output handling of the stochastic solver.", e);
+            } else {
+              throw Exceptions.sneakyThrow(_t);
+            }
+          }
+          _xtrycatchfinallyexpression = _xtrycatchfinallyexpression_1;
+        } catch (final Throwable _t_1) {
+          if (_t_1 instanceof Exception) {
+            final Exception e_1 = (Exception)_t_1;
+            if ((process != null)) {
+              process.destroyForcibly().waitFor();
+            }
+            throw e_1;
+          } else {
+            throw Exceptions.sneakyThrow(_t_1);
+          }
+        }
+        _xblockexpression = _xtrycatchfinallyexpression;
+      }
+      return _xblockexpression;
+    } catch (Throwable _e) {
+      throw Exceptions.sneakyThrow(_e);
+    }
+  }
+  
+  private ImmutableList<String> toCommandLine(@Extension final StormDftConfiguration configuration, final String dftFilePath) {
+    ImmutableList<String> _xblockexpression = null;
+    {
+      @Extension
+      final ImmutableList.Builder<String> optionsBuilder = ImmutableList.<String>builder();
+      String _elvis = null;
+      if (configuration.solverPath != null) {
+        _elvis = configuration.solverPath;
+      } else {
+        _elvis = StormDftConfiguration.DEFAULT_SOLVER_PATH;
+      }
+      optionsBuilder.add(_elvis);
+      if ((configuration.runtimeLimit != SolverConfiguration.Unlimited)) {
+        optionsBuilder.add("--timeout", Integer.valueOf(configuration.runtimeLimit).toString());
+      }
+      optionsBuilder.add("--precision", Double.valueOf(configuration.precision).toString());
+      if (configuration.bisimulation) {
+        optionsBuilder.add("--bisimulation");
+      }
+      if (configuration.symmetryReduction) {
+        optionsBuilder.add("--symmetryreduction");
+      }
+      if (configuration.modularization) {
+        optionsBuilder.add("--modularisation");
+      }
+      if ((!configuration.dontCarePropagation)) {
+        optionsBuilder.add("--disabledc");
+      }
+      boolean _isApproximationInUse = configuration.isApproximationInUse();
+      if (_isApproximationInUse) {
+        String _switchResult = null;
+        final ApproximationHeuristic approximationHeuristic = configuration.approximationHeuristic;
+        if (approximationHeuristic != null) {
+          switch (approximationHeuristic) {
+            case DEPTH:
+              _switchResult = "depth";
+              break;
+            default:
+              throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic));
+          }
+        } else {
+          throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic));
+        }
+        final String heuristicName = _switchResult;
+        optionsBuilder.add("--approximation", Double.valueOf(configuration.approximation).toString(), "--approximationheuristic", heuristicName);
+      }
+      optionsBuilder.add("--dftfile", dftFilePath);
+      final FtAnalysisObjective objective = configuration.objective;
+      boolean _matched = false;
+      if (Objects.equal(objective, FtAnalysisObjective.MTTF)) {
+        _matched=true;
+        optionsBuilder.add("--expectedtime");
+      }
+      if (!_matched) {
+        if (objective instanceof FtAnalysisObjective.TimeBound) {
+          _matched=true;
+          optionsBuilder.add("--timebound");
+        }
+      }
+      if (!_matched) {
+        throw new IllegalArgumentException(("Unknown analysis objective: " + configuration.objective));
+      }
+      boolean _equals = Objects.equal(configuration.documentationLevel, DocumentationLevel.FULL);
+      if (_equals) {
+        optionsBuilder.add("--verbose");
+      }
+      _xblockexpression = optionsBuilder.build();
+    }
+    return _xblockexpression;
+  }
+  
+  private ReliabilityResult.Solution readOutput(final InputStream inputStream, final boolean printOutput) {
+    try {
+      Object _xblockexpression = null;
+      {
+        InputStreamReader _inputStreamReader = new InputStreamReader(inputStream);
+        final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader);
+        try {
+          String line = null;
+          while (((line = bufferedReader.readLine()) != null)) {
+            {
+              if (printOutput) {
+                InputOutput.<String>println(line);
+              }
+              final Matcher matcher = StormDftHandler.RESULT_PATTERN.matcher(line);
+              boolean _find = matcher.find();
+              if (_find) {
+                try {
+                  final String single = matcher.group(StormDftHandler.SINGLE_RESULT_GROUP);
+                  if ((single != null)) {
+                    final double singleValue = Double.parseDouble(single);
+                    return new ReliabilityResult.Solution(singleValue);
+                  }
+                  final String lower = matcher.group(StormDftHandler.LOWER_BOUND_GROUP);
+                  final String upper = matcher.group(StormDftHandler.UPPER_BOUND_GROUP);
+                  if (((lower != null) && (upper != null))) {
+                    final double lowerValue = Double.parseDouble(lower);
+                    final double upperValue = Double.parseDouble(upper);
+                    return new ReliabilityResult.Solution(lowerValue, upperValue);
+                  }
+                  throw new StormDftException(("Inconsistent stochastic solver output: " + line));
+                } catch (final Throwable _t) {
+                  if (_t instanceof NumberFormatException) {
+                    final NumberFormatException e = (NumberFormatException)_t;
+                    throw new StormDftException("Malformatted number from stochastic solver.", e);
+                  } else {
+                    throw Exceptions.sneakyThrow(_t);
+                  }
+                }
+              }
+            }
+          }
+        } finally {
+          bufferedReader.close();
+        }
+        _xblockexpression = null;
+      }
+      return ((ReliabilityResult.Solution)_xblockexpression);
+    } catch (Throwable _e) {
+      throw Exceptions.sneakyThrow(_e);
+    }
+  }
+  
+  private String readError(final InputStream inputStream, final boolean printOutput) {
+    try {
+      String _xblockexpression = null;
+      {
+        InputStreamReader _inputStreamReader = new InputStreamReader(inputStream);
+        final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader);
+        String _xtrycatchfinallyexpression = null;
+        try {
+          String _xblockexpression_1 = null;
+          {
+            final ArrayList<String> lines = CollectionLiterals.<String>newArrayList();
+            String line = null;
+            while (((line = bufferedReader.readLine()) != null)) {
+              {
+                if (printOutput) {
+                  System.err.println(line);
+                }
+                lines.add(line);
+              }
+            }
+            _xblockexpression_1 = IterableExtensions.join(lines, "\n");
+          }
+          _xtrycatchfinallyexpression = _xblockexpression_1;
+        } finally {
+          bufferedReader.close();
+        }
+        _xblockexpression = _xtrycatchfinallyexpression;
+      }
+      return _xblockexpression;
+    } catch (Throwable _e) {
+      throw Exceptions.sneakyThrow(_e);
+    }
+  }
+  
+  private ReliabilityResult.Unknown interpretExitStatus(final int exitValue, final String error) {
+    ReliabilityResult.Unknown _switchResult = null;
+    boolean _matched = false;
+    if (Objects.equal(exitValue, StormDftHandler.STORM_GENERAL_ERROR)) {
+      _matched=true;
+      throw new StormDftException(("Storm error: " + error));
+    }
+    if (!_matched) {
+      if (Objects.equal(exitValue, StormDftHandler.STORM_TIMEOUT)) {
+        _matched=true;
+      }
+      if (!_matched) {
+        int _intValue = Signal.SIGXCPU.intValue();
+        int _plus = (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + _intValue);
+        if (Objects.equal(exitValue, _plus)) {
+          _matched=true;
+        }
+      }
+      if (_matched) {
+        _switchResult = ReliabilityResult.TIMEOUT;
+      }
+    }
+    if (!_matched) {
+      if (Objects.equal(exitValue, StormDftHandler.STORM_MEMOUT)) {
+        _matched=true;
+      }
+      if (!_matched) {
+        int _intValue_1 = Signal.SIGXFSZ.intValue();
+        int _plus_1 = (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + _intValue_1);
+        if (Objects.equal(exitValue, _plus_1)) {
+          _matched=true;
+        }
+      }
+      if (_matched) {
+        _switchResult = ReliabilityResult.MEMOUT;
+      }
+    }
+    if (!_matched) {
+      {
+        if ((exitValue > StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET)) {
+          final int signalNumber = (exitValue - StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET);
+          final Function1<Signal, Boolean> _function = (Signal it) -> {
+            int _intValue_2 = it.intValue();
+            return Boolean.valueOf((_intValue_2 == signalNumber));
+          };
+          final Signal signal = IterableExtensions.<Signal>findFirst(((Iterable<Signal>)Conversions.doWrapArray(Signal.values())), _function);
+          if ((signal != null)) {
+            throw new StormDftException(((("Storm unexpectedly killed by signal " + signal) + ": ") + error));
+          }
+        }
+        throw new StormDftException(((("Storm unexpectedly exit with status " + Integer.valueOf(exitValue)) + ": ") + error));
+      }
+    }
+    return _switchResult;
+  }
+}
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java
new file mode 100644
index 00000000..491e7fc1
--- /dev/null
+++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java
@@ -0,0 +1,79 @@
+package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
+
+import com.google.common.base.Objects;
+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.faulttree.transformation.solver.FtAnalysisObjective;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration;
+import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftHandler;
+import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
+
+@SuppressWarnings("all")
+public class StormDftSolver {
+  private static final String DFT_FILE_NAME = "ft.dft";
+  
+  private final Ft2GalileoTransformation ft2Galileo = new Ft2GalileoTransformation();
+  
+  private final StormDftHandler handler = new StormDftHandler();
+  
+  public ReliabilityResult solve(final ReliabilityModel reliabilityModel, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) {
+    ReliabilityResult _switchResult = null;
+    boolean _matched = false;
+    if (reliabilityModel instanceof FaultTree) {
+      _matched=true;
+      _switchResult = this.solve(((FaultTree)reliabilityModel), configuration, reasonerWorkspace);
+    }
+    if (!_matched) {
+      if (reliabilityModel instanceof ConstantModel) {
+        _matched=true;
+        ReliabilityResult.Solution _xblockexpression = null;
+        {
+          double _xifexpression = (double) 0;
+          boolean _isFailed = ((ConstantModel)reliabilityModel).isFailed();
+          if (_isFailed) {
+            _xifexpression = 0;
+          } else {
+            double _switchResult_1 = (double) 0;
+            final FtAnalysisObjective objective = configuration.objective;
+            boolean _matched_1 = false;
+            if (Objects.equal(objective, FtAnalysisObjective.MTTF)) {
+              _matched_1=true;
+              _switchResult_1 = Double.POSITIVE_INFINITY;
+            }
+            if (!_matched_1) {
+              if (objective instanceof FtAnalysisObjective.TimeBound) {
+                _matched_1=true;
+                _switchResult_1 = 1;
+              }
+            }
+            if (!_matched_1) {
+              throw new IllegalArgumentException(("Unknown objective: " + objective));
+            }
+            _xifexpression = _switchResult_1;
+          }
+          final double result = _xifexpression;
+          _xblockexpression = new ReliabilityResult.Solution(result);
+        }
+        _switchResult = _xblockexpression;
+      }
+    }
+    if (!_matched) {
+      throw new IllegalArgumentException(("Unknown reliability model: " + reliabilityModel));
+    }
+    return _switchResult;
+  }
+  
+  public ReliabilityResult solve(final FaultTree faultTree, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) {
+    ReliabilityResult _xblockexpression = null;
+    {
+      final CharSequence galileo = this.ft2Galileo.toGalileo(faultTree);
+      reasonerWorkspace.writeText(StormDftSolver.DFT_FILE_NAME, galileo);
+      final String dftFilePath = reasonerWorkspace.getFile(StormDftSolver.DFT_FILE_NAME).getAbsolutePath();
+      _xblockexpression = this.handler.callSolver(dftFilePath, configuration);
+    }
+    return _xblockexpression;
+  }
+}