Logical Encodings

eq < DeviceY | 'pressed' : false , ... > $ UserX 'pressButton' DeviceY

= < DeviceY | 'pressed' : true , ... > .

eq < DeviceY | 'pressed' : true , 'key' : nils , ... > $ UserX 'callAPI:setKey' DeviceY | KeyA

= < DeviceY | 'pressed' : false , 'key' : KeyA , ... > $ DeviceY 'callAPI:setKey' cloudA | KeyA .

eq < DeviceY | 'pressed' : true , 'key' : KeyB , ... > $ UserX 'callAPI:setKey' DeviceY | KeyA

= < DeviceY | 'pressed' : false , 'key' : KeyA , ... > $ DeviceY 'callAPI:setKey' cloudA | KeyA .

eq < cloudA | DeviceY : ('bdKey' : KeyB , 'owner' : OwnerX , ... ) , ... > $ DeviceY 'callAPI:setKey' cloudA | KeyA

= < cloudA | DeviceY : ('bdKey' : KeyA , 'owner' : OwnerX , ... ) , ... > .

eq < cloudA | DeviceY : ('bdKey' : KeyA , 'owner' : nils , ... ) , ... > $ UserX 'callAPI:bind' cloudA | DeviceY ; KeyA

= < cloudA | DeviceY : ('bdKey' : KeyA , 'owner' : UserX , ... ) , ... > .

eq < DeviceY | 'pressed' : true , 'key' : KeyA , ... > $ UserX 'callAPI:getKey' DeviceY

= < DeviceY | 'pressed' : false , 'key' : KeyA , ... > $ DeviceY 'sendKey' UserX | KeyA .

eq < UserX | 'key' : KeyB , ... > $ DeviceY 'sendKey' UserX | KeyA

= < UserX | 'key' : KeyA , ... > .

eq < cloudA | DeviceY : ('bdKey' : KeyA , 'owner' : OwnerX , ... ) , ... > $ UserX 'callAPI:reset' cloudA | DeviceY ; KeyA

= < cloudA | DeviceY : ('bdKey' : nils , 'owner' : nils , ... ) , ... > .

eq < UserX | 'localTo' : nils , ... > $ UserX 'approach' DeviceY

= < UserX | 'localTo' : DeviceY , ... > .

eq < UserX | 'localTo' : DeviceY , ... > $ UserX 'leave' DeviceY

= < UserX | 'localTo' : nils , ... > .

ev1(UserX,DeviceY) = $ UserX 'approach' DeviceY .

ev2(UserX,DeviceY) = $ UserX 'leave' DeviceY .

ev3(UserX,DeviceY) = $ UserX 'pressButton' DeviceY .

ev4(UserX,DeviceY,KeyA) = $ UserX 'callAPI:setKey' DeviceY | (KeyA) .

ev5(UserX,DeviceY) = $ UserX 'callAPI:getKey' DeviceY .

ev6(UserX,DeviceY,KeyA) = $ UserX 'callAPI:bind' cloudA | ((DeviceY) ; KeyA) .

ev7(UserX,DeviceY,KeyA) = $ UserX 'callAPI:reset' cloudA | ((DeviceY) ; KeyA) .

rl < UserX | 'localTo' : DeviceY , ... > < DeviceY | ... > -> ev3(UserX, DeviceY) .

rl < UserX | 'localTo' : DeviceY , ... > < DeviceY | ... > -> ev5(UserX, DeviceY) .

rl < UserX | 'localTo' : DeviceY , 'key' : KeyA , ... > < DeviceY | ... > -> ev4(UserX, DeviceY, KeyA) .

rl < UserX | 'localTo' : DeviceY , ... > < DeviceY | ... > -> ev2(UserX, DeviceY) .

rl < UserX | 'localTo' : nils , ... > < DeviceY | ... > -> ev1(UserX, DeviceY) .

