diff options
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 | 330 |
1 files changed, 330 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..46127425 --- /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,330 @@ | |||
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 org.eclipse.xtend2.lib.StringConcatenation; | ||
20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
21 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
22 | import org.eclipse.xtext.xbase.lib.Extension; | ||
23 | import org.eclipse.xtext.xbase.lib.Functions.Function0; | ||
24 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
25 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
26 | |||
27 | @SuppressWarnings("all") | ||
28 | public class StormDftHandler { | ||
29 | private static final String DOUBLE_REGEX = "[-+]?[0-9]*\\.?[0-9]+([eE][-+]?[0-9]+)?"; | ||
30 | |||
31 | private static final String SINGLE_RESULT_GROUP = "single"; | ||
32 | |||
33 | private static final String LOWER_BOUND_GROUP = "lower"; | ||
34 | |||
35 | private static final String UPPER_BOUND_GROUP = "upper"; | ||
36 | |||
37 | private static final String RESULT_REGEX = new Function0<String>() { | ||
38 | public String apply() { | ||
39 | StringConcatenation _builder = new StringConcatenation(); | ||
40 | _builder.append("^Result:\\s*\\[(?:(?<"); | ||
41 | _builder.append(StormDftHandler.SINGLE_RESULT_GROUP); | ||
42 | _builder.append(">"); | ||
43 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
44 | _builder.append(")|\\((?<"); | ||
45 | _builder.append(StormDftHandler.LOWER_BOUND_GROUP); | ||
46 | _builder.append(">"); | ||
47 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
48 | _builder.append("),\\s*(?<"); | ||
49 | _builder.append(StormDftHandler.UPPER_BOUND_GROUP); | ||
50 | _builder.append(">"); | ||
51 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
52 | _builder.append(")\\))\\]"); | ||
53 | return _builder.toString(); | ||
54 | } | ||
55 | }.apply(); | ||
56 | |||
57 | private static final Pattern RESULT_PATTERN = Pattern.compile(StormDftHandler.RESULT_REGEX); | ||
58 | |||
59 | private static final int SIGNAL_EXIT_VALUE_OFFSET = 0x80; | ||
60 | |||
61 | private static final int SIGXCPU = 24; | ||
62 | |||
63 | private static final int SIGXFSZ = 25; | ||
64 | |||
65 | private static final int STORM_GENERAL_ERROR = ((-1) & 0xff); | ||
66 | |||
67 | private static final int STORM_TIMEOUT = ((-2) & 0xff); | ||
68 | |||
69 | private static final int STORM_MEMOUT = ((-3) & 0xff); | ||
70 | |||
71 | public ReliabilityResult callSolver(final String dftFilePath, final StormDftConfiguration configuration) { | ||
72 | try { | ||
73 | ReliabilityResult _xblockexpression = null; | ||
74 | { | ||
75 | final ImmutableList<String> commandLine = this.toCommandLine(configuration, dftFilePath); | ||
76 | final DocumentationLevel documentationLevel = configuration.documentationLevel; | ||
77 | final boolean printOutput = (Objects.equal(documentationLevel, DocumentationLevel.NORMAL) || | ||
78 | Objects.equal(documentationLevel, DocumentationLevel.FULL)); | ||
79 | final ProcessBuilder processBuilder = new ProcessBuilder().command(commandLine); | ||
80 | Process process = null; | ||
81 | ReliabilityResult _xtrycatchfinallyexpression = null; | ||
82 | try { | ||
83 | ReliabilityResult _xtrycatchfinallyexpression_1 = null; | ||
84 | try { | ||
85 | ReliabilityResult _xblockexpression_1 = null; | ||
86 | { | ||
87 | process = processBuilder.start(); | ||
88 | process.getOutputStream().close(); | ||
89 | final ReliabilityResult.Solution result = this.readOutput(process.getInputStream(), printOutput); | ||
90 | final String error = this.readError(process.getErrorStream(), printOutput); | ||
91 | final int exitValue = process.waitFor(); | ||
92 | ReliabilityResult _xifexpression = null; | ||
93 | if ((result == null)) { | ||
94 | _xifexpression = this.interpretExitStatus(exitValue, error); | ||
95 | } else { | ||
96 | _xifexpression = result; | ||
97 | } | ||
98 | _xblockexpression_1 = _xifexpression; | ||
99 | } | ||
100 | _xtrycatchfinallyexpression_1 = _xblockexpression_1; | ||
101 | } catch (final Throwable _t) { | ||
102 | if (_t instanceof IOException) { | ||
103 | final IOException e = (IOException)_t; | ||
104 | throw new StormDftException("Error during input/output handling of the stochastic solver.", e); | ||
105 | } else { | ||
106 | throw Exceptions.sneakyThrow(_t); | ||
107 | } | ||
108 | } | ||
109 | _xtrycatchfinallyexpression = _xtrycatchfinallyexpression_1; | ||
110 | } catch (final Throwable _t_1) { | ||
111 | if (_t_1 instanceof Exception) { | ||
112 | final Exception e_1 = (Exception)_t_1; | ||
113 | if ((process != null)) { | ||
114 | process.destroyForcibly().waitFor(); | ||
115 | } | ||
116 | throw e_1; | ||
117 | } else { | ||
118 | throw Exceptions.sneakyThrow(_t_1); | ||
119 | } | ||
120 | } | ||
121 | _xblockexpression = _xtrycatchfinallyexpression; | ||
122 | } | ||
123 | return _xblockexpression; | ||
124 | } catch (Throwable _e) { | ||
125 | throw Exceptions.sneakyThrow(_e); | ||
126 | } | ||
127 | } | ||
128 | |||
129 | private ImmutableList<String> toCommandLine(@Extension final StormDftConfiguration configuration, final String dftFilePath) { | ||
130 | ImmutableList<String> _xblockexpression = null; | ||
131 | { | ||
132 | @Extension | ||
133 | final ImmutableList.Builder<String> optionsBuilder = ImmutableList.<String>builder(); | ||
134 | String _elvis = null; | ||
135 | if (configuration.solverPath != null) { | ||
136 | _elvis = configuration.solverPath; | ||
137 | } else { | ||
138 | _elvis = StormDftConfiguration.DEFAULT_SOLVER_PATH; | ||
139 | } | ||
140 | optionsBuilder.add(_elvis); | ||
141 | if ((configuration.runtimeLimit != SolverConfiguration.Unlimited)) { | ||
142 | optionsBuilder.add("--timeout", Integer.valueOf(configuration.runtimeLimit).toString()); | ||
143 | } | ||
144 | optionsBuilder.add("--precision", Double.valueOf(configuration.precision).toString()); | ||
145 | if (configuration.bisimulation) { | ||
146 | optionsBuilder.add("--bisimulation"); | ||
147 | } | ||
148 | if (configuration.symmetryReduction) { | ||
149 | optionsBuilder.add("--symmetryreduction"); | ||
150 | } | ||
151 | if (configuration.modularization) { | ||
152 | optionsBuilder.add("--modularisation"); | ||
153 | } | ||
154 | if ((!configuration.dontCarePropagation)) { | ||
155 | optionsBuilder.add("--disabledc"); | ||
156 | } | ||
157 | boolean _isApproximationInUse = configuration.isApproximationInUse(); | ||
158 | if (_isApproximationInUse) { | ||
159 | String _switchResult = null; | ||
160 | final ApproximationHeuristic approximationHeuristic = configuration.approximationHeuristic; | ||
161 | if (approximationHeuristic != null) { | ||
162 | switch (approximationHeuristic) { | ||
163 | case DEPTH: | ||
164 | _switchResult = "depth"; | ||
165 | break; | ||
166 | default: | ||
167 | throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic)); | ||
168 | } | ||
169 | } else { | ||
170 | throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic)); | ||
171 | } | ||
172 | final String heuristicName = _switchResult; | ||
173 | optionsBuilder.add("--approximation", Double.valueOf(configuration.approximation).toString(), "--approximationheuristic", heuristicName); | ||
174 | } | ||
175 | optionsBuilder.add("--dftfile", dftFilePath); | ||
176 | final FtAnalysisObjective objective = configuration.objective; | ||
177 | boolean _matched = false; | ||
178 | if (Objects.equal(objective, FtAnalysisObjective.MTTF)) { | ||
179 | _matched=true; | ||
180 | optionsBuilder.add("--expectedtime"); | ||
181 | } | ||
182 | if (!_matched) { | ||
183 | if (objective instanceof FtAnalysisObjective.TimeBound) { | ||
184 | _matched=true; | ||
185 | optionsBuilder.add("--timebound"); | ||
186 | } | ||
187 | } | ||
188 | if (!_matched) { | ||
189 | throw new IllegalArgumentException(("Unknown analysis objective: " + configuration.objective)); | ||
190 | } | ||
191 | boolean _equals = Objects.equal(configuration.documentationLevel, DocumentationLevel.FULL); | ||
192 | if (_equals) { | ||
193 | optionsBuilder.add("--verbose"); | ||
194 | } | ||
195 | _xblockexpression = optionsBuilder.build(); | ||
196 | } | ||
197 | return _xblockexpression; | ||
198 | } | ||
199 | |||
200 | private ReliabilityResult.Solution readOutput(final InputStream inputStream, final boolean printOutput) { | ||
201 | try { | ||
202 | Object _xblockexpression = null; | ||
203 | { | ||
204 | InputStreamReader _inputStreamReader = new InputStreamReader(inputStream); | ||
205 | final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader); | ||
206 | try { | ||
207 | String line = null; | ||
208 | while (((line = bufferedReader.readLine()) != null)) { | ||
209 | { | ||
210 | if (printOutput) { | ||
211 | InputOutput.<String>println(line); | ||
212 | } | ||
213 | final Matcher matcher = StormDftHandler.RESULT_PATTERN.matcher(line); | ||
214 | boolean _find = matcher.find(); | ||
215 | if (_find) { | ||
216 | try { | ||
217 | final String single = matcher.group(StormDftHandler.SINGLE_RESULT_GROUP); | ||
218 | if ((single != null)) { | ||
219 | final double singleValue = Double.parseDouble(single); | ||
220 | return new ReliabilityResult.Solution(singleValue); | ||
221 | } | ||
222 | final String lower = matcher.group(StormDftHandler.LOWER_BOUND_GROUP); | ||
223 | final String upper = matcher.group(StormDftHandler.UPPER_BOUND_GROUP); | ||
224 | if (((lower != null) && (upper != null))) { | ||
225 | final double lowerValue = Double.parseDouble(lower); | ||
226 | final double upperValue = Double.parseDouble(upper); | ||
227 | return new ReliabilityResult.Solution(lowerValue, upperValue); | ||
228 | } | ||
229 | throw new StormDftException(("Inconsistent stochastic solver output: " + line)); | ||
230 | } catch (final Throwable _t) { | ||
231 | if (_t instanceof NumberFormatException) { | ||
232 | final NumberFormatException e = (NumberFormatException)_t; | ||
233 | throw new StormDftException("Malformatted number from stochastic solver.", e); | ||
234 | } else { | ||
235 | throw Exceptions.sneakyThrow(_t); | ||
236 | } | ||
237 | } | ||
238 | } | ||
239 | } | ||
240 | } | ||
241 | } finally { | ||
242 | bufferedReader.close(); | ||
243 | } | ||
244 | _xblockexpression = null; | ||
245 | } | ||
246 | return ((ReliabilityResult.Solution)_xblockexpression); | ||
247 | } catch (Throwable _e) { | ||
248 | throw Exceptions.sneakyThrow(_e); | ||
249 | } | ||
250 | } | ||
251 | |||
252 | private String readError(final InputStream inputStream, final boolean printOutput) { | ||
253 | try { | ||
254 | String _xblockexpression = null; | ||
255 | { | ||
256 | InputStreamReader _inputStreamReader = new InputStreamReader(inputStream); | ||
257 | final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader); | ||
258 | String _xtrycatchfinallyexpression = null; | ||
259 | try { | ||
260 | String _xblockexpression_1 = null; | ||
261 | { | ||
262 | final ArrayList<String> lines = CollectionLiterals.<String>newArrayList(); | ||
263 | String line = null; | ||
264 | while (((line = bufferedReader.readLine()) != null)) { | ||
265 | { | ||
266 | if (printOutput) { | ||
267 | System.err.println(line); | ||
268 | } | ||
269 | lines.add(line); | ||
270 | } | ||
271 | } | ||
272 | _xblockexpression_1 = IterableExtensions.join(lines, "\n"); | ||
273 | } | ||
274 | _xtrycatchfinallyexpression = _xblockexpression_1; | ||
275 | } finally { | ||
276 | bufferedReader.close(); | ||
277 | } | ||
278 | _xblockexpression = _xtrycatchfinallyexpression; | ||
279 | } | ||
280 | return _xblockexpression; | ||
281 | } catch (Throwable _e) { | ||
282 | throw Exceptions.sneakyThrow(_e); | ||
283 | } | ||
284 | } | ||
285 | |||
286 | private ReliabilityResult.Unknown interpretExitStatus(final int exitValue, final String error) { | ||
287 | ReliabilityResult.Unknown _switchResult = null; | ||
288 | boolean _matched = false; | ||
289 | if (Objects.equal(exitValue, StormDftHandler.STORM_GENERAL_ERROR)) { | ||
290 | _matched=true; | ||
291 | throw new StormDftException(("Storm error: " + error)); | ||
292 | } | ||
293 | if (!_matched) { | ||
294 | if (Objects.equal(exitValue, StormDftHandler.STORM_TIMEOUT)) { | ||
295 | _matched=true; | ||
296 | } | ||
297 | if (!_matched) { | ||
298 | if (Objects.equal(exitValue, (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + StormDftHandler.SIGXCPU))) { | ||
299 | _matched=true; | ||
300 | } | ||
301 | } | ||
302 | if (_matched) { | ||
303 | _switchResult = ReliabilityResult.TIMEOUT; | ||
304 | } | ||
305 | } | ||
306 | if (!_matched) { | ||
307 | if (Objects.equal(exitValue, StormDftHandler.STORM_MEMOUT)) { | ||
308 | _matched=true; | ||
309 | } | ||
310 | if (!_matched) { | ||
311 | if (Objects.equal(exitValue, (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + StormDftHandler.SIGXFSZ))) { | ||
312 | _matched=true; | ||
313 | } | ||
314 | } | ||
315 | if (_matched) { | ||
316 | _switchResult = ReliabilityResult.MEMOUT; | ||
317 | } | ||
318 | } | ||
319 | if (!_matched) { | ||
320 | { | ||
321 | if ((exitValue > StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET)) { | ||
322 | final int signalNumber = (exitValue - StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET); | ||
323 | throw new StormDftException(((("Storm unexpectedly killed by signal " + Integer.valueOf(signalNumber)) + ": ") + error)); | ||
324 | } | ||
325 | throw new StormDftException(((("Storm unexpectedly exit with status " + Integer.valueOf(exitValue)) + ": ") + error)); | ||
326 | } | ||
327 | } | ||
328 | return _switchResult; | ||
329 | } | ||
330 | } | ||