Section 3: Action Invariants Deduced From Cycles

In this section, we present results obtained from recognizing if a state is reached again.Which actions have to occur how often yields vectors that are considered invariants since they leave the state of the model unchanged.Traces often generate large numbers of such vectors such that we will only consider a subset of vectors that are linearly independent.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 are not present in the set of invariants

There are no such actions. For this trace, all actions are covered by at least one invariant!

Set of linearly independent action invariants

Invariant 1:


ActionValue
Ac_disk_failure(a7)1
Ac_disk_repair(a6)1
Total2

Invariant 2:


ActionValue
Ac_disk_repair(a12)1
Ac_disk_failure(a13)1
Total2

Invariant 3:


ActionValue
Ac_disk_failure(a10)1
Ac_disk_repair(a9)1
Total2

Invariant 4:


ActionValue
Ac_disk_failure(a27)1
Ac_disk_repair(a26)1
Total2

Invariant 5:


ActionValue
Ac_disk_repair(a23)1
Ac_disk_failure(a24)1
Total2

Invariant 6:


ActionValue
Ac_disk_repair(a20)1
Ac_disk_failure(a21)1
Total2

Invariant 7:


ActionValue
Ac_controller_repair(a29)1
Ac_controller_failure(a30)1
Total2

Invariant 8:


ActionValue
Ac_processor_repair(a32)1
Ac_processor_failure(a33)1
Total2

Invariant 9:


ActionValue
Ac_controller_failure(a16)1
Ac_controller_repair(a15)1
Total2