equal
deleted
inserted
replaced
|
1 (* Title: HOL/UNITY/Network |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 The Communication Network |
|
7 |
|
8 From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 |
|
9 *) |
|
10 |
|
11 Network = UNITY + |
|
12 |
|
13 (*The state assigns a number to each process variable*) |
|
14 |
|
15 datatype pvar = Sent | Rcvd | Idle |
|
16 |
|
17 datatype pname = Aproc | Bproc |
|
18 |
|
19 types state = "pname * pvar => nat" |
|
20 |
|
21 end |