fig-11-terminator.rkt

#lang racket
(require termination)

(define (nondet) (- (random 1000) 500))
(define (nondet?) (> (random) 0.5))

;; Program with "ghost" states `d1`, `d2` tracking variable distances
(define (main* [x (nondet)] [y (nondet)] [z (nondet)])
  (printf "- init: ~a ~a ~a~n" x y z)
  (when (> y 0)
    (define (loop x z d1 d2)
      (printf "    + ~a ~a~n" x z)
      (define-values (x* z*)
        (if (nondet?)
            (values (+ x y) z)
            (values x (- x y))))
      (when (< x* y z*)
        (loop x* z* (- y x*) (- z* y))))
    (loop x z (- y x) (- z y))))

;; No false positive after 100 attempts
(for ([i (in-range 100)])
  (begin/termination (main*)))

;; Original program
(define (main [x (nondet)] [y (nondet)] [z (nondet)])
  (printf "- init: ~a ~a ~a~n" x y z)
  (when (> y 0)
    (define (loop x z)
      (printf "    + ~a ~a~n" x z)
      (define-values (x* z*)
        (if (nondet?)
            (values (+ x y) z)
            (values x (- x y))))
      (when (< x* y z*)
        (loop x* z*)))
    (loop x z)))

(for ([i (in-range 100)])
  (begin/termination (main)))
  
; possible-non-termination: Recursive call to code point `40` has no obvious descendence on any argument
; - Preceding call:
;   * arg 0: -146
;   * arg 1: 385
; - Subsequent call:
;   * arg 0: 28
;   * arg 1: 385
; New graph:
;   * 1 ↧ 1
;   * 1 ↓ 0
; Size-change violating graph:
;   * 1 ↧ 1
;   * 1 ↓ 0
; Call stack:
;   * 40
;   * 1
;   * 0