From 947f2fffa712eae46f3fbc3c37bd9fd9942693e7 Mon Sep 17 00:00:00 2001
From: jayaprabhakar <jayaprabhakar@gmail.com>
Date: Thu, 12 Feb 2026 12:25:07 -0800
Subject: [PATCH] Early deadlock detection

---
 main.go                   | 14 +++++++++-----
 modelchecker/processor.go | 24 ++++++++++++++++++++++--
 2 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/main.go b/main.go
index 131645b..582728b 100644
--- a/main.go
+++ b/main.go
@@ -6,10 +6,6 @@ import (
 	ast "fizz/proto"
 	"flag"
 	"fmt"
-	"github.com/fizzbee-io/fizzbee/lib"
-	"github.com/fizzbee-io/fizzbee/modelchecker"
-	"google.golang.org/protobuf/encoding/protojson"
-	"google.golang.org/protobuf/proto"
 	"os"
 	"os/signal"
 	"path/filepath"
@@ -19,6 +15,11 @@ import (
 	"sync/atomic"
 	"syscall"
 	"time"
+
+	"github.com/fizzbee-io/fizzbee/lib"
+	"github.com/fizzbee-io/fizzbee/modelchecker"
+	"google.golang.org/protobuf/encoding/protojson"
+	"google.golang.org/protobuf/proto"
 )
 
 var isPlayground bool
@@ -676,7 +677,10 @@ func modelCheckSingleSpec(f *ast.File, stateConfig *ast.StateSpaceOptions, dirPa
 			}
 
 		} else if failedNode != nil {
-			if failedNode.FailedInvariants != nil && len(failedNode.FailedInvariants) > 0 && len(failedNode.FailedInvariants[0]) > 0 {
+			if failedNode.Process.Deadlock {
+				fmt.Println("DEADLOCK detected")
+				fmt.Println("FAILED: Model checker failed")
+			} else if failedNode.FailedInvariants != nil && len(failedNode.FailedInvariants) > 0 && len(failedNode.FailedInvariants[0]) > 0 {
 				fmt.Println("FAILED: Model checker failed. Invariant: ", f.Invariants[failedNode.FailedInvariants[0][0]].Name)
 			} else if simulation {
 				fmt.Println("FAILED: Model checker failed. Deadlock/stuttering detected")
diff --git a/modelchecker/processor.go b/modelchecker/processor.go
index b17a861..3f06503 100644
--- a/modelchecker/processor.go
+++ b/modelchecker/processor.go
@@ -153,6 +153,7 @@ type Process struct {
 
 	Enabled        bool `json:"-"`
 	ThreadProgress bool `json:"-"`
+	Deadlock       bool `json:"-"`
 
 	Roles    []*lib.Role          `json:"roles"`
 	Channels map[int]*lib.Channel `json:"channels"`
@@ -915,6 +916,8 @@ func (n *Node) Duplicate(other *Node, yield bool) {
 		} else {
 			other.Name = n.Name
 		}
+	} else if yield {
+		other.Name = "yield"
 	}
 	parent := n.Inbound[0].Node
 	other.Inbound = append(other.Inbound, n.Inbound[0])
@@ -1184,6 +1187,7 @@ func (p *Processor) Start() (init *Node, failedNode *Node, err error) {
 
 		invariantFailure := false
 		symmetryFound := false
+		yieldFoundForStep := false
 		for {
 			if len(p.visited)%20000 == 0 && len(p.visited) != prevCount {
 				if p.isTest {
@@ -1198,7 +1202,7 @@ func (p *Processor) Start() (init *Node, failedNode *Node, err error) {
 				p.visited = make(map[string]*Node)
 			}
 
-			if node.Process != nil && p.config.Options.GetCrashOnYield() && node.Enabled && (node.Name == "yield" || node.Name == "crash") {
+			if node.Process != nil && p.config.GetOptions().GetCrashOnYield() && node.Enabled && (node.Name == "yield" || node.Name == "crash") {
 				failedCrashNode := p.crashProcess(node)
 				if failedCrashNode != nil && failedNode == nil {
 					failedNode = failedCrashNode
@@ -1207,12 +1211,28 @@ func (p *Processor) Start() (init *Node, failedNode *Node, err error) {
 					break
 				}
 			}
+			if node.Process != nil && (node.Name == "yield" || node.Name == "crash") {
+				yieldFoundForStep = true
+			}
 			if p.intermediateStates.Len() == 0 {
+				if !yieldFoundForStep && !invariantFailure && !p.stopped && p.config.GetDeadlockDetection() {
+					// Deadlock detected
+					//fmt.Printf("Deadlock detected at node: %v\n", node.Name)
+					if len(node.Inbound) > 0 {
+						failedNode = node.Inbound[0].Node
+					} else {
+						failedNode = node
+					}
+					failedNode.Process.Deadlock = true
+					invariantFailure = true
+				}
 				break
 			}
 			node, _ = p.intermediateStates.Remove()
 		}
-
+		if failedNode != nil {
+			break
+		}
 		if symmetryFound {
 			continue
 		}