rl < UserX | 'key' : KeyA , ... > < cloudA | DeviceY : ( ... ) ,... > -> ev6(UserX, DeviceY, KeyA) .

rl < UserX | 'key' : KeyA , ... > < cloudA | DeviceY : ( ... ) ,... > -> ev7(UserX, DeviceY, KeyA) .

eq < DeviceX | ... > $ UserA 'press' DeviceX

= < DeviceX | ... > $ DeviceX 'callAPI:setKey' cloudA | FreshKeyA .

eq < cloudA | DeviceX : ('ticket' : Tickets , 'owner' : OwnerX , ...) , ... > $ DeviceX 'callAPI:setKey' cloudA | KeyA

= < cloudA | DeviceX : ('ticket' : (('key' : KeyA , 'time' : CurrentTime), Tickets) , 'owner' : OwnerX , ...) , ... > .

ceq < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , ...) , ... > $ UserA 'callAPI:getKey' cloudA | DeviceX

= < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , ...) , ... > $ cloudA 'sendKey' UserA | KeyA

if CurrentTime < TimeA + 1 .

ceq < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , 'owner' : nils , ...) , ... > $ UserA 'callAPI:bind' cloudA | (DeviceX ; KeyA)

= < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , 'owner' : UserA , ...) , ... >

if CurrentTime < TimeA + 1 .

ceq < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , 'owner' : OwnerX , ...) , UserB : ('uid' : UidB , ...) , ... > $ UserA 'callAPI:bind' cloudA | (DeviceX ; KeyA)

= < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , 'owner' : UserA , ...) , UserB : ('uid' : UidB , ...) , ... > $ cloudA 'sendUID' UserA | UidB

if CurrentTime < TimeA + 1 .

ceq < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , 'owner' : UserB , ...) , UserB : ('uid' : UidB , ...) , ... > $ UserA 'callAPI:join' cloudA | (UidB ; KeyA)

= < cloudA | DeviceX : ('ticket' : ('key' : KeyA , 'time' : TimeA) , 'owner' : (UserB , UserA) , ...) , UserB : ('uid' : UidB , ...) , ... >

if CurrentTime < TimeA + 1 .

ceq < cloudA | DeviceX : ('ticket' : (('key' : KeyA , 'time' : TimeA), Tickets) , ...) , ... >

= < cloudA | DeviceX : ('ticket' : Tickets , ...) , ... >

if CurrentTime > TimeA + 2 .

eq < UserA | 'knowsKey' : SetX , ... > $ DeviceX 'sendKey' UserA | KeyA

= < UserA | 'knowsKey' : (SetX, KeyA) , ... > .

eq < UserA | 'knowsUID' : SetX , ... > $ DeviceX 'sendUID' UserA | UidB

= < UserA | 'knowsUID' : (SetX, UidB) , ... > .

eq < UserA | 'localTo' : SetX , ... > $ UserA 'approach' DeviceX

= < UserA | 'localTo' : (SetX , DeviceX) , ... > .

eq < UserA | 'localTo' : (SetX , DeviceX) , ... > $ UserA 'leave' DeviceX

= < UserA | 'localTo' : SetX , ... > .

vars DeviceX : Device .

vars UserA UserB : User .

vars OwnerX : Principal .

vars KeyA KeyB FreshKeyA : Qid .

vars UidB : Qid .

vars TimeA CurrentTime : Integer .

vars SetX : Set .

vars Tickets : Item .

eq ev1(UserA, DeviceX) = $ UserA 'press' DeviceX .

eq ev2(UserA, DeviceX) = $ UserA 'callAPI:getKey' cloudA | (DeviceX) .

eq ev3(UserA, DeviceX, KeyA) = $ UserA 'callAPI:bind' cloudA | ((DeviceX) ; KeyA) .

eq ev4(UserA, UidB, KeyA) = $ UserA 'callAPI:join' cloudA | ((UidB) ; KeyA) .

