theory Ricart_abdulla_int_defs

use import int.Int

type state = Idle | Wait | Use
type msg = Empty | Req | Ack | Ok

function timer : int
function timer' : int
function state int : state
function clock int : int
function last int : int
function channel_msg int int : msg
function channel_timestamp int int : int
function state' int : state
function clock' int : int
function last' int : int
function channel_msg' int int : msg
function channel_timestamp' int int : int

constant tick : int

end


theory Ricart_abdulla_int_invpreds

use import int.Int
use import Ricart_abdulla_int_defs

predicate invariantX127 =
not (exists z1 z2:int. z1 <> z2 /\ (state z2) = Idle /\
(channel_msg z2 z1) = Ack)

predicate invariantX127' =
not (exists z1 z2:int. z1 <> z2 /\ (state' z2) = Idle /\
(channel_msg' z2 z1) = Ack)

predicate invariantX111 =
not (exists z1 z2:int. z1 <> z2 /\ (state z2) = Use /\
(channel_msg z2 z1) = Ack)

predicate invariantX111' =
not (exists z1 z2:int. z1 <> z2 /\ (state' z2) = Use /\
(channel_msg' z2 z1) = Ack)

predicate invariantX95 =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg z2 z1) = Req /\
(channel_timestamp z2 z1) = (last z1))

predicate invariantX95' =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg' z2 z1) = Req /\
(channel_timestamp' z2 z1) = (last' z1))

predicate invariant50 =
not (exists z1 z2:int. z1 <> z2 /\ (state z1) = Wait /\
(channel_msg z1 z2) = Ok /\
(channel_msg z2 z1) = Req /\
(channel_timestamp z2 z1) < (last z1))

predicate invariant50' =
not (exists z1 z2:int. z1 <> z2 /\ (state' z1) = Wait /\
(channel_msg' z1 z2) = Ok /\
(channel_msg' z2 z1) = Req /\
(channel_timestamp' z2 z1) < (last' z1))

predicate invariant83 =
not (exists z1 z2:int. z1 <> z2 /\ (state z2) = Wait /\
(channel_msg z1 z2) = Req /\
(channel_msg z2 z1) = Ack /\
(channel_timestamp z1 z2) < (last z2))

predicate invariant83' =
not (exists z1 z2:int. z1 <> z2 /\ (state' z2) = Wait /\
(channel_msg' z1 z2) = Req /\
(channel_msg' z2 z1) = Ack /\
(channel_timestamp' z1 z2) < (last' z2))

predicate invariantX253 =
not (exists z1 z2:int. z1 <> z2 /\ (channel_timestamp z1 z2) < (last z2) /\
(channel_timestamp z2 z1) < (last z1))

predicate invariantX253' =
not (exists z1 z2:int. z1 <> z2 /\ (channel_timestamp' z1 z2) < (last' z2) /\
(channel_timestamp' z2 z1) < (last' z1))

predicate invariantX205 =
not (exists z1 z2:int. z1 <> z2 /\ (channel_timestamp z2 z1) = timer)

predicate invariantX205' =
not (exists z1 z2:int. z1 <> z2 /\ (channel_timestamp' z2 z1) = timer')

predicate invariantX44 =
not (exists z1 z2:int. z1 <> z2 /\ (state z1) = Idle /\
(channel_msg z1 z2) = Ok)

predicate invariantX44' =
not (exists z1 z2:int. z1 <> z2 /\ (state' z1) = Idle /\
(channel_msg' z1 z2) = Ok)

predicate invariantX171 =
not (exists z1:int. timer < (last z1))

predicate invariantX171' =
not (exists z1:int. timer' < (last' z1))

predicate invariantX9 =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg z1 z2) = Ok /\
(channel_msg z2 z1) = Ok)

predicate invariantX9' =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg' z1 z2) = Ok /\
(channel_msg' z2 z1) = Ok)

predicate invariantX214 =
not (exists z1 z2:int. z1 <> z2 /\ (state z2) = Use /\
(channel_msg z2 z1) = Req)

predicate invariantX214' =
not (exists z1 z2:int. z1 <> z2 /\ (state' z2) = Use /\
(channel_msg' z2 z1) = Req)

predicate invariantX21 =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg z1 z2) = Ok /\
(channel_msg z2 z1) = Ack)

predicate invariantX21' =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg' z1 z2) = Ok /\
(channel_msg' z2 z1) = Ack)

predicate invariantX35 =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg z1 z2) = Ack /\
(channel_msg z2 z1) = Ack)

predicate invariantX35' =
not (exists z1 z2:int. z1 <> z2 /\ (channel_msg' z1 z2) = Ack /\
(channel_msg' z2 z1) = Ack)

