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 =
(exists z s:int. z <> s /\
(
0 < tick /\
(state z) = Wait /\
(channel_msg s z) = Req /\
(channel_timestamp s z) < (last z)) /\
(
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 =
(exists z r:int. z <> r /\
(
0 < tick /\
(state z) = Wait /\
(channel_msg z r) = Ack) /\
(
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 =
(exists z:int.
(
0 < tick /\
(state z) = Idle) /\
(
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 =
(exists z s:int. z <> s /\
(
0 < tick /\
s < z /\
(state z) = Wait /\
(channel_msg s z) = Req /\
(channel_timestamp s z) = (last z)) /\
(
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 =
(exists z s:int. z <> s /\
(
0 < tick /\
(state z) = Idle /\
(channel_msg s z) = Req /\
(channel_timestamp s z) < (clock z)) /\
(
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 =
(exists z:int.
(
0 < tick /\
(state z) = Use) /\
(
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 =
(exists z:int.
(
(state z) = Wait
/\ (forall j:int.z = j \/
((channel_msg z j) = Ok))
) /\
(
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