eq ev5(UserA, DeviceX) = $ UserA 'approach' DeviceX .

eq ev6(UserA, DeviceX) = $ UserA 'leave' DeviceX .

rl < UserA | 'localTo' : DeviceX , ... > < DeviceX | ... > => ev1(UserA, DeviceX) .

rl < UserA | 'localTo' : DeviceX , ... > < DeviceX | ... > => ev2(UserA, DeviceX) .

rl < UserA | 'localTo' : DeviceX , ... > < DeviceX | ... > => ev6(UserA, DeviceX) .

rl < UserA | 'knowsKey' : KeyA , ... > => ev3(UserA, DeviceX, KeyA) .

rl < UserA | 'knowsKey' : KeyA , 'knowsUID' : UidB , ... > => ev4(UserA, UidB, KeyA) .

rl < UserA | 'localTo' : nils , ... > < DeviceX | ... > => ev5(UserA, DeviceX) .

eq < UserX | ('localTo' : nils , ..) > $ UserX 'approaches' DeviceY

= < UserX | ('localTo' : DeviceY , ..) > .

eq < UserX | ('localTo' : DeviceY , ..) > $ UserX 'leaves' DeviceY

= < UserX | ('localTo' : nils , ..) > .

eq < DeviceY | ('pressed' : false , 'online' : false , 'key' : KeyA , 'owner' : nils , ..) > $ UserX 'pressButton' DeviceY

= < DeviceY | ('pressed' : true , 'online' : true , 'key' : KeyA , 'owner' : nils , ..) > $ DeviceY 'sendKey' UserX | (KeyA) .

eq < UserX | ('key' : nils , ..) > $ DeviceY 'sendKey' UserX | (KeyA)

= < UserX | ('key' : KeyA , ..) > .

eq < cloudA | (DeviceY : ('key' : KeyA , 'owner' : nils , ..) , ...) > < DeviceY | ('online' : true , 'key' : KeyA , 'owner' : nils , ....) > $ UserX 'callAPI:bind' cloudA | (DeviceY ; KeyA)

= < cloudA | (DeviceY : ('key' : KeyA , 'owner' : UserX , ..) , ...) > < DeviceY | ('online' : true , 'key' : KeyA , 'owner' : UserX , ....) > .

eq < cloudA | (DeviceY : ('owner' : UserX , ..) , ...) > $ UserX 'callAPI:reset' cloudA | (DeviceY)

= < cloudA | (DeviceY : ('owner' : nils , ..) , ...) > $ cloudA 'resetDevice' DeviceY .

eq < DeviceY | ('online' : true , 'owner' : UserX , ..) > $ cloudA 'resetDevice' DeviceY

= < DeviceY | ('online' : false , 'owner' : nils , ..) > .

vars N : Nat .

vars KeyA : Qid .

vars DeviceY : Device .

vars UserX : User .

eq ev1(UserX, DeviceY) = $ UserX 'pressButton' DeviceY .

eq ev2(UserX, DeviceY, KeyA) = $ UserX 'callAPI:bind' cloudA | (DeviceY ; KeyA) .

eq ev3(UserX, DeviceY) = $ UserX 'callAPI:reset' cloudA | (DeviceY) .

eq ev4(UserX, DeviceY) = $ UserX 'leaves' DeviceY .

eq ev5(UserX, DeviceY) = $ UserX 'approaches' DeviceY .

rl  < UserX | ('localTo' : DeviceY , ..) >=>ev1(UserX, DeviceY) .

rl < UserX | ('key' : KeyA , ..) > < DeviceY | ... >=> ev2(UserX, DeviceY, KeyA) .

rl < UserX | ('key' : KeyA , ..) > < DeviceY | ... >=> ev3(UserX, DeviceY) .

rl  < UserX | ('localTo' : DeviceY , ..) >=> ev4(UserX, DeviceY) .

rl < UserX | ('localTo' : nils , ..) > < DeviceY | ... >=> ev5(UserX, DeviceY) .

