diff options
Diffstat (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver')
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 | |||
Binary files 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 --- /dev/null +++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin | |||
Binary files 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 --- /dev/null +++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin | |||
Binary files 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 @@ | |||
1 | /.StormDftSolver.java._trace | ||
2 | /.StormDftConfiguration.java._trace | ||
3 | /.StormDftMttfConfiguration.java._trace | ||
4 | /.FtAnalysisObjective.java._trace | ||
5 | /.ApproximationHeuristic.java._trace | ||
6 | /.StormDftHandler.java._trace | ||
7 | /.StormDftException.java._trace | ||
8 | /.ReliabilityModelSolution.java._trace | ||
9 | /.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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public enum ApproximationHeuristic { | ||
5 | NONE, | ||
6 | |||
7 | DEPTH; | ||
8 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public abstract class FtAnalysisObjective { | ||
5 | public static final class TimeBound extends FtAnalysisObjective { | ||
6 | public double timeBound = 0; | ||
7 | } | ||
8 | |||
9 | public static final FtAnalysisObjective MTTF = new FtAnalysisObjective() { | ||
10 | }; | ||
11 | |||
12 | private FtAnalysisObjective() { | ||
13 | } | ||
14 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | import org.eclipse.xtend.lib.annotations.Data; | ||
4 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor; | ||
5 | import org.eclipse.xtext.xbase.lib.Pure; | ||
6 | import org.eclipse.xtext.xbase.lib.util.ToStringBuilder; | ||
7 | |||
8 | @SuppressWarnings("all") | ||
9 | public abstract class ReliabilityResult { | ||
10 | @Data | ||
11 | public static final class Solution extends ReliabilityResult { | ||
12 | private final double lowerBound; | ||
13 | |||
14 | private final double upperBound; | ||
15 | |||
16 | public Solution(final double value) { | ||
17 | this(value, value); | ||
18 | } | ||
19 | |||
20 | public Solution(final double lowerBound, final double upperBound) { | ||
21 | if ((lowerBound > upperBound)) { | ||
22 | throw new IllegalArgumentException("lowerBound must not be larger than upperBound"); | ||
23 | } | ||
24 | this.lowerBound = lowerBound; | ||
25 | this.upperBound = upperBound; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public ReliabilityResult.Solution getOrThrow() { | ||
30 | return this; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | @Pure | ||
35 | public int hashCode() { | ||
36 | final int prime = 31; | ||
37 | int result = 1; | ||
38 | result = prime * result + (int) (Double.doubleToLongBits(this.lowerBound) ^ (Double.doubleToLongBits(this.lowerBound) >>> 32)); | ||
39 | return prime * result + (int) (Double.doubleToLongBits(this.upperBound) ^ (Double.doubleToLongBits(this.upperBound) >>> 32)); | ||
40 | } | ||
41 | |||
42 | @Override | ||
43 | @Pure | ||
44 | public boolean equals(final Object obj) { | ||
45 | if (this == obj) | ||
46 | return true; | ||
47 | if (obj == null) | ||
48 | return false; | ||
49 | if (getClass() != obj.getClass()) | ||
50 | return false; | ||
51 | ReliabilityResult.Solution other = (ReliabilityResult.Solution) obj; | ||
52 | if (Double.doubleToLongBits(other.lowerBound) != Double.doubleToLongBits(this.lowerBound)) | ||
53 | return false; | ||
54 | if (Double.doubleToLongBits(other.upperBound) != Double.doubleToLongBits(this.upperBound)) | ||
55 | return false; | ||
56 | return true; | ||
57 | } | ||
58 | |||
59 | @Override | ||
60 | @Pure | ||
61 | public String toString() { | ||
62 | return new ToStringBuilder(this) | ||
63 | .addAllFields() | ||
64 | .toString(); | ||
65 | } | ||
66 | |||
67 | @Pure | ||
68 | public double getLowerBound() { | ||
69 | return this.lowerBound; | ||
70 | } | ||
71 | |||
72 | @Pure | ||
73 | public double getUpperBound() { | ||
74 | return this.upperBound; | ||
75 | } | ||
76 | } | ||
77 | |||
78 | @Data | ||
79 | public static final class Unknown extends ReliabilityResult { | ||
80 | private final String message; | ||
81 | |||
82 | private final Throwable cause; | ||
83 | |||
84 | @FinalFieldsConstructor | ||
85 | public Unknown(final String message, final Throwable cause) { | ||
86 | super(); | ||
87 | this.message = message; | ||
88 | this.cause = cause; | ||
89 | } | ||
90 | |||
91 | public Unknown(final String message) { | ||
92 | this(message, null); | ||
93 | } | ||
94 | |||
95 | @Override | ||
96 | public ReliabilityResult.Solution getOrThrow() { | ||
97 | throw new RuntimeException(this.message, this.cause); | ||
98 | } | ||
99 | |||
100 | @Override | ||
101 | @Pure | ||
102 | public int hashCode() { | ||
103 | final int prime = 31; | ||
104 | int result = 1; | ||
105 | result = prime * result + ((this.message== null) ? 0 : this.message.hashCode()); | ||
106 | return prime * result + ((this.cause== null) ? 0 : this.cause.hashCode()); | ||
107 | } | ||
108 | |||
109 | @Override | ||
110 | @Pure | ||
111 | public boolean equals(final Object obj) { | ||
112 | if (this == obj) | ||
113 | return true; | ||
114 | if (obj == null) | ||
115 | return false; | ||
116 | if (getClass() != obj.getClass()) | ||
117 | return false; | ||
118 | ReliabilityResult.Unknown other = (ReliabilityResult.Unknown) obj; | ||
119 | if (this.message == null) { | ||
120 | if (other.message != null) | ||
121 | return false; | ||
122 | } else if (!this.message.equals(other.message)) | ||
123 | return false; | ||
124 | if (this.cause == null) { | ||
125 | if (other.cause != null) | ||
126 | return false; | ||
127 | } else if (!this.cause.equals(other.cause)) | ||
128 | return false; | ||
129 | return true; | ||
130 | } | ||
131 | |||
132 | @Override | ||
133 | @Pure | ||
134 | public String toString() { | ||
135 | return new ToStringBuilder(this) | ||
136 | .addAllFields() | ||
137 | .toString(); | ||
138 | } | ||
139 | |||
140 | @Pure | ||
141 | public String getMessage() { | ||
142 | return this.message; | ||
143 | } | ||
144 | |||
145 | @Pure | ||
146 | public Throwable getCause() { | ||
147 | return this.cause; | ||
148 | } | ||
149 | } | ||
150 | |||
151 | public static final ReliabilityResult.Unknown TIMEOUT = new ReliabilityResult.Unknown("Solver timed out"); | ||
152 | |||
153 | public static final ReliabilityResult.Unknown MEMOUT = new ReliabilityResult.Unknown("Solver out of memory"); | ||
154 | |||
155 | public abstract ReliabilityResult.Solution getOrThrow(); | ||
156 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | import com.google.common.base.Objects; | ||
4 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic; | ||
5 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective; | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration; | ||
7 | |||
8 | @SuppressWarnings("all") | ||
9 | public final class StormDftConfiguration extends SolverConfiguration { | ||
10 | public static final String DEFAULT_SOLVER_PATH = "storm-dft"; | ||
11 | |||
12 | public double precision = 1e-6; | ||
13 | |||
14 | public boolean bisimulation = true; | ||
15 | |||
16 | public boolean symmetryReduction = true; | ||
17 | |||
18 | public boolean modularization = true; | ||
19 | |||
20 | public boolean dontCarePropagation = true; | ||
21 | |||
22 | public double approximation = 0; | ||
23 | |||
24 | public ApproximationHeuristic approximationHeuristic = ApproximationHeuristic.NONE; | ||
25 | |||
26 | public FtAnalysisObjective objective; | ||
27 | |||
28 | public boolean isApproximationInUse() { | ||
29 | return (!Objects.equal(this.approximationHeuristic, ApproximationHeuristic.NONE)); | ||
30 | } | ||
31 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public class StormDftException extends RuntimeException { | ||
5 | public StormDftException(final String s) { | ||
6 | super(s); | ||
7 | } | ||
8 | |||
9 | public StormDftException(final String s, final Exception e) { | ||
10 | super(s, e); | ||
11 | } | ||
12 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | import com.google.common.base.Objects; | ||
4 | import com.google.common.collect.ImmutableList; | ||
5 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic; | ||
6 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective; | ||
7 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult; | ||
8 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration; | ||
9 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftException; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration; | ||
12 | import java.io.BufferedReader; | ||
13 | import java.io.IOException; | ||
14 | import java.io.InputStream; | ||
15 | import java.io.InputStreamReader; | ||
16 | import java.util.ArrayList; | ||
17 | import java.util.regex.Matcher; | ||
18 | import java.util.regex.Pattern; | ||
19 | import jnr.constants.platform.Signal; | ||
20 | import org.apache.commons.lang.SystemUtils; | ||
21 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
22 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
23 | import org.eclipse.xtext.xbase.lib.Conversions; | ||
24 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
25 | import org.eclipse.xtext.xbase.lib.Extension; | ||
26 | import org.eclipse.xtext.xbase.lib.Functions.Function0; | ||
27 | import org.eclipse.xtext.xbase.lib.Functions.Function1; | ||
28 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
29 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
30 | |||
31 | @SuppressWarnings("all") | ||
32 | public class StormDftHandler { | ||
33 | private static final String DOUBLE_REGEX = "[-+]?[0-9]*\\.?[0-9]+([eE][-+]?[0-9]+)?"; | ||
34 | |||
35 | private static final String SINGLE_RESULT_GROUP = "single"; | ||
36 | |||
37 | private static final String LOWER_BOUND_GROUP = "lower"; | ||
38 | |||
39 | private static final String UPPER_BOUND_GROUP = "upper"; | ||
40 | |||
41 | private static final String RESULT_REGEX = new Function0<String>() { | ||
42 | public String apply() { | ||
43 | StringConcatenation _builder = new StringConcatenation(); | ||
44 | _builder.append("^Result:\\s*\\[(?:(?<"); | ||
45 | _builder.append(StormDftHandler.SINGLE_RESULT_GROUP); | ||
46 | _builder.append(">"); | ||
47 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
48 | _builder.append(")|\\((?<"); | ||
49 | _builder.append(StormDftHandler.LOWER_BOUND_GROUP); | ||
50 | _builder.append(">"); | ||
51 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
52 | _builder.append("),\\s*(?<"); | ||
53 | _builder.append(StormDftHandler.UPPER_BOUND_GROUP); | ||
54 | _builder.append(">"); | ||
55 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
56 | _builder.append(")\\))\\]"); | ||
57 | return _builder.toString(); | ||
58 | } | ||
59 | }.apply(); | ||
60 | |||
61 | private static final Pattern RESULT_PATTERN = Pattern.compile(StormDftHandler.RESULT_REGEX); | ||
62 | |||
63 | private static final int SIGNAL_EXIT_VALUE_OFFSET = new Function0<Integer>() { | ||
64 | public Integer apply() { | ||
65 | int _xifexpression = (int) 0; | ||
66 | if (SystemUtils.IS_OS_SOLARIS) { | ||
67 | _xifexpression = 0; | ||
68 | } else { | ||
69 | _xifexpression = 0x80; | ||
70 | } | ||
71 | return _xifexpression; | ||
72 | } | ||
73 | }.apply().intValue(); | ||
74 | |||
75 | private static final int STORM_GENERAL_ERROR = ((-1) & 0xff); | ||
76 | |||
77 | private static final int STORM_TIMEOUT = ((-2) & 0xff); | ||
78 | |||
79 | private static final int STORM_MEMOUT = ((-3) & 0xff); | ||
80 | |||
81 | public ReliabilityResult callSolver(final String dftFilePath, final StormDftConfiguration configuration) { | ||
82 | try { | ||
83 | ReliabilityResult _xblockexpression = null; | ||
84 | { | ||
85 | final ImmutableList<String> commandLine = this.toCommandLine(configuration, dftFilePath); | ||
86 | final DocumentationLevel documentationLevel = configuration.documentationLevel; | ||
87 | final boolean printOutput = (Objects.equal(documentationLevel, DocumentationLevel.NORMAL) || | ||
88 | Objects.equal(documentationLevel, DocumentationLevel.FULL)); | ||
89 | final ProcessBuilder processBuilder = new ProcessBuilder().command(commandLine); | ||
90 | Process process = null; | ||
91 | ReliabilityResult _xtrycatchfinallyexpression = null; | ||
92 | try { | ||
93 | ReliabilityResult _xtrycatchfinallyexpression_1 = null; | ||
94 | try { | ||
95 | ReliabilityResult _xblockexpression_1 = null; | ||
96 | { | ||
97 | process = processBuilder.start(); | ||
98 | process.getOutputStream().close(); | ||
99 | final ReliabilityResult.Solution result = this.readOutput(process.getInputStream(), printOutput); | ||
100 | final String error = this.readError(process.getErrorStream(), printOutput); | ||
101 | final int exitValue = process.waitFor(); | ||
102 | ReliabilityResult _xifexpression = null; | ||
103 | if ((result == null)) { | ||
104 | _xifexpression = this.interpretExitStatus(exitValue, error); | ||
105 | } else { | ||
106 | _xifexpression = result; | ||
107 | } | ||
108 | _xblockexpression_1 = _xifexpression; | ||
109 | } | ||
110 | _xtrycatchfinallyexpression_1 = _xblockexpression_1; | ||
111 | } catch (final Throwable _t) { | ||
112 | if (_t instanceof IOException) { | ||
113 | final IOException e = (IOException)_t; | ||
114 | throw new StormDftException("Error during input/output handling of the stochastic solver.", e); | ||
115 | } else { | ||
116 | throw Exceptions.sneakyThrow(_t); | ||
117 | } | ||
118 | } | ||
119 | _xtrycatchfinallyexpression = _xtrycatchfinallyexpression_1; | ||
120 | } catch (final Throwable _t_1) { | ||
121 | if (_t_1 instanceof Exception) { | ||
122 | final Exception e_1 = (Exception)_t_1; | ||
123 | if ((process != null)) { | ||
124 | process.destroyForcibly().waitFor(); | ||
125 | } | ||
126 | throw e_1; | ||
127 | } else { | ||
128 | throw Exceptions.sneakyThrow(_t_1); | ||
129 | } | ||
130 | } | ||
131 | _xblockexpression = _xtrycatchfinallyexpression; | ||
132 | } | ||
133 | return _xblockexpression; | ||
134 | } catch (Throwable _e) { | ||
135 | throw Exceptions.sneakyThrow(_e); | ||
136 | } | ||
137 | } | ||
138 | |||
139 | private ImmutableList<String> toCommandLine(@Extension final StormDftConfiguration configuration, final String dftFilePath) { | ||
140 | ImmutableList<String> _xblockexpression = null; | ||
141 | { | ||
142 | @Extension | ||
143 | final ImmutableList.Builder<String> optionsBuilder = ImmutableList.<String>builder(); | ||
144 | String _elvis = null; | ||
145 | if (configuration.solverPath != null) { | ||
146 | _elvis = configuration.solverPath; | ||
147 | } else { | ||
148 | _elvis = StormDftConfiguration.DEFAULT_SOLVER_PATH; | ||
149 | } | ||
150 | optionsBuilder.add(_elvis); | ||
151 | if ((configuration.runtimeLimit != SolverConfiguration.Unlimited)) { | ||
152 | optionsBuilder.add("--timeout", Integer.valueOf(configuration.runtimeLimit).toString()); | ||
153 | } | ||
154 | optionsBuilder.add("--precision", Double.valueOf(configuration.precision).toString()); | ||
155 | if (configuration.bisimulation) { | ||
156 | optionsBuilder.add("--bisimulation"); | ||
157 | } | ||
158 | if (configuration.symmetryReduction) { | ||
159 | optionsBuilder.add("--symmetryreduction"); | ||
160 | } | ||
161 | if (configuration.modularization) { | ||
162 | optionsBuilder.add("--modularisation"); | ||
163 | } | ||
164 | if ((!configuration.dontCarePropagation)) { | ||
165 | optionsBuilder.add("--disabledc"); | ||
166 | } | ||
167 | boolean _isApproximationInUse = configuration.isApproximationInUse(); | ||
168 | if (_isApproximationInUse) { | ||
169 | String _switchResult = null; | ||
170 | final ApproximationHeuristic approximationHeuristic = configuration.approximationHeuristic; | ||
171 | if (approximationHeuristic != null) { | ||
172 | switch (approximationHeuristic) { | ||
173 | case DEPTH: | ||
174 | _switchResult = "depth"; | ||
175 | break; | ||
176 | default: | ||
177 | throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic)); | ||
178 | } | ||
179 | } else { | ||
180 | throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic)); | ||
181 | } | ||
182 | final String heuristicName = _switchResult; | ||
183 | optionsBuilder.add("--approximation", Double.valueOf(configuration.approximation).toString(), "--approximationheuristic", heuristicName); | ||
184 | } | ||
185 | optionsBuilder.add("--dftfile", dftFilePath); | ||
186 | final FtAnalysisObjective objective = configuration.objective; | ||
187 | boolean _matched = false; | ||
188 | if (Objects.equal(objective, FtAnalysisObjective.MTTF)) { | ||
189 | _matched=true; | ||
190 | optionsBuilder.add("--expectedtime"); | ||
191 | } | ||
192 | if (!_matched) { | ||
193 | if (objective instanceof FtAnalysisObjective.TimeBound) { | ||
194 | _matched=true; | ||
195 | optionsBuilder.add("--timebound"); | ||
196 | } | ||
197 | } | ||
198 | if (!_matched) { | ||
199 | throw new IllegalArgumentException(("Unknown analysis objective: " + configuration.objective)); | ||
200 | } | ||
201 | boolean _equals = Objects.equal(configuration.documentationLevel, DocumentationLevel.FULL); | ||
202 | if (_equals) { | ||
203 | optionsBuilder.add("--verbose"); | ||
204 | } | ||
205 | _xblockexpression = optionsBuilder.build(); | ||
206 | } | ||
207 | return _xblockexpression; | ||
208 | } | ||
209 | |||
210 | private ReliabilityResult.Solution readOutput(final InputStream inputStream, final boolean printOutput) { | ||
211 | try { | ||
212 | Object _xblockexpression = null; | ||
213 | { | ||
214 | InputStreamReader _inputStreamReader = new InputStreamReader(inputStream); | ||
215 | final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader); | ||
216 | try { | ||
217 | String line = null; | ||
218 | while (((line = bufferedReader.readLine()) != null)) { | ||
219 | { | ||
220 | if (printOutput) { | ||
221 | InputOutput.<String>println(line); | ||
222 | } | ||
223 | final Matcher matcher = StormDftHandler.RESULT_PATTERN.matcher(line); | ||
224 | boolean _find = matcher.find(); | ||
225 | if (_find) { | ||
226 | try { | ||
227 | final String single = matcher.group(StormDftHandler.SINGLE_RESULT_GROUP); | ||
228 | if ((single != null)) { | ||
229 | final double singleValue = Double.parseDouble(single); | ||
230 | return new ReliabilityResult.Solution(singleValue); | ||
231 | } | ||
232 | final String lower = matcher.group(StormDftHandler.LOWER_BOUND_GROUP); | ||
233 | final String upper = matcher.group(StormDftHandler.UPPER_BOUND_GROUP); | ||
234 | if (((lower != null) && (upper != null))) { | ||
235 | final double lowerValue = Double.parseDouble(lower); | ||
236 | final double upperValue = Double.parseDouble(upper); | ||
237 | return new ReliabilityResult.Solution(lowerValue, upperValue); | ||
238 | } | ||
239 | throw new StormDftException(("Inconsistent stochastic solver output: " + line)); | ||
240 | } catch (final Throwable _t) { | ||
241 | if (_t instanceof NumberFormatException) { | ||
242 | final NumberFormatException e = (NumberFormatException)_t; | ||
243 | throw new StormDftException("Malformatted number from stochastic solver.", e); | ||
244 | } else { | ||
245 | throw Exceptions.sneakyThrow(_t); | ||
246 | } | ||
247 | } | ||
248 | } | ||
249 | } | ||
250 | } | ||
251 | } finally { | ||
252 | bufferedReader.close(); | ||
253 | } | ||
254 | _xblockexpression = null; | ||
255 | } | ||
256 | return ((ReliabilityResult.Solution)_xblockexpression); | ||
257 | } catch (Throwable _e) { | ||
258 | throw Exceptions.sneakyThrow(_e); | ||
259 | } | ||
260 | } | ||
261 | |||
262 | private String readError(final InputStream inputStream, final boolean printOutput) { | ||
263 | try { | ||
264 | String _xblockexpression = null; | ||
265 | { | ||
266 | InputStreamReader _inputStreamReader = new InputStreamReader(inputStream); | ||
267 | final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader); | ||
268 | String _xtrycatchfinallyexpression = null; | ||
269 | try { | ||
270 | String _xblockexpression_1 = null; | ||
271 | { | ||
272 | final ArrayList<String> lines = CollectionLiterals.<String>newArrayList(); | ||
273 | String line = null; | ||
274 | while (((line = bufferedReader.readLine()) != null)) { | ||
275 | { | ||
276 | if (printOutput) { | ||
277 | System.err.println(line); | ||
278 | } | ||
279 | lines.add(line); | ||
280 | } | ||
281 | } | ||
282 | _xblockexpression_1 = IterableExtensions.join(lines, "\n"); | ||
283 | } | ||
284 | _xtrycatchfinallyexpression = _xblockexpression_1; | ||
285 | } finally { | ||
286 | bufferedReader.close(); | ||
287 | } | ||
288 | _xblockexpression = _xtrycatchfinallyexpression; | ||
289 | } | ||
290 | return _xblockexpression; | ||
291 | } catch (Throwable _e) { | ||
292 | throw Exceptions.sneakyThrow(_e); | ||
293 | } | ||
294 | } | ||
295 | |||
296 | private ReliabilityResult.Unknown interpretExitStatus(final int exitValue, final String error) { | ||
297 | ReliabilityResult.Unknown _switchResult = null; | ||
298 | boolean _matched = false; | ||
299 | if (Objects.equal(exitValue, StormDftHandler.STORM_GENERAL_ERROR)) { | ||
300 | _matched=true; | ||
301 | throw new StormDftException(("Storm error: " + error)); | ||
302 | } | ||
303 | if (!_matched) { | ||
304 | if (Objects.equal(exitValue, StormDftHandler.STORM_TIMEOUT)) { | ||
305 | _matched=true; | ||
306 | } | ||
307 | if (!_matched) { | ||
308 | int _intValue = Signal.SIGXCPU.intValue(); | ||
309 | int _plus = (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + _intValue); | ||
310 | if (Objects.equal(exitValue, _plus)) { | ||
311 | _matched=true; | ||
312 | } | ||
313 | } | ||
314 | if (_matched) { | ||
315 | _switchResult = ReliabilityResult.TIMEOUT; | ||
316 | } | ||
317 | } | ||
318 | if (!_matched) { | ||
319 | if (Objects.equal(exitValue, StormDftHandler.STORM_MEMOUT)) { | ||
320 | _matched=true; | ||
321 | } | ||
322 | if (!_matched) { | ||
323 | int _intValue_1 = Signal.SIGXFSZ.intValue(); | ||
324 | int _plus_1 = (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + _intValue_1); | ||
325 | if (Objects.equal(exitValue, _plus_1)) { | ||
326 | _matched=true; | ||
327 | } | ||
328 | } | ||
329 | if (_matched) { | ||
330 | _switchResult = ReliabilityResult.MEMOUT; | ||
331 | } | ||
332 | } | ||
333 | if (!_matched) { | ||
334 | { | ||
335 | if ((exitValue > StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET)) { | ||
336 | final int signalNumber = (exitValue - StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET); | ||
337 | final Function1<Signal, Boolean> _function = (Signal it) -> { | ||
338 | int _intValue_2 = it.intValue(); | ||
339 | return Boolean.valueOf((_intValue_2 == signalNumber)); | ||
340 | }; | ||
341 | final Signal signal = IterableExtensions.<Signal>findFirst(((Iterable<Signal>)Conversions.doWrapArray(Signal.values())), _function); | ||
342 | if ((signal != null)) { | ||
343 | throw new StormDftException(((("Storm unexpectedly killed by signal " + signal) + ": ") + error)); | ||
344 | } | ||
345 | } | ||
346 | throw new StormDftException(((("Storm unexpectedly exit with status " + Integer.valueOf(exitValue)) + ": ") + error)); | ||
347 | } | ||
348 | } | ||
349 | return _switchResult; | ||
350 | } | ||
351 | } | ||
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 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | import com.google.common.base.Objects; | ||
4 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantModel; | ||
5 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree; | ||
6 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ReliabilityModel; | ||
7 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo.Ft2GalileoTransformation; | ||
8 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective; | ||
9 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult; | ||
10 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration; | ||
11 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftHandler; | ||
12 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
13 | |||
14 | @SuppressWarnings("all") | ||
15 | public class StormDftSolver { | ||
16 | private static final String DFT_FILE_NAME = "ft.dft"; | ||
17 | |||
18 | private final Ft2GalileoTransformation ft2Galileo = new Ft2GalileoTransformation(); | ||
19 | |||
20 | private final StormDftHandler handler = new StormDftHandler(); | ||
21 | |||
22 | public ReliabilityResult solve(final ReliabilityModel reliabilityModel, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) { | ||
23 | ReliabilityResult _switchResult = null; | ||
24 | boolean _matched = false; | ||
25 | if (reliabilityModel instanceof FaultTree) { | ||
26 | _matched=true; | ||
27 | _switchResult = this.solve(((FaultTree)reliabilityModel), configuration, reasonerWorkspace); | ||
28 | } | ||
29 | if (!_matched) { | ||
30 | if (reliabilityModel instanceof ConstantModel) { | ||
31 | _matched=true; | ||
32 | ReliabilityResult.Solution _xblockexpression = null; | ||
33 | { | ||
34 | double _xifexpression = (double) 0; | ||
35 | boolean _isFailed = ((ConstantModel)reliabilityModel).isFailed(); | ||
36 | if (_isFailed) { | ||
37 | _xifexpression = 0; | ||
38 | } else { | ||
39 | double _switchResult_1 = (double) 0; | ||
40 | final FtAnalysisObjective objective = configuration.objective; | ||
41 | boolean _matched_1 = false; | ||
42 | if (Objects.equal(objective, FtAnalysisObjective.MTTF)) { | ||
43 | _matched_1=true; | ||
44 | _switchResult_1 = Double.POSITIVE_INFINITY; | ||
45 | } | ||
46 | if (!_matched_1) { | ||
47 | if (objective instanceof FtAnalysisObjective.TimeBound) { | ||
48 | _matched_1=true; | ||
49 | _switchResult_1 = 1; | ||
50 | } | ||
51 | } | ||
52 | if (!_matched_1) { | ||
53 | throw new IllegalArgumentException(("Unknown objective: " + objective)); | ||
54 | } | ||
55 | _xifexpression = _switchResult_1; | ||
56 | } | ||
57 | final double result = _xifexpression; | ||
58 | _xblockexpression = new ReliabilityResult.Solution(result); | ||
59 | } | ||
60 | _switchResult = _xblockexpression; | ||
61 | } | ||
62 | } | ||
63 | if (!_matched) { | ||
64 | throw new IllegalArgumentException(("Unknown reliability model: " + reliabilityModel)); | ||
65 | } | ||
66 | return _switchResult; | ||
67 | } | ||
68 | |||
69 | public ReliabilityResult solve(final FaultTree faultTree, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) { | ||
70 | ReliabilityResult _xblockexpression = null; | ||
71 | { | ||
72 | final CharSequence galileo = this.ft2Galileo.toGalileo(faultTree); | ||
73 | reasonerWorkspace.writeText(StormDftSolver.DFT_FILE_NAME, galileo); | ||
74 | final String dftFilePath = reasonerWorkspace.getFile(StormDftSolver.DFT_FILE_NAME).getAbsolutePath(); | ||
75 | _xblockexpression = this.handler.callSolver(dftFilePath, configuration); | ||
76 | } | ||
77 | return _xblockexpression; | ||
78 | } | ||
79 | } | ||