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

Set of computed variable invariants

Invariant 1:


VariableValue
disks_working1(sv1)1
disks_failed2(sv2)1
Total2

Invariant 2:


VariableValue
disks_working4(sv4)1
disks_failed5(sv5)1
Total2

Invariant 3:


VariableValue
disks_working7(sv7)1
disks_failed8(sv8)1
Total2

Invariant 4:


VariableValue
controllers_failed13(sv13)1
controllers_working11(sv11)1
Total2

Invariant 5:


VariableValue
disks_failed16(sv16)1
disks_working15(sv15)1
Total2

Invariant 6:


VariableValue
disks_failed19(sv19)1
disks_working18(sv18)1
Total2

Invariant 7:


VariableValue
disks_working21(sv21)1
disks_failed22(sv22)1
Total2

Invariant 8:


VariableValue
controllers_failed27(sv27)1
controllers_working25(sv25)1
Total2

Invariant 9:


VariableValue
processors_failed31(sv31)1
processors_working30(sv30)1
Total2