eq < UserX | ('localTo' : nils , ..) > $ UserX 'approaches' DeviceY

= < UserX | ('localTo' : DeviceY , ..) > .

eq < UserX | ('localTo' : DeviceY , ..) > $ UserX 'leaves' DeviceY

= < UserX | ('localTo' : nils , ..) > .

eq < system | ('counter' : N , ..) > < DeviceY | ('key' : KeyA , ...) > $ UserX 'pressButton' DeviceY

= < system | ('counter' : N + 1 , ..) > < DeviceY | ('key' : randomStr('KeyB', N) , ...) > .

eq < DeviceY | ('key' : KeyA , 'unlocked' : true , ..) > < UserX | ('key' : nils , ...) > $ UserX 'callAPI:getKey' DeviceY

= < DeviceY | ('key' : KeyA , 'unlocked' : true , ..) > < UserX | ('key' : KeyA , ...) > .

eq < DeviceY | ('key' : KeyA , 'unlocked' : true , ..) > $ UserX 'callAPI:lock' DeviceY | (KeyA)

= < DeviceY | ('key' : KeyA , 'unlocked' : false , ..) > .

eq < cloudA | (UserX : ('devices' : nils , 'members' : SetA , ..) , ...) > $ UserX 'callAPI:invite' cloudA | (UserY)

= < cloudA | (UserX : ('devices' : nils , 'members' : (SetA , UserY) , ..) , ...) > .

eq < cloudA | (UserX : ('devices' : nils , 'members' : (SetA , UserY) , ..) , ...) > $ UserX 'callAPI:kick' cloudA | (UserY)

= < cloudA | (UserX : ('devices' : nils , 'members' : SetA , ..) , ...) > .

eq < cloudA | (DeviceY : ('key' : KeyA , ..) , ...) > < UserX | ('members' : (SetA , UserY) , ....) > $ UserY 'cloudAPI:getKey' cloudA | (DeviceY) < UserY | ('key' : KeyA , .....) >

= < cloudA | (DeviceY : ('key' : KeyA , ..) , ...) > < UserX | ('members' : (SetA , UserY) , ....) > < UserY | ('key' : KeyA , .....) > .

eq < DeviceY | ('key' : KeyA , ..) > $ UserX 'callAPI:bind' cloudA | (DeviceY ; KeyA) < cloudA | (DeviceY : ('owner' : SetA , ...) , ....) >  *** after human fix one attribute value

= < cloudA | (DeviceY : ('owner' : (SetA , UserX) , ...) , ....) > < DeviceY | ('key' : KeyA , ..) > .

vars N : Nat .

vars UserX : User .

vars KeyA : Qid .

vars SetA : Set .

vars DeviceY : Device .

vars FreshKeyB : Qid .

vars UserY : User .

eq ev1(UserX, DeviceY) = $ UserX 'pressButton' DeviceY .

eq ev2(UserX, DeviceY) = $ UserX 'callAPI:getKey' DeviceY .

eq ev3(UserX, DeviceY, KeyA) = $ UserX 'callAPI:lock' DeviceY | (KeyA) .

eq ev4(UserX, DeviceY, KeyA) = $ UserX 'callAPI:bind' cloudA | (DeviceY ; KeyA) .

eq ev5(UserY, DeviceY) = $ UserY 'cloudAPI:getKey' cloudA | (DeviceY) .

eq ev6(UserX, UserY) = $ UserX 'callAPI:invite' cloudA | (UserY) .

eq ev7(UserX, UserY) = $ UserX 'callAPI:kick' cloudA | (UserY) .

eq ev8(UserX, DeviceY) = $ UserX 'leaves' DeviceY .

eq ev9(UserX, DeviceY) = $ UserX 'approaches' DeviceY .

*** transitions

rl < UserX | ('localTo' : DeviceY , ..) > => ev1(UserX, DeviceY)  .

