Trace Analysis Results for Action C2RestartIfFailed(8)

This text provides more details for action C2RestartIfFailed(8).
Action is of type: undirected interaction, may change variables of several processes.
Action C2RestartIfFailed(8) occurs 1 times, which accounts for 0.02 % of all events.
On average an action occurs 456.08 times, so this action is below average.
Action occurs at position 3473 for the first time, at position 3473 for the last time.
Note that the action is not(!) present in the last 2000 events, which is 36.54% of all events. May be it becomes rare or even dead?
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.

Variable	Enabling Range	State Transformation	Remarks
Avail(Avail)	= 0	not modified
Failed(Failed)	= 1	v'=v	Action performs identity function!
C1WaitsForServer(C1WaitsForServer)	= 1	v'=v+1
C1WaitsForUser(C1WaitsForUser)	= 0	not modified
C2WaitsForServer(C2WaitsForServer)	= 0	v'=v+1
C2WaitsForUser(C2WaitsForUser)	= 0	not modified
C1InService(C1InService)	= 0	not modified
C2InService(C2InService)	= 1	v'=v-1
Sidle(Sidle)	= 0	v'=v+1

List of Warnings

Type 7: Action C2RestartIfFailed(8) performs identity as state transformation to variable Failed(Failed).
Type 8: Action C2RestartIfFailed(8) occurs only once, linear state transformation for C1WaitsForServer(C1WaitsForServer) is possible but fitting is based on not enough data to be uniquely determined.
Type 8: Action C2RestartIfFailed(8) occurs only once, linear state transformation for C2InService(C2InService) is possible but fitting is based on not enough data to be uniquely determined.
Type 8: Action C2RestartIfFailed(8) occurs only once, linear state transformation for C2WaitsForServer(C2WaitsForServer) is possible but fitting is based on not enough data to be uniquely determined.
Type 8: Action C2RestartIfFailed(8) occurs only once, linear state transformation for Failed(Failed) is possible but fitting is based on not enough data to be uniquely determined.
Type 8: Action C2RestartIfFailed(8) occurs only once, linear state transformation for Sidle(Sidle) is possible but fitting is based on not enough data to be uniquely determined.
Type 10: Action C2RestartIfFailed(8) is not element of any action invariant computed for the linear state transformations performed by the actions of this trace.
Type 16: Action C2RestartIfFailed(8) may deadlock, because it occurs the last time at event 3473 and is not seen for the remaining 36.54 percent of the trace.