diff options
author | Kristóf Marussy <kris7topher@gmail.com> | 2019-02-16 00:43:11 +0100 |
---|---|---|
committer | Kristóf Marussy <kris7topher@gmail.com> | 2019-02-19 19:18:25 +0100 |
commit | d90bedacaafe87e06fddaa05a6ff9b7b796e97e7 (patch) | |
tree | 3631e27854b40de3bce7606f60113054c77bd391 /Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver | |
parent | Ecore2Cft transformation (diff) | |
download | VIATRA-Generator-d90bedacaafe87e06fddaa05a6ff9b7b796e97e7.tar.gz VIATRA-Generator-d90bedacaafe87e06fddaa05a6ff9b7b796e97e7.tar.zst VIATRA-Generator-d90bedacaafe87e06fddaa05a6ff9b7b796e97e7.zip |
Two-valued fault tree analyzer WIP
Diffstat (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver')
4 files changed, 325 insertions, 0 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 new file mode 100644 index 00000000..19c3d17d --- /dev/null +++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend | |||
@@ -0,0 +1,51 @@ | |||
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 new file mode 100644 index 00000000..d9059bfc --- /dev/null +++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend | |||
@@ -0,0 +1,45 @@ | |||
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 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 | } | ||
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 new file mode 100644 index 00000000..931b9f39 --- /dev/null +++ b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend | |||
@@ -0,0 +1,43 @@ | |||
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 | } | ||