diff options
Diffstat (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver')
4 files changed, 0 insertions, 321 deletions
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend deleted file mode 100644 index 19c3d17d..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend +++ /dev/null | |||
@@ -1,51 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver | ||
2 | |||
3 | import org.eclipse.xtend.lib.annotations.Data | ||
4 | import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor | ||
5 | |||
6 | abstract class ReliabilityResult { | ||
7 | public static val TIMEOUT = new Unknown("Solver timed out") | ||
8 | public static val MEMOUT = new Unknown("Solver out of memory") | ||
9 | |||
10 | abstract def Solution getOrThrow() | ||
11 | |||
12 | @Data | ||
13 | static final class Solution extends ReliabilityResult { | ||
14 | val double lowerBound | ||
15 | val double upperBound | ||
16 | |||
17 | new(double value) { | ||
18 | this(value, value) | ||
19 | } | ||
20 | |||
21 | new(double lowerBound, double upperBound) { | ||
22 | if (lowerBound > upperBound) { | ||
23 | throw new IllegalArgumentException("lowerBound must not be larger than upperBound") | ||
24 | } | ||
25 | this.lowerBound = lowerBound | ||
26 | this.upperBound = upperBound | ||
27 | } | ||
28 | |||
29 | override getOrThrow() { | ||
30 | this | ||
31 | } | ||
32 | } | ||
33 | |||
34 | @Data | ||
35 | static final class Unknown extends ReliabilityResult { | ||
36 | val String message | ||
37 | val Throwable cause | ||
38 | |||
39 | @FinalFieldsConstructor | ||
40 | new() { | ||
41 | } | ||
42 | |||
43 | new(String message) { | ||
44 | this(message, null) | ||
45 | } | ||
46 | |||
47 | override getOrThrow() { | ||
48 | throw new RuntimeException(message, cause) | ||
49 | } | ||
50 | } | ||
51 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend deleted file mode 100644 index d9059bfc..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend +++ /dev/null | |||
@@ -1,45 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration | ||
4 | |||
5 | final class StormDftConfiguration extends SolverConfiguration { | ||
6 | public static val DEFAULT_SOLVER_PATH = "storm-dft" | ||
7 | |||
8 | public double precision = 1e-6 | ||
9 | |||
10 | public boolean bisimulation = true | ||
11 | |||
12 | public boolean symmetryReduction = true | ||
13 | |||
14 | public boolean modularization = true | ||
15 | |||
16 | public boolean dontCarePropagation = true | ||
17 | |||
18 | public double approximation = 0 | ||
19 | |||
20 | public var approximationHeuristic = ApproximationHeuristic.NONE | ||
21 | |||
22 | public FtAnalysisObjective objective | ||
23 | |||
24 | def isApproximationInUse() { | ||
25 | approximationHeuristic != ApproximationHeuristic.NONE | ||
26 | } | ||
27 | } | ||
28 | |||
29 | abstract class FtAnalysisObjective { | ||
30 | public static val MTTF = new FtAnalysisObjective { | ||
31 | } | ||
32 | |||
33 | private new() { | ||
34 | } | ||
35 | |||
36 | static final class TimeBound extends FtAnalysisObjective { | ||
37 | public double timeBound = 0 | ||
38 | } | ||
39 | } | ||
40 | |||
41 | enum ApproximationHeuristic { | ||
42 | NONE, | ||
43 | DEPTH | ||
44 | // See https://github.com/moves-rwth/storm/issues/35 for additional approximation heuristics. | ||
45 | } | ||
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 @@ | |||
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 | |||
12 | class 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 | |||
22 | class 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 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend deleted file mode 100644 index 931b9f39..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend +++ /dev/null | |||
@@ -1,43 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver | ||
2 | |||
3 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantModel | ||
4 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree | ||
5 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ReliabilityModel | ||
6 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo.Ft2GalileoTransformation | ||
7 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace | ||
8 | |||
9 | class StormDftSolver { | ||
10 | static val DFT_FILE_NAME = "ft.dft" | ||
11 | |||
12 | val ft2Galileo = new Ft2GalileoTransformation | ||
13 | val handler = new StormDftHandler | ||
14 | |||
15 | def solve(ReliabilityModel reliabilityModel, StormDftConfiguration configuration, | ||
16 | ReasonerWorkspace reasonerWorkspace) { | ||
17 | switch (reliabilityModel) { | ||
18 | FaultTree: | ||
19 | solve(reliabilityModel, configuration, reasonerWorkspace) | ||
20 | ConstantModel: { | ||
21 | val result = if (reliabilityModel.failed) { | ||
22 | 0 | ||
23 | } else { | ||
24 | switch (objective : configuration.objective) { | ||
25 | case FtAnalysisObjective.MTTF: Double.POSITIVE_INFINITY | ||
26 | FtAnalysisObjective.TimeBound: 1 | ||
27 | default: throw new IllegalArgumentException("Unknown objective: " + objective) | ||
28 | } | ||
29 | } | ||
30 | new ReliabilityResult.Solution(result) | ||
31 | } | ||
32 | default: | ||
33 | throw new IllegalArgumentException("Unknown reliability model: " + reliabilityModel) | ||
34 | } | ||
35 | } | ||
36 | |||
37 | def solve(FaultTree faultTree, StormDftConfiguration configuration, ReasonerWorkspace reasonerWorkspace) { | ||
38 | val galileo = ft2Galileo.toGalileo(faultTree) | ||
39 | reasonerWorkspace.writeText(DFT_FILE_NAME, galileo) | ||
40 | val dftFilePath = reasonerWorkspace.getFile(DFT_FILE_NAME).absolutePath | ||
41 | handler.callSolver(dftFilePath, configuration) | ||
42 | } | ||
43 | } | ||