From aaa2203ff02678c152890eb744eb1311377e2d1d Mon Sep 17 00:00:00 2001 From: jayaprabhakar Date: Thu, 5 Feb 2026 15:24:53 -0800 Subject: [PATCH] Avoid deep cloning by using a single copy --- lib/jsonmarshaller.go | 5 + lib/starlark_role.go | 41 ++++-- modelchecker/clone.go | 24 +++- modelchecker/processor.go | 182 +++++++++++++++++++++--- modelchecker/state_visitor.go | 255 +++++++++++++++++++++++++++++++++- modelchecker/thread.go | 4 + 6 files changed, 468 insertions(+), 43 deletions(-) diff --git a/lib/jsonmarshaller.go b/lib/jsonmarshaller.go index e63a634..16c44fa 100644 --- a/lib/jsonmarshaller.go +++ b/lib/jsonmarshaller.go @@ -5,6 +5,7 @@ import ( "fmt" "go.starlark.net/starlark" "go.starlark.net/starlarkstruct" + "sort" "strings" ) @@ -84,6 +85,10 @@ func MarshalJSONStarlarkValue(m starlark.Value, depth int) ([]byte, error) { return []byte(buf.String()), nil case "genericmap", "dict": items := m.(starlark.IterableMapping).Items() + // Sort items by key to have deterministic output + sort.Slice(items, func(i, j int) bool { + return items[i][0].String() < items[j][0].String() + }) buf := strings.Builder{} buf.WriteString("{") first := true diff --git a/lib/starlark_role.go b/lib/starlark_role.go index 307e068..d6ed180 100644 --- a/lib/starlark_role.go +++ b/lib/starlark_role.go @@ -3,8 +3,9 @@ package lib import ( ast "fizz/proto" "fmt" - "go.starlark.net/starlark" "strings" + + "go.starlark.net/starlark" ) var ( @@ -22,7 +23,7 @@ func ClearRoleRefs() { } type Role struct { - Ref int64 + ID starlark.Value // Can be *ModelValue or *SymmetricValue Name string Symmetric bool Params *Struct @@ -30,6 +31,8 @@ type Role struct { Methods map[string]*starlark.Function RoleMethods map[string]*starlark.Builtin InitValues *Struct + + // Ref field is removed. Use GetRef() to retrieve the integer ID from the ID field. } func (r *Role) AddMethod(name string, val starlark.Value) error { @@ -81,10 +84,18 @@ func (r *Role) Attr(name string) (starlark.Value, error) { } func (r *Role) GetId() starlark.Value { - if r.Symmetric { - return NewSymmetricValue(r.Name, r.Ref) + return r.ID +} + +// GetRef returns the integer reference ID from the underlying ID object +func (r *Role) GetRef() int64 { + if sv, ok := r.ID.(*SymmetricValue); ok { + return sv.GetId() } - return NewModelValue(r.Name, r.Ref) + if mv, ok := r.ID.(*ModelValue); ok { + return mv.id + } + return -1 } func (r *Role) AttrNames() []string { @@ -93,7 +104,7 @@ func (r *Role) AttrNames() []string { func (r *Role) String() string { b := strings.Builder{} - b.WriteString(fmt.Sprintf("role %s#%d (", r.Name, r.Ref)) + b.WriteString(fmt.Sprintf("role %s#%d (", r.Name, r.GetRef())) if len(r.Params.AttrNames()) > 0 { b.WriteString(r.Params.String()) b.WriteString(",") @@ -107,7 +118,7 @@ func (r *Role) MarshalJSON() ([]byte, error) { b := strings.Builder{} b.WriteString("{") b.WriteString(fmt.Sprintf("\"name\": \"%s\",", r.Name)) - b.WriteString(fmt.Sprintf("\"ref\": %d,", r.Ref)) + b.WriteString(fmt.Sprintf("\"ref\": %d,", r.GetRef())) b.WriteString(fmt.Sprintf("\"ref_string\": \"%s\",", r.RefStringShort())) b.WriteString("\"params\": ") params, err := r.Params.MarshalJSON() @@ -128,7 +139,7 @@ func (r *Role) MarshalJSON() ([]byte, error) { } func (r *Role) RefString() string { - return GenerateRefString(r.Name, r.Ref) + return GenerateRefString(r.Name, r.GetRef()) } func GenerateRefString(name string, ref int64) string { @@ -136,7 +147,7 @@ func GenerateRefString(name string, ref int64) string { } func (r *Role) RefStringShort() string { - return fmt.Sprintf("%s#%d", r.Name, r.Ref) + return fmt.Sprintf("%s#%d", r.Name, r.GetRef()) } func (r *Role) Type() string { @@ -153,7 +164,7 @@ func (r *Role) Truth() starlark.Bool { func (r *Role) Hash() (uint32, error) { hash, _ := starlark.String(r.Name).Hash() - return hash + uint32(r.Ref), nil + return hash + uint32(r.GetRef()), nil } func (r *Role) IsSymmetric() bool { @@ -181,7 +192,15 @@ func CreateRoleBuiltin(astRole *ast.Role, symmetric bool, roles *[]*Role) *starl for _, function := range astRole.Functions { roleMethods[function.Name] = starlark.NewBuiltin(function.Name, fizz_func_always_error) } - r := &Role{Ref: nextRef, Name: name, Symmetric: symmetric, Params: params, Fields: fields, Methods: map[string]*starlark.Function{}, RoleMethods: roleMethods, InitValues: initValues} + + var id starlark.Value + if symmetric { + id = NewSymmetricValue(name, nextRef) + } else { + id = NewModelValue(name, nextRef) + } + + r := &Role{ID: id, Name: name, Symmetric: symmetric, Params: params, Fields: fields, Methods: map[string]*starlark.Function{}, RoleMethods: roleMethods, InitValues: initValues} *roles = append(*roles, r) return r, nil }) diff --git a/modelchecker/clone.go b/modelchecker/clone.go index 2ddface..e86df9b 100644 --- a/modelchecker/clone.go +++ b/modelchecker/clone.go @@ -222,16 +222,26 @@ func deepCloneStarlarkValueWithPermutations(value starlark.Value, refs map[starl case "role": r := value.(*lib.Role) prefix := r.Name - id := r.Ref + id := r.GetId() // Get the ID object directly if r.IsSymmetric() { - oldSymVal := lib.NewSymmetricValue(r.Name, r.Ref) - newVal, err := deepCloneStarlarkValueWithPermutations(oldSymVal, refs, permutations, alt) + // Cloning the ID object checks permutations + newVal, err := deepCloneStarlarkValueWithPermutations(r.ID, refs, permutations, alt) if err != nil { return nil, err } - newRoleId := newVal.(*lib.SymmetricValue) - prefix = newRoleId.GetPrefix() - id = newRoleId.GetId() + id = newVal // Use the new (permuted) ID object + + // If we need prefix from the new ID (though it shouldn't change for roles usually) + if sv, ok := id.(*lib.SymmetricValue); ok { + prefix = sv.GetPrefix() + } + } else { + // For non-symmetric roles, we still want to clone the ID model value + newVal, err := deepCloneStarlarkValueWithPermutations(r.ID, refs, permutations, alt) + if err != nil { + return nil, err + } + id = newVal } if cached, ok := refs[value]; ok { @@ -246,7 +256,7 @@ func deepCloneStarlarkValueWithPermutations(value starlark.Value, refs map[starl return nil, err } newRole := &lib.Role{ - Ref: id, + ID: id, Name: prefix, Symmetric: r.IsSymmetric(), Params: params.(*lib.Struct), diff --git a/modelchecker/processor.go b/modelchecker/processor.go index 747264a..b9c9e34 100644 --- a/modelchecker/processor.go +++ b/modelchecker/processor.go @@ -47,6 +47,10 @@ const ( // When false: permute all symmetric values from the definition const canonicalizeSymmetricValues = true +// When true: compare StateVisitor vs CloneWithRefs for collecting SymmetricValue pointers +// Enable for debugging pointer identity issues +const CompareSymmetricValueMethods = false + const enableCaptureStackTrace = false type Definition struct { @@ -358,6 +362,10 @@ func (p *Process) Fork() *Process { func (p *Process) CloneForAssert(permutations map[*lib.SymmetricValue][]*lib.SymmetricValue, alt int) *Process { refs := make(map[starlark.Value]starlark.Value) + return p.CloneWithRefs(permutations, alt, refs) +} + +func (p *Process) CloneWithRefs(permutations map[*lib.SymmetricValue][]*lib.SymmetricValue, alt int, refs map[starlark.Value]starlark.Value) *Process { p2 := &Process{ Name: p.Name, Heap: p.Heap.Clone(refs, permutations, alt), @@ -1701,11 +1709,21 @@ func (p *Processor) crashThread(node *Node) { } func (p *Process) getSymmetryTranslations() []string { - permMap, count := getSymmetryPermutations(p) + //fmt.Println("\nCalculating symmetry translations for process:", p.Name) + p2, refs, permMap, count := getSymmetryPermutations(p) + //fmt.Println("Symmetry permutations count:", count, permMap) + //fmt.Println("Permutation map:", permMap) hashes := make([]string, count) for i := 0; i < count; i++ { - hashes[i] = p.symmetricHash(permMap, i) + hashes[i] = p2.symmetricHashWithoutClone(refs, permMap, i) } + // Print unique hashes + uniqueHashes := make(map[string]bool) + for _, h := range hashes { + uniqueHashes[h] = true + } + //fmt.Printf("Unique hashes: %d out of %d\n", len(uniqueHashes), len(hashes)) + //fmt.Println(uniqueHashes) return hashes } @@ -1732,15 +1750,141 @@ func (p *Processor) findVisitedSymmetric(node *Node) (*Node, bool, string) { } func (p *Process) symmetricHash(permutations map[*lib.SymmetricValue][]*lib.SymmetricValue, alt int) string { - p2 := p.CloneForAssert(permutations, alt) + refs := make(map[starlark.Value]starlark.Value) + p2 := p.CloneWithRefs(permutations, alt, refs) return p2.HashCode() } +func (p *Process) symmetricHashWithoutClone(refs map[starlark.Value]starlark.Value, permutations map[*lib.SymmetricValue][]*lib.SymmetricValue, alt int) string { + // Debug: Verify consistency if needed (can be removed for production speed) + // p.CachedHashCode = "" + // p.CachedThreadHashes = nil + // p.Heap.CachedHashCode = "" + // hash0 := p.HashCode() + + // 1. Build refMappings (Prefix -> OldID -> NewID) + // This helps us apply the permutation to all instances of SymmetricValue/Role, + // not just the ones found as keys in the permutations map. + refMappings := make(map[string]map[int64]int64) + for symVal, perm := range permutations { + prefix := symVal.GetPrefix() + if refMappings[prefix] == nil { + refMappings[prefix] = make(map[int64]int64) + } + oldRef := symVal.GetId() + newRef := perm[alt].GetId() + refMappings[prefix][oldRef] = newRef + } + + // 2. Iterate refs to find ALL SymmetricValue and Role pointers, and mutate them if they have a mapping. + // We track original values to restore them later. + origSymVals := make(map[*lib.SymmetricValue]int64) + + // Helper to mutate SymmetricValue + mutateSymValue := func(sv *lib.SymmetricValue) { + if mapping, ok := refMappings[sv.GetPrefix()]; ok { + if newId, found := mapping[sv.GetId()]; found { + if _, recorded := origSymVals[sv]; !recorded { + origSymVals[sv] = sv.GetId() + sv.SetId(newId) + } + } + } + } + + // Iterate over all values in refs (which contains all reachable objects from the clone) + for _, val := range refs { + if sv, ok := val.(*lib.SymmetricValue); ok { + mutateSymValue(sv) + } + } + + // 3. (Removed explicit Role mutation loop as Roles now hold the same SymmetricValue pointers) + + // 3b. Repair Starlark Dicts + // Since we mutated SymmetricValues in-place, any Starlark Dicts using them as keys + // are now corrupted (keys in wrong hash buckets). We must re-insert entries. + var dictsToRepair []*starlark.Dict + for _, val := range refs { + if d, ok := val.(*starlark.Dict); ok { + dictsToRepair = append(dictsToRepair, d) + } + } + repairDicts := func() { + for _, d := range dictsToRepair { + items := d.Items() + d.Clear() + for _, item := range items { + d.SetKey(item[0], item[1]) + } + } + } + repairDicts() + + // 4. Update ChannelMessage receivers (String update) + // We construct a replacement map for strings "Name#OldID" -> "Name#NewID" + replacements := make(map[string]string) + for prefix, mapping := range refMappings { + for oldRef, newRef := range mapping { + // Role.RefStringShort is "Name#Ref" + oldStr := fmt.Sprintf("%s#%d", prefix, oldRef) + newStr := fmt.Sprintf("%s#%d", prefix, newRef) + replacements[oldStr] = newStr + } + } + + origReceivers := make(map[*ChannelMessage]string) + for _, msgs := range p.ChannelMessages { + for _, msg := range msgs { + if newReceiver, ok := replacements[msg.receiver]; ok { + origReceivers[msg] = msg.receiver + msg.receiver = newReceiver + } + } + } + + // 5. Sort p.Roles to ensure canonical order + // This is necessary because p.Roles is a slice and its order affects the state representation. + // We sort by Name then Ref. + origRoles := make([]*lib.Role, len(p.Roles)) + copy(origRoles, p.Roles) + sort.Slice(p.Roles, func(i, j int) bool { + if p.Roles[i].Name != p.Roles[j].Name { + return p.Roles[i].Name < p.Roles[j].Name + } + return p.Roles[i].GetRef() < p.Roles[j].GetRef() + }) + + // 6. Compute Hash + p.CachedHashCode = "" + p.CachedThreadHashes = nil + p.Heap.CachedHashCode = "" + hash1 := p.HashCode() + + // 7. Restore Everything + copy(p.Roles, origRoles) + for msg, oldReceiver := range origReceivers { + msg.receiver = oldReceiver + } + for sv, oldId := range origSymVals { + sv.SetId(oldId) + } + // No need to restore explicit Role refs + + // Repair Dicts again to restore original state validity + repairDicts() + + return hash1 + +} func (p *Process) GetSymmetryRoles() []*lib.SymmetricValues { m := make(map[string][]*lib.SymmetricValue) for _, role := range p.Roles { if role != nil && role.IsSymmetric() { - m[role.Name] = append(m[role.Name], lib.NewSymmetricValue(role.Name, role.Ref)) + sv, ok := role.GetId().(*lib.SymmetricValue) + if ok { + m[role.Name] = append(m[role.Name], sv) + } } } roleSymValues := make([]*lib.SymmetricValues, 0, len(m)) @@ -1765,7 +1909,7 @@ func (p *Process) addChannelMessage(channel *lib.Channel, roleShortRef string, f } } -func getSymmetryPermutations(process *Process) (map[*lib.SymmetricValue][]*lib.SymmetricValue, int) { +func getSymmetryPermutations(process *Process) (*Process, map[starlark.Value]starlark.Value, map[*lib.SymmetricValue][]*lib.SymmetricValue, int) { var values [][]*lib.SymmetricValue var usedValues [][]*lib.SymmetricValue @@ -1781,10 +1925,13 @@ func getSymmetryPermutations(process *Process) (map[*lib.SymmetricValue][]*lib.S var rotationalExtraMappings [][]staticMapping // extraMappingForPost maps postProcessingMappings index to the rotationalExtraMappings index. extraMappingForPost := make(map[int]int) - + var p2 *Process + var refs map[starlark.Value]starlark.Value if canonicalizeSymmetricValues { - // Collect only the symmetric values that are actually used in the state - allUsedValues := process.getUsedSymmetricValues() + // Collect symmetric values using clone-based approach (single clone to get actual pointers) + // This replaces both getUsedSymmetricValues() (StateVisitor) and GetSymmetryRoles() + var allUsedValues [][]*lib.SymmetricValue + p2, refs, allUsedValues = process.getUsedSymmetricValuesFromClone() // Build domain map from globals for accessing Reflection flag domainMap := make(map[string]*lib.SymmetryDomain) @@ -1969,18 +2116,9 @@ func getSymmetryPermutations(process *Process) (map[*lib.SymmetricValue][]*lib.S } } - // Add symmetric roles (these already only include instantiated roles) - // Roles are assumed Nominal - roles := process.GetSymmetryRoles() - for _, role := range roles { - v := make([]*lib.SymmetricValue, role.Len()) - for j := 0; j < role.Len(); j++ { - v[j] = role.Index(j) - } - slices.SortFunc(v, lib.CompareStringer[*lib.SymmetricValue]) - values = append(values, v) - usedValues = append(usedValues, v) - } + // Note: Symmetric roles are now included via getUsedSymmetricValuesFromClone() + // which extracts them from refs during the preliminary clone. + // No need for separate GetSymmetryRoles() call. // Generate all permutations permutations := lib.GenerateAllPermutations(values) @@ -1989,7 +2127,7 @@ func getSymmetryPermutations(process *Process) (map[*lib.SymmetricValue][]*lib.S v[i] = slices.Concat(permutation...) } - // Build permutation map with actual used values as keys + // Build permutation map - usedValues already contains actual pointers from clone permMap := make(map[*lib.SymmetricValue][]*lib.SymmetricValue) actualKeys := make([]*lib.SymmetricValue, 0) for _, used := range usedValues { @@ -2119,7 +2257,7 @@ func getSymmetryPermutations(process *Process) (map[*lib.SymmetricValue][]*lib.S if finalCount == 0 { finalCount = len(v) } - return permMap, finalCount + return p2, refs, permMap, finalCount } func (p *Processor) processInit(node *Node) bool { diff --git a/modelchecker/state_visitor.go b/modelchecker/state_visitor.go index 623eac3..9c0cf39 100644 --- a/modelchecker/state_visitor.go +++ b/modelchecker/state_visitor.go @@ -1,6 +1,7 @@ package modelchecker import ( + "fmt" "slices" "github.com/fizzbee-io/fizzbee/lib" @@ -14,8 +15,8 @@ type StateVisitor interface { // UsedSymmetricValuesCollector collects all SymmetricValue instances in the current state type UsedSymmetricValuesCollector struct { - usedValues map[string]map[int64]bool // prefix -> set of IDs - limits map[string]int // prefix -> Limit (for rotational domains) + usedValues map[string]map[int64]bool // prefix -> set of IDs + limits map[string]int // prefix -> Limit (for rotational domains) pointers map[string]map[int64]*lib.SymmetricValue // prefix -> ID -> actual pointer from state } @@ -182,7 +183,7 @@ func visitStarlarkValue(value starlark.Value, visitor StateVisitor, visited map[ case "role": role := value.(*lib.Role) if role.IsSymmetric() { - roleId := lib.NewSymmetricValue(role.Name, role.Ref) + roleId := lib.NewSymmetricValue(role.Name, role.GetRef()) visitor.VisitSymmetricValue(roleId) // roleId is already a pointer now } visitStarlarkValue(role.Fields, visitor, visited) @@ -309,3 +310,251 @@ func (p *Process) getUsedSymmetricValues() [][]*lib.SymmetricValue { return result } + +// getUsedSymmetricValuesFromRefs extracts SymmetricValue pointers from refs map after cloning +// This is an alternative to using StateVisitor - the refs map keys ARE the original pointers +func (p *Process) getUsedSymmetricValuesFromRefs() [][]*lib.SymmetricValue { + // Clone with nil permutations just to populate refs + refs := make(map[starlark.Value]starlark.Value) + _ = p.CloneWithRefs(nil, 0, refs) + + // Extract SymmetricValues from refs keys, grouped by prefix + byPrefix := make(map[string]map[int64]*lib.SymmetricValue) + for key := range refs { + if sv, ok := key.(*lib.SymmetricValue); ok { + prefix := sv.GetPrefix() + if byPrefix[prefix] == nil { + byPrefix[prefix] = make(map[int64]*lib.SymmetricValue) + } + byPrefix[prefix][sv.GetId()] = sv + } + } + + // Build a map of materialized rotational domains from globals + materializedDomains := make(map[string]*lib.SymmetryDomain) + for _, val := range p.Heap.globals { + if domain, ok := val.(*lib.SymmetryDomain); ok { + if domain.Materialize && domain.Kind == lib.SymmetryKindRotational { + materializedDomains[domain.Name] = domain + } + } + } + + // Get all symmetric value definitions to maintain ordering + defs := p.Heap.GetSymmetryDefs() + + result := make([][]*lib.SymmetricValue, 0) + for _, def := range defs { + if def.Len() == 0 { + continue + } + + prefix := def.Index(0).GetPrefix() + + // For materialized rotational domains, return the full set + if domain, ok := materializedDomains[prefix]; ok { + fullSet := make([]*lib.SymmetricValue, domain.Limit) + for i := 0; i < domain.Limit; i++ { + fullSet[i] = lib.NewRotationalSymmetricValue(prefix, int64(i), domain.Limit) + } + result = append(result, fullSet) + continue + } + + // Get values from refs for this prefix + if prefixMap, ok := byPrefix[prefix]; ok && len(prefixMap) > 0 { + // Sort by ID + ids := make([]int64, 0, len(prefixMap)) + for id := range prefixMap { + ids = append(ids, id) + } + slices.Sort(ids) + + values := make([]*lib.SymmetricValue, len(ids)) + for i, id := range ids { + values[i] = prefixMap[id] + } + result = append(result, values) + } + } + + return result +} + +// CompareSymmetricValueMethods compares StateVisitor vs CloneWithRefs approaches +// Returns true if they produce the same pointers, false otherwise with details +func (p *Process) CompareSymmetricValueMethods() (bool, string) { + visitorResult := p.getUsedSymmetricValues() + refsResult := p.getUsedSymmetricValuesFromRefs() + + if len(visitorResult) != len(refsResult) { + return false, fmt.Sprintf("different number of groups: visitor=%d, refs=%d", len(visitorResult), len(refsResult)) + } + + for i := range visitorResult { + if len(visitorResult[i]) != len(refsResult[i]) { + return false, fmt.Sprintf("group %d has different sizes: visitor=%d, refs=%d", i, len(visitorResult[i]), len(refsResult[i])) + } + + for j := range visitorResult[i] { + vPtr := visitorResult[i][j] + rPtr := refsResult[i][j] + + // Check if same pointer + if vPtr != rPtr { + // Check if same values but different pointers + if vPtr.GetPrefix() == rPtr.GetPrefix() && vPtr.GetId() == rPtr.GetId() { + return false, fmt.Sprintf("group %d, index %d: same value but DIFFERENT pointers - visitor=%p, refs=%p (prefix=%s, id=%d)", + i, j, vPtr, rPtr, vPtr.GetPrefix(), vPtr.GetId()) + } + return false, fmt.Sprintf("group %d, index %d: different values - visitor=%v, refs=%v", i, j, vPtr, rPtr) + } + } + } + + return true, "all pointers match" +} + +// getActualSymmetricValuePointers returns a map from prefix to the actual SymmetricValue pointers +// found during cloning. These are the real pointers that will be encountered when cloning +// with permutations, so they should be used as map keys for efficient O(1) lookup. +func (p *Process) getActualSymmetricValuePointers() map[string][]*lib.SymmetricValue { + _, _, result := p.cloneAndGetSymmetricValuePointers() + return result +} + +// cloneAndGetSymmetricValuePointers does a preliminary clone and returns both: +// 1. The map from prefix to actual SymmetricValue pointers (for use as permutation map keys) +// 2. These pointers are the REAL pointers from the state, not newly created ones +// This replaces both getUsedSymmetricValues() and GetSymmetryRoles() with a single clone operation. +func (p *Process) cloneAndGetSymmetricValuePointers() (*Process, map[starlark.Value]starlark.Value, map[string][]*lib.SymmetricValue) { + // Clone with nil permutations to populate refs with actual pointers + refs := make(map[starlark.Value]starlark.Value) + p2 := p.CloneWithRefs(nil, 0, refs) + + // Count total SymmetricValue pointers vs unique (prefix, id) pairs + totalSVPointers := 0 + totalRolePointers := 0 + uniquePairs := make(map[string]bool) + rolesByName := make(map[string]int) + for _, val := range refs { + if sv, ok := val.(*lib.SymmetricValue); ok { + totalSVPointers++ + key := fmt.Sprintf("%s:%d", sv.GetPrefix(), sv.GetId()) + uniquePairs[key] = true + } + if role, ok := val.(*lib.Role); ok { + totalRolePointers++ + rolesByName[role.Name]++ + } + } + if totalSVPointers != len(uniquePairs) { + // fmt.Printf("DEBUG: Found %d SymmetricValue pointers but only %d unique (prefix,id) pairs\n", totalSVPointers, len(uniquePairs)) + } + if totalRolePointers > 0 { + // fmt.Printf("DEBUG: Found %d Role pointers: %v\n", totalRolePointers, rolesByName) + } + + // Extract SymmetricValues from refs - collect ALL pointers, not just unique (prefix, id) + // Group by (prefix, id) to track multiple pointers with same logical value + type svKey struct { + prefix string + id int64 + } + allPointersByKey := make(map[svKey][]*lib.SymmetricValue) + for _, val := range refs { + if sv, ok := val.(*lib.SymmetricValue); ok { + key := svKey{prefix: sv.GetPrefix(), id: sv.GetId()} + allPointersByKey[key] = append(allPointersByKey[key], sv) + } + } + + // For the result, we just need one representative pointer per (prefix, id) for permutation generation + // But we'll need all pointers for mutation - store them in p2 for later use + byPrefix := make(map[string]map[int64]*lib.SymmetricValue) + for key, ptrs := range allPointersByKey { + if byPrefix[key.prefix] == nil { + byPrefix[key.prefix] = make(map[int64]*lib.SymmetricValue) + } + // Use the first pointer as representative + byPrefix[key.prefix][key.id] = ptrs[0] + } + + // Convert to sorted slices + result := make(map[string][]*lib.SymmetricValue) + for prefix, idMap := range byPrefix { + ids := make([]int64, 0, len(idMap)) + for id := range idMap { + ids = append(ids, id) + } + slices.Sort(ids) + + values := make([]*lib.SymmetricValue, len(ids)) + for i, id := range ids { + values[i] = idMap[id] + } + result[prefix] = values + } + + return p2, refs, result +} + +// getUsedSymmetricValuesFromClone returns the symmetric values grouped for permutation generation. +// This replaces getUsedSymmetricValues() by using actual pointers from cloning. +// Returns [][]*lib.SymmetricValue in the same format as getUsedSymmetricValues. +// Also returns the refs map which contains ALL SymmetricValue pointers (for mutation during hashing). +func (p *Process) getUsedSymmetricValuesFromClone() (*Process, map[starlark.Value]starlark.Value, [][]*lib.SymmetricValue) { + p2, refs, byPrefix := p.cloneAndGetSymmetricValuePointers() + + // Build a map of materialized rotational domains from globals + materializedDomains := make(map[string]*lib.SymmetryDomain) + for _, val := range p.Heap.globals { + if domain, ok := val.(*lib.SymmetryDomain); ok { + if domain.Materialize && domain.Kind == lib.SymmetryKindRotational { + materializedDomains[domain.Name] = domain + } + } + } + + // Get all symmetric value definitions to maintain ordering + defs := p.Heap.GetSymmetryDefs() + + // Track which prefixes we've already added + addedPrefixes := make(map[string]bool) + + result := make([][]*lib.SymmetricValue, 0) + + // First, add values from definitions (to maintain ordering) + for _, def := range defs { + if def.Len() == 0 { + continue + } + + prefix := def.Index(0).GetPrefix() + addedPrefixes[prefix] = true + + // For materialized rotational domains, return the full set + if domain, ok := materializedDomains[prefix]; ok { + fullSet := make([]*lib.SymmetricValue, domain.Limit) + for i := 0; i < domain.Limit; i++ { + fullSet[i] = lib.NewRotationalSymmetricValue(prefix, int64(i), domain.Limit) + } + result = append(result, fullSet) + continue + } + + // Get values from refs for this prefix + if values, ok := byPrefix[prefix]; ok && len(values) > 0 { + result = append(result, values) + } + } + + // Then, add any remaining prefixes (e.g., symmetric roles not in definitions) + for prefix, values := range byPrefix { + if !addedPrefixes[prefix] && len(values) > 0 { + result = append(result, values) + } + } + + return p2, refs, result +} diff --git a/modelchecker/thread.go b/modelchecker/thread.go index 0ba39ec..a110fb1 100644 --- a/modelchecker/thread.go +++ b/modelchecker/thread.go @@ -234,6 +234,10 @@ func (h *Heap) update(k string, v starlark.Value) bool { return false } +func (h *Heap) GetValue(k string) starlark.Value { + return h.state[k] +} + func (h *Heap) insert(k string, v starlark.Value) bool { h.state[k] = v return true