(import (scheme base))
(include "tmc-part3.scm")

;; ticket lock implementation ----
(INIT 'grant 0)
(INIT 'ticket 0)

(define (take-ticket)
  (ATOMIC
    (let* ((tk (READ 'ticket))
           (tck (+ tk 1)))
      (WRITE 'ticket tck)
      tck)))

(define (wait-grant v)
  (unless (= v (READ 'grant))
    (AWAIT 'grant)
    (wait-grant v))
  v)

(define (release t)
  (WRITE 'grant (+ 1 t)))

(define (acquire) ;
  (wait-grant (take-ticket)))

;; client code ----
(INIT 'x 0)

(define (task)
  (let ((t (acquire)))
    (let ((a (READ 'x)))
      (WRITE 'x (+ a 1))
      (release t))))

;; create tasks and explore ----
(SPAWN task)
(SPAWN task)
(SPAWN task)

(EXPLORE
  (lambda ()
    (= (READ 'x) 3)))