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