feat(modelchecker): expose action returns on Link + add no-state-retu…

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

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

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)
 			}

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,19 +278,22 @@ 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,
 		"name":             p.Name,
 		"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

proto/graph.proto

@@ -30,6 +30,11 @@ message Link {
   int64 req_id = 7;
   map<int64, int64> 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 {