paulson@4776: (*  Title:      HOL/UNITY/Token
paulson@4776:     ID:         $Id$
paulson@4776:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776:     Copyright   1998  University of Cambridge
paulson@4776: 
paulson@4776: The Token Ring.
paulson@4776: 
paulson@4776: From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
paulson@4776: *)
paulson@4776: 
paulson@4776: 
paulson@5277: Token = WFair + 
paulson@4776: 
paulson@4776: (*process states*)
paulson@5232: datatype pstate = Hungry | Eating | Thinking
paulson@4776: 
paulson@5232: record state =
paulson@5232:   token :: nat
paulson@5232:   proc  :: nat => pstate
paulson@4776: 
paulson@4776: 
paulson@4776: constdefs
paulson@4776:   HasTok :: nat => state set
paulson@5232:     "HasTok i == {s. token s = i}"
paulson@4776: 
paulson@4776:   H :: nat => state set
paulson@5232:     "H i == {s. proc s i = Hungry}"
paulson@4776: 
paulson@4776:   E :: nat => state set
paulson@5232:     "E i == {s. proc s i = Eating}"
paulson@4776: 
paulson@4776:   T :: nat => state set
paulson@5232:     "T i == {s. proc s i = Thinking}"
paulson@4776: 
paulson@4776: 
paulson@5420: locale Token =
paulson@5420:   fixes
paulson@5420:     N         :: nat	 (*number of nodes in the ring*)
paulson@5420:     acts      :: "(state*state)set set"
paulson@5420:     nodeOrder :: "nat => (nat*nat)set"
paulson@5420:     next      :: nat => nat
paulson@4776: 
paulson@5420:   assumes
paulson@5420:     N_positive "0<N"
paulson@5420: 
paulson@5420:     skip "id: acts"
paulson@5420: 
paulson@5420:     TR2  "!!i. constrains acts (T i) (T i Un H i)"
paulson@4776: 
paulson@5420:     TR3  "!!i. constrains acts (H i) (H i Un E i)"
paulson@5420: 
paulson@5420:     TR4  "!!i. constrains acts (H i - HasTok i) (H i)"
paulson@4776: 
paulson@5420:     TR5  "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
paulson@5420: 
paulson@5420:     TR6  "!!i. leadsTo acts (H i Int HasTok i) (E i)"
paulson@4776: 
paulson@5420:     TR7  "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
paulson@4776: 
paulson@5420:   defines
paulson@5420:     nodeOrder_def
paulson@5420:       "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
paulson@5420: 		      (lessThan N Times lessThan N)"
paulson@4776: 
paulson@5420:     next_def
paulson@5420:       "next i == (Suc i) mod N"
paulson@4776: 
paulson@4776: end