Mux Ast Protocol

This problem has been used as an example in the paper "Automatic verification of parameterized networks of processes by abstraction" presented by Lessens and Saidi in ENTCS 97.

The abstraction is done by counting the number of processes at each program point. In our system we can not do this automatically. So the abstracted system has been computed by hand. Also the proof requires a linear invariant that could not be discovered automatically. In fact this predicate can not be discovered using from pre-images of the concrete counter-example.

However if that predicate is provided by the user then the remainder of the proof can be carried out automatically.

;;; Adapted from mux-ast example.
;;;
;;; The protocol is abstracted so that n1, n2, n3 ... are the number of
;;; processes in state 1, 2, 3 ... This abstraction is done manually since our
;;; method can't do this. Then we need to prove that n8<=1 to show that at most
;;; one process is in the critical section. Also our predicate discovery method
;;; couldn't find the invariant C31. So it has been added manually.
;;;

(murphi-program

 (global-state (y rat)
               (n1 rat)
               (n2 rat)
               (n3 rat)
               (n4 rat)
               (n5 rat)
               (n6 rat)
               (n7 rat)
               (n8 rat)
               (n9 rat)
               (n10 rat)
               (n11 rat)
               (n12 rat)
               (n13 rat)
               (n14 rat))

 (axiom (and (>= n1 0) (>= n2 0) (>= n3 0) (>= n4 0) (>= n5 0) (>= n6 0)
             (>= n7 0) (>= n8 0) (>= n9 0) (>= n1 10) (>= n11 0) (>= n12 0)
             (>= n13 0) (>= n14 0)))

 (initialize
  (progn
    (setq n2 0)
    (setq n3 0)
    (setq n4 0)
    (setq n5 0)
    (setq n6 0)
    (setq n7 0)
    (setq n8 0)
    (setq n9 0)
    (setq n10 0)
    (setq n11 0)
    (setq n12 0)
    (setq n13 0)
    (setq n14 0)
    (setq y 1)))

 (rules
  (==> (> n1 0)
       (progn
         (setq n1 (- n1 1))
         (setq n2 (+ n2 1))))

  (==> (and (> n2 0) (> y 0))
       (progn
         (setq n2 (- n2 1))
         (setq n3 (+ n3 1))))

  (==> (and (> n3 0) (> y 1))
       (progn
         (setq n3 (- n3 1))
         (setq n4 (+ n4 1))
         (setq y (- y 1))))

  (==> (and (> n3 0) (= y 1))
       (progn
         (setq n3 (- n3 1))
         (setq n5 (+ n5 1))
         (setq y (- y 1))))

  (==> (and (> n3 0) (< y 1))
       (progn
         (setq n3 (- n3 1))
         (setq n6 (+ n6 1))
         (setq y (- y 1))))

  (==> (> n4 0)
       (progn
         (setq n4 (- n4 1))
         (setq n12 (+ n12 1))))

  (==> (> n5 0)
       (progn
         (setq n5 (- n5 1))
         (setq n8 (+ n8 1))))

  (==> (> n6 0)
       (progn
         (setq n6 (- n6 1))
         (setq n7 (+ n7 1))))

  (==> (> n7 0)
       (progn
         (setq n7 (- n7 1))
         (setq n1 (+ n1 1))
         (setq y (+ y 1))))

  (==> (> n8 0)
       (progn
         (setq n8 (- n8 1))
         (setq n9 (+ n9 1))))

  (==> (> n9 0)
       (progn
         (setq n9 (- n9 1))
         (setq n10 (+ n10 1))
         (setq y (+ y 1))))

  (==> (> n10 0)
       (progn
         (setq n10 (- n10 1))
         (setq n11 (+ n11 1))))

  (==> (> n11 0)
       (progn
         (setq n11 (- n11 1))
         (setq n1 (+ n1 1))))

  (==> (> n12 0)
       (progn
         (setq n12 (- n12 1))
         (setq n13 (+ n13 1))
         (setq y (+ y 1))))

  (==> (> n13 0)
       (progn
         (setq n13 (- n13 1))
         (setq n14 (+ n14 1))))

  (==> (> n14 0)
       (progn
         (setq n14 (- n14 1))
         (setq n1 (+ n1 1)))))

 (invariant (<= n8 1))

 (abstraction

  ;; Initial predicates
  (B0 (<= n8 1))

  ;; Manual predicate
  (C31 (= (+ y n4 n5 n6 n7 n8 n9 n12) 1))

  ;; Automatically generated predicates

  ;; Iteration 1
  (C01 (< Y 0))

  ;; Iteration 2
  (C02 (NOT (= N8 0)))

  ;; Iteration 3
  (C03 (< (+ -1 (* 1 N8)) 0))
  (C04 (= Y 0))

  ;; Iteration 4
  (C05 (NOT (= (+ 0 (* -1 N12)) 0)))
  (C06 (< (+ 1 (* -1 N5)) 0))

  ;; Iteration 5
  (C07 (= (+ 1 (* -1 N5)) 0))
  (C08 (NOT (= (+ 0 (* -1 N9)) 0)))

  ;; Iteration 6
  (C09 (< (+ 0 (* -1 N5)) 0))
  (C10 (NOT (= (+ -1 (* 1 Y)) 0)))))