@@ -283,7 +283,7 @@ module Make<RegexTreeViewSig TreeImpl> {
283
283
}
284
284
285
285
/**
286
- * Gets a tuple tuple reachable from the end state `(succ, succ, succ)` in a backwards exploratory search.
286
+ * Gets a state tuple that can reach the end state `(succ, succ, succ)`, found via a backwards exploratory search.
287
287
* Where the end state was reachable from a forwards search from the start state `(pivot, pivot, pivot)`.
288
288
* The resulting tuples are exactly those that are on a path from the start state to the end state.
289
289
*/
@@ -302,16 +302,16 @@ module Make<RegexTreeViewSig TreeImpl> {
302
302
}
303
303
304
304
/**
305
- * Holds if there exists a transition from `r ` to `q ` in the product automaton.
306
- * Where `r ` and `q ` are both on a path from a start state to an end state.
305
+ * Holds if there exists a transition from `src ` to `dst ` in the product automaton.
306
+ * Where `src ` and `dst ` are both on a path from a start state to an end state.
307
307
* Notice that the arguments are flipped, and thus the direction is backwards.
308
308
*/
309
309
pragma [ noinline]
310
- predicate tupleDeltaBackwards ( StateTuple q , StateTuple r ) {
311
- step ( r , _, _, _, q ) and
312
- // `step` ensures that `r ` and `q ` have the same pivot and succ.
313
- r = getARelevantStateTuple ( _, _) and
314
- q = getARelevantStateTuple ( _, _)
310
+ predicate tupleDeltaBackwards ( StateTuple dst , StateTuple src ) {
311
+ step ( src , _, _, _, dst ) and
312
+ // `step` ensures that `src ` and `dst ` have the same pivot and succ.
313
+ src = getARelevantStateTuple ( _, _) and
314
+ dst = getARelevantStateTuple ( _, _)
315
315
}
316
316
317
317
/**
0 commit comments