(*
File: TLA/Inc/Inc.thy
ID: $Id$
Author: Stephan Merz
Copyright: 1997 University of Munich
Theory Name: Inc
Logic Image: TLA
*)
header {* Lamport's "increment" example *}
theory Inc
imports TLA
begin
(* program counter as an enumeration type *)
datatype pcount = a | b | g
consts
(* program variables *)
x :: "nat stfun"
y :: "nat stfun"
sem :: "nat stfun"
pc1 :: "pcount stfun"
pc2 :: "pcount stfun"
(* names of actions and predicates *)
M1 :: action
M2 :: action
N1 :: action
N2 :: action
alpha1 :: action
alpha2 :: action
beta1 :: action
beta2 :: action
gamma1 :: action
gamma2 :: action
InitPhi :: stpred
InitPsi :: stpred
PsiInv :: stpred
PsiInv1 :: stpred
PsiInv2 :: stpred
PsiInv3 :: stpred
(* temporal formulas *)
Phi :: temporal
Psi :: temporal
axioms
(* the "base" variables, required to compute enabledness predicates *)
Inc_base: "basevars (x, y, sem, pc1, pc2)"
(* definitions for high-level program *)
InitPhi_def: "InitPhi == PRED x = # 0 & y = # 0"
M1_def: "M1 == ACT x$ = Suc<$x> & y$ = $y"
M2_def: "M2 == ACT y$ = Suc<$y> & x$ = $x"
Phi_def: "Phi == TEMP Init InitPhi & [][M1 | M2]_(x,y)
& WF(M1)_(x,y) & WF(M2)_(x,y)"
(* definitions for low-level program *)
InitPsi_def: "InitPsi == PRED pc1 = #a & pc2 = #a
& x = # 0 & y = # 0 & sem = # 1"
alpha1_def: "alpha1 == ACT $pc1 = #a & pc1$ = #b & $sem = Suc<sem$>
& unchanged(x,y,pc2)"
alpha2_def: "alpha2 == ACT $pc2 = #a & pc2$ = #b & $sem = Suc<sem$>
& unchanged(x,y,pc1)"
beta1_def: "beta1 == ACT $pc1 = #b & pc1$ = #g & x$ = Suc<$x>
& unchanged(y,sem,pc2)"
beta2_def: "beta2 == ACT $pc2 = #b & pc2$ = #g & y$ = Suc<$y>
& unchanged(x,sem,pc1)"
gamma1_def: "gamma1 == ACT $pc1 = #g & pc1$ = #a & sem$ = Suc<$sem>
& unchanged(x,y,pc2)"
gamma2_def: "gamma2 == ACT $pc2 = #g & pc2$ = #a & sem$ = Suc<$sem>
& unchanged(x,y,pc1)"
N1_def: "N1 == ACT (alpha1 | beta1 | gamma1)"
N2_def: "N2 == ACT (alpha2 | beta2 | gamma2)"
Psi_def: "Psi == TEMP Init InitPsi
& [][N1 | N2]_(x,y,sem,pc1,pc2)
& SF(N1)_(x,y,sem,pc1,pc2)
& SF(N2)_(x,y,sem,pc1,pc2)"
PsiInv1_def: "PsiInv1 == PRED sem = # 1 & pc1 = #a & pc2 = #a"
PsiInv2_def: "PsiInv2 == PRED sem = # 0 & pc1 = #a & (pc2 = #b | pc2 = #g)"
PsiInv3_def: "PsiInv3 == PRED sem = # 0 & pc2 = #a & (pc1 = #b | pc1 = #g)"
PsiInv_def: "PsiInv == PRED (PsiInv1 | PsiInv2 | PsiInv3)"
ML {* use_legacy_bindings (the_context ()) *}
end