Trace Analysis Results for Action depart.unnamed(a5.unnamed)

This text provides more details for action depart.unnamed(a5.unnamed).
Action is of type: local, supposed to change variables of a single process only.
Action depart.unnamed(a5.unnamed) occurs 500 times, which accounts for 50.00 % of all events.
On average an action occurs 500.00 times, so this action is above average.
Action occurs at position 2 for the first time, at position 1000 for the last time.
It never follows another action in zero time, there is always a non-zero delay observed before this action occurs.

Enabling Set and State Transformations

The following table shows for what value setting of variables the action occurs and what state transformation it performs.The table shows only those variables that belong to processes that the action corresponds to.
VariableEnabling RangeState TransformationRemarks
pop.unnamed(a3.unnamed) in {1,...,12} v'=v-1

List of Warnings

There are no specific warnings for this action.