author | paulson |
Fri, 12 May 2000 15:05:02 +0200 | |
changeset 8862 | 78643f8449c6 |
parent 5111 | 8f4b72f0c15d |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/Network ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge The Communication Network From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 *) Network = UNITY + (*The state assigns a number to each process variable*) datatype pvar = Sent | Rcvd | Idle datatype pname = Aproc | Bproc types state = "pname * pvar => nat" end