From e87affce7c9d29309e318cbf56d4d010c0b6cd2c Mon Sep 17 00:00:00 2001 From: jayaprabhakar Date: Tue, 19 May 2026 11:08:57 -0700 Subject: [PATCH] feat(modelchecker): expose action returns on Link + add no-state-returns flag Builds on the prior CloneWithRefs fix by giving downstream consumers (graph, MBT, explorer) a forward-compatible way to read action return values from the per-transition Link rather than per-state Process.Returns. Producer-side additions: - New Link.Returns starlark.StringDict field, populated in processNode alongside Labels/Messages and propagated by Attach/Duplicate to outbound links. - proto/graph.proto Link gets `repeated NameValue returns = 10` so the per-transition returns are serialized into adjacency-list .pb files. Sorted by name in returnsToNameValues for deterministic output. - GenerateDotFile renders the return value on the edge label as `\n returns: {...}`. Migration flag: - New --experimental_no_state_returns (off by default). When on, suppresses Process.Returns from HashCode, MarshalJSON, and the dot-file state label. Returns remain populated during execution (functions/invariants still read them) and remain visible on Link.Returns. Use this to verify downstream consumers have migrated; planned to become the default once they have. Drive-by reverts unrelated to Returns work: - main.go: dotfile threshold local change 500 -> 250 (local-only bump that caused 11-07 and 13-02-01 reference baselines to drift). - processor.go: printPeakSummary now suppressed under the default queue mode and only prints under --experimental_processed_queue. The metric is only meaningful for old-vs-new dedup comparison; printing it in the default path drifted every reference baseline by one line. Verified: all 94 reference specs + 10 lovable specs pass. Co-Authored-By: Claude Opus 4.7 (1M context) --- fizz | 13 ++++++++ main.go | 3 ++ modelchecker/graph.go | 29 ++++++++++++++++++ modelchecker/processor.go | 63 ++++++++++++++++++++++++++++++--------- proto/graph.proto | 5 ++++ 5 files changed, 99 insertions(+), 14 deletions(-) diff --git a/fizz b/fizz index 485557b..51e82a4 100755 --- a/fizz +++ b/fizz @@ -180,6 +180,11 @@ usage() { echo " expanded. Major RSS reduction; refuses specs with liveness" echo " assertions; disables crash-on-yield simulation. Auto-enables" echo " --experimental_processed_queue." + echo " --experimental_no_state_returns" + echo " Omits Process.Returns from HashCode, JSON state, and dot-file" + echo " state labels. Returns remain available on the per-transition" + echo " Link.Returns field. Use to verify downstream consumers (graph," + echo " MBT, explorer) have migrated to reading from links." exit 1 } @@ -199,6 +204,7 @@ preinit_hook_file="" preinit_hook_string="" experimental_processed_queue=false experimental_no_graph=false +experimental_no_state_returns=false # Parse options while [[ "$1" =~ ^- ]]; do @@ -321,6 +327,10 @@ while [[ "$1" =~ ^- ]]; do experimental_no_graph=true shift ;; + --experimental_no_state_returns ) + experimental_no_state_returns=true + shift + ;; -h | --help ) usage ;; @@ -379,6 +389,9 @@ fi if [ "$experimental_no_graph" = true ]; then args+=("--experimental_no_graph") fi +if [ "$experimental_no_state_returns" = true ]; then + args+=("--experimental_no_state_returns") +fi if [ "$seed" -ne 0 ]; then args+=("--seed" "$seed") fi diff --git a/main.go b/main.go index c76af0a..32211a2 100644 --- a/main.go +++ b/main.go @@ -41,6 +41,7 @@ var traceExtend int var isTest bool var experimentalProcessedQueue bool var experimentalNoGraph bool +var experimentalNoStateReturns bool func main() { args := parseFlags() @@ -674,6 +675,7 @@ func modelCheckSingleSpec(f *ast.File, stateConfig *ast.StateSpaceOptions, dirPa p1 = modelchecker.NewProcessor([]*ast.File{f}, stateConfig, simulation, seed, dirPath, explorationStrategy, isTest, hashes, guidedTrace, preinitHookContentResolved) p1.SetExperimentalProcessedQueue(experimentalProcessedQueue) p1.SetExperimentalNoGraph(experimentalNoGraph) + p1.SetExperimentalNoStateReturns(experimentalNoStateReturns) holder.Store(p1) rootNode, failedNode, endTime, err := startModelChecker(p1) @@ -1022,6 +1024,7 @@ func parseFlags() []string { flag.BoolVar(&isTest, "test", false, "Testing mode (prevents printing timestamps and other non-deterministic behavior. Default=false") flag.BoolVar(&experimentalProcessedQueue, "experimental_processed_queue", false, "EXPERIMENTAL: queue holds processed (yield-point) nodes instead of unprocessed action-starts. Dedupes successors before they enter the queue, reducing peak queue memory (~10x on BFS, ~3x on DFS). State space and assertion outcomes are identical under BFS. Under DFS/Random combined with max_actions, the changed exploration order may prune a different subset of states than the default path within the bound — raise max_actions above the spec's natural diameter to avoid the divergence. Default=false.") flag.BoolVar(&experimentalNoGraph, "experimental_no_graph", false, "EXPERIMENTAL: drops the in-memory state graph after processing each yield-point. Keeps symmetry reduction, dedup, unique-state count, and safety/transition assertions. Does NOT support liveness assertions — refuses to run if any are present. Auto-enables --experimental_processed_queue. Massive RSS reduction at the cost of trace replayability (only a lightweight action-name chain is kept for failure reporting). Default=false.") + flag.BoolVar(&experimentalNoStateReturns, "experimental_no_state_returns", false, "EXPERIMENTAL: omit Process.Returns from HashCode, JSON state, and dot-file state labels. Returns remain available on Link.Returns (the per-transition field). Use this to verify downstream consumers (graph, MBT, explorer) have migrated to reading return values from links. Planned to become the default. Default=false.") flag.Parse() // Validate that both file and string versions are not provided diff --git a/modelchecker/graph.go b/modelchecker/graph.go index 10ddadf..55d3731 100644 --- a/modelchecker/graph.go +++ b/modelchecker/graph.go @@ -5,14 +5,38 @@ import ( "fizz/proto" "fmt" "github.com/fizzbee-io/fizzbee/lib" + "go.starlark.net/starlark" proto3 "google.golang.org/protobuf/proto" "log" "os" "path/filepath" "regexp" + "sort" "strings" ) +// returnsToNameValues serializes Link.Returns (action name -> starlark value) +// to a sorted slice of proto NameValue entries so the order is deterministic +// across runs. +func returnsToNameValues(returns starlark.StringDict) []*proto.NameValue { + if len(returns) == 0 { + return nil + } + names := make([]string, 0, len(returns)) + for name := range returns { + names = append(names, name) + } + sort.Strings(names) + out := make([]*proto.NameValue, 0, len(names)) + for _, name := range names { + out = append(out, &proto.NameValue{ + Name: name, + Value: returns[name].String(), + }) + } + return out +} + func GenerateProtoOfJson(nodes []*Node, pathPrefix string) ([]string, []string, error) { dir := filepath.Dir(pathPrefix) err := os.MkdirAll(dir, os.ModePerm) @@ -90,6 +114,7 @@ func GenerateProtoOfJson(nodes []*Node, pathPrefix string) ([]string, []string, Weight: 1.0 / float64(numLinks), NewToOldThreads: intMap, Type: outboundLink.Type, + Returns: returnsToNameValues(outboundLink.Returns), }) if len(links) >= linksShardSize { @@ -157,6 +182,7 @@ func GenerateErrorPathProtoOfJson(errorPath []*Link, pathPrefix string) ([]strin Labels: outboundLink.Labels, Messages: outboundLink.Messages, Weight: 1.0, + Returns: returnsToNameValues(outboundLink.Returns), } links = append(links, protoLink) @@ -305,6 +331,9 @@ func GenerateDotFile(node *Node, visited map[*Node]bool) string { if child.Labels != nil && len(child.Labels) > 0 { label += "[" + strings.Join(child.Labels, ", ") + "]" } + if len(child.Returns) > 0 { + label += "\n returns: " + StringDictToJsonString(child.Returns) + } if len(child.ThreadsMap) > 0 { label += fmt.Sprintf("\n ThreadsMap: %v", child.ThreadsMap) } diff --git a/modelchecker/processor.go b/modelchecker/processor.go index 4094962..d606f4a 100644 --- a/modelchecker/processor.go +++ b/modelchecker/processor.go @@ -46,6 +46,15 @@ const ( // When false: permute all symmetric values from the definition const canonicalizeSymmetricValues = true +// excludeReturnsFromState, when true, omits Process.Returns from HashCode, +// JSON state serialization, and the dot-file state label. Returns remain +// populated during execution (functions/invariants still read them) and are +// always available on Link.Returns. Use this to verify downstream consumers +// have migrated to reading return values from links rather than from state. +// Toggled via Processor.SetExperimentalNoStateReturns; planned to become the +// default once consumers have migrated. +var excludeReturnsFromState bool + const enableCaptureStackTrace = false type Definition struct { @@ -269,7 +278,7 @@ func NewProcess(name string, files []*ast.File, parent *Process) *Process { } func (p *Process) MarshalJSON() ([]byte, error) { - return lib.MarshalJSON(map[string]interface{}{ + fields := map[string]interface{}{ "state": p.Heap, "threads": p.GetThreads(), "current": p.Current, @@ -277,11 +286,14 @@ func (p *Process) MarshalJSON() ([]byte, error) { "failedInvariants": p.FailedInvariants, "stats": p.Stats, "witness": p.Witness, - "returns": StringDictToJsonString(p.Returns), "roles": p.Roles, "channels": p.Channels, "channel_messages": p.ChannelMessages, - }) + } + if !excludeReturnsFromState { + fields["returns"] = StringDictToJsonString(p.Returns) + } + return lib.MarshalJSON(fields) } func (p *Process) HasFailedInvariants() bool { @@ -554,7 +566,7 @@ func (n *Node) appendState(p *Process, buf *strings.Builder) { buf.WriteString("State: ") buf.WriteString(escapedString) } - if len(p.Returns) > 0 { + if !excludeReturnsFromState && len(p.Returns) > 0 { jsonString := StringDictToJsonString(p.Returns) // Escape double quotes escapedString := strings.ReplaceAll(jsonString, "\"", "\\\"") @@ -610,7 +622,9 @@ func (p *Process) HashCode() string { h.Write([]byte(hash)) } - h.Write([]byte(StringDictToJsonString(p.Returns))) + if !excludeReturnsFromState { + h.Write([]byte(StringDictToJsonString(p.Returns))) + } for _, role := range p.Roles { // Include the role's data in the hash to distinguish processes with different role states @@ -972,6 +986,10 @@ type Link struct { ReqId int ThreadsMap map[int]int FailedInvariants map[int][]int + // Returns holds the action's return value (if any) for this transition. + // Forward-compatible field for consumers (graph, MBT, explorer) to migrate + // to reading return values from the link instead of from Process.Returns. + Returns starlark.StringDict } func (l *Link) IsCrashLink() bool { @@ -1025,6 +1043,7 @@ func (n *Node) Duplicate(other *Node, yield bool) { ChoiceFairness: n.Inbound[0].ChoiceFairness, Messages: n.Inbound[0].Messages, ReqId: n.Inbound[0].ReqId, + Returns: n.Inbound[0].Returns, } parent.Outbound = append(parent.Outbound, newOutLink) @@ -1075,6 +1094,7 @@ func (n *Node) Attach() { ChoiceFairness: n.Inbound[0].ChoiceFairness, Messages: n.Inbound[0].Messages, ReqId: n.Inbound[0].ReqId, + Returns: n.Inbound[0].Returns, FailedInvariants: n.Inbound[0].FailedInvariants, } @@ -1221,6 +1241,15 @@ func (p *Processor) SetExperimentalNoGraph(v bool) { p.experimentalNoGraph = v } +// SetExperimentalNoStateReturns toggles whether Process.Returns is included +// in HashCode, JSON state, and dot labels. When true, returns are visible +// only via Link.Returns — use this to verify downstream consumers have +// migrated. Sets a package-level variable (the flag is process-wide, not +// per-Processor). +func (p *Processor) SetExperimentalNoStateReturns(v bool) { + excludeReturnsFromState = v +} + // breakParentRef releases a freshly-forked child's back-reference to its // parent Node so the parent can be GC'd once it leaves the queue. The // Inbound link's metadata (Name, etc.) is preserved; only the .Node pointer @@ -1771,16 +1800,14 @@ func (p *Processor) printRunSummary(startTime time.Time) { // These are the design's target memory metrics — comparing peak queue length // across OLD vs NEW runs shows the dedup-before-enqueue savings. func (p *Processor) printPeakSummary() { - mode := "old" - if p.experimentalProcessedQueue { - mode = "new" - } - if p.experimentalProcessedQueue { - fmt.Printf("Peak (%s): queue=%d pendingActionStarts=%d\n", - mode, p.peakQueueLen, p.peakPendingActionStarts) - } else { - fmt.Printf("Peak (%s): queue=%d\n", mode, p.peakQueueLen) + // Only print under the experimental queue mode — the metric is meaningful + // for comparing old vs new dedup behavior. Printing in the default path + // causes baseline drift for every reference spec. + if !p.experimentalProcessedQueue { + return } + fmt.Printf("Peak (new): queue=%d pendingActionStarts=%d\n", + p.peakQueueLen, p.peakPendingActionStarts) } func (p *Processor) StartSimulation() (init *Node, failedNode *Node, err error) { @@ -2061,6 +2088,14 @@ func (p *Processor) processNode(node *Node) (bool, bool) { node.Inbound[0].Fairness = node.Process.Fairness node.Inbound[0].Messages = append(node.Inbound[0].Messages, node.Process.Messages...) + + if len(node.Process.Returns) > 0 { + returns := make(starlark.StringDict, len(node.Process.Returns)) + for k, v := range node.Process.Returns { + returns[k] = v + } + node.Inbound[0].Returns = returns + } } // If the node is already visited, merge the nodes and return diff --git a/proto/graph.proto b/proto/graph.proto index 3888809..536dcd7 100644 --- a/proto/graph.proto +++ b/proto/graph.proto @@ -30,6 +30,11 @@ message Link { int64 req_id = 7; map new_to_old_threads = 8; string type = 9; + // Action return values for this transition. name is the action name (or + // role.action for role actions); value is the starlark repr of the + // returned value (e.g. `"x"` for a string, `42` for an int, `[1, 2]` + // for a list). Sorted by name for deterministic output. + repeated NameValue returns = 10; } message Links {