diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-02-16 00:43:11 +0100 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-02-19 19:18:25 +0100 |
commit | d90bedacaafe87e06fddaa05a6ff9b7b796e97e7 (patch) | |
tree | 3631e27854b40de3bce7606f60113054c77bd391 /Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java | |
parent | Ecore2Cft transformation (diff) | |
download | VIATRA-Generator-d90bedacaafe87e06fddaa05a6ff9b7b796e97e7.tar.gz VIATRA-Generator-d90bedacaafe87e06fddaa05a6ff9b7b796e97e7.tar.zst VIATRA-Generator-d90bedacaafe87e06fddaa05a6ff9b7b796e97e7.zip |
Two-valued fault tree analyzer WIP
Diffstat (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java')
-rw-r--r-- | Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java | 351 |
1 files changed, 351 insertions, 0 deletions
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 | } | ||