aboutsummaryrefslogtreecommitdiffstats
path: root/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java
diff options
context:
space:
mode:
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.java330
1 files changed, 0 insertions, 330 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
deleted file mode 100644
index 46127425..00000000
--- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java
+++ /dev/null
@@ -1,330 +0,0 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3import com.google.common.base.Objects;
4import com.google.common.collect.ImmutableList;
5import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic;
6import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
7import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult;
8import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration;
9import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftException;
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration;
12import java.io.BufferedReader;
13import java.io.IOException;
14import java.io.InputStream;
15import java.io.InputStreamReader;
16import java.util.ArrayList;
17import java.util.regex.Matcher;
18import java.util.regex.Pattern;
19import org.eclipse.xtend2.lib.StringConcatenation;
20import org.eclipse.xtext.xbase.lib.CollectionLiterals;
21import org.eclipse.xtext.xbase.lib.Exceptions;
22import org.eclipse.xtext.xbase.lib.Extension;
23import org.eclipse.xtext.xbase.lib.Functions.Function0;
24import org.eclipse.xtext.xbase.lib.InputOutput;
25import org.eclipse.xtext.xbase.lib.IterableExtensions;
26
27@SuppressWarnings("all")
28public 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}
generated by cgit v1.2.3-54-g00ecf (git 2.45.2) at 2024-07-16 20:22:03 +0000