diff --git a/tests/paper3.yaml b/tests/paper3.yaml
index 76f4cbb..41089d6 100644
--- a/tests/paper3.yaml
+++ b/tests/paper3.yaml
@@ -33,13 +33,13 @@ tcp-phi1-drop-bidirectional:
 
 tcp-phi1-replay-AtoB:
   - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoB --output=temp.pml --eval --cleanup --mem=1
-  - intended: no violation
-  - explanation: replaying A's messages cannot create half-open; B reaching Established still requires valid handshake, and A cannot close without teardown
+  - intended: property violation
+  - explanation: replay attacker copies A's message non-destructively, allowing normal handshake and teardown; after A returns to Closed, the replayed stale message drives B through a new handshake into Established, creating a half-open state
 
 tcp-phi1-replay-bidirectional:
   - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=replay --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=1
-  - intended: no violation
-  - explanation: replay on both channels still cannot violate the structural invariant; A must pass through Established before reaching Closed
+  - intended: property violation
+  - explanation: replay on both channels injects stale handshake messages in both directions; after A tears down to Closed, replayed messages push B into Established without A's participation
 
 tcp-phi1-reorder-bidirectional:
   - command: python src/main.py --model=tests/tcp/tcp-phi1.pml --attacker=reorder --chan=AtoB,BtoA --output=temp.pml --eval --cleanup --mem=2
@@ -51,6 +51,11 @@ tcp-phi1-reorder-bidirectional:
 # Expected: drop on both channels can strand both sides post-Established
 # (e.g., both in FinWait1 after FINs are dropped)
 
+tcp-phi3-drop-AtoB-nodeadlock:
+  - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=0
+  - intended: no violation
+  - explanation: with mem=0 the drop attacker cannot consume any messages; it goes straight to BREAK, leaving the model unmodified; timeout transitions prevent permanent stalls in the base model
+
 tcp-phi3-drop-AtoB:
   - command: python src/main.py --model=tests/tcp/tcp-phi3.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1
   - intended: acceptance cycle
@@ -75,6 +80,12 @@ tcp-phi3-reorder-bidirectional:
 # SynReceived implies eventually (Established or FinWait1 or Closed)
 # Expected: drop on AtoB traps A in SynReceived (no timeout modeled)
 
+
+tcp-phi5-replay-BtoA:
+  - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=replay --chan=BtoA --output=temp.pml --eval --cleanup --mem=1
+  - intended: no violation
+  - explanation: replaying B's messages on BtoA delivers extra SYNs to A; if A enters SynReceived, the replayed messages do not prevent ACK delivery on AtoB (which is unattacked), so SynReceived resolves normally
+
 tcp-phi5-drop-AtoB:
   - command: python src/main.py --model=tests/tcp/tcp-phi5.pml --attacker=drop --chan=AtoB --output=temp.pml --eval --cleanup --mem=1
   - intended: acceptance cycle
diff --git a/tests/tcp/pan b/tests/tcp/pan
index 8d793e1..b304ec1 100755
Binary files a/tests/tcp/pan and b/tests/tcp/pan differ
diff --git a/tests/tcp/tcp-phi2.pml.trail b/tests/tcp/tcp-phi2.pml.trail
index 7c3fba0..745e3e2 100644
--- a/tests/tcp/tcp-phi2.pml.trail
+++ b/tests/tcp/tcp-phi2.pml.trail
@@ -1,53 +1,43 @@
--2:3:-2
+-2:2:-2
 -4:-4:-4
-1:0:129
-2:2:122
-3:0:129
-4:2:123
-5:0:129
-6:2:124
-7:0:129
-8:2:125
-9:0:129
-10:4:0
-11:0:129
-12:4:1
-13:0:129
-14:4:2
-15:0:129
-16:4:9
-17:0:129
-18:3:0
-19:0:129
-20:3:1
-21:0:129
-22:3:2
-23:0:129
-24:3:9
-25:0:129
-26:4:17
-27:0:129
-28:4:1
-29:0:129
-30:4:3
-31:0:129
-32:4:22
-33:0:127
-34:1:116
+1:0:121
+2:1:114
+3:0:121
+4:1:115
+5:0:121
+6:1:116
+7:0:121
+8:1:117
+9:0:121
+10:3:0
+11:0:121
+12:3:1
+13:0:121
+14:3:2
+15:0:121
+16:3:9
+17:0:121
+18:2:0
+19:0:121
+20:2:1
+21:0:121
+22:2:2
+23:0:121
+24:2:9
+25:0:121
+26:3:17
+27:0:121
+28:3:1
 -1:-1:-1
