fix(modelchecker): preserve action return values across symmetric clones (#354)

CloneWithRefs was initializing the clone's Returns field to an empty
StringDict. Since the symmetric-permutation hashing path (findVisitedSymmetric
-> getSymmetryTranslations -> symmetricHashWithoutClone -> p2.HashCode())
operates on a clone, per-action return values were silently stripped from
the dedup key. Two yield-points that differ only in what an action returned
collapsed into one node.

Copy p.Returns into the clone so the symmetric hash matches the original
HashCode (which includes Returns at line 604). This restores the pre-#297
behavior where actions returning values produce distinct nodes — needed
for visualization, MBT, and explorer consumers that depend on the return
value being visible in the graph.

Regression introduced by #297 ("Consistently use min hash value") when
the dedup lookup switched from `visited[node.HashCode()]` to
`visited[minHash]` — the new path always goes through CloneWithRefs.

Co-authored-by: jayaprabhakar <jayaprabhakar@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: 3 people

modelchecker/processor.go

@@ -396,6 +396,15 @@ func (p *Process) CloneForAssert(permutations map[*lib.SymmetricValue][]*lib.Sym
 }
 
 func (p *Process) CloneWithRefs(permutations map[*lib.SymmetricValue][]*lib.SymmetricValue, alt int, refs map[starlark.Value]starlark.Value) *Process {
+	// Copy p.Returns so the clone's HashCode (used by symmetric-permutation
+	// hashing) sees the same action-return data as the original. A fresh
+	// empty map here would silently strip per-action returns from the
+	// dedup key and collapse states that differ only in what an action
+	// returned.
+	returnsCopy := make(starlark.StringDict, len(p.Returns))
+	for k, v := range p.Returns {
+		returnsCopy[k] = v
+	}
 	p2 := &Process{
 		Name:      p.Name,
 		Heap:      p.Heap.Clone(refs, permutations, alt),
@@ -408,7 +417,7 @@ func (p *Process) CloneWithRefs(permutations map[*lib.SymmetricValue][]*lib.Symm
 
 		Children:    []*Process{},
 		Files:       p.Files,
-		Returns:     make(starlark.StringDict),
+		Returns:     returnsCopy,
 		SymbolTable: p.SymbolTable,
 		Modules:     p.Modules,
 		Labels:      make([]string, 0),