From aad1bb7bc5fd98eed46dcc7ec64b3439d3073dc4 Mon Sep 17 00:00:00 2001
From: fizzbee <152331581+jp-fizzbee@users.noreply.github.com>
Date: Mon, 10 Feb 2025 18:06:03 -0800
Subject: [PATCH] Fix crash node deduplication. If a non-crash node is a
 duplicate of a crash node, check if the thread could be crashed, if so, crash
 that thread. Also fix the name (#147)

Co-authored-by: jayaprabhakar <jayaprabhakar@gmail.com>
---
 modelchecker/processor.go | 37 +++++++++++++++++++++++++++++--------
 1 file changed, 29 insertions(+), 8 deletions(-)

diff --git a/modelchecker/processor.go b/modelchecker/processor.go
index be1e55d..c447ade 100644
--- a/modelchecker/processor.go
+++ b/modelchecker/processor.go
@@ -774,7 +774,11 @@ func (n *Node) Duplicate(other *Node, yield bool) {
 		return
 	}
 	if n.Name != "crash" && other.Name == "crash" {
-		other.Name = n.Name
+		if yield {
+			other.Name = "yield"
+		} else {
+			other.Name = n.Name
+		}
 	}
 	parent := n.Inbound[0].Node
 	other.Inbound = append(other.Inbound, n.Inbound[0])
@@ -1289,6 +1293,11 @@ func (p *Processor) processNode(node *Node) (bool, bool) {
 		// We will keep the enabled state in the node, during execution but have to be
 		// copied to the link/transition when attaching/merging similar to Fairness.
 		if other.Enabled || !node.Enabled {
+			if yield && other.Name == "crash" {
+				if p.shouldThreadCrash(other) {
+					p.crashThread(other)
+				}
+			}
 			node.Duplicate(other, yield)
 			return false, false
 		} else {
@@ -1301,6 +1310,11 @@ func (p *Processor) processNode(node *Node) (bool, bool) {
 		for _, hash := range hashes {
 			if other, ok := p.visited[hash]; ok {
 				if other.Enabled || !node.Enabled {
+					if yield && other.Name == "crash" {
+						if p.shouldThreadCrash(other) {
+							p.crashThread(other)
+						}
+					}
 					node.Duplicate(other, yield)
 					return false, true
 				}
@@ -1341,16 +1355,11 @@ func (p *Processor) processNode(node *Node) (bool, bool) {
 			p.YieldNode(node)
 		}
 		node.Name = "yield"
-		if node.Process.GetThreadsCount() == 0 || node.Process.Current == -1 || !*p.config.Options.CrashOnYield {
-			return false, false
-		}
-		frameName := node.Process.currentThread().Stack.RawArray()[0].Name
 
-		if p.config.ActionOptions[frameName] != nil && p.config.ActionOptions[frameName].CrashOnYield != nil && !p.config.ActionOptions[frameName].GetCrashOnYield() {
-			return false, false
+		if p.shouldThreadCrash(node) {
+			p.crashThread(node)
 		}
 
-		p.crashThread(node)
 		return false, false
 	}
 	return false, false
@@ -1845,6 +1854,18 @@ func (p *Processor) ResetEphemeralVariables(node *Node, oldRole *lib.Role) {
 	}
 }
 
+func (p *Processor) shouldThreadCrash(node *Node) bool {
+	if node.Process.GetThreadsCount() == 0 || node.Process.Current == -1 || !*p.config.Options.CrashOnYield {
+		return false
+	}
+	frameName := node.Process.currentThread().Stack.RawArray()[0].Name
+
+	if p.config.ActionOptions[frameName] != nil && p.config.ActionOptions[frameName].CrashOnYield != nil && !p.config.ActionOptions[frameName].GetCrashOnYield() {
+		return false
+	}
+	return true
+}
+
 func captureStackTrace() string {
 	if !enableCaptureStackTrace {
 		return ""