theory Bakery_defs

use import int.Int

type t = Idle | Wait | Crit | Crash

function a int : t
function a' int : t

end


theory Bakery_invpreds

use import int.Int
use import Bakery_defs

predicate invariant1 =
not (exists z1 z2:int. z1 <> z2 /\ (a z1) = Crit /\
(a z2) = Crit)

predicate invariant1' =
not (exists z1 z2:int. z1 <> z2 /\ (a' z1) = Crit /\
(a' z2) = Crit)

predicate invariant3 =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a z1) = Crit /\
(a z2) = Wait)

predicate invariant3' =
not (exists z1 z2:int. z1 <> z2 /\ z2 < z1 /\
(a' z1) = Crit /\
(a' z2) = Wait)


end


theory Bakery_trdefs

use import int.Int
use import Bakery_defs

predicate transition__tr3 =
(* transition tr3 *)
(exists z:int. 
( (* requires *)
(a z) = Crit) /\
( (* actions *)
(forall j:int.
if j = z then
 a' j = Idle
else a' j = (a j))))


predicate transition__tr2 =
(* transition tr2 *)
(exists z:int. 
( (* requires *)
(a z) = Wait) /\
( (* actions *)
(forall j:int.
if j = z then
 a' j = Crit
else if z < j then
 a' j = (a j)
else if j < z /\
(a j) = Idle then
 a' j = Idle
else a' j = Crash)))


predicate transition__tr1 =
(* transition tr1 *)
(exists z:int. 
( (* requires *)
(a z) = Idle) /\
( (* actions *)
(forall j:int.
if j = z then
 a' j = Wait
else if j < z then
 a' j = (a j)
else if z < j /\
(a j) = Idle then
 a' j = (a j)
else a' j = Crash)))


predicate tau =
(transition__tr1 \/ transition__tr2 \/ transition__tr3)


end


theory Bakery_initialisation

use import int.Int
use import Bakery_defs
use import Bakery_invpreds

predicate init =
    forall z:int. ((a z) = Idle)

goal initialisation:
    init -> (invariant3 /\ invariant1)


end


theory Bakery_property

use import int.Int
use import Bakery_defs
use import Bakery_invpreds

goal property:
    (invariant3 /\ invariant1) -> (not (exists z1 z2:int. z1 <> z2 /\ (a z1) = Crit /\
(a z2) = Crit))


end


theory Bakery_hint_1

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs

lemma hint_1:
    (invariant1 /\ invariant3 /\ tau)
    -> invariant1'



end


theory Bakery_hint_2

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs

lemma hint_2:
    (invariant3 /\ tau)
    -> invariant3'



end


theory Bakery_preservation

use import int.Int
use import Bakery_defs
use import Bakery_invpreds
use import Bakery_trdefs
use import Bakery_hint_2
use import Bakery_hint_1

goal preservation:
    (invariant3 /\ invariant1 /\ tau)
    ->
    (invariant3' /\ invariant1')


end