-35:0:134
-36:1:117
-37:0:127
-38:3:15
-39:0:134
-40:3:16
-41:0:127
-42:4:42
-43:0:134
-44:4:1
-45:0:129
-46:4:3
-47:0:129
-48:4:22
-49:0:127
-50:1:116
+29:0:121
+30:3:3
+31:0:121
+32:3:22
+33:0:119
+34:2:15
+35:0:126
+36:2:16
+37:0:119
+38:3:42
+39:0:126
+40:3:1
diff --git a/tests/tcp/tcp-phi4.pml.trail b/tests/tcp/tcp-phi4.pml.trail
index 88bdbca..cf64d44 100644
--- a/tests/tcp/tcp-phi4.pml.trail
+++ b/tests/tcp/tcp-phi4.pml.trail
@@ -1,322 +1,157 @@
--2:3:-2
+-2:2:-2
 -4:-4:-4
-1:0:130
-2:2:122
-3:0:130
-4:2:123
-5:0:130
-6:2:124
-7:0:130
-8:2:125
-9:0:130
-10:4:0
-11:0:130
-12:4:1
-13:0:130
-14:4:2
-15:0:130
-16:4:9
-17:0:130
-18:3:0
-19:0:130
-20:3:1
-21:0:130
-22:3:2
-23:0:130
-24:3:9
-25:0:130
-26:4:17
-27:0:130
-28:4:1
-29:0:130
-30:4:3
-31:0:130
-32:4:22
-33:0:130
-34:1:116
-35:0:130
-36:1:117
-37:0:130
-38:3:10
-39:0:130
-40:3:11
-41:3:12
-42:0:130
-43:3:47
-44:0:130
-45:1:114
-46:0:130
-47:1:115
-48:0:130
-49:4:23
-50:0:130
-51:4:27
-52:0:130
-53:4:47
-54:0:130
-55:1:114
-56:0:130
-57:1:115
-58:0:130
-59:4:48
-60:0:130
-61:4:55
-62:0:130
-63:4:56
-64:0:130
-65:4:66
-66:0:130
-67:1:116
-68:0:130
-69:1:117
-70:0:130
-71:3:48
-72:0:130
-73:3:55
-74:0:130
-75:3:56
-76:0:130
-77:3:66
-78:0:130
-79:1:114
-80:0:130
-81:1:115
-82:0:130
-83:4:67
-84:0:130
-85:4:68
-86:0:130
-87:4:94
-88:0:130
-89:1:116
-90:0:130
-91:1:117
-92:0:130
-93:3:67
-94:0:130
-95:3:68
-96:0:130
-97:3:94
-98:0:130
-99:1:114
-100:0:130
-101:1:115
-102:0:130
-103:4:95
-104:0:130
-105:4:110
-106:0:130
-107:4:1
-108:0:130
-109:4:2
-110:0:130
-111:4:9
-112:0:130
-113:1:116
-114:0:130
-115:1:117
-116:0:130
-117:3:95
-118:0:130
-119:3:110
-120:0:130
-121:3:1
-122:0:130
-123:3:2
-124:0:130
-125:3:9
-126:0:130
-127:4:17
-128:0:130
-129:4:1
-130:0:130
-131:4:3
-132:0:130
-133:1:116
-134:0:130
-135:1:117
-136:0:130
-137:3:10
-138:0:130
-139:3:11
-140:3:12
-141:0:130
-142:3:47
-143:0:130
-144:1:114
-145:0:130
-146:1:115
-147:0:130
-148:1:114
-149:0:130
-150:4:22
-151:0:130
-152:4:23
-153:0:130
-154:4:27
-155:0:130
-156:1:115
-157:0:130
-158:1:116
-159:0:130
-160:4:47
-161:0:130
-162:4:48
-163:0:130
-164:4:55
-165:0:130
-166:4:56
-167:0:130
-168:1:117
-169:0:130
-170:3:48
-171:0:130
-172:3:55
-173:0:130
-174:3:56
-175:0:130
-176:3:66
-177:0:130
-178:1:114
-179:0:130
-180:1:115
-181:0:130
-182:1:116
-183:0:130
-184:4:66
-185:0:130
-186:4:67
-187:0:130
-188:4:68
-189:0:130
-190:1:117
-191:0:130
-192:3:67
-193:0:130
-194:3:68
-195:0:130
-196:3:94
-197:0:130
-198:1:114
-199:0:130
-200:1:115
-201:0:130
-202:1:116
-203:0:130
-204:4:94
-205:0:130
-206:4:95
-207:0:130
-208:4:110
-209:0:130
-210:4:1
-211:0:130
-212:4:2
-213:0:130
-214:1:117
-215:0:130
-216:3:95
-217:0:130
-218:3:110
-219:0:130
-220:3:1
-221:0:130
-222:3:3
-223:0:130
-224:4:9
-225:0:130
-226:3:22
-227:0:130
-228:1:114
-229:0:130
-230:1:115
-231:0:130
-232:4:10
-233:0:130
-234:4:11
-235:4:12
-236:0:130
-237:4:47
-238:0:130
-239:1:116
-240:0:130
-241:1:117
-242:0:130
-243:3:23
-244:0:130
-245:3:27
-246:0:130
-247:1:114
-248:0:130
-249:1:115
-250:0:130
-251:4:48
-252:0:130
-253:4:55
-254:0:130
-255:4:56
-256:0:130
-257:4:66
-258:0:130
-259:1:116
-260:0:130
-261:1:117
-262:0:130
-263:1:116
-264:0:130
-265:3:47
-266:0:130
-267:3:48
-268:0:130
-269:3:55
-270:0:130
-271:3:56
-272:0:130
-273:3:66
-274:0:130
-275:1:117
-276:0:130
-277:3:67
-278:0:130
-279:3:68
-280:0:130
-281:1:114
-282:0:130
-283:1:115
-284:0:130
-285:4:67
-286:0:130
-287:1:114
-288:0:130
-289:4:68
-290:0:130
-291:4:94
-292:0:130
-293:1:115
-294:0:130
-295:4:95
-296:0:130
-297:4:110
-298:0:130
-299:4:1
-300:0:130
-301:4:3
-302:0:130
-303:4:22
-304:0:130
-305:3:94
-306:0:130
-307:1:116
-308:0:130
-309:1:117
-310:0:130
-311:3:95
-312:0:130
-313:3:110
-314:0:130
-315:3:1
-316:0:130
-317:3:3
-318:0:130
-319:3:22
-320:0:127
+1:0:122
+2:1:114
+3:0:122
+4:1:115
+5:0:122
+6:1:116
+7:0:122
+8:1:117
+9:0:122
+10:3:0
+11:0:122
+12:3:1
+13:0:122
+14:3:2
+15:0:122
+16:3:9
+17:0:122
+18:2:0
+19:0:122
+20:2:1
+21:0:122
+22:2:2
+23:0:122
+24:2:9
+25:0:122
+26:3:17
+27:0:122
+28:3:1
+29:0:122
+30:3:3
+31:0:122
+32:3:22
+33:0:122
+34:2:10
+35:0:122
+36:2:11
+37:2:12
+38:0:122
+39:3:23
+40:0:122
+41:3:24
+42:0:122
+43:3:25
+44:0:122
+45:3:55
+46:0:122
+47:3:56
+48:0:122
+49:3:66
+50:0:122
+51:2:47
+52:0:122
+53:2:48
+54:0:122
+55:2:55
+56:0:122
+57:2:56
+58:0:122
+59:3:67
+60:0:122
+61:3:68
+62:0:122
+63:3:94
+64:0:122
+65:2:66
+66:0:122
+67:2:67
+68:0:122
+69:2:68
+70:0:122
+71:3:95
+72:0:122
+73:3:110
+74:0:122
+75:3:1
+76:0:122
+77:3:2
+78:0:122
+79:2:94
+80:0:122
+81:2:95
+82:0:122
+83:2:110
+84:0:122
+85:2:1
+86:0:122
+87:2:3
+88:0:122
+89:3:9
+90:0:122
+91:3:10
+92:0:122
+93:3:11
+94:3:12
+95:0:122
+96:3:47
+97:0:122
+98:2:22
+99:0:122
+100:2:23
+101:0:122
+102:2:24
+103:0:122
+104:2:25
+105:0:122
+106:3:48
+107:0:122
+108:3:55
+109:0:122
+110:3:56
+111:0:122
+112:2:55
+113:0:122
+114:2:56
+115:0:122
+116:2:66
+117:0:122
+118:3:66
+119:0:122
+120:3:67
+121:0:122
+122:3:68
+123:0:122
+124:2:67
+125:0:122
+126:2:68
+127:0:122
+128:2:94
+129:0:122
+130:3:94
+131:0:122
+132:3:95
+133:0:122
+134:3:110
+135:0:122
+136:3:1
+137:0:122
+138:3:3
+139:0:122
+140:3:22
+141:0:122
+142:2:95
+143:0:122
+144:2:110
+145:0:122
+146:2:1
+147:0:122
+148:2:3
+149:0:122
+150:3:23
+151:0:122
+152:3:27
+153:0:122
+154:2:22
+155:0:119
diff --git a/tests/tcp/tcp-phi5.pml.trail b/tests/tcp/tcp-phi5.pml.trail
index 3ac1dc9..ad988b0 100644
--- a/tests/tcp/tcp-phi5.pml.trail
+++ b/tests/tcp/tcp-phi5.pml.trail
@@ -1,86 +1,64 @@
--2:3:-2
+-2:2:-2
 -4:-4:-4
