Error Trace panel does not show modification of some variables between states

[burkostya]

Here pc is marked as modified between states. But inner second pc does not have mark M.

Here the same for resource_needed variable

Extension's version: 1.5.0

TLC2 output

@!@!@STARTMSG 2262:0 @!@!@
TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99)
@!@!@ENDMSG 2262 @!@!@
@!@!@STARTMSG 2187:0 @!@!@
Running breadth-first search Model-Checking with fp 81 and seed -7895493024671220822 with 1 worker on 4 cores with 3506MB heap and 64MB offheap memory [pid: 276112] (Linux 5.7.6-arch1-1 amd64, N/A 14.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
@!@!@ENDMSG 2187 @!@!@
@!@!@STARTMSG 2220:0 @!@!@
Starting SANY...
@!@!@ENDMSG 2220 @!@!@
Parsing file /home/burkostya/src/github.com/burkostya/spec/tla/spec/cache/cache.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Integers
Semantic processing of module cache
@!@!@STARTMSG 2219:0 @!@!@
SANY finished.
@!@!@ENDMSG 2219 @!@!@
@!@!@STARTMSG 2185:0 @!@!@
Starting... (2020-07-27 19:17:51)
@!@!@ENDMSG 2185 @!@!@
@!@!@STARTMSG 2189:0 @!@!@
Computing initial states...
@!@!@ENDMSG 2189 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 2 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 4 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 8 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2269:0 @!@!@
Computed 16 initial states...
@!@!@ENDMSG 2269 @!@!@
@!@!@STARTMSG 2191:0 @!@!@
Finished computing initial states: 24 states generated, with 18 of them distinct at 2020-07-27 19:17:51.
@!@!@ENDMSG 2191 @!@!@
@!@!@STARTMSG 2110:1 @!@!@
Invariant ResourceInvariant is violated.
@!@!@ENDMSG 2110 @!@!@
@!@!@STARTMSG 2121:1 @!@!@
The behavior up to this point is:
@!@!@ENDMSG 2121 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ resources_cap = 1
/\ resources_left = 1
/\ reserved = 0
/\ pc = (a1 :> "WairForResources" @@ a2 :> "WairForResources" @@ "time" :> "Tick")
/\ resources_needed = (a1 :> 1 @@ a2 :> 2)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <WairForResources line 74, col 27 to line 79, col 61 of module cache>
/\ resources_cap = 1
/\ resources_left = 1
/\ reserved = 2
/\ pc = (a1 :> "WairForResources" @@ a2 :> "UseResource" @@ "time" :> "Tick")
/\ resources_needed = (a1 :> 1 @@ a2 :> 2)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <UseResource line 81, col 22 to line 90, col 63 of module cache>
/\ resources_cap = 1
/\ resources_left = 0
/\ reserved = 2
/\ pc = (a1 :> "WairForResources" @@ a2 :> "UseResource" @@ "time" :> "Tick")
/\ resources_needed = (a1 :> 1 @@ a2 :> 1)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <UseResource line 81, col 22 to line 90, col 63 of module cache>
/\ resources_cap = 1
/\ resources_left = -1
/\ reserved = 2
/\ pc = (a1 :> "WairForResources" @@ a2 :> "UseResource" @@ "time" :> "Tick")
/\ resources_needed = (a1 :> 1 @@ a2 :> 0)

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2201:0 @!@!@
The coverage statistics at 2020-07-27 19:17:51
@!@!@ENDMSG 2201 @!@!@
@!@!@STARTMSG 2773:0 @!@!@
<Init line 65, col 1 to line 65, col 4 of module cache>: 48:48
@!@!@ENDMSG 2773 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 66, col 12 to line 66, col 43 of module cache: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 67, col 12 to line 67, col 41 of module cache: 12
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 70, col 12 to line 70, col 61 of module cache: 12
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 71, col 12 to line 72, col 67 of module cache: 48
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<WairForResources line 74, col 1 to line 74, col 22 of module cache>: 16:25
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 74, col 30 to line 74, col 58 of module cache: 95
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 74, col 30 to line 74, col 37 of module cache: 70
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 75, col 30 to line 75, col 80 of module cache: 25
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 75, col 30 to line 75, col 62 of module cache: 52
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 75, col 67 to line 75, col 80 of module cache: 52
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 76, col 30 to line 76, col 74 of module cache: 25
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 77, col 30 to line 77, col 70 of module cache: 25
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 78, col 30 to line 79, col 61 of module cache: 25
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<UseResource line 81, col 1 to line 81, col 17 of module cache>: 14:20
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 81, col 25 to line 81, col 48 of module cache: 86
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 81, col 25 to line 81, col 32 of module cache: 69
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 82, col 28 to line 82, col 53 of module cache: 18
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 83, col 36 to line 83, col 71 of module cache: 15
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 83, col 54 to line 83, col 71 of module cache: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 84, col 36 to line 84, col 117 of module cache: 15
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 84, col 56 to line 84, col 117 of module cache: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 85, col 36 to line 85, col 76 of module cache: 15
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 85, col 42 to line 85, col 76 of module cache: 16
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 87, col 38 to line 87, col 94 of module cache: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 86, col 45 to line 86, col 61 of module cache: 2
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 88, col 36 to line 88, col 81 of module cache: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 89, col 36 to line 89, col 59 of module cache: 4
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 90, col 25 to line 90, col 63 of module cache: 19
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2772:0 @!@!@
<Tick line 94, col 1 to line 94, col 4 of module cache>: 10:35
@!@!@ENDMSG 2772 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 94, col 12 to line 94, col 30 of module cache: 70
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  |line 94, col 12 to line 94, col 21 of module cache: 35
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 95, col 12 to line 95, col 42 of module cache: 35
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 96, col 12 to line 96, col 24 of module cache: 35
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 97, col 12 to line 97, col 47 of module cache: 35
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 98, col 12 to line 98, col 58 of module cache: 35
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2774:0 @!@!@
<ResourceInvariant line 57, col 1 to line 57, col 17 of module cache>
@!@!@ENDMSG 2774 @!@!@
@!@!@STARTMSG 2221:0 @!@!@
  line 57, col 22 to line 57, col 40 of module cache: 58
@!@!@ENDMSG 2221 @!@!@
@!@!@STARTMSG 2202:0 @!@!@
End of statistics.
@!@!@ENDMSG 2202 @!@!@
@!@!@STARTMSG 2200:0 @!@!@
Progress(4) at 2020-07-27 19:17:51: 95 states generated (5,465 s/min), 58 distinct states found (3,336 ds/min), 25 states left on queue.
@!@!@ENDMSG 2200 @!@!@
@!@!@STARTMSG 2199:0 @!@!@
95 states generated, 58 distinct states found, 25 states left on queue.
@!@!@ENDMSG 2199 @!@!@
@!@!@STARTMSG 2194:0 @!@!@
The depth of the complete state graph search is 4.
@!@!@ENDMSG 2194 @!@!@
@!@!@STARTMSG 2268:0 @!@!@
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3).
@!@!@ENDMSG 2268 @!@!@
@!@!@STARTMSG 2186:0 @!@!@
Finished in 1056ms at (2020-07-27 19:17:51)
@!@!@ENDMSG 2186 @!@!@