Benchmark

Initially, userA is local to deviceB and has the key 'secretA', while userC is not local to deviceB and possesses the key 'secretC'. The cloudA records deviceB's information, with its binding key as '' and its owner as an empty set. DeviceB is not pressed and its key is an empty set.

If a user is not local to a device and approaches the device, the user will become local to it. Conversely, if a user is local to a device and leaves it, the user will become remote to the device. If a user presses the button on a device, the device records that it has been pressed. When a device is pressed without a key, and a user calls the device API 'callAPI:setKey', the device will change its state to not pressed, record the new key, call cloudA's API 'callAPI:setKey' with the new binding key as an argument, and update its state to reflect that it now has a key. If a device that already has a key is pressed and a user calls 'callAPI:setKey', the device will again change its state to not pressed, record the new key, and call cloudA's API 'callAPI:setKey' with the new binding key. Upon receiving a 'callAPI:setKey' event from any device, cloudA updates its binding key record for that device. When a user calls 'callAPI:bind' with the device and binding key as arguments to cloudA, and the binding key matches the record in cloudA, cloudA updates the owner from an empty set to the user. If a device that already has a key is pressed and a user calls 'callAPI:getKey', the device will change its state to not pressed and trigger an event to send its key to the user. Should a device send a user a key and the user already knows a key, the user will update their key with the new one. If a device has an owner, any user can call 'callAPI:reset' on cloudA with the device and binding key matching cloudA's record, resetting the owner to an empty set and setting the binding key to empty.

If a user is local to a device, the user can press the device button, call the device's API 'callAPI:getKey', or use their key to call any device's API 'callAPI:setKey'. If the user has a key, they can use it to call cloudA's API 'callAPI:bind' or 'callAPI:reset'. When a user is local to a device, they can leave the device, and when a user is not local to a device, they can approach it.

[properties]

The userA will always take operations in the order (press button, call device's API 'callAPI:setKey', and call cloud's 'callAPI:bind') until reset.

If the userA is the owner of deviceB, userA will not take any operations in the next time point.

If in the next point, userA reset the deviceB, the userA calls 'callAPI:bind' and is not the owner of deviceB.

If reset happens, the userA will eventually press the button of deviceB.

In the meantime, the userC can perform any operations between or after the userA.

Eventually, there is a time point that userC is not local to deviceB and is not the owner of deviceB, and the next time userC is not local and the owner of deviceB.

Initially, there is a device called deviceB. UserA is local to deviceB and knows nothing, while userC is not local to deviceB and also knows nothing. The cloudA records deviceB's information, where the owner is empty and there are no tickets.

If a user is not local to a device and approaches it, the user becomes local to that device. Conversely, if a user is local to a device and leaves it, the user becomes remote to the device. When a user presses the button on a device, the device calls the cloud API 'callAPI:setKey' with a random secret string. If the cloud records any device's information and detects tickets, and the device calls the cloud API 'callAPI:setKey' with any key, the cloud adds a ticket that records the key and the current time. This ticket is stored in a set containing all tickets.

If a user calls the cloud API 'callAPI:getKey' with the device as an argument, and the cloud has a ticket indicating that the device has a key, and the current time is less than the time recorded in the ticket plus one, the cloud triggers an event to send the key to the user. If the cloud records that a device has no owner and a user calls 'callAPI:bind' to cloudA, passing the device and the key as arguments, the cloud checks whether the provided key matches the ticket. If the key matches, cloudA updates the owner from nil to a set containing the user, signifying a successful binding. If the device already has an owner, any user can call 'callAPI:join' to cloudA, passing the device and the key. If the key matches the ticket in cloudA, the cloud adds the user as another owner. Tickets in cloudA are removed when the current time exceeds the time recorded in the ticket plus two. When cloudA sends a key to a user, the user adds the key to their knowledge.

When a user is local to a device, they can press the device button or call the device's API 'callAPI:getKey.' If a user has any key, they can use it to call cloudA's API 'callAPI:bind' or 'callAPI:join.' A user who is local to a device can leave the device, and a user who is not local to a device can approach it.

[properties]

The userA will always take operations in the order (press button, call API 'callAPI:getKey', and call cloud's 'callAPI:bind').

If the userA is the owner of deviceB, userA will not take any operations in the next time point.

In the meantime, the userC can perform any operations between or after the userA.

Eventually, there is a time point that userC is not local to deviceB and is not the owner of deviceB, and the next time userC is not local and the owner of deviceB.