-1:0:129
-2:2:122
-3:0:129
-4:2:123
-5:0:129
-6:2:124
-7:0:129
-8:2:125
-9:0:129
-10:4:0
-11:0:129
-12:4:1
-13:0:129
-14:4:2
-15:0:129
-16:4:9
-17:0:129
-18:3:0
-19:0:129
-20:3:1
-21:0:129
-22:3:2
-23:0:129
-24:3:9
-25:0:129
-26:4:17
-27:0:129
-28:4:1
-29:0:129
-30:4:3
-31:0:129
-32:4:22
-33:0:129
-34:1:116
-35:0:129
-36:1:117
-37:0:129
-38:3:10
-39:0:129
-40:3:11
-41:3:12
-42:0:129
-43:3:47
-44:0:127
-45:1:114
-46:0:134
-47:1:115
-48:0:134
-49:4:23
-50:0:134
-51:4:27
-52:0:134
-53:4:47
-54:0:134
-55:1:114
-56:0:134
-57:1:115
-58:0:134
-59:4:48
-60:0:134
-61:4:55
-62:0:134
-63:4:56
-64:0:134
-65:4:66
-66:0:134
-67:1:116
-68:0:134
-69:1:117
-70:0:134
-71:3:50
-72:0:134
-73:3:51
-74:0:134
-75:1:116
-76:0:134
-77:1:117
-78:0:134
-79:3:50
-80:0:134
-81:3:51
+1:0:121
+2:1:114
+3:0:121
+4:1:115
+5:0:121
+6:1:116
+7:0:121
+8:1:117
+9:0:121
+10:3:0
+11:0:121
+12:3:1
+13:0:121
+14:3:2
+15:0:121
+16:3:9
+17:0:121
+18:2:0
+19:0:121
+20:2:1
+21:0:121
+22:2:2
+23:0:121
+24:2:9
+25:0:121
+26:3:17
+27:0:121
+28:3:1
+29:0:121
+30:3:3
+31:0:121
+32:3:22
+33:0:121
+34:2:10
+35:0:121
+36:2:11
+37:2:12
+38:0:121
+39:3:23
+40:0:121
+41:3:24
+42:0:121
+43:3:25
+44:0:121
+45:3:55
+46:0:121
+47:3:56
+48:0:121
+49:3:66
+50:0:121
+51:2:47
+52:0:119
+53:2:50
+54:0:126
+55:2:51
+56:0:126
+57:2:50
+58:0:126
+59:2:51
 -1:-1:-1
