diff options
Diffstat (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend')
-rw-r--r-- | Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend | 186 |
1 files changed, 186 insertions, 0 deletions
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend new file mode 100644 index 00000000..91c6a0d0 --- /dev/null +++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend | |||
@@ -0,0 +1,186 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver | ||
2 | |||
3 | import com.google.common.collect.ImmutableList | ||
4 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel | ||
5 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration | ||
6 | import java.io.BufferedReader | ||
7 | import java.io.IOException | ||
8 | import java.io.InputStream | ||
9 | import java.io.InputStreamReader | ||
10 | import java.util.regex.Pattern | ||
11 | import jnr.constants.platform.Signal | ||
12 | import org.apache.commons.lang.SystemUtils | ||
13 | |||
14 | class StormDftException extends RuntimeException { | ||
15 | new(String s) { | ||
16 | super(s) | ||
17 | } | ||
18 | |||
19 | new(String s, Exception e) { | ||
20 | super(s, e) | ||
21 | } | ||
22 | } | ||
23 | |||
24 | class StormDftHandler { | ||
25 | static val DOUBLE_REGEX = "[-+]?[0-9]*\\.?[0-9]+([eE][-+]?[0-9]+)?" | ||
26 | static val SINGLE_RESULT_GROUP = "single" | ||
27 | static val LOWER_BOUND_GROUP = "lower" | ||
28 | static val UPPER_BOUND_GROUP = "upper" | ||
29 | static val RESULT_REGEX = '''^Result:\s*\[(?:(?<«SINGLE_RESULT_GROUP»>«DOUBLE_REGEX»)|\((?<«LOWER_BOUND_GROUP»>«DOUBLE_REGEX»),\s*(?<«UPPER_BOUND_GROUP»>«DOUBLE_REGEX»)\))\]''' | ||
30 | static val RESULT_PATTERN = Pattern.compile(RESULT_REGEX) | ||
31 | |||
32 | // See http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/jdk7-b147/src/solaris/native/java/lang/UNIXProcess_md.c#l332 | ||
33 | static val SIGNAL_EXIT_VALUE_OFFSET = if(SystemUtils.IS_OS_SOLARIS) 0 else 0x80 | ||
34 | |||
35 | static val STORM_GENERAL_ERROR = (-1).bitwiseAnd(0xff) | ||
36 | static val STORM_TIMEOUT = (-2).bitwiseAnd(0xff) | ||
37 | static val STORM_MEMOUT = (-3).bitwiseAnd(0xff) | ||
38 | |||
39 | def callSolver(String dftFilePath, StormDftConfiguration configuration) { | ||
40 | val commandLine = configuration.toCommandLine(dftFilePath) | ||
41 | val documentationLevel = configuration.documentationLevel | ||
42 | val printOutput = documentationLevel == DocumentationLevel.NORMAL || | ||
43 | documentationLevel == DocumentationLevel.FULL | ||
44 | val processBuilder = new ProcessBuilder().command(commandLine) | ||
45 | var Process process = null | ||
46 | try { | ||
47 | try { | ||
48 | process = processBuilder.start | ||
49 | process.outputStream.close | ||
50 | val result = readOutput(process.inputStream, printOutput) | ||
51 | val error = readError(process.errorStream, printOutput) | ||
52 | val exitValue = process.waitFor | ||
53 | if (result === null) { | ||
54 | interpretExitStatus(exitValue, error) | ||
55 | } else { | ||
56 | result | ||
57 | } | ||
58 | } catch (IOException e) { | ||
59 | throw new StormDftException("Error during input/output handling of the stochastic solver.", e) | ||
60 | } | ||
61 | } catch (Exception e) { | ||
62 | if (process !== null) { | ||
63 | process.destroyForcibly.waitFor | ||
64 | } | ||
65 | throw e | ||
66 | } | ||
67 | } | ||
68 | |||
69 | private def toCommandLine(extension StormDftConfiguration configuration, String dftFilePath) { | ||
70 | extension val optionsBuilder = ImmutableList.builder | ||
71 | add(solverPath ?: StormDftConfiguration.DEFAULT_SOLVER_PATH) | ||
72 | if (runtimeLimit != SolverConfiguration.Unlimited) { | ||
73 | add("--timeout", runtimeLimit.toString) | ||
74 | } | ||
75 | add("--precision", precision.toString) | ||
76 | if (bisimulation) { | ||
77 | add("--bisimulation") | ||
78 | } | ||
79 | if (symmetryReduction) { | ||
80 | add("--symmetryreduction") | ||
81 | } | ||
82 | if (modularization) { | ||
83 | add("--modularisation") | ||
84 | } | ||
85 | if (!dontCarePropagation) { | ||
86 | add("--disabledc") | ||
87 | } | ||
88 | if (approximationInUse) { | ||
89 | val heuristicName = switch (approximationHeuristic) { | ||
90 | case DEPTH: | ||
91 | "depth" | ||
92 | default: | ||
93 | throw new IllegalArgumentException("Unknown approximation heuristic: " + approximationHeuristic) | ||
94 | } | ||
95 | add("--approximation", approximation.toString, "--approximationheuristic", heuristicName) | ||
96 | } | ||
97 | add("--dftfile", dftFilePath) | ||
98 | switch (objective) { | ||
99 | case FtAnalysisObjective.MTTF: | ||
100 | add("--expectedtime") | ||
101 | FtAnalysisObjective.TimeBound: | ||
102 | add("--timebound") | ||
103 | default: | ||
104 | throw new IllegalArgumentException("Unknown analysis objective: " + objective) | ||
105 | } | ||
106 | if (documentationLevel == DocumentationLevel.FULL) { | ||
107 | add("--verbose") | ||
108 | } | ||
109 | build | ||
110 | } | ||
111 | |||
112 | private def readOutput(InputStream inputStream, boolean printOutput) { | ||
113 | val bufferedReader = new BufferedReader(new InputStreamReader(inputStream)) | ||
114 | try { | ||
115 | var String line | ||
116 | while ((line = bufferedReader.readLine) !== null) { | ||
117 | if (printOutput) { | ||
118 | println(line) | ||
119 | } | ||
120 | val matcher = RESULT_PATTERN.matcher(line) | ||
121 | if (matcher.find) { | ||
122 | try { | ||
123 | val single = matcher.group(SINGLE_RESULT_GROUP) | ||
124 | if (single !== null) { | ||
125 | val singleValue = Double.parseDouble(single) | ||
126 | return new ReliabilityResult.Solution(singleValue) | ||
127 | } | ||
128 | val lower = matcher.group(LOWER_BOUND_GROUP) | ||
129 | val upper = matcher.group(UPPER_BOUND_GROUP) | ||
130 | if (lower !== null && upper !== null) { | ||
131 | val lowerValue = Double.parseDouble(lower) | ||
132 | val upperValue = Double.parseDouble(upper) | ||
133 | return new ReliabilityResult.Solution(lowerValue, upperValue) | ||
134 | } | ||
135 | throw new StormDftException("Inconsistent stochastic solver output: " + line) | ||
136 | } catch (NumberFormatException e) { | ||
137 | throw new StormDftException("Malformatted number from stochastic solver.", e) | ||
138 | } | ||
139 | } | ||
140 | } | ||
141 | } finally { | ||
142 | bufferedReader.close | ||
143 | } | ||
144 | null | ||
145 | } | ||
146 | |||
147 | private def readError(InputStream inputStream, boolean printOutput) { | ||
148 | val bufferedReader = new BufferedReader(new InputStreamReader(inputStream)) | ||
149 | try { | ||
150 | val lines = newArrayList | ||
151 | var String line | ||
152 | while ((line = bufferedReader.readLine) !== null) { | ||
153 | if (printOutput) { | ||
154 | System.err.println(line) | ||
155 | } | ||
156 | lines += line | ||
157 | } | ||
158 | lines.join("\n") | ||
159 | } finally { | ||
160 | bufferedReader.close | ||
161 | } | ||
162 | } | ||
163 | |||
164 | private def interpretExitStatus(int exitValue, String error) { | ||
165 | switch (exitValue) { | ||
166 | case STORM_GENERAL_ERROR: | ||
167 | throw new StormDftException("Storm error: " + error) | ||
168 | case STORM_TIMEOUT, | ||
169 | case SIGNAL_EXIT_VALUE_OFFSET + Signal.SIGXCPU.intValue: | ||
170 | ReliabilityResult.TIMEOUT | ||
171 | case STORM_MEMOUT, | ||
172 | case SIGNAL_EXIT_VALUE_OFFSET + Signal.SIGXFSZ.intValue: | ||
173 | ReliabilityResult.MEMOUT | ||
174 | default: { | ||
175 | if (exitValue > SIGNAL_EXIT_VALUE_OFFSET) { | ||
176 | val signalNumber = exitValue - SIGNAL_EXIT_VALUE_OFFSET | ||
177 | val signal = Signal.values.findFirst[intValue == signalNumber] | ||
178 | if (signal !== null) { | ||
179 | throw new StormDftException("Storm unexpectedly killed by signal " + signal + ": " + error) | ||
180 | } | ||
181 | } | ||
182 | throw new StormDftException("Storm unexpectedly exit with status " + exitValue + ": " + error) | ||
183 | } | ||
184 | } | ||
185 | } | ||
186 | } | ||