EWD687a_anim_2.out

TLC2 Version 2.16 of Day Month 20?? (rev: ${git.shortRevision})
Running Random Simulation with seed -5852271152884400068 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 46371] (Mac OS X 12.1 aarch64, Homebrew 17.0.1 x86_64).
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/ewd687a/EWD687a_anim.tla
Parsing file /Users/markus/src/TLA/_specs/examples/specifications/ewd687a/EWD687a.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/Integers.tla (jar:file:/Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/Sequences.tla (jar:file:/Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/SVG.tla (jar:file:/Users/markus/src/TLA/_specs/CommunityModules/dist/CommunityModules-deps.jar!/SVG.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/TLC.tla (jar:file:/Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/IOUtils.tla (jar:file:/Users/markus/src/TLA/_specs/CommunityModules/dist/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/Naturals.tla (jar:file:/Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/Graphs.tla (jar:file:/Users/markus/src/TLA/_specs/CommunityModules/dist/CommunityModules-deps.jar!/Graphs.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/SequencesExt.tla (jar:file:/Users/markus/src/TLA/_specs/CommunityModules/dist/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/FiniteSets.tla (jar:file:/Users/markus/src/TLA/tla/tlatools/org.lamport.tlatools/dist/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/FiniteSetsExt.tla (jar:file:/Users/markus/src/TLA/_specs/CommunityModules/dist/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/Functions.tla (jar:file:/Users/markus/src/TLA/_specs/CommunityModules/dist/CommunityModules-deps.jar!/Functions.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-15134305854507711192/Folds.tla (jar:file:/Users/markus/src/TLA/_specs/CommunityModules/dist/CommunityModules-deps.jar!/Folds.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module TLC
Semantic processing of module SequencesExt
Semantic processing of module Graphs
Semantic processing of module EWD687a
Semantic processing of module SVG
Semantic processing of module IOUtils
Semantic processing of module EWD687a_anim
Starting... (2021-12-21 20:13:36)
Implied-temporal checking--satisfiability problem has 1 branches.
Computed 1 initial states...
Error: Invariant InterestingBehavior is violated.
Error: The behavior up to this point is:
State 1: <Init line 281, col 9 to line 286, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 1</text><text x='350' y='140'>A:  Init[]</text><text x='350' y='160'>A': SendMsg[p |-> L]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'></text><text x='1104' y='330'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'></text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g></g><g><g><rect x='1309' y='189' fill='red' rx='15' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='black' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 2: <SendMsg line 298, col 15 to line 302, col 64 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 2</text><text x='350' y='140'>A:  SendMsg[p |-> L]</text><text x='350' y='160'>A': RcvMsg[p |-> P2, e |-> &lt;&lt;L, P2&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'>m</text><text x='1240' y='236'>-1</text><text x='1104' y='330'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'></text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g></g><g><g><rect x='1309' y='189' fill='red' rx='15' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='black' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 3: <RcvMsg line 365, col 19 to line 373, col 52 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 3</text><text x='350' y='140'>A:  RcvMsg[p |-> P2, e |-> &lt;&lt;L, P2&gt;&gt;]</text><text x='350' y='160'>A': SendMsg[p |-> P2]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'></text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='15' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 4: <SendMsg line 298, col 15 to line 302, col 64 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 4</text><text x='350' y='140'>A:  SendMsg[p |-> P2]</text><text x='350' y='160'>A': Idle[p |-> L]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'>m</text><text x='933' y='567'>-1</text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='15' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 5: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 5</text><text x='350' y='140'>A:  Idle[p |-> L]</text><text x='350' y='160'>A': RcvMsg[p |-> P5, e |-> &lt;&lt;P2, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'>m</text><text x='933' y='567'>-1</text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 6: <RcvMsg line 365, col 19 to line 373, col 52 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 6</text><text x='350' y='140'>A:  RcvMsg[p |-> P5, e |-> &lt;&lt;P2, P5&gt;&gt;]</text><text x='350' y='160'>A': SendMsg[p |-> P2]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 7: <SendMsg line 298, col 15 to line 302, col 64 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 7</text><text x='350' y='140'>A:  SendMsg[p |-> P2]</text><text x='350' y='160'>A': SendMsg[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>m</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 8: <SendMsg line 298, col 15 to line 302, col 64 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 8</text><text x='350' y='140'>A:  SendMsg[p |-> P5]</text><text x='350' y='160'>A': RcvMsg[p |-> P4, e |-> &lt;&lt;P5, P4&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>m</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'>m</text><text x='661' y='1040'>-1</text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 9: <RcvMsg line 365, col 19 to line 373, col 52 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 9</text><text x='350' y='140'>A:  RcvMsg[p |-> P4, e |-> &lt;&lt;P5, P4&gt;&gt;]</text><text x='350' y='160'>A': Idle[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>m</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='15' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 10: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 10</text><text x='350' y='140'>A:  Idle[p |-> P5]</text><text x='350' y='160'>A': Idle[p |-> P4]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>m</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='15' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 11: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 11</text><text x='350' y='140'>A:  Idle[p |-> P4]</text><text x='350' y='160'>A': Idle[p |-> P2]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>m</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='15' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 12: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 12</text><text x='350' y='140'>A:  Idle[p |-> P2]</text><text x='350' y='160'>A': RcvMsg[p |-> P3, e |-> &lt;&lt;P2, P3&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>m</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 13: <RcvMsg line 365, col 19 to line 373, col 52 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 13</text><text x='350' y='140'>A:  RcvMsg[p |-> P3, e |-> &lt;&lt;P2, P3&gt;&gt;]</text><text x='350' y='160'>A': SendMsg[p |-> P3]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='15' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 14: <SendMsg line 298, col 15 to line 302, col 64 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 14</text><text x='350' y='140'>A:  SendMsg[p |-> P3]</text><text x='350' y='160'>A': RcvMsg[p |-> P5, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>m</text><text x='1035' y='993'>-1</text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='15' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 15: <RcvMsg line 365, col 19 to line 373, col 52 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 15</text><text x='350' y='140'>A:  RcvMsg[p |-> P5, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='160'>A': SendAck[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'>-1</text><text x='763' y='1087'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='15' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 16: <SendAck line 335, col 15 to line 351, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 16</text><text x='350' y='140'>A:  SendAck[p |-> P5]</text><text x='350' y='160'>A': Idle[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>a</text><text x='1035' y='993'>-1</text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='15' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 17: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 17</text><text x='350' y='140'>A:  Idle[p |-> P5]</text><text x='350' y='160'>A': SendMsg[p |-> P3]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>a</text><text x='1035' y='993'>-1</text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='15' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 18: <SendMsg line 298, col 15 to line 302, col 64 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 18</text><text x='350' y='140'>A:  SendMsg[p |-> P3]</text><text x='350' y='160'>A': SendMsg[p |-> P3]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>ma</text><text x='1035' y='993'>-2</text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='15' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 19: <SendMsg line 298, col 15 to line 302, col 64 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 19</text><text x='350' y='140'>A:  SendMsg[p |-> P3]</text><text x='350' y='160'>A': Idle[p |-> P3]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>mma</text><text x='1035' y='993'>-3</text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='15' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 20: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 20</text><text x='350' y='140'>A:  Idle[p |-> P3]</text><text x='350' y='160'>A': RcvMsg[p |-> P5, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>mma</text><text x='1035' y='993'>-3</text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 21: <RcvMsg line 365, col 19 to line 373, col 52 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 21</text><text x='350' y='140'>A:  RcvMsg[p |-> P5, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='160'>A': Idle[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>ma</text><text x='1035' y='993'>-3</text><text x='763' y='1087'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 22: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 22</text><text x='350' y='140'>A:  Idle[p |-> P5]</text><text x='350' y='160'>A': RcvMsg[p |-> P5, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>ma</text><text x='1035' y='993'>-3</text><text x='763' y='1087'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 23: <RcvMsg line 365, col 19 to line 373, col 52 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 23</text><text x='350' y='140'>A:  RcvMsg[p |-> P5, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='160'>A': Idle[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>a</text><text x='1035' y='993'>-3</text><text x='763' y='1087'>2</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='15' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 24: <Idle line 382, col 12 to line 383, col 72 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 24</text><text x='350' y='140'>A:  Idle[p |-> P5]</text><text x='350' y='160'>A': RcvAck[p |-> P3, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>a</text><text x='1035' y='993'>-3</text><text x='763' y='1087'>2</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 25: <RcvAck line 311, col 19 to line 314, col 68 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 25</text><text x='350' y='140'>A:  RcvAck[p |-> P3, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='160'>A': SendAck[p |-> P4]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'>-2</text><text x='763' y='1087'>2</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'>-1</text><text x='729' y='851'>1</text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='643' y1='1151' x2='779' y2='773'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='red' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 26: <SendAck line 335, col 15 to line 351, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 26</text><text x='350' y='140'>A:  SendAck[p |-> P4]</text><text x='350' y='160'>A': RcvAck[p |-> P5, e |-> &lt;&lt;P5, P4&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'>-2</text><text x='763' y='1087'>2</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'>a</text><text x='661' y='1040'>-1</text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 27: <RcvAck line 311, col 19 to line 314, col 68 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 27</text><text x='350' y='140'>A:  RcvAck[p |-> P5, e |-> &lt;&lt;P5, P4&gt;&gt;]</text><text x='350' y='160'>A': SendAck[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'>-2</text><text x='763' y='1087'>2</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 28: <SendAck line 335, col 15 to line 351, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 28</text><text x='350' y='140'>A:  SendAck[p |-> P5]</text><text x='350' y='160'>A': RcvAck[p |-> P3, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>a</text><text x='1035' y='993'>-2</text><text x='763' y='1087'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 29: <RcvAck line 311, col 19 to line 314, col 68 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 29</text><text x='350' y='140'>A:  RcvAck[p |-> P3, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='160'>A': SendAck[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'>-1</text><text x='763' y='1087'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 30: <SendAck line 335, col 15 to line 351, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 30</text><text x='350' y='140'>A:  SendAck[p |-> P5]</text><text x='350' y='160'>A': RcvAck[p |-> P3, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'>a</text><text x='1035' y='993'>-1</text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 31: <RcvAck line 311, col 19 to line 314, col 68 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 31</text><text x='350' y='140'>A:  RcvAck[p |-> P3, e |-> &lt;&lt;P3, P5&gt;&gt;]</text><text x='350' y='160'>A': SendAck[p |-> P3]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'>-1</text><text x='1138' y='804'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='1188' y2='962'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='red' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 32: <SendAck line 335, col 15 to line 351, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 32</text><text x='350' y='140'>A:  SendAck[p |-> P3]</text><text x='350' y='160'>A': SendAck[p |-> P5]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>a</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'>-1</text><text x='729' y='945'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1052' y1='394' x2='643' y2='1151'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='red' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 33: <SendAck line 335, col 15 to line 351, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 33</text><text x='350' y='140'>A:  SendAck[p |-> P5]</text><text x='350' y='160'>A': RcvAck[p |-> P2, e |-> &lt;&lt;P2, P3&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'>a</text><text x='1070' y='520'>-1</text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'>a</text><text x='933' y='567'>-1</text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 34: <RcvAck line 311, col 19 to line 314, col 68 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 34</text><text x='350' y='140'>A:  RcvAck[p |-> P2, e |-> &lt;&lt;P2, P3&gt;&gt;]</text><text x='350' y='160'>A': RcvAck[p |-> P2, e |-> &lt;&lt;P2, P5&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'>a</text><text x='933' y='567'>-1</text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 35: <RcvAck line 311, col 19 to line 314, col 68 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 35</text><text x='350' y='140'>A:  RcvAck[p |-> P2, e |-> &lt;&lt;P2, P5&gt;&gt;]</text><text x='350' y='160'>A': SendAck[p |-> P2]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'>-1</text><text x='1104' y='330'>1</text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'></text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g><g><line stroke='orange' stroke-width='5' stroke-dasharray='5' x1='1325' y1='205' x2='1052' y2='394'></line></g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='red' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 36: <SendAck line 335, col 15 to line 351, col 58 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 36</text><text x='350' y='140'>A:  SendAck[p |-> P2]</text><text x='350' y='160'>A': RcvAck[p |-> L, e |-> &lt;&lt;L, P2&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'>a</text><text x='1240' y='236'>-1</text><text x='1104' y='330'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'></text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g></g><g><g><rect x='1309' y='189' fill='red' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='black' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

State 37: <RcvAck line 311, col 19 to line 314, col 68 of module EWD687a>
/\ _animator = "<defs><marker id='arrow' markerWidth='35' markerHeight='35' refX='14' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='black' /></marker></defs><g><g><text x='350' y='120'>Step: 37</text><text x='350' y='140'>A:  RcvAck[p |-> L, e |-> &lt;&lt;L, P2&gt;&gt;]</text><text x='350' y='160'>A': RcvAck[p |-> L, e |-> &lt;&lt;L, P2&gt;&gt;]</text><text x='350' y='180'>~neutral procs red, round when also active</text></g><g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1325' y2='583'></line><text x='1309' y='378'></text><text x='1309' y='283'></text><text x='1309' y='472'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1052' y2='394'></line><text x='1172' y='283'></text><text x='1240' y='236'></text><text x='1104' y='330'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='205' x2='1188' y2='962'></line><text x='1240' y='567'></text><text x='1274' y='378'></text><text x='1206' y='756'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='1052' y2='394'></line><text x='1172' y='472'></text><text x='1240' y='519'></text><text x='1104' y='425'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1325' y1='583' x2='779' y2='773'></line><text x='1036' y='662'></text><text x='1172' y='614'></text><text x='899' y='709'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='1188' y2='962'></line><text x='1104' y='662'></text><text x='1070' y='520'></text><text x='1138' y='804'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1052' y1='394' x2='643' y2='1151'></line><text x='831' y='756'></text><text x='933' y='567'></text><text x='729' y='945'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='1325' y2='583'></line><text x='1240' y='756'></text><text x='1206' y='851'></text><text x='1274' y='661'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='1188' y1='962' x2='643' y2='1151'></line><text x='899' y='1040'></text><text x='1035' y='993'></text><text x='763' y='1087'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='1188' y2='962'></line><text x='967' y='851'></text><text x='865' y='804'></text><text x='1069' y='898'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='779' y1='773' x2='643' y2='1151'></line><text x='695' y='946'></text><text x='729' y='851'></text><text x='661' y='1040'></text></g><g><line stroke='black' stroke-width='2' marker-end='url(#arrow)' x1='643' y1='1151' x2='779' y2='773'></line><text x='695' y='946'></text><text x='661' y='1040'></text><text x='729' y='851'></text></g></g><g></g><g><g><rect x='1309' y='189' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='212' fill='white'>L</text></g><g><rect x='1309' y='567' fill='black' rx='0' width='32' height='32'></rect><text x='1320' y='590' fill='white'>P1</text></g><g><rect x='1036' y='378' fill='black' rx='0' width='32' height='32'></rect><text x='1047' y='401' fill='white'>P2</text></g><g><rect x='1172' y='946' fill='black' rx='0' width='32' height='32'></rect><text x='1183' y='969' fill='white'>P3</text></g><g><rect x='763' y='757' fill='black' rx='0' width='32' height='32'></rect><text x='774' y='780' fill='white'>P4</text></g><g><rect x='627' y='1135' fill='black' rx='0' width='32' height='32'></rect><text x='638' y='1158' fill='white'>P5</text></g></g></g>"
/\ file = [exitValue |-> 0, stdout |-> "", stderr |-> ""]

The number of states generated: 4638
Simulation using seed -5852271152884400068 and aril 0
Progress: 4638 states checked, 100 traces generated (trace length: mean=32, var(x)=805, sd=28)
Finished in 01s at (2021-12-21 20:13:37)