rl < UserX | ('localTo' : DeviceY , ..) >=> ev2(UserX, deviceB) ..

rl < UserX | ('key' : KeyA , 'localTo' : DeviceY , ..) > =>  ev3(UserX, deviceB, KeyA) .

rl  < UserX | ('key' : KeyA , ..) > < DeviceY | ... > => ev4(UserX, DeviceY, KeyA) .

rl < UserY | ('key' : KeyA , ..) > < DeviceY | ... >=> ev5(UserY, DeviceY) .

rl  => ev6(userC, userA)  .

rl => ev7(userC, userA)  .

rl=> ev8(UserX, DeviceY) .

rl < UserX | ('localTo' : nils , ..) >=> ev9(UserX, deviceB) .

eq < DeviceY | ('pressed' : false , ..) > $ UserX 'pressButton' DeviceY

= < DeviceY | ('pressed' : true , ..) > .

eq < DeviceY | ('pressed' : true , 'key' : nils , ..) > $ UserX 'callAPI:setKey' DeviceY | (KeyA)

= < DeviceY | ('pressed' : false , 'key' : KeyA , ..) > .

eq < DeviceY | ('key' : KeyA , ..) > $ UserX 'callAPI:discover' DeviceY

= < DeviceY | ('key' : KeyA , ..) > $ DeviceY 'callAPI:bind' cloudA | (KeyA) .

eq < cloudA | (UserX : ('key' : KeyA , ..) , DeviceY : ('owner' : nils , ...) , ....) > $ DeviceY 'callAPI:bind' cloudA | (KeyA)

= < cloudA | (UserX : ('key' : KeyA , ..) , DeviceY : ('owner' : UserX , ...) , ....) > .

eq < UserX | ('localTo' : nils , ..) > $ UserX 'approaches' DeviceY

= < UserX | ('localTo' : DeviceY , ..) > .

eq < UserX | ('localTo' : DeviceY , ..) > $ UserX 'leaves' DeviceY

= < UserX | ('localTo' : nils , ..) > .

ops ev1 : User Device -> Event .

ops ev2 : User Device -> Event .

ops ev3 : User Device Qid -> Event .

ops ev4 : User Device -> Event .

ops ev5 : User Device -> Event .

eq ev1(UserX, DeviceY) = $ UserX 'pressButton' DeviceY .

eq ev2(UserX, DeviceY) = $ UserX 'callAPI:discover' DeviceY .

eq ev3(UserX, DeviceY, KeyA) = $ UserX 'callAPI:setKey' DeviceY | (KeyA) .

eq ev4(UserX, DeviceY) = $ UserX 'leaves' DeviceY .

eq ev5(UserX, DeviceY) = $ UserX 'approaches' DeviceY .

*** transitions

rl < UserX | ('localTo' : DeviceY , ..) >=> ev1(UserX, DeviceY) .

rl < UserX | ('localTo' : DeviceY , ..) >=> ev2(UserX, DeviceY) .

rl < UserX | ('localTo' : DeviceY , ..) > < cloudA | (UserX : ('key' : KeyA , ...) , ....) >=>  ev3(UserX, DeviceY, KeyA) ..

rl < UserX | ('localTo' : DeviceY , ..) >=> ev4(UserX, DeviceY) .

rl < UserX | ('localTo' : nils , ..) > < DeviceY | ... >=> ev5(UserX, DeviceY) .

eq < DeviceX | 'key' : nils, ... >

   $ cloudA 'callAPI:openWindow' DeviceX | KeyD

= < DeviceX | 'key' : KeyD, ... > .

eq < DeviceX | 'key' : KeyA, ... >

   $ cloudA 'callAPI:openWindow' DeviceX | KeyD

= < DeviceX | 'key' : KeyD, ... > .

eq < DeviceX | 'key' : KeyD, 'owners' : SetO, ... >

   $ UserX 'callAPI:bind' DeviceX | KeyD

