-
-
Notifications
You must be signed in to change notification settings - Fork 194
/
EC.java
418 lines (359 loc) · 20.4 KB
/
EC.java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
package tlc2.output;
import java.util.Set;
import java.util.stream.Collectors;
import java.util.stream.Stream;
/**
* Interface containing the error code constants
* @author Simon Zambrovski
* @version $Id$
*/
public interface EC
{
// This is reserved so that an optional error code can be safely represented in a single int
public static final int NO_ERROR = 0;
// Check and CheckImpl
// check if the TLC option is the same for params
public static final int CHECK_FAILED_TO_CHECK = 3000;
public static final int CHECK_COULD_NOT_READ_TRACE = 3001;
public static final int CHECK_PARAM_EXPECT_CONFIG_FILENAME = 3100;
public static final int CHECK_PARAM_USAGE = 3101;
public static final int CHECK_PARAM_MISSING_TLA_MODULE = 3102;
public static final int CHECK_PARAM_NEED_TO_SPECIFY_CONFIG_DIR = 3103;
public static final int CHECK_PARAM_WORKER_NUMBER_REQUIRED = 3104;
public static final int CHECK_PARAM_WORKER_NUMBER_TOO_SMALL = 3105;
public static final int CHECK_PARAM_WORKER_NUMBER_REQUIRED2 = 3106;
public static final int CHECK_PARAM_DEPTH_REQUIRED = 3107;
public static final int CHECK_PARAM_DEPTH_REQUIRED2 = 3108;
public static final int CHECK_PARAM_TRACE_REQUIRED = 3109;
public static final int CHECK_PARAM_COVREAGE_REQUIRED = 3110;
public static final int CHECK_PARAM_COVREAGE_REQUIRED2 = 3111;
public static final int CHECK_PARAM_COVREAGE_TOO_SMALL = 3112;
public static final int CHECK_PARAM_UNRECOGNIZED = 3113;
public static final int CHECK_PARAM_TOO_MANY_INPUT_FILES = 3114;
public final static int SANY_PARSER_CHECK_1 = 4000;
public final static int SANY_PARSER_CHECK_2 = 4001;
public final static int SANY_PARSER_CHECK_3 = 4002;
public static final int UNKNOWN = -1; // TODO remove all these
public final static int UNIT_TEST = -123456;
/**
* A feature of TLA+/TLC is not supported by TLC's current mode. E.g.
* TLCGet/TLCSet operator cannot be used in distributed TLC.
*/
public static final int TLC_FEATURE_UNSUPPORTED = 2156;
public static final int TLC_FEATURE_UNSUPPORTED_LIVENESS_SYMMETRY = 2279;
public static final int TLC_FEATURE_LIVENESS_CONSTRAINTS = 2284;
public static final int GENERAL = 1000;
public static final int SYSTEM_OUT_OF_MEMORY = 1001;
public static final int SYSTEM_OUT_OF_MEMORY_TOO_MANY_INIT = 1002;
public static final int SYSTEM_STACK_OVERFLOW = 1005;
public static final int WRONG_COMMANDLINE_PARAMS_SIMULATOR = 1101;
public static final int WRONG_COMMANDLINE_PARAMS_TLC = 1102;
public static final int TLC_PP_PARSING_VALUE = 2000;
public static final int TLC_PP_FORMATING_VALUE = 2001;
public static final int TLC_METADIR_EXISTS = 2100;
public static final int TLC_METADIR_CAN_NOT_BE_CREATED = 2101;
public static final int TLC_INITIAL_STATE = 2102;
public static final int TLC_NESTED_EXPRESSION = 2103;
public static final int TLC_ASSUMPTION_FALSE = 2104;
public static final int TLC_ASSUMPTION_EVALUATION_ERROR = 2105;
public static final int TLC_STATE_NOT_COMPLETELY_SPECIFIED_INITIAL = 2106;
public static final int TLC_INVARIANT_VIOLATED_INITIAL = 2107;
public static final int TLC_PROPERTY_VIOLATED_INITIAL = 2108;
public static final int TLC_STATE_NOT_COMPLETELY_SPECIFIED_NEXT = 2109;
public static final int TLC_INVARIANT_VIOLATED_BEHAVIOR = 2110;
public static final int TLC_INVARIANT_EVALUATION_FAILED = 2111;
public static final int TLC_INVARIANT_VIOLATED_LEVEL = 2146;
public static final int TLC_ACTION_PROPERTY_VIOLATED_BEHAVIOR = 2112;
public static final int TLC_ACTION_PROPERTY_EVALUATION_FAILED = 2113;
public static final int TLC_DEADLOCK_REACHED = 2114;
public static final int TLC_STATES_AND_NO_NEXT_ACTION = 2115;
public static final int TLC_TEMPORAL_PROPERTY_VIOLATED = 2116;
public static final int TLC_FAILED_TO_RECOVER_NEXT = 2117;
public static final int TLC_NO_STATES_SATISFYING_INIT = 2118;
public static final int TLC_STRING_MODULE_NOT_FOUND = 2119;
public static final int TLC_ERROR_STATE = 2120;
public static final int TLC_BEHAVIOR_UP_TO_THIS_POINT = 2121;
public static final int TLC_BACK_TO_STATE = 2122; // The "back to state" message from a liveness-error trace.
public static final int TLC_FAILED_TO_RECOVER_INIT = 2123;
public static final int TLC_REPORTER_DIED = 2124;
public static final int SYSTEM_ERROR_READING_POOL = 2125;
public static final int SYSTEM_CHECKPOINT_RECOVERY_CORRUPT = 2126;
public static final int SYSTEM_ERROR_WRITING_POOL = 2127;
public static final int SYSTEM_ERROR_CLEANING_POOL = 2270;
public static final int SYSTEM_INDEX_ERROR = 2134;
public static final int SYSTEM_STREAM_EMPTY = 2135;
public static final int SYSTEM_FILE_NULL = 2137;
public static final int SYSTEM_INTERRUPTED = 2138;
public static final int SYSTEM_UNABLE_NOT_RENAME_FILE = 2160;
public static final int SYSTEM_DISK_IO_ERROR_FOR_FILE = 2161;
public static final int SYSTEM_METADIR_EXISTS = 2162;
public static final int SYSTEM_METADIR_CREATION_ERROR = 2163;
public static final int SYSTEM_UNABLE_TO_OPEN_FILE = 2167;
public static final int TLC_BUG = 2128; // TODO Bad description
public static final int TLC_FINGERPRINT_EXCEPTION = 2147;
public static final int SYSTEM_DISKGRAPH_ACCESS = 2129; // TODO refactor
public static final int TLC_AAAAAAA = 2130;
public static final int TLC_REGISTRY_INIT_ERROR = 2131;
public static final int TLC_CHOOSE_ARGUMENTS_WRONG = 2164;
public static final int TLC_CHOOSE_UPPER_BOUND = 2165;
public static final int TLC_VALUE_ASSERT_FAILED = 2132;
public static final int TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE = 2154;
public static final int TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_LOADED = 2168;
public static final int TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MISMATCH = 2400;
public static final int TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_MODULE_MISMATCH = 2402;
public static final int TLC_MODULE_VALUE_JAVA_METHOD_OVERRIDE_IDENTIFIER_MISMATCH = 2403;
// User-provided module overrides print to stdout.
public static final int TLC_MODULE_OVERRIDE_STDOUT = 20000;
public static final int TLC_FP_NOT_IN_SET = 2133;
public static final int TLC_FP_VALUE_ALREADY_ON_DISK = 2166;
public static final int TLC_LIVE_BEGRAPH_FAILED_TO_CONSTRUCT = 2159;
public static final int TLC_PARAMETER_MUST_BE_POSTFIX = 2136;
public static final int TLC_COULD_NOT_DETERMINE_SUBSCRIPT = 2139;
public static final int TLC_SUBSCRIPT_CONTAIN_NO_STATE_VAR = 2140;
public static final int TLC_WRONG_TUPLE_FIELD_NAME = 2141;
public static final int TLC_WRONG_RECORD_FIELD_NAME = 2142;
public static final int TLC_UNCHANGED_VARIABLE_CHANGED = 2143;
public static final int TLC_EXCEPT_APPLIED_TO_UNKNOWN_FIELD = 2144;
public static final int TLC_MODULE_TLCGET_UNDEFINED = 2145;
/** Attempted to compare %1% with the value\n%2% */
public static final int TLC_MODULE_COMPARE_VALUE = 2155;
public static final int TLC_MODULE_CHECK_MEMBER_OF = 2158;
public static final int TLC_MODULE_TRANSITIVE_CLOSURE = 2157;
/** The %1% argument of %2% should be a %3%, but instead it is:<br>%4% */
public static final int TLC_MODULE_ARGUMENT_ERROR = 2169;
/** Simon used an argument like "\bn apple" to TLC_MODULE_ARGUMENT_ERROR to turn
* an "a" into an "an". This doesn't work on the Toolbox's console. Hence, LL added
* the following message type on 21 May 2012. */
public static final int TLC_MODULE_ARGUMENT_ERROR_AN = 2266;
public static final int TLC_MODULE_ONE_ARGUMENT_ERROR = 2283;
public static final int TLC_ARGUMENT_MISMATCH = 2170;
public static final int TLC_PARSING_FAILED2 = 2171;
public static final int TLC_PARSING_FAILED = 3002;
public static final int TLC_TOO_MNY_POSSIBLE_STATES = 2172;
public static final int TLC_ERROR_REPLACING_MODULES = 2173;
public static final int SYSTEM_ERROR_READING_STATES = 2174;
public static final int SYSTEM_ERROR_WRITING_STATES = 2175;
public static final int TLC_MODULE_APPLYING_TO_WRONG_VALUE = 2176;
public static final int TLC_MODULE_BAG_UNION1 = 2177;
public static final int TLC_MODULE_OVERFLOW = 2178;
public static final int TLC_MODULE_DIVISION_BY_ZERO = 2179;
public static final int TLC_MODULE_NULL_POWER_NULL = 2180;
public static final int TLC_MODULE_COMPUTING_CARDINALITY = 2181;
public static final int TLC_MODULE_EVALUATING = 2182;
/** The %1% argument of %2% must be in the domain of its first argument:<br>%3%<br>, but instead it is<br>%4% */
public static final int TLC_MODULE_ARGUMENT_NOT_IN_DOMAIN = 2183;
public static final int TLC_MODULE_APPLY_EMPTY_SEQ = 2184;
public static final int TLC_SYMMETRY_SET_TOO_SMALL = 2300;
public static final int TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS = 2301;
public static final int TLC_STARTING = 2185;
public static final int TLC_FINISHED = 2186;
// distributed TLC
public static final int TLC_DISTRIBUTED_SERVER_RUNNING = 7000;
public static final int TLC_DISTRIBUTED_WORKER_REGISTERED = TLC_DISTRIBUTED_SERVER_RUNNING + 1;
public static final int TLC_DISTRIBUTED_WORKER_DEREGISTERED = TLC_DISTRIBUTED_WORKER_REGISTERED + 1;
public static final int TLC_DISTRIBUTED_WORKER_STATS = TLC_DISTRIBUTED_WORKER_DEREGISTERED + 1;
public static final int TLC_DISTRIBUTED_SERVER_NOT_RUNNING = TLC_DISTRIBUTED_WORKER_STATS + 1;
public static final int TLC_DISTRIBUTED_VM_VERSION = TLC_DISTRIBUTED_SERVER_NOT_RUNNING + 1;
public static final int TLC_DISTRIBUTED_WORKER_LOST = TLC_DISTRIBUTED_VM_VERSION + 1;
public static final int TLC_DISTRIBUTED_EXCEED_BLOCKSIZE = TLC_DISTRIBUTED_WORKER_LOST + 1;
public static final int TLC_DISTRIBUTED_SERVER_FPSET_WAITING = TLC_DISTRIBUTED_EXCEED_BLOCKSIZE + 1;
public static final int TLC_DISTRIBUTED_SERVER_FPSET_REGISTERED = TLC_DISTRIBUTED_SERVER_FPSET_WAITING + 1;
public static final int TLC_DISTRIBUTED_SERVER_FINISHED = TLC_DISTRIBUTED_SERVER_FPSET_REGISTERED + 1;
// errors during parsing of the model configuration
public static final int CFG_ERROR_READING_FILE = 5001;
public static final int CFG_GENERAL = 5002;
public static final int CFG_MISSING_ID = 5003;
public static final int CFG_TWICE_KEYWORD = 5004;
public static final int CFG_EXPECT_ID = 5005;
public static final int CFG_EXPECTED_SYMBOL = 5006;
public static final int TLC_MODE_MC = 2187;
public static final int TLC_MODE_MC_DFS = 2271;
public static final int TLC_MODE_SIMU = 2188;
public static final int TLC_COMPUTING_INIT = 2189;
public static final int TLC_COMPUTING_INIT_PROGRESS = 2269;
public static final int TLC_INIT_GENERATED1 = 2190;
public static final int TLC_INIT_GENERATED2 = 2191;
public static final int TLC_INIT_GENERATED3 = 2207;
public static final int TLC_INIT_GENERATED4 = 2208;
public static final int TLC_CHECKING_TEMPORAL_PROPS = 2192;
public static final int TLC_CHECKING_TEMPORAL_PROPS_END = 2267;
public static final int TLC_SUCCESS = 2193;
public static final int TLC_SEARCH_DEPTH = 2194;
public static final int TLC_STATE_GRAPH_OUTDEGREE = 2268;
public static final int TLC_CHECKPOINT_START = 2195;
public static final int TLC_CHECKPOINT_END = 2196;
public static final int TLC_CHECKPOINT_RECOVER_START = 2197;
public static final int TLC_CHECKPOINT_RECOVER_END = 2198;
public static final int TLC_STATS = 2199;
public static final int TLC_STATS_DFID = 2204;
public static final int TLC_STATS_SIMU = 2210;
public static final int TLC_PROGRESS_STATS = 2200;
public static final int TLC_COVERAGE_START = 2201;
public static final int TLC_COVERAGE_END = 2202;
public static final int TLC_CHECKPOINT_RECOVER_END_DFID = 2203;
public static final int TLC_PROGRESS_START_STATS_DFID = 2205;
public static final int TLC_PROGRESS_STATS_DFID = 2206;
public static final int TLC_PROGRESS_SIMU = 2209;
public static final int TLC_FP_COMPLETED = 2211;
public static final int TLC_LIVE_IMPLIED = 2212;
public static final int TLC_LIVE_CANNOT_HANDLE_FORMULA = 2213;
public static final int TLC_LIVE_WRONG_FORMULA_FORMAT = 2214;
public static final int TLC_LIVE_ENCOUNTERED_ACTIONS = 2249;
public static final int TLC_LIVE_STATE_PREDICATE_NON_BOOL = 2250;
public static final int TLC_LIVE_CANNOT_EVAL_FORMULA = 2251;
public static final int TLC_LIVE_ENCOUNTERED_NONBOOL_PREDICATE = 2252;
public static final int TLC_LIVE_FORMULA_TAUTOLOGY = 2253;
public static final int TLC_EXPECTED_VALUE = 2215;
public static final int TLC_EXPECTED_EXPRESSION = 2246;
public static final int TLC_EXPECTED_EXPRESSION_IN_COMPUTING = 2247;
public static final int TLC_EXPECTED_EXPRESSION_IN_COMPUTING2 = 2248;
// state printing
public static final int TLC_STATE_PRINT1 = 2216;
public static final int TLC_STATE_PRINT2 = 2217;
public static final int TLC_STATE_PRINT3 = 2218; // This seems to be a "Stuttering" message from a liveness-error trace
public static final int TLC_SANY_END = 2219;
public static final int TLC_SANY_START = 2220;
public static final int TLC_COVERAGE_MISMATCH = 2776;
public static final int TLC_COVERAGE_VALUE = 2221;
public static final int TLC_COVERAGE_VALUE_COST = 2775;
public static final int TLC_COVERAGE_NEXT = 2772;
public static final int TLC_COVERAGE_INIT = 2773;
public static final int TLC_COVERAGE_PROPERTY = 2774;
public static final int TLC_COVERAGE_END_OVERHEAD = 2777;
// config file errors
public static final int TLC_CONFIG_VALUE_NOT_ASSIGNED_TO_CONSTANT_PARAM = 2222;
public static final int TLC_CONFIG_RHS_ID_APPEARED_AFTER_LHS_ID = 2223;
public static final int TLC_CONFIG_WRONG_SUBSTITUTION = 2224;
public static final int TLC_CONFIG_WRONG_SUBSTITUTION_NUMBER_OF_ARGS = 2225;
public static final int TLC_CONFIG_UNDEFINED_OR_NO_OPERATOR = 2280;
public static final int TLC_CONFIG_SUBSTITUTION_NON_CONSTANT = 2281;
public static final int TLC_CONFIG_ID_DOES_NOT_APPEAR_IN_SPEC = 2226;
public static final int TLC_CONFIG_NOT_BOTH_SPEC_AND_INIT = 2227;
public static final int TLC_CONFIG_ID_REQUIRES_NO_ARG = 2228;
public static final int TLC_CONFIG_SPECIFIED_NOT_DEFINED = 2229;
public static final int TLC_CONFIG_ID_HAS_VALUE = 2230;
public static final int TLC_CONFIG_MISSING_INIT = 2231;
public static final int TLC_CONFIG_MISSING_NEXT = 2232;
public static final int TLC_CONFIG_ID_MUST_NOT_BE_CONSTANT = 2233;
public static final int TLC_CONFIG_OP_NO_ARGS = 2234;
public static final int TLC_CONFIG_OP_NOT_IN_SPEC = 2235;
public static final int TLC_CONFIG_OP_IS_EQUAL = 2236;
public static final int TLC_CONFIG_SPEC_IS_TRIVIAL = 2237;
public static final int TLC_CANT_HANDLE_SUBSCRIPT = 2238;
public static final int TLC_CANT_HANDLE_CONJUNCT = 2239;
public static final int TLC_CANT_HANDLE_TOO_MANY_NEXT_STATE_RELS = 2240;
public static final int TLC_CONFIG_PROPERTY_NOT_CORRECTLY_DEFINED = 2241;
public static final int TLC_CONFIG_OP_ARITY_INCONSISTENT = 2242;
public static final int TLC_CONFIG_NO_STATE_TYPE = 2243;
public static final int TLC_CANT_HANDLE_REAL_NUMBERS = 2244;
public static final int TLC_NO_MODULES = 2245;
public static final int TLC_ENABLED_WRONG_FORMULA = 2260;
public static final int TLC_ENCOUNTERED_FORMULA_IN_PREDICATE = 2261;
public static final int TLC_VERSION = 2262;
public static final int TLC_USAGE = 2263;
public static final int TLC_COUNTER_EXAMPLE = 2264;
public static final int TLC_INTEGER_TOO_BIG = 2265;
public static final int TLC_TRACE_TOO_LONG = 2282;
public static final int TLC_ENVIRONMENT_JVM_GC = 2401;
//**************************************************************//
// Mapping error constants above to process exit/return values. //
// Because Linux and macOS only support 8-bit exit values, this //
// mapping is necessary. //
//**************************************************************//
public static class ExitStatus {
public static final int ERROR = 255;
public static final int SUCCESS = 0;
// (Safety/Liveness) Violations
public static final int VIOLATION_ASSUMPTION = 10;
public static final int VIOLATION_DEADLOCK = VIOLATION_ASSUMPTION + 1;
public static final int VIOLATION_SAFETY = VIOLATION_DEADLOCK + 1;
public static final int VIOLATION_LIVENESS = VIOLATION_SAFETY + 1;
public static final int VIOLATION_ASSERT = VIOLATION_LIVENESS + 1;
// Evaluation failures
public static final int FAILURE_SPEC_EVAL = 75;
public static final int FAILURE_SAFETY_EVAL = FAILURE_SPEC_EVAL + 1;
public static final int FAILURE_LIVENESS_EVAL = FAILURE_SAFETY_EVAL + 1;
// Errors
public static final int ERROR_SPEC_PARSE = 150;
public static final int ERROR_CONFIG_PARSE = ERROR_SPEC_PARSE + 1;
public static final int ERROR_STATESPACE_TOO_LARGE = ERROR_CONFIG_PARSE + 1;
public static final int ERROR_SYSTEM = ERROR_STATESPACE_TOO_LARGE + 1;
/**
* Returns an exit status for an error code.
*/
public static int errorConstantToExitStatus(final int ec) {
// TODO Allocate a range of exit status to indicate classes of errors.
// For a great example of potential classes see: https://github.com/tlaplus/tlaplus/pull/308#discussion_r285840112
switch (ec) {
case NO_ERROR:
return SUCCESS;
// failures
case TLC_LIVE_FORMULA_TAUTOLOGY:
return FAILURE_LIVENESS_EVAL;
case TLC_STATE_NOT_COMPLETELY_SPECIFIED_NEXT:
case TLC_STATES_AND_NO_NEXT_ACTION:
case TLC_NESTED_EXPRESSION:
case TLC_FINGERPRINT_EXCEPTION:
return FAILURE_SPEC_EVAL;
case TLC_INVARIANT_EVALUATION_FAILED:
case TLC_INVARIANT_VIOLATED_LEVEL:
return FAILURE_SAFETY_EVAL;
// violations
case TLC_INVARIANT_VIOLATED_INITIAL:
case TLC_INVARIANT_VIOLATED_BEHAVIOR:
return VIOLATION_SAFETY;
case TLC_ACTION_PROPERTY_VIOLATED_BEHAVIOR:
case TLC_ACTION_PROPERTY_EVALUATION_FAILED:
case TLC_TEMPORAL_PROPERTY_VIOLATED:
case TLC_PROPERTY_VIOLATED_INITIAL:
return VIOLATION_LIVENESS;
case TLC_DEADLOCK_REACHED:
return VIOLATION_DEADLOCK;
case TLC_ASSUMPTION_FALSE:
case TLC_ASSUMPTION_EVALUATION_ERROR:
return VIOLATION_ASSUMPTION;
case TLC_VALUE_ASSERT_FAILED:
return VIOLATION_ASSERT;
// errors
case TLC_CONFIG_VALUE_NOT_ASSIGNED_TO_CONSTANT_PARAM:
case TLC_CONFIG_RHS_ID_APPEARED_AFTER_LHS_ID:
case TLC_CONFIG_WRONG_SUBSTITUTION:
case TLC_CONFIG_WRONG_SUBSTITUTION_NUMBER_OF_ARGS:
case TLC_CONFIG_UNDEFINED_OR_NO_OPERATOR:
case TLC_CONFIG_SUBSTITUTION_NON_CONSTANT:
case TLC_CONFIG_ID_DOES_NOT_APPEAR_IN_SPEC:
case TLC_CONFIG_NOT_BOTH_SPEC_AND_INIT:
case TLC_CONFIG_ID_REQUIRES_NO_ARG:
case TLC_CONFIG_SPECIFIED_NOT_DEFINED:
case TLC_CONFIG_ID_HAS_VALUE:
case TLC_CONFIG_MISSING_INIT:
case TLC_CONFIG_MISSING_NEXT:
case TLC_CONFIG_ID_MUST_NOT_BE_CONSTANT:
case TLC_CONFIG_OP_NO_ARGS:
case TLC_CONFIG_OP_NOT_IN_SPEC:
case TLC_CONFIG_OP_IS_EQUAL:
case TLC_CONFIG_SPEC_IS_TRIVIAL:
case TLC_CANT_HANDLE_SUBSCRIPT:
case TLC_CANT_HANDLE_CONJUNCT:
case TLC_CANT_HANDLE_TOO_MANY_NEXT_STATE_RELS:
case TLC_CONFIG_PROPERTY_NOT_CORRECTLY_DEFINED:
case TLC_CONFIG_OP_ARITY_INCONSISTENT:
case TLC_CONFIG_NO_STATE_TYPE:
case TLC_CANT_HANDLE_REAL_NUMBERS: // might also be in the spec
case TLC_NO_MODULES:
return ERROR_CONFIG_PARSE;
case TLC_PARSING_FAILED2:
case TLC_PARSING_FAILED:
return ERROR_SPEC_PARSE;
default:
return 255;
}
}
private static final Set<Integer> knownExitValues = Stream.of(SUCCESS, FAILURE_LIVENESS_EVAL, FAILURE_SPEC_EVAL,
FAILURE_SAFETY_EVAL, VIOLATION_SAFETY, VIOLATION_LIVENESS, VIOLATION_DEADLOCK, VIOLATION_ASSUMPTION,
VIOLATION_ASSERT, ERROR_CONFIG_PARSE, ERROR_SPEC_PARSE).collect(Collectors.toSet());
public static boolean exitStatusToCrash(final int exitStatus) {
return !knownExitValues.contains(exitStatus);
}
}
}