aboutsummaryrefslogtreecommitdiffstats
path: root/Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver
diff options
context:
space:
mode:
Diffstat (limited to 'Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver')
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.ReliabilityResult.xtendbinbin5435 -> 0 bytes
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftConfiguration.xtendbinbin4311 -> 0 bytes
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftHandler.xtendbinbin13570 -> 0 bytes
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.StormDftSolver.xtendbinbin4801 -> 0 bytes
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/.gitignore20
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ApproximationHeuristic.java8
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/FtAnalysisObjective.java14
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/ReliabilityResult.java156
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftConfiguration.java31
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftException.java12
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftHandler.java330
-rw-r--r--Stochastic/hu.bme.mit.inf.dslreasoner.faulttree.transformation/xtend-gen/hu/bme/mit/inf/dslreasoner/faulttree/transformation/solver/StormDftSolver.java79
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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3@SuppressWarnings("all")
4public 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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3@SuppressWarnings("all")
4public 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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3import org.eclipse.xtend.lib.annotations.Data;
4import org.eclipse.xtend.lib.annotations.FinalFieldsConstructor;
5import org.eclipse.xtext.xbase.lib.Pure;
6import org.eclipse.xtext.xbase.lib.util.ToStringBuilder;
7
8@SuppressWarnings("all")
9public 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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3import com.google.common.base.Objects;
4import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic;
5import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
6import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration;
7
8@SuppressWarnings("all")
9public 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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3@SuppressWarnings("all")
4public 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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3import com.google.common.base.Objects;
4import com.google.common.collect.ImmutableList;
5import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ApproximationHeuristic;
6import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
7import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult;
8import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration;
9import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftException;
10import hu.bme.mit.inf.dslreasoner.logic.model.builder.DocumentationLevel;
11import hu.bme.mit.inf.dslreasoner.logic.model.builder.SolverConfiguration;
12import java.io.BufferedReader;
13import java.io.IOException;
14import java.io.InputStream;
15import java.io.InputStreamReader;
16import java.util.ArrayList;
17import java.util.regex.Matcher;
18import java.util.regex.Pattern;
19import org.eclipse.xtend2.lib.StringConcatenation;
20import org.eclipse.xtext.xbase.lib.CollectionLiterals;
21import org.eclipse.xtext.xbase.lib.Exceptions;
22import org.eclipse.xtext.xbase.lib.Extension;
23import org.eclipse.xtext.xbase.lib.Functions.Function0;
24import org.eclipse.xtext.xbase.lib.InputOutput;
25import org.eclipse.xtext.xbase.lib.IterableExtensions;
26
27@SuppressWarnings("all")
28public 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 @@
1package hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver;
2
3import com.google.common.base.Objects;
4import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ConstantModel;
5import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.FaultTree;
6import hu.bme.mit.inf.dslreasoner.faulttree.model.ft.ReliabilityModel;
7import hu.bme.mit.inf.dslreasoner.faulttree.transformation.ft2galileo.Ft2GalileoTransformation;
8import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.FtAnalysisObjective;
9import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.ReliabilityResult;
10import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftConfiguration;
11import hu.bme.mit.inf.dslreasoner.faulttree.transformation.solver.StormDftHandler;
12import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace;
13
14@SuppressWarnings("all")
15public 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}
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-08-25 14:37:50 +0000