= < DeviceX | 'key' : KeyD, 'owners' : (SetO, UserX), ... > .

eq < DeviceX | 'owners' : (SetO, UserX), 'on' : false, ... >

   $ UserX 'callAPI:toggle' DeviceX

= < DeviceX | 'owners' : (SetO, UserX), 'on' : true, ... > .

eq < cloudA | UserX : ('members' : SetM, ... ), ... >

   $ UserX 'callAPI:invite' cloudA | UserY

= < cloudA | UserX : ('members' : (SetM, UserY), ... ), ... > .

eq < cloudA | UserX : ('members' : (SetM, UserY), ... ), ... >

   $ UserX 'callAPI:kick' cloudA | UserY

= < cloudA | UserX : ('members' : SetM, ... ), ... > .

eq < cloudA | UserX : ('members' : (SetM, MemberY), 'device' : DeviceX, ... ), ... >

   $ MemberY 'callAPI:openWindow' cloudA | DeviceX

= < cloudA | UserX : ('members' : (SetM, MemberY), 'device' : DeviceX, ... ), ... >

  $ cloudA 'callAPI:openWindow' DeviceX | FreshKeyZ

  $ cloudA 'send' MemberY | FreshKeyZ .

eq < UserX | 'knowledge' : SetK, ... >

   $ cloudA 'send' UserX | KeyZ

= < UserX | 'knowledge' : (SetK, KeyZ), ... > .

eq ev1(UserX, DeviceX, KeyD) = $ UserX 'callAPI:bind' DeviceX | (KeyD) .

eq ev2(UserX, DeviceX) = $ UserX 'callAPI:toggle' DeviceX .

eq ev3(UserX, UserY) = $ UserX 'callAPI:invite' cloudA | (UserY) .

eq ev4(UserX, UserY) = $ UserX 'callAPI:kick' cloudA | (UserY) .

eq ev5(MemberY, DeviceX) = $ MemberY 'callAPI:openWindow' cloudA | (DeviceX) .

rl < MemberY | 'knowledge' : KeyD , ... > => ev5(MemberY, cloudA) .

rl < UserX | ... > < DeviceX | ... > => ev2(UserX, DeviceX) .

rl => ev3(userA, userC) .

rl => ev3(userC, userA) .

rl < cloudA | UserX : 'members' : UserY , ... > => ev4(UserX, UserY) .

eq < DeviceX | 'key' : nils, ... >

   $ cloudA 'callAPI:openWindow' DeviceX | KeyD

= < DeviceX | 'key' : KeyD, ... > .

eq < DeviceX | 'key' : KeyA, ... >

   $ cloudA 'callAPI:openWindow' DeviceX | KeyD

= < DeviceX | 'key' : KeyD, ... > .

eq < DeviceX | 'key' : KeyD, 'owners' : SetO, ... >

   $ UserX 'callAPI:bind' DeviceX | KeyD

= < DeviceX | 'key' : KeyD, 'owners' : (SetO, UserX), ... > .

eq < DeviceX | 'owners' : (SetO, UserX), 'on' : false, ... >

   $ UserX 'callAPI:toggle' DeviceX

= < DeviceX | 'owners' : (SetO, UserX), 'on' : true, ... > .

eq < cloudA | UserX : ('members' : SetM, ... ), ... >

   $ UserX 'callAPI:invite' cloudA | UserY

= < cloudA | UserX : ('members' : (SetM, UserY), ... ), ... > .

eq < cloudA | UserX : ('members' : (SetM, UserY), ... ), ... >

   $ UserX 'callAPI:kick' cloudA | UserY

= < cloudA | UserX : ('members' : SetM, ... ), ... > .

eq < cloudA | UserX : ('members' : (SetM, MemberY), 'device' : DeviceX, ... ), ... >

   $ MemberY 'callAPI:openWindow' cloudA | DeviceX

