Section 4: Action Invariants Derieved From State Transformation Functions

In this section, we present results obtained from an invariant analysis that applies only to a specific class of state transformations. If all actions perform only linear state transformations of the type v' = v + c, where c is some integer constant, the state transformations are those of an ordinary Petri net and an invariant computation known for Petri nets can be applied.
In the following we present a set of computed action invariants, that are not necessarily present in the current trace but a corresponding sequence of actions would return to its starting state.Actions that do not contribute to invariants are likely to represent irregular or faulty behavior such that we list those actions separately and upfront.

List of actions that had to be excluded from the calculation of invariants

For this trace, all actions are taken into consideration, however this does not mean all of them are actually covered by some invariant!

List of actions that are not covered by any invariant

For this trace, all actions are covered by some invariant!

Set of computed action invariants

Invariant 1:

Action	Value
Ac_disk_repair(a6)	1
Ac_disk_failure(a7)	1
Total	2

Invariant 2:

Action	Value
Ac_controller_failure(a16)	1
Ac_controller_repair(a15)	1
Total	2

Invariant 3:

Action	Value
Ac_disk_repair(a20)	1
Ac_disk_failure(a21)	1
Total	2

Invariant 4:

Action	Value
Ac_disk_repair(a26)	1
Ac_disk_failure(a27)	1
Total	2

Invariant 5:

Action	Value
Ac_processor_failure(a33)	1
Ac_processor_repair(a32)	1
Total	2

Invariant 6:

Action	Value
Ac_disk_repair(a9) (case1)	1
Ac_disk_failure(a10) (case1)	1
Total	2

Invariant 7:

Action	Value
Ac_disk_repair(a9) (case2)	1
Ac_disk_failure(a10) (case2)	1
Total	2

Invariant 8:

Action	Value
Ac_disk_failure(a13) (case1)	1
Ac_disk_repair(a12) (case1)	1
Total	2

Invariant 9:

Action	Value
Ac_disk_repair(a12) (case2)	1
Ac_disk_failure(a13) (case2)	1
Total	2

Invariant 10:

Action	Value
Ac_disk_failure(a24) (case1)	1
Ac_disk_repair(a23) (case1)	1
Total	2

Invariant 11:

Action	Value
Ac_disk_repair(a23) (case2)	1
Ac_disk_failure(a24) (case2)	1
Total	2

Invariant 12:

Action	Value
Ac_controller_failure(a30) (case1)	1
Ac_controller_repair(a29) (case1)	1
Total	2

Invariant 13:

Action	Value
Ac_controller_repair(a29) (case2)	1
Ac_controller_failure(a30) (case2)	1
Total	2

Invariant 14:

Action	Value
Ac_disk_repair(a9) (case2)	1
Ac_disk_repair(a9) (case1)	1
Ac_disk_failure(a10) (case2)	1
Ac_disk_failure(a10) (case1)	1
Total	4

Invariant 15:

Action	Value
Ac_disk_repair(a9) (case2)	1
Ac_disk_repair(a12) (case1)	1
Ac_disk_failure(a10) (case1)	1
Ac_disk_failure(a13) (case2)	1
Total	4

Invariant 16:

Action	Value
Ac_disk_repair(a9) (case2)	1
Ac_disk_failure(a10) (case1)	1
Ac_disk_failure(a24) (case2)	1
Ac_disk_repair(a23) (case1)	1
Total	4

Invariant 17:

Action	Value
Ac_disk_repair(a9) (case2)	1
Ac_controller_repair(a29) (case1)	1
Ac_controller_failure(a30) (case2)	1
Ac_disk_failure(a10) (case1)	1
Total	4

Invariant 18:

Action	Value
Ac_disk_repair(a9) (case1)	1
Ac_disk_failure(a13) (case1)	1
Ac_disk_failure(a10) (case2)	1
Ac_disk_repair(a12) (case2)	1
Total	4

Invariant 19:

Action	Value
Ac_disk_failure(a13) (case1)	1
Ac_disk_repair(a12) (case2)	1
Ac_disk_repair(a12) (case1)	1
Ac_disk_failure(a13) (case2)	1
Total	4

Invariant 20:

Action	Value
Ac_disk_failure(a13) (case1)	1
Ac_disk_repair(a12) (case2)	1
Ac_disk_failure(a24) (case2)	1
Ac_disk_repair(a23) (case1)	1
Total	4

Invariant 21:

Action	Value
Ac_controller_repair(a29) (case1)	1
Ac_disk_failure(a13) (case1)	1
Ac_controller_failure(a30) (case2)	1
Ac_disk_repair(a12) (case2)	1
Total	4

Invariant 22:

Action	Value
Ac_disk_failure(a24) (case1)	1
Ac_disk_repair(a9) (case1)	1
Ac_disk_failure(a10) (case2)	1
Ac_disk_repair(a23) (case2)	1
Total	4

Invariant 23:

Action	Value
Ac_disk_failure(a24) (case1)	1
Ac_disk_repair(a12) (case1)	1
Ac_disk_repair(a23) (case2)	1
Ac_disk_failure(a13) (case2)	1
Total	4

Invariant 24:

Action	Value
Ac_disk_failure(a24) (case1)	1
Ac_disk_repair(a23) (case2)	1
Ac_disk_failure(a24) (case2)	1
Ac_disk_repair(a23) (case1)	1
Total	4

Invariant 25:

Action	Value
Ac_controller_repair(a29) (case1)	1
Ac_disk_failure(a24) (case1)	1
Ac_controller_failure(a30) (case2)	1
Ac_disk_repair(a23) (case2)	1
Total	4

Invariant 26:

Action	Value
Ac_controller_failure(a30) (case1)	1
Ac_disk_repair(a9) (case1)	1
Ac_controller_repair(a29) (case2)	1
Ac_disk_failure(a10) (case2)	1
Total	4

Invariant 27:

Action	Value
Ac_controller_failure(a30) (case1)	1
Ac_controller_repair(a29) (case2)	1
Ac_disk_repair(a12) (case1)	1
Ac_disk_failure(a13) (case2)	1
Total	4

Invariant 28:

Action	Value
Ac_controller_failure(a30) (case1)	1
Ac_controller_repair(a29) (case2)	1
Ac_disk_failure(a24) (case2)	1
Ac_disk_repair(a23) (case1)	1
Total	4

Invariant 29:

Action	Value
Ac_controller_failure(a30) (case1)	1
Ac_controller_repair(a29) (case1)	1
Ac_controller_repair(a29) (case2)	1
Ac_controller_failure(a30) (case2)	1
Total	4