blob: 27903708adb9810135609a6129e712841cac13dc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
% EXPECT: sat
% Preamble --------------
DATATYPE UNIT = Unit END;
DATATYPE BOOL = Truth | Falsity END;
% Decls --------------
node$type: TYPE;
value$type: TYPE;
Nodes$elem$type: TYPE = node$type;
Nodes$t$type: TYPE;
node_pair_set$type: TYPE = ARRAY node$type OF ARRAY node$type OF BOOL;
failure_pattern$type: TYPE = node_pair_set$type;
is_faulty:(node$type, failure_pattern$type) -> BOOL = (LAMBDA (p: node$type,
deliver: failure_pattern$type):
(IF (EXISTS (q: node$type):
(NOT ((((deliver)[
(p)])[
(q)]) =
(Truth)))) THEN
(Truth) ELSE (Falsity) ENDIF));
CHECKSAT;
|