-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathMALFO.p9
More file actions
44 lines (44 loc) · 3.98 KB
/
MALFO.p9
File metadata and controls
44 lines (44 loc) · 3.98 KB
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
formulas(sos).
(all x ((State(x) | Process(x) | Event(x)) -> Occurrent(x))).
(all x (State(x) -> -(Process(x) | Event(x)))).
(all x (Process(x) -> -(Event(x)))).
(all x all y (causeOf(x,y) -> (Occurrent(x) & Occurrent(y)))).
(all x all y -(causeOf(x,x))).
(all x all y (causeOf(x,y) -> -(causeOf(y,x)))).
(all x all y (causeOf(x,y) <-> (achieves(x,y) | prevents(x,y) | allows(x,y) | disallows(x,y)))).
(all x all y (posCauseOf(x,y) <-> (achieves(x,y) | allows(x,y) | facilPreconditionFor(x,y)))).
(all x all y (achieves(x,y) -> ((Event(x) | Process(x) | State(x)) & (Process(y) | State(y)) & -(State(x) & Process(y))))).
(all x all y (prevents(x,y) <-> (exists z (State(z) & incompatibleWith(z,y) & achieves(x,z))))).
(all x all y (prevents(x,y) -> ((Event(x) | Process(x) | State(x)) & (Process(y) | State(y)) & -(State(x) & Process(y))))).
(all z all y (facilPreconditionFor(z,y) -> (State(z) & (Event(y) | Process(y) | State(y))))).
(all z all y (prevPreconditionFor(z,y) -> (State(z) & (Event(y) | Process(y) | State(y))))).
(all z all y all w ((incompatibleWith(z,w) & prevPreconditionFor(w,y)) -> facilPreconditionFor(z,y))).
(all z all y all w ((incompatibleWith(z,w) & facilPreconditionFor(w,y)) -> prevPreconditionFor(z,y))).
(all x all y (allows(x,y) <-> (exists z (((achieves(x,z) | maintains(x,z)) & facilPreconditionFor(z,y)) | (prevents(x,z) & prevPreconditionFor(z,y) & -(exists w (State(w) & achieves(x,w) & prevPreconditionFor(w,y)))))))).
(all x all y (allows(x,y) -> ((Event(x) | Process(x)) & (Event(y) | Process(y) | State(y))))).
(all x all y (disallows(x,y) <-> (exists z (((achieves(x,z) | maintains(x,z)) & prevPreconditionFor(z,y)) | (prevents(x,z) & facilPreconditionFor(z,y)))))).
(all x all y (disallows(x,y) -> ((Event(x) | Process(x)) & (Event(y) | Process(y) | State(y))))).
(all x all y all t (participatesIn(x,y,t) -> (Object(x) & Occurrent(y) & Time(t)))).
(all x all y (hasPhysicalConseq(x,y) -> (Occurrent(x) & Occurrent(y)))).
(all x all y all z ((hasPhysicalConseq(x,y) & hasPhysicalConseq(y,z)) -> hasPhysicalConseq(x,z))).
(all x all y all z ((achieves(x,y) & hasPhysicalConseq(y,z)) -> achieves(x,z))).
(all x all y all z ((allows(x,y) & hasPhysicalConseq(y,z)) -> allows(x,z))).
(all x all y all z ((prevents(x,y) & hasPhysicalConseq(y,z)) -> prevents(x,z))).
(all x all y all z ((disallows(x,y) & hasPhysicalConseq(y,z)) -> disallows(x,z))).
(all x all y all z ((achieves(x,y) & hasPhysicalConseq(z,x)) -> achieves(z,x))).
(all x all y all z ((prevents(x,y) & hasPhysicalConseq(z,x)) -> prevents(z,x))).
(all x all y all z ((allows(x,y) & hasPhysicalConseq(z,x)) -> allows(z,x))).
(all x all y all z ((disallows(x,y) & hasPhysicalConseq(z,x)) -> disallows(z,x))).
(all x all f (functionIncompatible(x,f) <-> (exists o exists b exists t (participatesIn(o,x,t) & functionOf_sys(f,o) & CF(b,f,t) & incompatibleWith(x,b))))).
(all x (Malfunction(x) <-> (exists f functionIncompatible(x,f)))).
(all x all y (posCauseOf(x,y) -> posCauseOf_cross(x,y))).
(all x all y all z ((posCauseOf(x,y) & posCauseOf_cross(y,z)) -> posCauseOf_cross(x,z))).
(all x (FailureMechanism(x) <-> ((Process(x) | Event(x)) & -(Malfunction(x)) & (exists y (Failure(y) & posCauseOf_cross(x,y)))))).
(all x (FailureCondition(x) <-> (State(x) & -(Malfunction(x)) & (exists y (Failure(y) & (posCauseOf_cross(x,y) | (exists z (prevPreconditionFor(x,z) & disallows(z,y))))))))).
(all x (MereSymptom(x) <-> (-(Malfunction(x)) & -(FailureCondition(x)) & -(FailureMechanism(x)) & (exists z (Malfunction(z) & causeOf(z,x)))))).
(all x (Fault(x) <-> (Malfunction(x) & State(x) & (exists z (internalTo(z,x) & achieves(z,x)))))).
(all x (AbormalExternalDisabledState(x) <-> (Malfunction(x) & State(x) & -(Fault(x))))).
(all x (Failure(x) <-> (Malfunction(x) & Event(x) & (exists y (Fault(y) & achieves(x,y)))))).
(all x (NonPerformanceEvent(x) <-> (Malfunction(x) & Event(x) & -(Failure(x))))).
(all x (MalfunctionProcess(x) <-> (Malfunction(x) & Process(x)))).
end_of_list.