Section 5: Variable 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 variable invariants, such that a weighted summation performed for any state in the trace will yield the same constant value throughout the trace.Variables 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 variables that had to be excluded from the calculation of invariants

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

List of variables that are not covered by any invariant

system_fail33(sv33)

Set of computed variable invariants

Invariant 1:

Variable	Value
disks_working1(sv1)	1
disks_failed2(sv2)	1
Total	2

Invariant 2:

Variable	Value
disks_working4(sv4)	1
disks_failed5(sv5)	1
Total	2

Invariant 3:

Variable	Value
disks_working7(sv7)	1
disks_failed8(sv8)	1
Total	2

Invariant 4:

Variable	Value
controllers_failed13(sv13)	1
controllers_working11(sv11)	1
Total	2

Invariant 5:

Variable	Value
disks_failed16(sv16)	1
disks_working15(sv15)	1
Total	2

Invariant 6:

Variable	Value
disks_failed19(sv19)	1
disks_working18(sv18)	1
Total	2

Invariant 7:

Variable	Value
disks_working21(sv21)	1
disks_failed22(sv22)	1
Total	2

Invariant 8:

Variable	Value
controllers_failed27(sv27)	1
controllers_working25(sv25)	1
Total	2

Invariant 9:

Variable	Value
processors_failed31(sv31)	1
processors_working30(sv30)	1
Total	2