theory German_baukus_defs
use import bool.Bool
use import int.Int
type state = Invalid | Shared | Exclusive
type msg = Empty | Reqs | Reqe | Inv | Invack | Gnts | Gnte
function exgntd : bool
function curcmd : msg
function curClient : int
function exgntd' : bool
function curcmd' : msg
function curClient' : int
function chan1 int : msg
function chan2 int : msg
function chan3 int : msg
function cache int : state
function invset int : bool
function shrset int : bool
function chan1' int : msg
function chan2' int : msg
function chan3' int : msg
function cache' int : state
function invset' int : bool
function shrset' int : bool
end
theory German_baukus_invpreds
use import bool.Bool
use import int.Int
use import German_baukus_defs
predicate invariantX512 =
not (exists z1:int. (cache z1) <> Invalid /\
(shrset z1) = False)
predicate invariantX512' =
not (exists z1:int. (cache' z1) <> Invalid /\
(shrset' z1) = False)
predicate invariant1 =
not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(cache z2) <> Invalid)
predicate invariant1' =
not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(cache' z2) <> Invalid)
predicate invariantX186 =
not (exists z1:int. curcmd = Empty /\
(chan2 z1) = Inv)
predicate invariantX186' =
not (exists z1:int. curcmd' = Empty /\
(chan2' z1) = Inv)
predicate invariant456 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan3 z2) = Invack)
predicate invariant456' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan3' z2) = Invack)
predicate invariantX117 =
not (exists z1:int. (chan2 z1) = Inv /\
(chan3 z1) = Invack)
predicate invariantX117' =
not (exists z1:int. (chan2' z1) = Inv /\
(chan3' z1) = Invack)
predicate invariantX307 =
not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(invset z2) = True)
predicate invariantX307' =
not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(invset' z2) = True)
predicate invariant974 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z1) = Empty /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(cache z1) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant974' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z1) = Empty /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(cache' z1) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant910 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(invset z1) = True /\
(invset z2) = True)
predicate invariant910' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(invset' z1) = True /\
(invset' z2) = True)
predicate invariant528 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Empty /\
(chan3 z2) = Invack /\
(invset z1) = True)
predicate invariant528' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Empty /\
(chan3' z2) = Invack /\
(invset' z1) = True)
predicate invariant530 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan2 z1) = Inv /\
(chan2 z2) = Inv /\
(chan3 z2) = Empty)
predicate invariant530' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan2' z1) = Inv /\
(chan2' z2) = Inv /\
(chan3' z2) = Empty)
predicate invariantX238 =
not (exists z1 z2:int. z1 <> z2 /\ (chan3 z2) = Invack /\
(cache z1) = Exclusive)
predicate invariantX238' =
not (exists z1 z2:int. z1 <> z2 /\ (chan3' z2) = Invack /\
(cache' z1) = Exclusive)
predicate invariantX494 =
not (exists z1:int. (chan2 z1) = Gnts /\
(chan3 z1) = Invack)
predicate invariantX494' =
not (exists z1:int. (chan2' z1) = Gnts /\
(chan3' z1) = Invack)
predicate invariantX428 =
not (exists z1:int. (cache z1) = Exclusive /\
(shrset z1) = False)
predicate invariantX428' =
not (exists z1:int. (cache' z1) = Exclusive /\
(shrset' z1) = False)
predicate invariantX172 =
not (exists z1:int. curcmd = Empty /\
(chan3 z1) = Invack)
predicate invariantX172' =
not (exists z1:int. curcmd' = Empty /\
(chan3' z1) = Invack)
predicate invariant407 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan3 z1) = Invack /\
(chan3 z2) = Invack)
predicate invariant407' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan3' z1) = Invack /\
(chan3' z2) = Invack)
predicate invariant87 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Gnte)
predicate invariant87' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Gnte)
predicate invariantX40 =
not (exists z1:int. exgntd = False /\
(cache z1) = Exclusive)
predicate invariantX40' =
not (exists z1:int. exgntd' = False /\
(cache' z1) = Exclusive)
predicate invariant731 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Inv /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(invset z2) = True)
predicate invariant731' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Inv /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(invset' z2) = True)
predicate invariantX101 =
not (exists z1:int. (chan2 z1) = Inv /\
(shrset z1) = False)
predicate invariantX101' =
not (exists z1:int. (chan2' z1) = Inv /\
(shrset' z1) = False)
predicate invariant732 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Inv /\
(chan3 z2) = Empty /\
(invset z1) = True)
predicate invariant732' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Inv /\
(chan3' z2) = Empty /\
(invset' z1) = True)
predicate invariant28 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z2) = Gnts /\
(cache z1) = Exclusive)
predicate invariant28' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z2) = Gnts /\
(cache' z1) = Exclusive)
predicate invariant796 =
not (exists z1:int. (chan2 z1) = Gnte /\
(shrset z1) = False)
predicate invariant796' =
not (exists z1:int. (chan2' z1) = Gnte /\
(shrset' z1) = False)
predicate invariant30 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z2) = Gnte /\
(cache z1) = Exclusive)
predicate invariant30' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z2) = Gnte /\
(cache' z1) = Exclusive)
predicate invariant31 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(cache z2) <> Invalid)
predicate invariant31' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(cache' z2) <> Invalid)
predicate invariantX160 =
not (exists z1:int. (chan2 z1) = Inv /\
(invset z1) = True)
predicate invariantX160' =
not (exists z1:int. (chan2' z1) = Inv /\
(invset' z1) = True)
predicate invariant225 =
not (exists z1:int. (chan2 z1) = Gnte /\
(chan3 z1) = Invack)
predicate invariant225' =
not (exists z1:int. (chan2' z1) = Gnte /\
(chan3' z1) = Invack)
predicate invariantX285 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z2) = Inv /\
(cache z1) = Exclusive)
predicate invariantX285' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z2) = Inv /\
(cache' z1) = Exclusive)
predicate invariant422 =
not (exists z1 z2:int. z1 <> z2 /\ curcmd = Reqs /\
(chan2 z1) = Inv /\
(chan3 z2) = Invack)
predicate invariant422' =
not (exists z1 z2:int. z1 <> z2 /\ curcmd' = Reqs /\
(chan2' z1) = Inv /\
(chan3' z2) = Invack)
predicate invariantX217 =
not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan2 z1) = Inv)
predicate invariantX217' =
not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan2' z1) = Inv)
predicate invariantX88 =
not (exists z1:int. (chan3 z1) = Invack /\
(shrset z1) = False)
predicate invariantX88' =
not (exists z1:int. (chan3' z1) = Invack /\
(shrset' z1) = False)
predicate invariantX151 =
not (exists z1:int. (chan3 z1) = Invack /\
(invset z1) = True)
predicate invariantX151' =
not (exists z1:int. (chan3' z1) = Invack /\
(invset' z1) = True)
predicate invariant687 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(shrset z2) = True)
predicate invariant687' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(shrset' z2) = True)
predicate invariantX529 =
not (exists z1:int. (chan3 z1) = Invack /\
(cache z1) <> Invalid)
predicate invariantX529' =
not (exists z1:int. (chan3' z1) = Invack /\
(cache' z1) <> Invalid)
predicate invariantX465 =
not (exists z1:int. (chan2 z1) = Gnts /\
(shrset z1) = False)
predicate invariantX465' =
not (exists z1:int. (chan2' z1) = Gnts /\
(shrset' z1) = False)
predicate invariantX336 =
not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(shrset z2) = True)
predicate invariantX336' =
not (exists z1 z2:int. z1 <> z2 /\ (cache' z1) = Exclusive /\
(shrset' z2) = True)
predicate invariant625 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(invset z2) = True)
predicate invariant625' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(invset' z2) = True)
predicate invariantX399 =
not (exists z1:int. exgntd = True /\
(chan2 z1) = Gnts)
predicate invariantX399' =
not (exists z1:int. exgntd' = True /\
(chan2' z1) = Gnts)
predicate invariant946 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z2) = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant946' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z2) = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant947 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z1) = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant947' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z1) = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant1012 =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z3) = Empty /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(cache z3) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant1012' =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z3) = Empty /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(cache' z3) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant948 =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z3) = Reqs /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant948' =
not (exists z1 z2 z3:int. z2 <> z3 /\ z1 <> z3 /\ z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z3) = Reqs /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariant565 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Inv)
predicate invariant565' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Inv)
predicate invariantX199 =
not (exists z1:int. exgntd = False /\
curcmd = Reqs /\
(chan3 z1) = Invack)
predicate invariantX199' =
not (exists z1:int. exgntd' = False /\
curcmd' = Reqs /\
(chan3' z1) = Invack)
predicate invariantX134 =
not (exists z1:int. (invset z1) = True /\
(shrset z1) = False)
predicate invariantX134' =
not (exists z1:int. (invset' z1) = True /\
(shrset' z1) = False)
predicate invariant59 =
not (exists z1 z2:int. z1 <> z2 /\ (chan2 z1) = Gnte /\
(chan2 z2) = Gnts)
predicate invariant59' =
not (exists z1 z2:int. z1 <> z2 /\ (chan2' z1) = Gnte /\
(chan2' z2) = Gnts)
predicate invariant188 =
not (exists z1:int. exgntd = False /\
(chan2 z1) = Gnte)
predicate invariant188' =
not (exists z1:int. exgntd' = False /\
(chan2' z1) = Gnte)
predicate invariant958 =
not (exists z1 z2:int. z1 <> z2 /\ exgntd = True /\
curcmd = Empty /\
(chan1 z2) = Empty /\
(chan2 z1) = Empty /\
(chan2 z2) = Empty /\
(chan3 z2) = Empty /\
(cache z2) = Invalid /\
(shrset z1) = True /\
(shrset z2) = True)
predicate invariant958' =
not (exists z1 z2:int. z1 <> z2 /\ exgntd' = True /\
curcmd' = Empty /\
(chan1' z2) = Empty /\
(chan2' z1) = Empty /\
(chan2' z2) = Empty /\
(chan3' z2) = Empty /\
(cache' z2) = Invalid /\
(shrset' z1) = True /\
(shrset' z2) = True)
predicate invariantX65 =
not (exists z1:int. (chan3 z1) = Invack /\
(cache z1) = Exclusive)
predicate invariantX65' =
not (exists z1:int. (chan3' z1) = Invack /\
(cache' z1) = Exclusive)
end
theory German_baukus_trdefs
use import bool.Bool
use import int.Int
use import German_baukus_defs
predicate transition__send_invack =
(exists n:int.
(
(chan2 n) = Inv /\
(chan3 n) = Empty) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan2' j = Empty
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
chan3' j = Invack
else chan3' j = (chan3 j)) /\
(forall j:int.
if j = n then
cache' j = Invalid
else cache' j = (cache j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__send_req_shared =
(exists n:int.
(
(chan1 n) = Empty /\
(cache n) = Invalid) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan1' j = Reqs
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recv_gnt_exclusive =
(exists n:int.
(
(chan2 n) = Gnte) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
cache' j = Exclusive
else cache' j = (cache j)) /\
(forall j:int.
if j = n then
chan2' j = Empty
else chan2' j = (chan2 j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__send_gnt_exclusive =
(exists n:int.
(
curcmd = Reqe /\
curClient = n /\
(chan2 n) = Empty /\
(shrset n) = False
/\ (forall j:int.n = j \/
((shrset j) = False))
) /\
(
curcmd' = Empty /\
exgntd' = True /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan2' j = Gnte
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
shrset' j = True
else shrset' j = (shrset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) ))
predicate transition__send_req_exclusive_2 =
(exists n:int.
(
(chan1 n) = Empty /\
(cache n) = Shared) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan1' j = Reqe
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recv_req_exclusive =
(exists n:int.
(
curcmd = Empty /\
(chan1 n) = Reqe) /\
(
curcmd' = Reqe /\
curClient' = n /\
exgntd' = exgntd /\
(forall j:int.
invset' j = (shrset j)) /\
(forall j:int.
if j = n then
chan1' j = Empty
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recv_gnt_shared =
(exists n:int.
(
(chan2 n) = Gnts) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
cache' j = Shared
else cache' j = (cache j)) /\
(forall j:int.
if j = n then
chan2' j = Empty
else chan2' j = (chan2 j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__send_gnt_shared =
(exists n:int.
(
exgntd = False /\
curcmd = Reqs /\
curClient = n /\
(chan2 n) = Empty) /\
(
curcmd' = Empty /\
exgntd' = exgntd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan2' j = Gnts
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
shrset' j = True
else shrset' j = (shrset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) ))
predicate transition__recv_req_shared =
(exists n:int.
(
curcmd = Empty /\
(chan1 n) = Reqs) /\
(
curcmd' = Reqs /\
curClient' = n /\
exgntd' = exgntd /\
(forall j:int.
invset' j = (shrset j)) /\
(forall j:int.
if j = n then
chan1' j = Empty
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__recv_invack =
(exists n:int.
(
curcmd <> Empty /\
(chan3 n) = Invack) /\
(
exgntd' = False /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan3' j = Empty
else chan3' j = (chan3 j)) /\
(forall j:int.
if j = n then
shrset' j = False
else shrset' j = (shrset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) ))
predicate transition__send_inv_2 =
(exists n:int.
(
exgntd = True /\
curcmd = Reqs /\
(chan2 n) = Empty /\
(invset n) = True) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan2' j = Inv
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
invset' j = False
else invset' j = (invset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__send_inv_1 =
(exists n:int.
(
curcmd = Reqe /\
(chan2 n) = Empty /\
(invset n) = True) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan2' j = Inv
else chan2' j = (chan2 j)) /\
(forall j:int.
if j = n then
invset' j = False
else invset' j = (invset j)) /\
(forall z1:int. chan1' z1 = chan1 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate transition__send_req_exclusive_1 =
(exists n:int.
(
(chan1 n) = Empty /\
(cache n) = Invalid) /\
(
exgntd' = exgntd /\
curcmd' = curcmd /\
curClient' = curClient /\
(forall j:int.
if j = n then
chan1' j = Reqe
else chan1' j = (chan1 j)) /\
(forall z1:int. chan2' z1 = chan2 z1) /\
(forall z1:int. chan3' z1 = chan3 z1) /\
(forall z1:int. cache' z1 = cache z1) /\
(forall z1:int. invset' z1 = invset z1) /\
(forall z1:int. shrset' z1 = shrset z1) ))
predicate tau =
(transition__send_req_exclusive_1 \/ transition__send_inv_1 \/ transition__send_inv_2 \/ transition__recv_invack \/ transition__recv_req_shared \/ transition__send_gnt_shared \/ transition__recv_gnt_shared \/ transition__recv_req_exclusive \/ transition__send_req_exclusive_2 \/ transition__send_gnt_exclusive \/ transition__recv_gnt_exclusive \/ transition__send_req_shared \/ transition__send_invack)
end
theory German_baukus_initialisation
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
predicate init =
forall z:int. (exgntd = False /\
curcmd = Empty /\
(chan1 z) = Empty /\
(chan2 z) = Empty /\
(chan3 z) = Empty /\
(cache z) = Invalid /\
(invset z) = False /\
(shrset z) = False)
goal initialisation:
init -> (invariantX65 /\ invariant958 /\ invariant188 /\ invariant59 /\ invariantX134 /\ invariantX199 /\ invariant565 /\ invariant948 /\ invariant1012 /\ invariant947 /\ invariant946 /\ invariantX399 /\ invariant625 /\ invariantX336 /\ invariantX465 /\ invariantX529 /\ invariant687 /\ invariantX151 /\ invariantX88 /\ invariantX217 /\ invariant422 /\ invariantX285 /\ invariant225 /\ invariantX160 /\ invariant31 /\ invariant30 /\ invariant796 /\ invariant28 /\ invariant732 /\ invariantX101 /\ invariant731 /\ invariantX40 /\ invariant87 /\ invariant407 /\ invariantX172 /\ invariantX428 /\ invariantX494 /\ invariantX238 /\ invariant530 /\ invariant528 /\ invariant910 /\ invariant974 /\ invariantX307 /\ invariantX117 /\ invariant456 /\ invariantX186 /\ invariant1 /\ invariantX512)
end
theory German_baukus_property
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
goal property:
(invariantX65 /\ invariant958 /\ invariant188 /\ invariant59 /\ invariantX134 /\ invariantX199 /\ invariant565 /\ invariant948 /\ invariant1012 /\ invariant947 /\ invariant946 /\ invariantX399 /\ invariant625 /\ invariantX336 /\ invariantX465 /\ invariantX529 /\ invariant687 /\ invariantX151 /\ invariantX88 /\ invariantX217 /\ invariant422 /\ invariantX285 /\ invariant225 /\ invariantX160 /\ invariant31 /\ invariant30 /\ invariant796 /\ invariant28 /\ invariant732 /\ invariantX101 /\ invariant731 /\ invariantX40 /\ invariant87 /\ invariant407 /\ invariantX172 /\ invariantX428 /\ invariantX494 /\ invariantX238 /\ invariant530 /\ invariant528 /\ invariant910 /\ invariant974 /\ invariantX307 /\ invariantX117 /\ invariant456 /\ invariantX186 /\ invariant1 /\ invariantX512) -> (not (exists z1 z2:int. z1 <> z2 /\ (cache z1) = Exclusive /\
(cache z2) <> Invalid))
end
theory German_baukus_hint_1
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_1:
(invariantX529 /\ invariantX494 /\ invariantX172 /\ invariantX151 /\ invariantX88 /\ invariant225 /\ tau)
-> invariantX529'
end
theory German_baukus_hint_2
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_2:
(invariantX529 /\ invariantX512 /\ invariantX465 /\ invariantX134 /\ invariant796 /\ tau)
-> invariantX512'
end
theory German_baukus_hint_3
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_3:
(invariantX494 /\ invariantX399 /\ invariantX199 /\ invariantX172 /\ invariantX88 /\ tau)
-> invariantX494'
end
theory German_baukus_hint_4
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_4:
(invariantX494 /\ invariantX465 /\ invariantX399 /\ tau)
-> invariantX465'
end
theory German_baukus_hint_5
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_5:
(invariantX428 /\ invariantX134 /\ invariantX65 /\ invariantX40 /\ invariant796 /\ tau)
-> invariantX428'
end
theory German_baukus_hint_6
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_6:
(invariantX465 /\ invariantX399 /\ tau)
-> invariantX399'
end
theory German_baukus_hint_7
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_7:
(invariantX428 /\ invariantX336 /\ invariantX307 /\ invariantX285 /\ invariantX65 /\ invariantX40 /\ invariant687 /\ tau)
-> invariantX336'
end
theory German_baukus_hint_8
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_8:
(invariantX428 /\ invariantX336 /\ invariantX307 /\ invariantX285 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant625 /\ tau)
-> invariantX307'
end
theory German_baukus_hint_9
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_9:
(invariantX428 /\ invariantX307 /\ invariantX285 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant565 /\ tau)
-> invariantX285'
end
theory German_baukus_hint_10
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_10:
(invariantX428 /\ invariantX285 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant456 /\ tau)
-> invariantX238'
end
theory German_baukus_hint_11
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_11:
(invariantX217 /\ invariantX186 /\ invariantX117 /\ invariant422 /\ tau)
-> invariantX217'
end
theory German_baukus_hint_12
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_12:
(invariantX529 /\ invariantX494 /\ invariantX217 /\ invariantX199 /\ invariantX172 /\ invariant188 /\ invariant407 /\ tau)
-> invariantX199'
end
theory German_baukus_hint_13
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_13:
(invariantX217 /\ invariantX186 /\ invariantX101 /\ tau)
-> invariantX186'
end
theory German_baukus_hint_14
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_14:
(invariantX199 /\ invariantX186 /\ invariantX172 /\ invariantX88 /\ tau)
-> invariantX172'
end
theory German_baukus_hint_15
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_15:
(invariantX186 /\ invariantX160 /\ invariantX117 /\ invariantX101 /\ tau)
-> invariantX160'
end
theory German_baukus_hint_16
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_16:
(invariantX172 /\ invariantX160 /\ invariantX151 /\ invariantX88 /\ tau)
-> invariantX151'
end
theory German_baukus_hint_17
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_17:
(invariantX151 /\ invariantX134 /\ invariantX101 /\ tau)
-> invariantX134'
end
theory German_baukus_hint_18
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_18:
(invariantX151 /\ invariantX117 /\ invariantX88 /\ tau)
-> invariantX117'
end
theory German_baukus_hint_19
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_19:
(invariantX134 /\ invariantX117 /\ invariantX101 /\ tau)
-> invariantX101'
end
theory German_baukus_hint_20
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_20:
(invariantX101 /\ invariantX88 /\ tau)
-> invariantX88'
end
theory German_baukus_hint_21
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_21:
(invariantX65 /\ invariantX40 /\ invariant225 /\ tau)
-> invariantX65'
end
theory German_baukus_hint_22
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_22:
(invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant188 /\ tau)
-> invariantX40'
end
theory German_baukus_hint_23
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_23:
(invariantX428 /\ invariantX307 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant1 /\ invariant28 /\ invariant30 /\ invariant31 /\ tau)
-> invariant1'
end
theory German_baukus_hint_24
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_24:
(invariantX428 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant1 /\ invariant28 /\ invariant59 /\ tau)
-> invariant28'
end
theory German_baukus_hint_25
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_25:
(invariantX428 /\ invariantX238 /\ invariantX65 /\ invariantX40 /\ invariant1 /\ invariant30 /\ invariant87 /\ tau)
-> invariant30'
end
theory German_baukus_hint_26
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_26:
(invariantX512 /\ invariant31 /\ invariant59 /\ invariant87 /\ invariant188 /\ invariant225 /\ invariant796 /\ tau)
-> invariant31'
end
theory German_baukus_hint_27
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_27:
(invariantX465 /\ invariant31 /\ invariant59 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant796 /\ tau)
-> invariant59'
end
theory German_baukus_hint_28
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_28:
(invariant31 /\ invariant87 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant796 /\ tau)
-> invariant87'
end
theory German_baukus_hint_29
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_29:
(invariant188 /\ invariant225 /\ invariant456 /\ tau)
-> invariant188'
end
theory German_baukus_hint_30
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_30:
(invariantX529 /\ invariantX172 /\ invariantX88 /\ invariant188 /\ invariant225 /\ tau)
-> invariant225'
end
theory German_baukus_hint_31
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_31:
(invariantX529 /\ invariantX494 /\ invariantX172 /\ invariantX151 /\ invariant225 /\ invariant407 /\ invariant422 /\ tau)
-> invariant407'
end
theory German_baukus_hint_32
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_32:
(invariantX186 /\ invariantX117 /\ invariant422 /\ invariant528 /\ invariant530 /\ tau)
-> invariant422'
end
theory German_baukus_hint_33
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_33:
(invariantX88 /\ invariant31 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant565 /\ invariant796 /\ tau)
-> invariant456'
end
theory German_baukus_hint_34
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_34:
(invariantX399 /\ invariantX172 /\ invariantX160 /\ invariant456 /\ invariant528 /\ invariant732 /\ tau)
-> invariant528'
end
theory German_baukus_hint_35
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_35:
(invariantX186 /\ invariantX117 /\ invariant422 /\ invariant530 /\ invariant731 /\ invariant732 /\ tau)
-> invariant530'
end
theory German_baukus_hint_36
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_36:
(invariantX101 /\ invariant31 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant565 /\ invariant625 /\ invariant796 /\ tau)
-> invariant565'
end
theory German_baukus_hint_37
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_37:
(invariantX134 /\ invariant31 /\ invariant188 /\ invariant225 /\ invariant456 /\ invariant565 /\ invariant625 /\ invariant687 /\ invariant796 /\ tau)
-> invariant625'
end
theory German_baukus_hint_38
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_38:
(invariant31 /\ invariant188 /\ invariant225 /\ invariant565 /\ invariant625 /\ invariant687 /\ invariant796 /\ tau)
-> invariant687'
end
theory German_baukus_hint_39
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_39:
(invariantX399 /\ invariantX186 /\ invariant565 /\ invariant731 /\ invariant910 /\ tau)
-> invariant731'
end
theory German_baukus_hint_40
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_40:
(invariantX399 /\ invariantX186 /\ invariantX160 /\ invariant565 /\ invariant732 /\ invariant910 /\ tau)
-> invariant732'
end
theory German_baukus_hint_41
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_41:
(invariantX512 /\ invariant188 /\ invariant225 /\ invariant796 /\ tau)
-> invariant796'
end
theory German_baukus_hint_42
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_42:
(invariantX399 /\ invariantX160 /\ invariant625 /\ invariant910 /\ invariant946 /\ invariant947 /\ invariant948 /\ tau)
-> invariant910'
end
theory German_baukus_hint_43
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_43:
(invariantX399 /\ invariantX186 /\ invariant687 /\ invariant946 /\ invariant958 /\ tau)
-> invariant946'
end
theory German_baukus_hint_44
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_44:
(invariantX399 /\ invariantX186 /\ invariant687 /\ invariant947 /\ invariant974 /\ tau)
-> invariant947'
end
theory German_baukus_hint_45
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_45:
(invariantX399 /\ invariantX186 /\ invariant687 /\ invariant948 /\ invariant958 /\ invariant974 /\ invariant1012 /\ tau)
-> invariant948'
end
theory German_baukus_hint_46
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_46:
(invariantX399 /\ invariantX186 /\ invariant687 /\ invariant958 /\ tau)
-> invariant958'
end
theory German_baukus_hint_47
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_47:
(invariantX399 /\ invariantX186 /\ invariant687 /\ invariant958 /\ invariant974 /\ tau)
-> invariant974'
end
theory German_baukus_hint_48
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
lemma hint_48:
(invariantX399 /\ invariantX186 /\ invariant687 /\ invariant958 /\ invariant974 /\ invariant1012 /\ tau)
-> invariant1012'
end
theory German_baukus_preservation
use import bool.Bool
use import int.Int
use import German_baukus_defs
use import German_baukus_invpreds
use import German_baukus_trdefs
use import German_baukus_hint_48
use import German_baukus_hint_47
use import German_baukus_hint_46
use import German_baukus_hint_45
use import German_baukus_hint_44
use import German_baukus_hint_43
use import German_baukus_hint_42
use import German_baukus_hint_41
use import German_baukus_hint_40
use import German_baukus_hint_39
use import German_baukus_hint_38
use import German_baukus_hint_37
use import German_baukus_hint_36
use import German_baukus_hint_35
use import German_baukus_hint_34
use import German_baukus_hint_33
use import German_baukus_hint_32
use import German_baukus_hint_31
use import German_baukus_hint_30
use import German_baukus_hint_29
use import German_baukus_hint_28
use import German_baukus_hint_27
use import German_baukus_hint_26
use import German_baukus_hint_25
use import German_baukus_hint_24
use import German_baukus_hint_23
use import German_baukus_hint_22
use import German_baukus_hint_21
use import German_baukus_hint_20
use import German_baukus_hint_19
use import German_baukus_hint_18
use import German_baukus_hint_17
use import German_baukus_hint_16
use import German_baukus_hint_15
use import German_baukus_hint_14
use import German_baukus_hint_13
use import German_baukus_hint_12
use import German_baukus_hint_11
use import German_baukus_hint_10
use import German_baukus_hint_9
use import German_baukus_hint_8
use import German_baukus_hint_7
use import German_baukus_hint_6
use import German_baukus_hint_5
use import German_baukus_hint_4
use import German_baukus_hint_3
use import German_baukus_hint_2
use import German_baukus_hint_1
goal preservation:
(invariantX65 /\ invariant958 /\ invariant188 /\ invariant59 /\ invariantX134 /\ invariantX199 /\ invariant565 /\ invariant948 /\ invariant1012 /\ invariant947 /\ invariant946 /\ invariantX399 /\ invariant625 /\ invariantX336 /\ invariantX465 /\ invariantX529 /\ invariant687 /\ invariantX151 /\ invariantX88 /\ invariantX217 /\ invariant422 /\ invariantX285 /\ invariant225 /\ invariantX160 /\ invariant31 /\ invariant30 /\ invariant796 /\ invariant28 /\ invariant732 /\ invariantX101 /\ invariant731 /\ invariantX40 /\ invariant87 /\ invariant407 /\ invariantX172 /\ invariantX428 /\ invariantX494 /\ invariantX238 /\ invariant530 /\ invariant528 /\ invariant910 /\ invariant974 /\ invariantX307 /\ invariantX117 /\ invariant456 /\ invariantX186 /\ invariant1 /\ invariantX512 /\ tau)
->
(invariantX65' /\ invariant958' /\ invariant188' /\ invariant59' /\ invariantX134' /\ invariantX199' /\ invariant565' /\ invariant948' /\ invariant1012' /\ invariant947' /\ invariant946' /\ invariantX399' /\ invariant625' /\ invariantX336' /\ invariantX465' /\ invariantX529' /\ invariant687' /\ invariantX151' /\ invariantX88' /\ invariantX217' /\ invariant422' /\ invariantX285' /\ invariant225' /\ invariantX160' /\ invariant31' /\ invariant30' /\ invariant796' /\ invariant28' /\ invariant732' /\ invariantX101' /\ invariant731' /\ invariantX40' /\ invariant87' /\ invariant407' /\ invariantX172' /\ invariantX428' /\ invariantX494' /\ invariantX238' /\ invariant530' /\ invariant528' /\ invariant910' /\ invariant974' /\ invariantX307' /\ invariantX117' /\ invariant456' /\ invariantX186' /\ invariant1' /\ invariantX512')
end