Simple

This example was used as an illustrative example in:

Thread-modular Abstraction Refinement. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Proceedings of the 15th International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science, Springer-Verlag, 2003.

Murphi-- can do this completely automatically.

;;; The example appeared in:

;;; "Thread-modular Abstraction Refinement" by Thomas A. Henzinger, Ranjit
;;; Jhala, Rupak Majumdar, and Shaz Qadeer, CAV 2003.

;;; Total calls to CVC: 230
;;; Iterations: 4

;;; It would have been more interesting if it were not limited to 2 threads
;;; only. Then quantified predicates will be necessary and we can do that. I
;;; suspect TAR can't handle that.

(murphi-program

 (global-state (t1-pc rat)
               (t2-pc rat)
               (m rat)
               (x rat))

 (initialize
  (progn
    (setq t1-pc 1)
    (setq t2-pc 1)
    (setq m 0)))

 ;; Thread 1
 (rules
  ;; acquire(m)
  (==> (and (= t1-pc 1) (= m 0))
       (progn
         (setq m 1)
         (setq t1-pc 2)))

  ;; x=i
  (==> (= t1-pc 2)
       (progn
         (setq x 1)
         (setq t1-pc 3)))

  ;; release(m)
  (==> (= t1-pc 3)
       (progn
         (setq m 0)
         (setq t1-pc 1))))

 
 ;; Thread 2
 (rules
  ;; acquire(m)
  (==> (and (= t2-pc 1) (= m 0))
       (progn
         (setq m 2)
         (setq t2-pc 2)))

  ;; x=i
  (==> (= t2-pc 2)
       (progn
         (setq x 2)
         (setq t2-pc 3)))

  ;; release(m)
  (==> (= t2-pc 3)
       (progn
         (setq m 0)
         (setq t2-pc 1))))

 (invariant (not (and (= t1-pc 2) (= t2-pc 2))))

 (abstraction
  ;; Initial predicates
  (B0 (= t1-pc 2))
  (B1 (= t2-pc 2))

  ;; Iteration 1
  (B2 (NOT (= M 0)))

  ;; Iteration 2
  (B3 (NOT (= T1-PC 3)))

  ;; Iteration 3
  (B4 (NOT (= T2-PC 3)))))