author | berghofe |
Fri, 23 Oct 1998 22:36:15 +0200 | |
changeset 5760 | 7e2cf2820684 |
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