Trace Analysis Results
Information directly extracted from trace file:
comment: Purpose of this trace: model checking
model: 0.1
simulator: 0.1
Outline
The following table outlines characteristics for each process. Note that there are two types of processes, basic ones that contain variables and actions and sets of processes that contain a set of other processes. The sum of values in column local actions gives the total number of local actions, however this does not work for interactions since those are shared between processes.
| Process | Type | Variables | Local Actions | Interactions | Remarks |
|---|
| Link (0-1)(0L1) | basic | 1 | 2 | 4 | |
| Link (1-2)(1L2) | basic | 1 | 2 | 4 | |
| Link (2-3)(2L3) | basic | 1 | 2 | 4 | |
| Link (3-4)(3L4) | basic | 1 | 2 | 4 | |
| Link (4-5)(4L5) | basic | 1 | 2 | 4 | |
| Link (5-6)(5L6) | basic | 1 | 2 | 4 | |
| Link (6-0)(6L0) | basic | 1 | 2 | 4 | |
| Node 4(4)(4) | basic | 4 | 8 | 4 | |
| Node 0(0)(0) | basic | 4 | 8 | 4 | |
| Node 5(5)(5) | basic | 4 | 8 | 4 | |
| Node 1(1)(1) | basic | 4 | 8 | 4 | |
| Node 6(6)(6) | basic | 4 | 8 | 4 | |
| Node 2(2)(2) | basic | 4 | 8 | 4 | |
| Node 3(3)(3) | basic | 4 | 8 | 4 | |
The trace declares 98 actions and 35 variables.
It contains 1 sequence of events.
The total number of events is 1000, add the initial state to obtain the number of states.
The following graph shows how often each variable is assigned a value:
The following graph shows how often each action occurred:
The following graph shows how many states of the state space get explored and in which order:
The following graph shows the progress measure of the sequence, which is the length of the trace if cycles are removed:
For more details check corresponding sections below or follow links for entries in the table above:
Section 1 on variables for all processes
Section 2 on actions for all processes
Section 3 on action invariants observed in the trace
Section 4 on action invariants derived from invariant analysis (does not apply in general)
Section 5 on variable invariants derived from invariant analysis (does not apply in general)
Section 6 Warnings