= < cloudA | UserX : ('members' : (SetM, MemberY), 'device' : DeviceX, ... ), ... >

  $ cloudA 'callAPI:openWindow' DeviceX | FreshKeyZ

  $ cloudA 'send' MemberY | FreshKeyZ .

eq < UserX | 'knowledge' : SetK, ... >

   $ cloudA 'send' UserX | KeyZ

= < UserX | 'knowledge' : (SetK, KeyZ), ... > .

eq ev1(UserX, DeviceX, KeyD) = $ UserX 'callAPI:bind' DeviceX | (KeyD) .

eq ev2(UserX, DeviceX) = $ UserX 'callAPI:toggle' DeviceX .

eq ev3(UserX, UserY) = $ UserX 'callAPI:invite' cloudA | (UserY) .

eq ev4(UserX, UserY) = $ UserX 'callAPI:kick' cloudA | (UserY) .

eq ev5(MemberY, DeviceX) = $ MemberY 'callAPI:openWindow' cloudA | (DeviceX) .

rl < MemberY | 'knowledge' : KeyD , ... > => ev5(MemberY, cloudA) .

rl < UserX | ... > < DeviceX | ... > => ev2(UserX, DeviceX) .

rl => ev3(userA, userC) .

rl => ev3(userC, userA) .

rl < cloudA | UserX : 'members' : UserY , ... > => ev4(UserX, UserY) .

eq < DeviceY | ('pressed' : false , ..) > $ UserX 'pressButton' DeviceY

= < DeviceY | ('pressed' : true , ..) > .

eq < DeviceY | ('pressed' : true , 'key' : nils , ..) > $ UserX 'callAPI:setKey' DeviceY | (KeyA)

= < DeviceY | ('pressed' : false , 'key' : KeyA , ..) > .

eq < DeviceY | ('key' : KeyA , ..) > $ UserX 'callAPI:discover' DeviceY

= < DeviceY | ('key' : KeyA , ..) > $ DeviceY 'callAPI:bind' cloudA | (KeyA) .

eq < cloudA | (UserX : ('key' : KeyA , ..) , DeviceY : ('owner' : nils , ...) , ....) > $ DeviceY 'callAPI:bind' cloudA | (KeyA)

= < cloudA | (UserX : ('key' : KeyA , ..) , DeviceY : ('owner' : UserX , ...) , ....) > .

eq < UserX | ('localTo' : nils , ..) > $ UserX 'approaches' DeviceY

= < UserX | ('localTo' : DeviceY , ..) > .

eq < UserX | ('localTo' : DeviceY , ..) > $ UserX 'leaves' DeviceY

= < UserX | ('localTo' : nils , ..) > .

vars N : Nat .

vars DeviceY : Device .

vars UserX UserY : User .

vars KeyA : Qid .

eq ev1(UserX, DeviceY) = $ UserX 'pressButton' DeviceY .

eq ev2(UserX, DeviceY) = $ UserX 'callAPI:discover' DeviceY .

eq ev3(UserX, DeviceY, KeyA) = $ UserX 'callAPI:setKey' DeviceY | (KeyA) .

eq ev4(UserX, DeviceY) = $ UserX 'leaves' DeviceY .

eq ev5(UserX, DeviceY) = $ UserX 'approaches' DeviceY .

rl  < UserX | ('localTo' : DeviceY , ..) >=>ev1(UserX, DeviceY) .

rl< UserX | ('localTo' : DeviceY , ..) >=> ev2(UserX, DeviceY) .

rl [ < cloudA | (UserY : ('key' : KeyA , ..) , ...) > < UserX | ('localTo' : DeviceY , ....) >=> ev3(UserX, DeviceY, KeyA) .

rl  UserX | ('localTo' : DeviceY , ..) >=> ev4(UserX, DeviceY) .

rl < UserX | ('localTo' : nils , ..) > < DeviceY | ... >=> ev5(UserX, DeviceY) .