src/HOL/UNITY/Token.thy
author paulson
Tue Sep 01 15:07:11 1998 +0200 (1998-09-01)
changeset 5420 b48ab3281944
parent 5277 e4297d03e5d2
child 5608 a82a038a3e7a
permissions -rw-r--r--
New approach, using a locale
paulson@4776
     1
(*  Title:      HOL/UNITY/Token
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
The Token Ring.
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
paulson@4776
     9
*)
paulson@4776
    10
paulson@4776
    11
paulson@5277
    12
Token = WFair + 
paulson@4776
    13
paulson@4776
    14
(*process states*)
paulson@5232
    15
datatype pstate = Hungry | Eating | Thinking
paulson@4776
    16
paulson@5232
    17
record state =
paulson@5232
    18
  token :: nat
paulson@5232
    19
  proc  :: nat => pstate
paulson@4776
    20
paulson@4776
    21
paulson@4776
    22
constdefs
paulson@4776
    23
  HasTok :: nat => state set
paulson@5232
    24
    "HasTok i == {s. token s = i}"
paulson@4776
    25
paulson@4776
    26
  H :: nat => state set
paulson@5232
    27
    "H i == {s. proc s i = Hungry}"
paulson@4776
    28
paulson@4776
    29
  E :: nat => state set
paulson@5232
    30
    "E i == {s. proc s i = Eating}"
paulson@4776
    31
paulson@4776
    32
  T :: nat => state set
paulson@5232
    33
    "T i == {s. proc s i = Thinking}"
paulson@4776
    34
paulson@4776
    35
paulson@5420
    36
locale Token =
paulson@5420
    37
  fixes
paulson@5420
    38
    N         :: nat	 (*number of nodes in the ring*)
paulson@5420
    39
    acts      :: "(state*state)set set"
paulson@5420
    40
    nodeOrder :: "nat => (nat*nat)set"
paulson@5420
    41
    next      :: nat => nat
paulson@4776
    42
paulson@5420
    43
  assumes
paulson@5420
    44
    N_positive "0<N"
paulson@5420
    45
paulson@5420
    46
    skip "id: acts"
paulson@5420
    47
paulson@5420
    48
    TR2  "!!i. constrains acts (T i) (T i Un H i)"
paulson@4776
    49
paulson@5420
    50
    TR3  "!!i. constrains acts (H i) (H i Un E i)"
paulson@5420
    51
paulson@5420
    52
    TR4  "!!i. constrains acts (H i - HasTok i) (H i)"
paulson@4776
    53
paulson@5420
    54
    TR5  "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
paulson@5420
    55
paulson@5420
    56
    TR6  "!!i. leadsTo acts (H i Int HasTok i) (E i)"
paulson@4776
    57
paulson@5420
    58
    TR7  "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
paulson@4776
    59
paulson@5420
    60
  defines
paulson@5420
    61
    nodeOrder_def
paulson@5420
    62
      "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
paulson@5420
    63
		      (lessThan N Times lessThan N)"
paulson@4776
    64
paulson@5420
    65
    next_def
paulson@5420
    66
      "next i == (Suc i) mod N"
paulson@4776
    67
paulson@4776
    68
end