src/HOL/UNITY/Handshake.thy

use HOLogic.Not;
export indexify_names;

(*  Title:      HOL/UNITY/Handshake.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Handshake Protocol

From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
*)

Handshake = Union +

record state =
  BB :: bool
  NF :: nat
  NG :: nat

constdefs
  (*F's program*)
  cmdF :: "(state*state) set"
    "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"

  F :: "state program"
    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"

  (*G's program*)
  cmdG :: "(state*state) set"
    "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"

  G :: "state program"
    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"

  (*the joint invariant*)
  invFG :: "state set"
    "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"

end