@@ -277,17 +277,6 @@ private class Trace extends TTrace {
277
277
result = "Step(" + s1 + ", " + s2 + ", " + t + ")"
278
278
)
279
279
}
280
-
281
- /** Holds if the `i`th pair of this trace is `(s1, s2)`. */
282
- predicate hasPair ( int i , InputSymbol s1 , InputSymbol s2 ) {
283
- this = Step ( s1 , s2 , _) and
284
- i = 0
285
- or
286
- exists ( Trace t |
287
- this = Step ( _, _, t ) and
288
- t .hasPair ( i - 1 , s1 , s2 )
289
- )
290
- }
291
280
}
292
281
293
282
/**
@@ -329,14 +318,25 @@ private class RelevantTrace extends Trace {
329
318
)
330
319
}
331
320
321
+ private Trace getSuffix ( int i ) {
322
+ i = 0 and
323
+ result = this
324
+ or
325
+ this .getSuffix ( i - 1 ) = Step ( _, _, result )
326
+ }
327
+
328
+ private predicate hasTuple ( int i , InputSymbol s1 , InputSymbol s2 ) {
329
+ this .getSuffix ( i ) = Step ( s1 , s2 , _)
330
+ }
331
+
332
332
/** Gets a string corresponding to this trace. */
333
333
// the pragma is needed for the case where `intersect(s1, s2)` has multiple values,
334
334
// not for recursion
335
335
language [ monotonicAggregates]
336
336
string concretise ( ) {
337
337
result =
338
338
concat ( int i , InputSymbol s1 , InputSymbol s2 |
339
- this .hasPair ( i , s1 , s2 )
339
+ this .hasTuple ( i , s1 , s2 )
340
340
|
341
341
intersect ( s1 , s2 ) order by i desc
342
342
)
0 commit comments