diff options
Diffstat (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver')
12 files changed, 0 insertions, 650 deletions
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin deleted file mode 100644 index cdaacb58..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbin +++ /dev/null | |||
Binary files differ | |||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin deleted file mode 100644 index 6e1908aa..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbin +++ /dev/null | |||
Binary files differ | |||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin deleted file mode 100644 index 5772b0e7..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbin +++ /dev/null | |||
Binary files differ | |||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin deleted file mode 100644 index e1c1a8c7..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbin +++ /dev/null | |||
Binary files differ | |||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore deleted file mode 100644 index 8a74c101..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore +++ /dev/null | |||
@@ -1,20 +0,0 @@ | |||
1 | /.StormDftSolver.java._trace | ||
2 | /.StormDftConfiguration.java._trace | ||
3 | /.StormDftMttfConfiguration.java._trace | ||
4 | /.FtAnalysisObjective.java._trace | ||
5 | /.ApproximationHeuristic.java._trace | ||
6 | /.StormDftHandler.java._trace | ||
7 | /.StormDftException.java._trace | ||
8 | /.ReliabilityModelSolution.java._trace | ||
9 | /.ReliabilityResult.java._trace | ||
10 | /.ReliabilityResult.xtendbin | ||
11 | /.StormDftConfiguration.xtendbin | ||
12 | /.StormDftHandler.xtendbin | ||
13 | /.StormDftSolver.xtendbin | ||
14 | /ApproximationHeuristic.java | ||
15 | /FtAnalysisObjective.java | ||
16 | /ReliabilityResult.java | ||
17 | /StormDftConfiguration.java | ||
18 | /StormDftException.java | ||
19 | /StormDftHandler.java | ||
20 | /StormDftSolver.java | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java deleted file mode 100644 index 822d4f36..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java +++ /dev/null | |||
@@ -1,8 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public enum ApproximationHeuristic { | ||
5 | NONE, | ||
6 | |||
7 | DEPTH; | ||
8 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java deleted file mode 100644 index 528ada42..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java +++ /dev/null | |||
@@ -1,14 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public abstract class FtAnalysisObjective { | ||
5 | public static final class TimeBound extends FtAnalysisObjective { | ||
6 | public double timeBound = 0; | ||
7 | } | ||
8 | |||
9 | public static final FtAnalysisObjective MTTF = new FtAnalysisObjective() { | ||
10 | }; | ||
11 | |||
12 | private FtAnalysisObjective() { | ||
13 | } | ||
14 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java deleted file mode 100644 index c8c8b000..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java +++ /dev/null | |||
@@ -1,156 +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 | import org.eclipse.xtext.xbase.lib.Pure; | ||
6 | import org.eclipse.xtext.xbase.lib.util.ToStringBuilder; | ||
7 | |||
8 | @SuppressWarnings("all") | ||
9 | public abstract class ReliabilityResult { | ||
10 | @Data | ||
11 | public static final class Solution extends ReliabilityResult { | ||
12 | private final double lowerBound; | ||
13 | |||
14 | private final double upperBound; | ||
15 | |||
16 | public Solution(final double value) { | ||
17 | this(value, value); | ||
18 | } | ||
19 | |||
20 | public Solution(final double lowerBound, final double upperBound) { | ||
21 | if ((lowerBound > upperBound)) { | ||
22 | throw new IllegalArgumentException("lowerBound must not be larger than upperBound"); | ||
23 | } | ||
24 | this.lowerBound = lowerBound; | ||
25 | this.upperBound = upperBound; | ||
26 | } | ||
27 | |||
28 | @Override | ||
29 | public ReliabilityResult.Solution getOrThrow() { | ||
30 | return this; | ||
31 | } | ||
32 | |||
33 | @Override | ||
34 | @Pure | ||
35 | public int hashCode() { | ||
36 | final int prime = 31; | ||
37 | int result = 1; | ||
38 | result = prime * result + (int) (Double.doubleToLongBits(this.lowerBound) ^ (Double.doubleToLongBits(this.lowerBound) >>> 32)); | ||
39 | return prime * result + (int) (Double.doubleToLongBits(this.upperBound) ^ (Double.doubleToLongBits(this.upperBound) >>> 32)); | ||
40 | } | ||
41 | |||
42 | @Override | ||
43 | @Pure | ||
44 | public boolean equals(final Object obj) { | ||
45 | if (this == obj) | ||
46 | return true; | ||
47 | if (obj == null) | ||
48 | return false; | ||
49 | if (getClass() != obj.getClass()) | ||
50 | return false; | ||
51 | ReliabilityResult.Solution other = (ReliabilityResult.Solution) obj; | ||
52 | if (Double.doubleToLongBits(other.lowerBound) != Double.doubleToLongBits(this.lowerBound)) | ||
53 | return false; | ||
54 | if (Double.doubleToLongBits(other.upperBound) != Double.doubleToLongBits(this.upperBound)) | ||
55 | return false; | ||
56 | return true; | ||
57 | } | ||
58 | |||
59 | @Override | ||
60 | @Pure | ||
61 | public String toString() { | ||
62 | return new ToStringBuilder(this) | ||
63 | .addAllFields() | ||
64 | .toString(); | ||
65 | } | ||
66 | |||
67 | @Pure | ||
68 | public double getLowerBound() { | ||
69 | return this.lowerBound; | ||
70 | } | ||
71 | |||
72 | @Pure | ||
73 | public double getUpperBound() { | ||
74 | return this.upperBound; | ||
75 | } | ||
76 | } | ||
77 | |||
78 | @Data | ||
79 | public static final class Unknown extends ReliabilityResult { | ||
80 | private final String message; | ||
81 | |||
82 | private final Throwable cause; | ||
83 | |||
84 | @FinalFieldsConstructor | ||
85 | public Unknown(final String message, final Throwable cause) { | ||
86 | super(); | ||
87 | this.message = message; | ||
88 | this.cause = cause; | ||
89 | } | ||
90 | |||
91 | public Unknown(final String message) { | ||
92 | this(message, null); | ||
93 | } | ||
94 | |||
95 | @Override | ||
96 | public ReliabilityResult.Solution getOrThrow() { | ||
97 | throw new RuntimeException(this.message, this.cause); | ||
98 | } | ||
99 | |||
100 | @Override | ||
101 | @Pure | ||
102 | public int hashCode() { | ||
103 | final int prime = 31; | ||
104 | int result = 1; | ||
105 | result = prime * result + ((this.message== null) ? 0 : this.message.hashCode()); | ||
106 | return prime * result + ((this.cause== null) ? 0 : this.cause.hashCode()); | ||
107 | } | ||
108 | |||
109 | @Override | ||
110 | @Pure | ||
111 | public boolean equals(final Object obj) { | ||
112 | if (this == obj) | ||
113 | return true; | ||
114 | if (obj == null) | ||
115 | return false; | ||
116 | if (getClass() != obj.getClass()) | ||
117 | return false; | ||
118 | ReliabilityResult.Unknown other = (ReliabilityResult.Unknown) obj; | ||
119 | if (this.message == null) { | ||
120 | if (other.message != null) | ||
121 | return false; | ||
122 | } else if (!this.message.equals(other.message)) | ||
123 | return false; | ||
124 | if (this.cause == null) { | ||
125 | if (other.cause != null) | ||
126 | return false; | ||
127 | } else if (!this.cause.equals(other.cause)) | ||
128 | return false; | ||
129 | return true; | ||
130 | } | ||
131 | |||
132 | @Override | ||
133 | @Pure | ||
134 | public String toString() { | ||
135 | return new ToStringBuilder(this) | ||
136 | .addAllFields() | ||
137 | .toString(); | ||
138 | } | ||
139 | |||
140 | @Pure | ||
141 | public String getMessage() { | ||
142 | return this.message; | ||
143 | } | ||
144 | |||
145 | @Pure | ||
146 | public Throwable getCause() { | ||
147 | return this.cause; | ||
148 | } | ||
149 | } | ||
150 | |||
151 | public static final ReliabilityResult.Unknown TIMEOUT = new ReliabilityResult.Unknown("Solver timed out"); | ||
152 | |||
153 | public static final ReliabilityResult.Unknown MEMOUT = new ReliabilityResult.Unknown("Solver out of memory"); | ||
154 | |||
155 | public abstract ReliabilityResult.Solution getOrThrow(); | ||
156 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java deleted file mode 100644 index e1bb3625..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java +++ /dev/null | |||
@@ -1,31 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | import com.google.common.base.Objects; | ||
4 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic; | ||
5 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective; | ||
6 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration; | ||
7 | |||
8 | @SuppressWarnings("all") | ||
9 | public final class StormDftConfiguration extends SolverConfiguration { | ||
10 | public static final String DEFAULT_SOLVER_PATH = "storm-dft"; | ||
11 | |||
12 | public double precision = 1e-6; | ||
13 | |||
14 | public boolean bisimulation = true; | ||
15 | |||
16 | public boolean symmetryReduction = true; | ||
17 | |||
18 | public boolean modularization = true; | ||
19 | |||
20 | public boolean dontCarePropagation = true; | ||
21 | |||
22 | public double approximation = 0; | ||
23 | |||
24 | public ApproximationHeuristic approximationHeuristic = ApproximationHeuristic.NONE; | ||
25 | |||
26 | public FtAnalysisObjective objective; | ||
27 | |||
28 | public boolean isApproximationInUse() { | ||
29 | return (!Objects.equal(this.approximationHeuristic, ApproximationHeuristic.NONE)); | ||
30 | } | ||
31 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java deleted file mode 100644 index 955c9ed1..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java +++ /dev/null | |||
@@ -1,12 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | @SuppressWarnings("all") | ||
4 | public class StormDftException extends RuntimeException { | ||
5 | public StormDftException(final String s) { | ||
6 | super(s); | ||
7 | } | ||
8 | |||
9 | public StormDftException(final String s, final Exception e) { | ||
10 | super(s, e); | ||
11 | } | ||
12 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java deleted file mode 100644 index 46127425..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java +++ /dev/null | |||
@@ -1,330 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | import com.google.common.base.Objects; | ||
4 | import com.google.common.collect.ImmutableList; | ||
5 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic; | ||
6 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective; | ||
7 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult; | ||
8 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration; | ||
9 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftException; | ||
10 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel; | ||
11 | import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration; | ||
12 | import java.io.BufferedReader; | ||
13 | import java.io.IOException; | ||
14 | import java.io.InputStream; | ||
15 | import java.io.InputStreamReader; | ||
16 | import java.util.ArrayList; | ||
17 | import java.util.regex.Matcher; | ||
18 | import java.util.regex.Pattern; | ||
19 | import org.eclipse.xtend2.lib.StringConcatenation; | ||
20 | import org.eclipse.xtext.xbase.lib.CollectionLiterals; | ||
21 | import org.eclipse.xtext.xbase.lib.Exceptions; | ||
22 | import org.eclipse.xtext.xbase.lib.Extension; | ||
23 | import org.eclipse.xtext.xbase.lib.Functions.Function0; | ||
24 | import org.eclipse.xtext.xbase.lib.InputOutput; | ||
25 | import org.eclipse.xtext.xbase.lib.IterableExtensions; | ||
26 | |||
27 | @SuppressWarnings("all") | ||
28 | public class StormDftHandler { | ||
29 | private static final String DOUBLE_REGEX = "[-+]?[0-9]*\\.?[0-9]+([eE][-+]?[0-9]+)?"; | ||
30 | |||
31 | private static final String SINGLE_RESULT_GROUP = "single"; | ||
32 | |||
33 | private static final String LOWER_BOUND_GROUP = "lower"; | ||
34 | |||
35 | private static final String UPPER_BOUND_GROUP = "upper"; | ||
36 | |||
37 | private static final String RESULT_REGEX = new Function0<String>() { | ||
38 | public String apply() { | ||
39 | StringConcatenation _builder = new StringConcatenation(); | ||
40 | _builder.append("^Result:\\s*\\[(?:(?<"); | ||
41 | _builder.append(StormDftHandler.SINGLE_RESULT_GROUP); | ||
42 | _builder.append(">"); | ||
43 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
44 | _builder.append(")|\\((?<"); | ||
45 | _builder.append(StormDftHandler.LOWER_BOUND_GROUP); | ||
46 | _builder.append(">"); | ||
47 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
48 | _builder.append("),\\s*(?<"); | ||
49 | _builder.append(StormDftHandler.UPPER_BOUND_GROUP); | ||
50 | _builder.append(">"); | ||
51 | _builder.append(StormDftHandler.DOUBLE_REGEX); | ||
52 | _builder.append(")\\))\\]"); | ||
53 | return _builder.toString(); | ||
54 | } | ||
55 | }.apply(); | ||
56 | |||
57 | private static final Pattern RESULT_PATTERN = Pattern.compile(StormDftHandler.RESULT_REGEX); | ||
58 | |||
59 | private static final int SIGNAL_EXIT_VALUE_OFFSET = 0x80; | ||
60 | |||
61 | private static final int SIGXCPU = 24; | ||
62 | |||
63 | private static final int SIGXFSZ = 25; | ||
64 | |||
65 | private static final int STORM_GENERAL_ERROR = ((-1) & 0xff); | ||
66 | |||
67 | private static final int STORM_TIMEOUT = ((-2) & 0xff); | ||
68 | |||
69 | private static final int STORM_MEMOUT = ((-3) & 0xff); | ||
70 | |||
71 | public ReliabilityResult callSolver(final String dftFilePath, final StormDftConfiguration configuration) { | ||
72 | try { | ||
73 | ReliabilityResult _xblockexpression = null; | ||
74 | { | ||
75 | final ImmutableList<String> commandLine = this.toCommandLine(configuration, dftFilePath); | ||
76 | final DocumentationLevel documentationLevel = configuration.documentationLevel; | ||
77 | final boolean printOutput = (Objects.equal(documentationLevel, DocumentationLevel.NORMAL) || | ||
78 | Objects.equal(documentationLevel, DocumentationLevel.FULL)); | ||
79 | final ProcessBuilder processBuilder = new ProcessBuilder().command(commandLine); | ||
80 | Process process = null; | ||
81 | ReliabilityResult _xtrycatchfinallyexpression = null; | ||
82 | try { | ||
83 | ReliabilityResult _xtrycatchfinallyexpression_1 = null; | ||
84 | try { | ||
85 | ReliabilityResult _xblockexpression_1 = null; | ||
86 | { | ||
87 | process = processBuilder.start(); | ||
88 | process.getOutputStream().close(); | ||
89 | final ReliabilityResult.Solution result = this.readOutput(process.getInputStream(), printOutput); | ||
90 | final String error = this.readError(process.getErrorStream(), printOutput); | ||
91 | final int exitValue = process.waitFor(); | ||
92 | ReliabilityResult _xifexpression = null; | ||
93 | if ((result == null)) { | ||
94 | _xifexpression = this.interpretExitStatus(exitValue, error); | ||
95 | } else { | ||
96 | _xifexpression = result; | ||
97 | } | ||
98 | _xblockexpression_1 = _xifexpression; | ||
99 | } | ||
100 | _xtrycatchfinallyexpression_1 = _xblockexpression_1; | ||
101 | } catch (final Throwable _t) { | ||
102 | if (_t instanceof IOException) { | ||
103 | final IOException e = (IOException)_t; | ||
104 | throw new StormDftException("Error during input/output handling of the stochastic solver.", e); | ||
105 | } else { | ||
106 | throw Exceptions.sneakyThrow(_t); | ||
107 | } | ||
108 | } | ||
109 | _xtrycatchfinallyexpression = _xtrycatchfinallyexpression_1; | ||
110 | } catch (final Throwable _t_1) { | ||
111 | if (_t_1 instanceof Exception) { | ||
112 | final Exception e_1 = (Exception)_t_1; | ||
113 | if ((process != null)) { | ||
114 | process.destroyForcibly().waitFor(); | ||
115 | } | ||
116 | throw e_1; | ||
117 | } else { | ||
118 | throw Exceptions.sneakyThrow(_t_1); | ||
119 | } | ||
120 | } | ||
121 | _xblockexpression = _xtrycatchfinallyexpression; | ||
122 | } | ||
123 | return _xblockexpression; | ||
124 | } catch (Throwable _e) { | ||
125 | throw Exceptions.sneakyThrow(_e); | ||
126 | } | ||
127 | } | ||
128 | |||
129 | private ImmutableList<String> toCommandLine(@Extension final StormDftConfiguration configuration, final String dftFilePath) { | ||
130 | ImmutableList<String> _xblockexpression = null; | ||
131 | { | ||
132 | @Extension | ||
133 | final ImmutableList.Builder<String> optionsBuilder = ImmutableList.<String>builder(); | ||
134 | String _elvis = null; | ||
135 | if (configuration.solverPath != null) { | ||
136 | _elvis = configuration.solverPath; | ||
137 | } else { | ||
138 | _elvis = StormDftConfiguration.DEFAULT_SOLVER_PATH; | ||
139 | } | ||
140 | optionsBuilder.add(_elvis); | ||
141 | if ((configuration.runtimeLimit != SolverConfiguration.Unlimited)) { | ||
142 | optionsBuilder.add("--timeout", Integer.valueOf(configuration.runtimeLimit).toString()); | ||
143 | } | ||
144 | optionsBuilder.add("--precision", Double.valueOf(configuration.precision).toString()); | ||
145 | if (configuration.bisimulation) { | ||
146 | optionsBuilder.add("--bisimulation"); | ||
147 | } | ||
148 | if (configuration.symmetryReduction) { | ||
149 | optionsBuilder.add("--symmetryreduction"); | ||
150 | } | ||
151 | if (configuration.modularization) { | ||
152 | optionsBuilder.add("--modularisation"); | ||
153 | } | ||
154 | if ((!configuration.dontCarePropagation)) { | ||
155 | optionsBuilder.add("--disabledc"); | ||
156 | } | ||
157 | boolean _isApproximationInUse = configuration.isApproximationInUse(); | ||
158 | if (_isApproximationInUse) { | ||
159 | String _switchResult = null; | ||
160 | final ApproximationHeuristic approximationHeuristic = configuration.approximationHeuristic; | ||
161 | if (approximationHeuristic != null) { | ||
162 | switch (approximationHeuristic) { | ||
163 | case DEPTH: | ||
164 | _switchResult = "depth"; | ||
165 | break; | ||
166 | default: | ||
167 | throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic)); | ||
168 | } | ||
169 | } else { | ||
170 | throw new IllegalArgumentException(("Unknown approximation heuristic: " + configuration.approximationHeuristic)); | ||
171 | } | ||
172 | final String heuristicName = _switchResult; | ||
173 | optionsBuilder.add("--approximation", Double.valueOf(configuration.approximation).toString(), "--approximationheuristic", heuristicName); | ||
174 | } | ||
175 | optionsBuilder.add("--dftfile", dftFilePath); | ||
176 | final FtAnalysisObjective objective = configuration.objective; | ||
177 | boolean _matched = false; | ||
178 | if (Objects.equal(objective, FtAnalysisObjective.MTTF)) { | ||
179 | _matched=true; | ||
180 | optionsBuilder.add("--expectedtime"); | ||
181 | } | ||
182 | if (!_matched) { | ||
183 | if (objective instanceof FtAnalysisObjective.TimeBound) { | ||
184 | _matched=true; | ||
185 | optionsBuilder.add("--timebound"); | ||
186 | } | ||
187 | } | ||
188 | if (!_matched) { | ||
189 | throw new IllegalArgumentException(("Unknown analysis objective: " + configuration.objective)); | ||
190 | } | ||
191 | boolean _equals = Objects.equal(configuration.documentationLevel, DocumentationLevel.FULL); | ||
192 | if (_equals) { | ||
193 | optionsBuilder.add("--verbose"); | ||
194 | } | ||
195 | _xblockexpression = optionsBuilder.build(); | ||
196 | } | ||
197 | return _xblockexpression; | ||
198 | } | ||
199 | |||
200 | private ReliabilityResult.Solution readOutput(final InputStream inputStream, final boolean printOutput) { | ||
201 | try { | ||
202 | Object _xblockexpression = null; | ||
203 | { | ||
204 | InputStreamReader _inputStreamReader = new InputStreamReader(inputStream); | ||
205 | final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader); | ||
206 | try { | ||
207 | String line = null; | ||
208 | while (((line = bufferedReader.readLine()) != null)) { | ||
209 | { | ||
210 | if (printOutput) { | ||
211 | InputOutput.<String>println(line); | ||
212 | } | ||
213 | final Matcher matcher = StormDftHandler.RESULT_PATTERN.matcher(line); | ||
214 | boolean _find = matcher.find(); | ||
215 | if (_find) { | ||
216 | try { | ||
217 | final String single = matcher.group(StormDftHandler.SINGLE_RESULT_GROUP); | ||
218 | if ((single != null)) { | ||
219 | final double singleValue = Double.parseDouble(single); | ||
220 | return new ReliabilityResult.Solution(singleValue); | ||
221 | } | ||
222 | final String lower = matcher.group(StormDftHandler.LOWER_BOUND_GROUP); | ||
223 | final String upper = matcher.group(StormDftHandler.UPPER_BOUND_GROUP); | ||
224 | if (((lower != null) && (upper != null))) { | ||
225 | final double lowerValue = Double.parseDouble(lower); | ||
226 | final double upperValue = Double.parseDouble(upper); | ||
227 | return new ReliabilityResult.Solution(lowerValue, upperValue); | ||
228 | } | ||
229 | throw new StormDftException(("Inconsistent stochastic solver output: " + line)); | ||
230 | } catch (final Throwable _t) { | ||
231 | if (_t instanceof NumberFormatException) { | ||
232 | final NumberFormatException e = (NumberFormatException)_t; | ||
233 | throw new StormDftException("Malformatted number from stochastic solver.", e); | ||
234 | } else { | ||
235 | throw Exceptions.sneakyThrow(_t); | ||
236 | } | ||
237 | } | ||
238 | } | ||
239 | } | ||
240 | } | ||
241 | } finally { | ||
242 | bufferedReader.close(); | ||
243 | } | ||
244 | _xblockexpression = null; | ||
245 | } | ||
246 | return ((ReliabilityResult.Solution)_xblockexpression); | ||
247 | } catch (Throwable _e) { | ||
248 | throw Exceptions.sneakyThrow(_e); | ||
249 | } | ||
250 | } | ||
251 | |||
252 | private String readError(final InputStream inputStream, final boolean printOutput) { | ||
253 | try { | ||
254 | String _xblockexpression = null; | ||
255 | { | ||
256 | InputStreamReader _inputStreamReader = new InputStreamReader(inputStream); | ||
257 | final BufferedReader bufferedReader = new BufferedReader(_inputStreamReader); | ||
258 | String _xtrycatchfinallyexpression = null; | ||
259 | try { | ||
260 | String _xblockexpression_1 = null; | ||
261 | { | ||
262 | final ArrayList<String> lines = CollectionLiterals.<String>newArrayList(); | ||
263 | String line = null; | ||
264 | while (((line = bufferedReader.readLine()) != null)) { | ||
265 | { | ||
266 | if (printOutput) { | ||
267 | System.err.println(line); | ||
268 | } | ||
269 | lines.add(line); | ||
270 | } | ||
271 | } | ||
272 | _xblockexpression_1 = IterableExtensions.join(lines, "\n"); | ||
273 | } | ||
274 | _xtrycatchfinallyexpression = _xblockexpression_1; | ||
275 | } finally { | ||
276 | bufferedReader.close(); | ||
277 | } | ||
278 | _xblockexpression = _xtrycatchfinallyexpression; | ||
279 | } | ||
280 | return _xblockexpression; | ||
281 | } catch (Throwable _e) { | ||
282 | throw Exceptions.sneakyThrow(_e); | ||
283 | } | ||
284 | } | ||
285 | |||
286 | private ReliabilityResult.Unknown interpretExitStatus(final int exitValue, final String error) { | ||
287 | ReliabilityResult.Unknown _switchResult = null; | ||
288 | boolean _matched = false; | ||
289 | if (Objects.equal(exitValue, StormDftHandler.STORM_GENERAL_ERROR)) { | ||
290 | _matched=true; | ||
291 | throw new StormDftException(("Storm error: " + error)); | ||
292 | } | ||
293 | if (!_matched) { | ||
294 | if (Objects.equal(exitValue, StormDftHandler.STORM_TIMEOUT)) { | ||
295 | _matched=true; | ||
296 | } | ||
297 | if (!_matched) { | ||
298 | if (Objects.equal(exitValue, (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + StormDftHandler.SIGXCPU))) { | ||
299 | _matched=true; | ||
300 | } | ||
301 | } | ||
302 | if (_matched) { | ||
303 | _switchResult = ReliabilityResult.TIMEOUT; | ||
304 | } | ||
305 | } | ||
306 | if (!_matched) { | ||
307 | if (Objects.equal(exitValue, StormDftHandler.STORM_MEMOUT)) { | ||
308 | _matched=true; | ||
309 | } | ||
310 | if (!_matched) { | ||
311 | if (Objects.equal(exitValue, (StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET + StormDftHandler.SIGXFSZ))) { | ||
312 | _matched=true; | ||
313 | } | ||
314 | } | ||
315 | if (_matched) { | ||
316 | _switchResult = ReliabilityResult.MEMOUT; | ||
317 | } | ||
318 | } | ||
319 | if (!_matched) { | ||
320 | { | ||
321 | if ((exitValue > StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET)) { | ||
322 | final int signalNumber = (exitValue - StormDftHandler.SIGNAL_EXIT_VALUE_OFFSET); | ||
323 | throw new StormDftException(((("Storm unexpectedly killed by signal " + Integer.valueOf(signalNumber)) + ": ") + error)); | ||
324 | } | ||
325 | throw new StormDftException(((("Storm unexpectedly exit with status " + Integer.valueOf(exitValue)) + ": ") + error)); | ||
326 | } | ||
327 | } | ||
328 | return _switchResult; | ||
329 | } | ||
330 | } | ||
diff --git a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java b/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java deleted file mode 100644 index 491e7fc1..00000000 --- a/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java +++ /dev/null | |||
@@ -1,79 +0,0 @@ | |||
1 | package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver; | ||
2 | |||
3 | import com.google.common.base.Objects; | ||
4 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantModel; | ||
5 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree; | ||
6 | import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ReliabilityModel; | ||
7 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo.Ft2GalileoTransformation; | ||
8 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective; | ||
9 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult; | ||
10 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration; | ||
11 | import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftHandler; | ||
12 | import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace; | ||
13 | |||
14 | @SuppressWarnings("all") | ||
15 | public class StormDftSolver { | ||
16 | private static final String DFT_FILE_NAME = "ft.dft"; | ||
17 | |||
18 | private final Ft2GalileoTransformation ft2Galileo = new Ft2GalileoTransformation(); | ||
19 | |||
20 | private final StormDftHandler handler = new StormDftHandler(); | ||
21 | |||
22 | public ReliabilityResult solve(final ReliabilityModel reliabilityModel, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) { | ||
23 | ReliabilityResult _switchResult = null; | ||
24 | boolean _matched = false; | ||
25 | if (reliabilityModel instanceof FaultTree) { | ||
26 | _matched=true; | ||
27 | _switchResult = this.solve(((FaultTree)reliabilityModel), configuration, reasonerWorkspace); | ||
28 | } | ||
29 | if (!_matched) { | ||
30 | if (reliabilityModel instanceof ConstantModel) { | ||
31 | _matched=true; | ||
32 | ReliabilityResult.Solution _xblockexpression = null; | ||
33 | { | ||
34 | double _xifexpression = (double) 0; | ||
35 | boolean _isFailed = ((ConstantModel)reliabilityModel).isFailed(); | ||
36 | if (_isFailed) { | ||
37 | _xifexpression = 0; | ||
38 | } else { | ||
39 | double _switchResult_1 = (double) 0; | ||
40 | final FtAnalysisObjective objective = configuration.objective; | ||
41 | boolean _matched_1 = false; | ||
42 | if (Objects.equal(objective, FtAnalysisObjective.MTTF)) { | ||
43 | _matched_1=true; | ||
44 | _switchResult_1 = Double.POSITIVE_INFINITY; | ||
45 | } | ||
46 | if (!_matched_1) { | ||
47 | if (objective instanceof FtAnalysisObjective.TimeBound) { | ||
48 | _matched_1=true; | ||
49 | _switchResult_1 = 1; | ||
50 | } | ||
51 | } | ||
52 | if (!_matched_1) { | ||
53 | throw new IllegalArgumentException(("Unknown objective: " + objective)); | ||
54 | } | ||
55 | _xifexpression = _switchResult_1; | ||
56 | } | ||
57 | final double result = _xifexpression; | ||
58 | _xblockexpression = new ReliabilityResult.Solution(result); | ||
59 | } | ||
60 | _switchResult = _xblockexpression; | ||
61 | } | ||
62 | } | ||
63 | if (!_matched) { | ||
64 | throw new IllegalArgumentException(("Unknown reliability model: " + reliabilityModel)); | ||
65 | } | ||
66 | return _switchResult; | ||
67 | } | ||
68 | |||
69 | public ReliabilityResult solve(final FaultTree faultTree, final StormDftConfiguration configuration, final ReasonerWorkspace reasonerWorkspace) { | ||
70 | ReliabilityResult _xblockexpression = null; | ||
71 | { | ||
72 | final CharSequence galileo = this.ft2Galileo.toGalileo(faultTree); | ||
73 | reasonerWorkspace.writeText(StormDftSolver.DFT_FILE_NAME, galileo); | ||
74 | final String dftFilePath = reasonerWorkspace.getFile(StormDftSolver.DFT_FILE_NAME).getAbsolutePath(); | ||
75 | _xblockexpression = this.handler.callSolver(dftFilePath, configuration); | ||
76 | } | ||
77 | return _xblockexpression; | ||
78 | } | ||
79 | } | ||