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 --- .../solver/.ReliabilityResult.xtendbin | Bin 0 -> 5435 bytes .../solver/.StormDftConfiguration.xtendbin | Bin 0 -> 4311 bytes .../solver/.StormDftHandler.xtendbin | Bin 0 -> 13615 bytes .../transformation/solver/.StormDftSolver.xtendbin | Bin 0 -> 4801 bytes .../faulttree/transformation/solver/.gitignore | 9 + .../solver/ApproximationHeuristic.java | 8 + .../transformation/solver/FtAnalysisObjective.java | 14 + .../transformation/solver/ReliabilityResult.java | 156 +++++++++ .../solver/StormDftConfiguration.java | 31 ++ .../transformation/solver/StormDftException.java | 12 + .../transformation/solver/StormDftHandler.java | 351 +++++++++++++++++++++ .../transformation/solver/StormDftSolver.java | 79 +++++ 12 files changed, 660 insertions(+) create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver') 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 Binary files /dev/null and b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin differ 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 Binary files /dev/null and b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin differ 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 Binary files /dev/null and b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin differ 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 Binary files /dev/null and b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin differ 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() { + 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() { + 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 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 toCommandLine(@Extension final StormDftConfiguration configuration, final String dftFilePath) { + ImmutableList _xblockexpression = null; + { + @Extension + final ImmutableList.Builder optionsBuilder = ImmutableList.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.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 lines = CollectionLiterals.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 _function = (Signal it) -> { + int _intValue_2 = it.intValue(); + return Boolean.valueOf((_intValue_2 == signalNumber)); + }; + final Signal signal = IterableExtensions.findFirst(((Iterable)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; + } +} -- cgit v1.2.3-70-g09d2