aboutsummaryrefslogtreecommitdiffstats
path: root/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver
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')
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.xtend51
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.xtend45
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.xtend182
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/src/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.xtend43
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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
2
3import org.eclipse.xtend.lib.annotations.Data
4import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor
5
6abstract 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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
2
3import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration
4
5final 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
29abstract 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
41enum 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 @@
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}
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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver
2
3import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantModel
4import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree
5import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ReliabilityModel
6import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo.Ft2GalileoTransformation
7import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
8
9class 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}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-08-25 17:36:12 +0000