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

Packet hopping from node 0 to node 1(node0_h_0L1)
Node 0 receiving packet from node 1(node0_r_0L1)
Packet hopping from node 1 to node 0(node1_h_0L1)
Node 1 receiving packet from node 0(node1_r_0L1)
Packet hopping from node 1 to node 2(node1_h_1L2)
Node 1 receiving packet from node 2(node1_r_1L2)
Packet hopping from node 2 to node 1(node2_h_1L2)
Node 2 receiving packet from node 1(node2_r_1L2)
Packet hopping from node 2 to node 3(node2_h_2L3)
Node 2 receiving packet from node 3(node2_r_2L3)
Packet hopping from node 3 to node 2(node3_h_2L3)
Node 3 receiving packet from node 2(node3_r_2L3)
Packet hopping from node 3 to node 4(node3_h_3L4)
Node 3 receiving packet from node 4(node3_r_3L4)
Packet hopping from node 4 to node 3(node4_h_3L4)
Node 4 receiving packet from node 3(node4_r_3L4)
Packet hopping from node 4 to node 5(node4_h_4L5)
Node 4 receiving packet from node 5(node4_r_4L5)
Packet hopping from node 5 to node 4(node5_h_4L5)
Node 5 receiving packet from node 4(node5_r_4L5)
Packet hopping from node 5 to node 6(node5_h_5L6)
Node 5 receiving packet from node 6(node5_r_5L6)
Packet hopping from node 6 to node 5(node6_h_5L6)
Node 6 receiving packet from node 5(node6_r_5L6)
Packet hopping from node 6 to node 0(node6_h_6L0)
Node 6 receiving packet from node 0(node6_r_6L0)
Packet hopping from node 0 to node 6(node0_h_6L0)
Node 0 receiving packet from node 6(node0_r_6L0)

Set of computed action invariants

Invariant 1:

Action	Value
Node 4 enqueued packet to node 3(node4_+_node3)	1
Total	1

Invariant 2:

Action	Value
Node 4 dequeued packet to node 3(node4_-_node3)	1
Total	1

Invariant 3:

Action	Value
Node 4 enqueued packet to node 5(node4_+_node5)	1
Total	1

Invariant 4:

Action	Value
Node 4 dequeued packet to node 5(node4_-_node5)	1
Total	1

Invariant 5:

Action	Value
Node 0 enqueued packet to node 1(node0_+_node1)	1
Total	1

Invariant 6:

Action	Value
Node 0 dequeued packet to node 1(node0_-_node1)	1
Total	1

Invariant 7:

Action	Value
Node 0 enqueued packet to node 6(node0_+_node6)	1
Total	1

Invariant 8:

Action	Value
Node 0 dequeued packet to node 6(node0_-_node6)	1
Total	1

Invariant 9:

Action	Value
Node 5 enqueued packet to node 4(node5_+_node4)	1
Total	1

Invariant 10:

Action	Value
Node 5 dequeued packet to node 4(node5_-_node4)	1
Total	1

Invariant 11:

Action	Value
Node 5 enqueued packet to node 6(node5_+_node6)	1
Total	1

Invariant 12:

Action	Value
Node 5 dequeued packet to node 6(node5_-_node6)	1
Total	1

Invariant 13:

Action	Value
Node 1 enqueued packet to node 0(node1_+_node0)	1
Total	1

Invariant 14:

Action	Value
Node 1 dequeued packet to node 0(node1_-_node0)	1
Total	1

Invariant 15:

Action	Value
Node 1 enqueued packet to node 2(node1_+_node2)	1
Total	1

Invariant 16:

Action	Value
Node 1 dequeued packet to node 2(node1_-_node2)	1
Total	1

Invariant 17:

Action	Value
Node 6 enqueued packet to node 5(node6_+_node5)	1
Total	1

Invariant 18:

Action	Value
Node 6 dequeued packet to node 5(node6_-_node5)	1
Total	1

Invariant 19:

Action	Value
Node 6 enqueued packet to node 0(node6_+_node0)	1
Total	1

Invariant 20:

Action	Value
Node 6 dequeued packet to node 0(node6_-_node0)	1
Total	1

Invariant 21:

Action	Value
Node 2 enqueued packet to node 1(node2_+_node1)	1
Total	1

Invariant 22:

Action	Value
Node 2 dequeued packet to node 1(node2_-_node1)	1
Total	1

Invariant 23:

Action	Value
Node 2 enqueued packet to node 3(node2_+_node3)	1
Total	1

Invariant 24:

Action	Value
Node 2 dequeued packet to node 3(node2_-_node3)	1
Total	1

Invariant 25:

Action	Value
Node 3 enqueued packet to node 2(node3_+_node2)	1
Total	1

Invariant 26:

Action	Value
Node 3 dequeued packet to node 2(node3_-_node2)	1
Total	1

Invariant 27:

Action	Value
Node 3 enqueued packet to node 4(node3_+_node4)	1
Total	1

Invariant 28:

Action	Value
Node 3 dequeued packet to node 4(node3_-_node4)	1
Total	1