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 --- .../transformation/solver/StormDftHandler.java | 351 +++++++++++++++++++++ 1 file changed, 351 insertions(+) create mode 100644 Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java') 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; + } +} -- cgit v1.2.3-54-g00ecf