Extend trace by few levels of actions to make the explorer work (#320)

Co-authored-by: jayaprabhakar <jayaprabhakar@gmail.com>

Author: jp-fizzbee

fizz

@@ -46,6 +46,7 @@ copy_ast=true
 output_dir=""
 trace_file=""
 trace_string=""
+trace_extend=0
 preinit_hook_file=""
 preinit_hook_string=""
 
@@ -105,6 +106,15 @@ while [[ "$1" =~ ^- ]]; do
         usage
       fi
       ;;
+    --trace-extend )
+      if [[ -n "$2" ]] && [[ "$2" =~ ^[0-9]+$ ]]; then
+        trace_extend="$2"
+        shift 2
+      else
+        echo "Error: --trace-extend requires a numeric value." 1>&2
+        usage
+      fi
+      ;;
     --preinit-hook-file )
       if [[ -n "$2" ]]; then
         preinit_hook_file="$2"
@@ -211,6 +221,9 @@ fi
 if [ -n "$trace_string" ]; then
   args+=("--trace" "$trace_string")
 fi
+if [ "$trace_extend" -ne 0 ]; then
+  args+=("--trace-extend" "$trace_extend")
+fi
 if [ -n "$preinit_hook_file" ]; then
   args+=("--preinit-hook-file" "$preinit_hook_file")
 fi

main.go

@@ -34,6 +34,7 @@ var traceFile string
 var preinitHookFile string
 var trace string
 var preinitHook string
+var traceExtend int
 
 var isTest bool
 
@@ -543,6 +544,12 @@ func modelCheckSingleSpec(f *ast.File, stateConfig *ast.StateSpaceOptions, dirPa
 		}
 	}
 
+	// Set trace extension depth if configured
+	if guidedTrace != nil && traceExtend > 0 {
+		guidedTrace.ExtendDepth = traceExtend
+		fmt.Printf("Trace will extend %d action(s) beyond the guided path\n", traceExtend)
+	}
+
 	// Resolve preinit hook content (either from file or string)
 	var preinitHookContentResolved string
 	if preinitHookFile != "" {
@@ -848,6 +855,7 @@ func parseFlags() []string {
 	flag.StringVar(&traceFile, "trace-file", "", "Path to trace file for guided execution")
 	flag.StringVar(&preinitHookFile, "preinit-hook-file", "", "Path to Starlark file to execute after preinit but before freezing globals")
 	flag.StringVar(&trace, "trace", "", "Trace content as a string for guided execution (multiline supported)")
+	flag.IntVar(&traceExtend, "trace-extend", 0, "After trace ends, explore this many additional action depths (0 = stop at trace end)")
 	flag.StringVar(&preinitHook, "preinit-hook", "", "Starlark code as a string to execute after preinit but before freezing globals (multiline supported)")
 	flag.BoolVar(&isTest, "test", false, "Testing mode (prevents printing timestamps and other non-deterministic behavior. Default=false")
 	flag.Parse()

modelchecker/trace.go

@@ -11,6 +11,8 @@ import (
 type GuidedTrace struct {
 	LinkNames    []string
 	currentIndex int
+	ExtendDepth  int // How many actions to explore after trace ends (0 = stop)
+	extendedCount int // How many extended actions taken so far
 }
 
 // parseTrace parses trace content from a scanner
@@ -114,6 +116,11 @@ func (p *Processor) ShouldScheduleNode(node *Node) bool {
 
 	// Check if trace is exhausted
 	if node.guidedTrace.IsExhausted() {
+		// Allow extension if configured
+		if node.guidedTrace.ExtendDepth > 0 && node.guidedTrace.extendedCount < node.guidedTrace.ExtendDepth {
+			node.guidedTrace.extendedCount++
+			return true
+		}
 		return false
 	}