-82:0:134
-83:0:134
+60:0:126
+61:0:126
diff --git a/tests/tcp/tcp-phi6.pml.trail b/tests/tcp/tcp-phi6.pml.trail
index 8bc7191..1840bcf 100644
--- a/tests/tcp/tcp-phi6.pml.trail
+++ b/tests/tcp/tcp-phi6.pml.trail
@@ -1,122 +1,88 @@
--2:3:-2
+-2:2:-2
 -4:-4:-4
-1:0:129
-2:2:122
-3:0:129
-4:2:123
-5:0:129
-6:2:124
-7:0:129
-8:2:125
-9:0:129
-10:4:0
-11:0:129
-12:4:1
-13:0:129
-14:4:2
-15:0:129
-16:4:9
-17:0:129
-18:3:0
-19:0:129
-20:3:1
-21:0:129
-22:3:2
-23:0:129
-24:3:9
-25:0:129
-26:4:17
-27:0:129
-28:4:1
-29:0:129
-30:4:3
-31:0:129
-32:4:22
-33:0:129
-34:1:116
-35:0:129
-36:1:117
-37:0:129
-38:3:10
-39:0:129
-40:3:11
-41:3:12
-42:0:129
-43:3:47
-44:0:129
-45:1:114
-46:0:129
-47:1:115
-48:0:129
-49:4:23
-50:0:129
-51:4:27
-52:0:129
-53:4:47
-54:0:129
-55:1:114
-56:0:129
-57:1:115
-58:0:129
-59:4:48
-60:0:129
-61:4:55
-62:0:129
-63:4:56
-64:0:129
-65:4:66
-66:0:129
-67:1:116
-68:0:129
-69:1:117
-70:0:129
-71:3:48
-72:0:129
-73:3:55
-74:0:129
-75:3:56
-76:0:129
-77:3:66
-78:0:129
-79:1:114
-80:0:129
-81:1:115
-82:0:129
-83:4:67
-84:0:129
-85:4:68
-86:0:129
-87:4:94
-88:0:129
-89:1:116
-90:0:129
-91:1:117
-92:0:129
-93:3:67
-94:0:129
-95:3:68
-96:0:129
-97:3:94
-98:0:129
-99:1:114
-100:0:129
-101:1:115
-102:0:129
-103:4:95
-104:0:129
-105:4:110
-106:0:129
-107:4:1
-108:0:129
-109:4:2
-110:0:129
-111:4:9
-112:0:129
-113:1:116
-114:0:129
-115:1:117
-116:0:129
-117:3:95
-118:0:127
-119:3:110
-120:0:134
+1:0:121
+2:1:114
+3:0:121
+4:1:115
+5:0:121
+6:1:116
+7:0:121
+8:1:117
+9:0:121
+10:3:0
+11:0:121
+12:3:1
+13:0:121
+14:3:2
+15:0:121
+16:3:9
+17:0:121
+18:2:0
+19:0:121
+20:2:1
+21:0:121
+22:2:2
+23:0:121
+24:2:9
+25:0:121
+26:3:17
+27:0:121
+28:3:1
+29:0:121
+30:3:3
+31:0:121
+32:3:22
+33:0:121
+34:2:10
+35:0:121
+36:2:11
+37:2:12
+38:0:121
+39:3:23
+40:0:121
+41:3:24
+42:0:121
+43:3:25
+44:0:121
+45:3:55
+46:0:121
+47:3:56
+48:0:121
+49:3:66
+50:0:121
+51:2:47
+52:0:121
+53:2:48
+54:0:121
+55:2:55
+56:0:121
+57:2:56
+58:0:121
+59:3:67
+60:0:121
+61:3:68
+62:0:121
+63:3:94
+64:0:121
+65:2:66
+66:0:121
+67:2:67
+68:0:121
+69:2:68
+70:0:121
+71:3:95
+72:0:121
+73:3:110
+74:0:121
+75:3:1
+76:0:121
+77:3:2
+78:0:121
+79:3:9
+80:0:121
+81:2:94
+82:0:121
+83:2:95
+84:0:119
+85:2:110
+86:0:126