@@ -283,7 +283,7 @@ module Make<RegexTreeViewSig TreeImpl> {
283283 }
284284
285285 /**
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.
287287 * Where the end state was reachable from a forwards search from the start state `(pivot, pivot, pivot)`.
288288 * The resulting tuples are exactly those that are on a path from the start state to the end state.
289289 */
@@ -302,16 +302,16 @@ module Make<RegexTreeViewSig TreeImpl> {
302302 }
303303
304304 /**
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.
307307 * Notice that the arguments are flipped, and thus the direction is backwards.
308308 */
309309 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 ( _, _)
315315 }
316316
317317 /**
0 commit comments