CheckTemporalRecursion analyzes a program for potentially problematic recursive temporal rules. Returns a list of warnings about patterns that may cause non-termination or performance issues.
(programInfo *ProgramInfo)
| 62 | // CheckTemporalRecursion analyzes a program for potentially problematic recursive temporal rules. |
| 63 | // Returns a list of warnings about patterns that may cause non-termination or performance issues. |
| 64 | func CheckTemporalRecursion(programInfo *ProgramInfo) []TemporalWarning { |
| 65 | var warnings []TemporalWarning |
| 66 | |
| 67 | // Build a set of temporal predicates |
| 68 | temporalPreds := make(map[ast.PredicateSym]bool) |
| 69 | for pred, decl := range programInfo.Decls { |
| 70 | if decl.IsTemporal() { |
| 71 | temporalPreds[pred] = true |
| 72 | } |
| 73 | } |
| 74 | |
| 75 | if len(temporalPreds) == 0 { |
| 76 | return nil // No temporal predicates, nothing to check |
| 77 | } |
| 78 | |
| 79 | // Build dependency graph using existing depGraph type from stratification.go |
| 80 | dep := buildTemporalDepGraph(programInfo) |
| 81 | |
| 82 | // Find strongly connected components using existing sccs() method |
| 83 | sccs := dep.sccs() |
| 84 | |
| 85 | // Check each SCC for problematic patterns |
| 86 | for _, scc := range sccs { |
| 87 | if len(scc) == 1 { |
| 88 | // Single predicate - check for self-recursion |
| 89 | for pred := range scc { |
| 90 | // Check if there's a self-loop (edge from pred to itself) |
| 91 | if edges, ok := dep[pred]; ok { |
| 92 | if _, hasSelfLoop := edges[pred]; hasSelfLoop { |
| 93 | // Self-recursive temporal predicate |
| 94 | if temporalPreds[pred] { |
| 95 | warnings = append(warnings, TemporalWarning{ |
| 96 | Predicate: pred, |
| 97 | Message: "self-recursive temporal predicate may cause interval explosion; ensure coalescing or use interval limits", |
| 98 | Severity: SeverityWarning, |
| 99 | }) |
| 100 | } |
| 101 | } |
| 102 | } |
| 103 | } |
| 104 | } else { |
| 105 | // Multi-predicate SCC - mutual recursion |
| 106 | hasTemporalPred := false |
| 107 | for pred := range scc { |
| 108 | if temporalPreds[pred] { |
| 109 | hasTemporalPred = true |
| 110 | break |
| 111 | } |
| 112 | } |
| 113 | if hasTemporalPred { |
| 114 | // Get first predicate for the warning message |
| 115 | var firstPred ast.PredicateSym |
| 116 | for pred := range scc { |
| 117 | firstPred = pred |
| 118 | break |
| 119 | } |
| 120 | warnings = append(warnings, TemporalWarning{ |
| 121 | Predicate: firstPred, |