predicate invariantX195 =
not (exists z1:int. (last z1) = timer)

predicate invariantX195' =
not (exists z1:int. (last' z1) = timer')

predicate invariantX226 =
not (exists z1 z2:int. z1 <> z2 /\ (state z2) = Idle /\
(channel_msg z2 z1) = Req)

predicate invariantX226' =
not (exists z1 z2:int. z1 <> z2 /\ (state' z2) = Idle /\
(channel_msg' z2 z1) = Req)

predicate invariantX273 =
not (exists z1 z2:int. z1 <> z2 /\ timer < (channel_timestamp z2 z1))

predicate invariantX273' =
not (exists z1 z2:int. z1 <> z2 /\ timer' < (channel_timestamp' z2 z1))


end


theory Ricart_abdulla_int_trdefs

use import int.Int
use import Ricart_abdulla_int_defs

predicate transition__t6 =
(* transition t6 *)
(exists z s:int. z <> s /\ 
( (* requires *)
0 < tick /\
(state z) = Wait /\
(channel_msg s z) = Req /\
(channel_timestamp s z) < (last z)) /\
( (* actions *)
timer' = (timer+tick) /\
(forall _j17:int.
(if _j17 = z then
 (clock' _j17) = timer
else (clock' _j17) = (clock _j17))) /\
(forall _j18 _j19:int.
(if _j18 = s /\
_j19 = z then
 (channel_msg' _j18 _j19) = Ack
else (channel_msg' _j18 _j19) = (channel_msg _j18 _j19))) /\
(forall _j20 _j21:int.
(if _j20 = s /\
_j21 = z then
 (channel_timestamp' _j20 _j21) = timer
else (channel_timestamp' _j20 _j21) = (channel_timestamp _j20 _j21))) /\
(forall z1:int. state' z1 = state z1) /\
(forall z1:int. last' z1 = last z1) ))


predicate transition__t2 =
(* transition t2 *)
(exists z r:int. z <> r /\ 
( (* requires *)
0 < tick /\
(state z) = Wait /\
(channel_msg z r) = Ack) /\
( (* actions *)
timer' = (timer+tick) /\
(forall _j4:int.
(if _j4 = z then
 (clock' _j4) = timer
else (clock' _j4) = (clock _j4))) /\
(forall _j5 _j6:int.
(if _j5 = z /\
_j6 = r then
 (channel_msg' _j5 _j6) = Ok
else (channel_msg' _j5 _j6) = (channel_msg _j5 _j6))) /\
(forall _j7 _j8:int.
(if _j7 = z /\
_j8 = r then
 (channel_timestamp' _j7 _j8) = timer
else (channel_timestamp' _j7 _j8) = (channel_timestamp _j7 _j8))) /\
(forall z1:int. state' z1 = state z1) /\
(forall z1:int. last' z1 = last z1) ))


predicate transition__t1 =
(* transition t1 *)
(exists z:int. 
( (* requires *)
0 < tick /\
(state z) = Idle) /\
( (* actions *)
timer' = (timer+tick) /\
(forall _j1:int.
(if _j1 = z then
 (state' _j1) = Wait
else (state' _j1) = (state _j1))) /\
(forall _j2:int.
(if _j2 = z then
 (clock' _j2) = timer
else (clock' _j2) = (clock _j2))) /\
(forall _j3:int.
(if _j3 = z then
 (last' _j3) = timer
else (last' _j3) = (last _j3))) /\
(forall s r:int.
(if s = z /\
(channel_msg s r) = Empty then
 (channel_msg' s r) = Req
else (channel_msg' s r) = (channel_msg s r))) /\
(forall s r:int.
(if s = z /\
(channel_msg s r) = Empty then
 (channel_timestamp' s r) = timer
else (channel_timestamp' s r) = (channel_timestamp s r)))))


predicate transition__t7 =
(* transition t7 *)
(exists z s:int. z <> s /\ 
( (* requires *)
0 < tick /\
s < z /\
(state z) = Wait /\
(channel_msg s z) = Req /\
(channel_timestamp s z) = (last z)) /\
( (* actions *)
timer' = (timer+tick) /\
(forall _j22:int.
(if _j22 = z then
 (clock' _j22) = timer
else (clock' _j22) = (clock _j22))) /\
(forall _j23 _j24:int.
(if _j23 = s /\
_j24 = z then
 (channel_msg' _j23 _j24) = Ack
else (channel_msg' _j23 _j24) = (channel_msg _j23 _j24))) /\
(forall _j25 _j26:int.
(if _j25 = s /\
_j26 = z then
 (channel_timestamp' _j25 _j26) = timer
else (channel_timestamp' _j25 _j26) = (channel_timestamp _j25 _j26))) /\
(forall z1:int. state' z1 = state z1) /\
(forall z1:int. last' z1 = last z1) ))


predicate transition__t5 =
(* transition t5 *)
(exists z s:int. z <> s /\ 
( (* requires *)
0 < tick /\
(state z) = Idle /\
(channel_msg s z) = Req /\
(channel_timestamp s z) < (clock z)) /\
( (* actions *)
timer' = (timer+tick) /\
(forall _j12:int.
(if _j12 = z then
 (clock' _j12) = timer
else (clock' _j12) = (clock _j12))) /\
(forall _j13 _j14:int.
(if _j13 = s /\
_j14 = z then
 (channel_msg' _j13 _j14) = Ack
else (channel_msg' _j13 _j14) = (channel_msg _j13 _j14))) /\
(forall _j15 _j16:int.
(if _j15 = s /\
_j16 = z then
 (channel_timestamp' _j15 _j16) = timer
else (channel_timestamp' _j15 _j16) = (channel_timestamp _j15 _j16))) /\
(forall z1:int. state' z1 = state z1) /\
(forall z1:int. last' z1 = last z1) ))


predicate transition__t4 =
(* transition t4 *)
(exists z:int. 
( (* requires *)
0 < tick /\
(state z) = Use) /\
( (* actions *)
timer' = (timer+tick) /\
(forall _j10:int.
(if _j10 = z then
 (state' _j10) = Idle
else (state' _j10) = (state _j10))) /\
(forall _j11:int.
(if _j11 = z then
 (clock' _j11) = timer
else (clock' _j11) = (clock _j11))) /\
(forall s r:int.
(if s = z /\
(channel_msg s r) = Ok then
 (channel_msg' s r) = Empty
else (if r = z /\
(channel_msg s r) = Req then
 (channel_msg' s r) = Ack
else (channel_msg' s r) = (channel_msg s r)))) /\
(forall s r:int.
(if r = z /\
(channel_msg s r) = Req then
 (channel_timestamp' s r) = timer
else (channel_timestamp' s r) = (channel_timestamp s r))) /\
(forall z1:int. last' z1 = last z1) ))


predicate transition__t3 =
(* transition t3 *)
(exists z:int. 
( (* requires *)
(state z) = Wait
/\ (forall j:int.z = j \/ 
((channel_msg z j) = Ok))
) /\
( (* actions *)
timer' = timer /\
(forall _j9:int.
(if _j9 = z then
 (state' _j9) = Use
else (state' _j9) = (state _j9))) /\
(forall z1:int. clock' z1 = clock z1) /\
(forall z1:int. last' z1 = last z1) /\
(forall z1 z2:int. channel_msg' z1 z2 = channel_msg z1 z2) /\
(forall z1 z2:int. channel_timestamp' z1 z2 = channel_timestamp z1 z2) ))


predicate tau =
(transition__t3 \/ transition__t4 \/ transition__t5 \/ transition__t7 \/ transition__t1 \/ transition__t2 \/ transition__t6)


end


theory Ricart_abdulla_int_initialisation

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds

predicate init =
    forall z z1:int. (timer = 1 /\
(state z) = Idle /\
(clock z) = 0 /\
(last z) = 0 /\
(channel_msg z z1) = Empty /\
(channel_timestamp z z1) = 0)

goal initialisation:
    init -> (invariantX273 /\ invariantX226 /\ invariantX195 /\ invariantX35 /\ invariantX21 /\ invariantX214 /\ invariantX9 /\ invariantX171 /\ invariantX44 /\ invariantX205 /\ invariantX253 /\ invariant83 /\ invariant50 /\ invariantX95 /\ invariantX111 /\ invariantX127)


end


theory Ricart_abdulla_int_property

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds

goal property:
    (invariantX273 /\ invariantX226 /\ invariantX195 /\ invariantX35 /\ invariantX21 /\ invariantX214 /\ invariantX9 /\ invariantX171 /\ invariantX44 /\ invariantX205 /\ invariantX253 /\ invariant83 /\ invariant50 /\ invariantX95 /\ invariantX111 /\ invariantX127) -> (not (exists z1 z2:int. z1 <> z2 /\ (state z1) = Use /\
(state z2) = Use /\
(channel_msg z1 z2) = Ok /\
(channel_msg z2 z1) = Ok))


end


theory Ricart_abdulla_int_hint_1

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_1:
    (invariantX273 /\ tau)
    -> invariantX273'



end


theory Ricart_abdulla_int_hint_2

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_2:
    (invariantX253 /\ invariantX226 /\ invariantX171 /\ invariantX127 /\ invariantX44 /\ tau)
    -> invariantX253'



end


theory Ricart_abdulla_int_hint_3

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_3:
    (invariantX226 /\ invariantX214 /\ tau)
    -> invariantX226'



end


theory Ricart_abdulla_int_hint_4

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_4:
    (invariantX214 /\ tau)
    -> invariantX214'



end


theory Ricart_abdulla_int_hint_5

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_5:
    (invariantX273 /\ invariantX205 /\ tau)
    -> invariantX205'



end


theory Ricart_abdulla_int_hint_6

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_6:
    (invariantX195 /\ invariantX171 /\ tau)
    -> invariantX195'



end


theory Ricart_abdulla_int_hint_7

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_7:
    (invariantX171 /\ tau)
    -> invariantX171'



end


theory Ricart_abdulla_int_hint_8

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_8:
    (invariantX226 /\ invariantX127 /\ invariantX111 /\ invariantX95 /\ invariantX35 /\ invariantX21 /\ tau)
    -> invariantX127'



end


theory Ricart_abdulla_int_hint_9

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_9:
    (invariantX214 /\ invariantX111 /\ invariantX95 /\ invariantX35 /\ invariantX21 /\ tau)
    -> invariantX111'



end


theory Ricart_abdulla_int_hint_10

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_10:
    (invariantX205 /\ invariantX195 /\ invariantX95 /\ tau)
    -> invariantX95'



end


theory Ricart_abdulla_int_hint_11

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_11:
    (invariantX44 /\ invariantX21 /\ invariantX9 /\ tau)
    -> invariantX44'



end


theory Ricart_abdulla_int_hint_12

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_12:
    (invariantX127 /\ invariantX111 /\ invariantX95 /\ invariantX35 /\ invariant83 /\ tau)
    -> invariantX35'



end


theory Ricart_abdulla_int_hint_13

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_13:
    (invariantX95 /\ invariantX44 /\ invariantX35 /\ invariantX21 /\ invariant50 /\ tau)
    -> invariantX21'



end


theory Ricart_abdulla_int_hint_14

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_14:
    (invariantX21 /\ invariantX9 /\ tau)
    -> invariantX9'



end


theory Ricart_abdulla_int_hint_15

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_15:
    (invariantX226 /\ invariantX214 /\ invariantX171 /\ invariantX44 /\ invariant50 /\ invariant83 /\ tau)
    -> invariant50'



end


theory Ricart_abdulla_int_hint_16

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs

lemma hint_16:
    (invariantX253 /\ invariantX226 /\ invariantX214 /\ invariantX171 /\ invariantX127 /\ invariantX95 /\ invariant83 /\ tau)
    -> invariant83'



end


theory Ricart_abdulla_int_preservation

use import int.Int
use import Ricart_abdulla_int_defs
use import Ricart_abdulla_int_invpreds
use import Ricart_abdulla_int_trdefs
use import Ricart_abdulla_int_hint_16
use import Ricart_abdulla_int_hint_15
use import Ricart_abdulla_int_hint_14
use import Ricart_abdulla_int_hint_13
use import Ricart_abdulla_int_hint_12
use import Ricart_abdulla_int_hint_11
use import Ricart_abdulla_int_hint_10
use import Ricart_abdulla_int_hint_9
use import Ricart_abdulla_int_hint_8
use import Ricart_abdulla_int_hint_7
use import Ricart_abdulla_int_hint_6
use import Ricart_abdulla_int_hint_5
use import Ricart_abdulla_int_hint_4
use import Ricart_abdulla_int_hint_3
use import Ricart_abdulla_int_hint_2
use import Ricart_abdulla_int_hint_1

goal preservation:
    (invariantX273 /\ invariantX226 /\ invariantX195 /\ invariantX35 /\ invariantX21 /\ invariantX214 /\ invariantX9 /\ invariantX171 /\ invariantX44 /\ invariantX205 /\ invariantX253 /\ invariant83 /\ invariant50 /\ invariantX95 /\ invariantX111 /\ invariantX127 /\ tau)
    ->
    (invariantX273' /\ invariantX226' /\ invariantX195' /\ invariantX35' /\ invariantX21' /\ invariantX214' /\ invariantX9' /\ invariantX171' /\ invariantX44' /\ invariantX205' /\ invariantX253' /\ invariant83' /\ invariant50' /\ invariantX95' /\ invariantX111' /\ invariantX127')


end