diff --git a/fizz b/fizz index 6f72afd..e37d501 100755 --- a/fizz +++ b/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 diff --git a/main.go b/main.go index 131645b..af17730 100644 --- a/main.go +++ b/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() diff --git a/modelchecker/trace.go b/modelchecker/trace.go index c5d1805..a0a6c72 100644 --- a/modelchecker/trace.go +++ b/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 }