[init]

Initially, the userA is local to the deviceB and has no key; The userC is not local and has no key; The cloud records that deviceB's key is 'secret' and the owner is empty; The deviceB is not online, its key is 'secret', and its owner is empty.

[state changes]

When any user is not local to any device and the user approaches the device, the user will be local to the device.

When any user is local to any device and the user leaves any device, the user will be remote to the device.

When any user presses the button on any device, then the device will record that it is pressed, is online, and trigger an event to send the user its key.

When any device sends any user its key and the user has no key, the user will know the key.

When the cloudA records that the device has any key, the user calls 'callAPI:bind' with the device and the same key as arguments to cloudA, and the device is online, then the cloudA will update the owner from empty set to the user, and the device will update its owner from empty to the user.

When cloud records that any device has an owner, the owner can call 'callAPI:reset' of cloudA with the device, and then the cloudA will reset the owner to empty set, and trigger an event to reset the device.

When any device is online and cloudA wants to reset the device, the device will be offline and change its owner to empty.

[events]

If any user is local to any device, the user can press the device button.

If any user has some key, the user can:

1. use the key to call cloudA 's API 'callAPI:bind' ;

2. use the key to call cloudA 's API 'callAPI:reset'.

When any user is local to any device, the user can leave the device.

When any user is not local to any device, the user can approach the device.

Imagine you are an engineering expert and you can help me generate formalization of the protocol in a Maude

# The grammar

## Strictly follow the following syntax in EBNF

<Maude> ::= sorts <Sort>+ . |

    subsorts <Sort>+ ( < <Sort>+ )+ . |

    op <OpForm> : <Type>* <Arrow> <Type> . |

    ops ( <OpId> | ( <OpForm> ) )+ : <Type>* <Arrow> <Type> . |

    vars <VarId>+ : <Type> . |

    <Statement>|

    <Statement'> .

<Statement>  ::=  eq <Term> = <Term> |

    ceq <Term> = <Term> if <Condition>

<Statement'> ::= rl <Term> => <Term> |

    crl <Term> => <Term> if <Condition'>

<Condition> ::= <ConditionFragment> ( /\\ <ConditionFragment> )*

<Condition'> ::= <ConditionFragment'>

                 ( /\\ <ConditionFragment'> )*

<ConditionFragment> ::= <Term> = <Term> | <Term> := <Term>

                        | <Term> : <Sort>

<ConditionFragment'> ::= <ConditionFragment> | <Term> => <Term>

<Sort> ::= <SortId> | <Sort> { <Sort> ( , <Sort> )* }

<SortId>      %%% simple identifier, by convention capitalized

<VarId>       %%% simple identifier, by convention capitalized

<OpId>        %%% identifier possibly with underscores

<OpForm> ::= <OpId> | ( <OpForm> ) | <OpForm>+

<Nat>         %%% a natural number

<Term> ::= <Token> | ( <Term> ) | <Term>+

<Token>       %%% Any symbol other than ( or )

<TokenString> ::= <Token> | ( <TokenString> ) | <TokenString>*

# The semantics is Rewriting Logic

# The input includes the initial states and a protocol description in natural language.

# The output is Maude code in a code block, nothing else, no explanations or comments.

# Take your time, think step by step, no hurry to draw a conclusion

Now, please answer the below input:

mod SYSTEM is

sorts User Device Cloud Key State Event .

subsorts User Device Cloud Key < State .

subsorts Event < State .

ops userA userC : -> User .

ops deviceB : -> Device .

ops cloudA : -> Cloud .

ops secret : -> Key .

ops empty : -> Key .

vars U : User .

vars D : Device .

vars C : Cloud .

vars K : Key .

op local : User Device -> State .

op remote : User Device -> State .

op hasKey : User Key -> State .

op noKey : User -> State .

op online : Device -> State .

op offline : Device -> State .

op owner : Device User -> State .

op noOwner : Device -> State .

op cloudRecord : Cloud Device Key -> State .

op cloudOwner : Cloud Device User -> State .

op pressed : Device -> State .

op approach : User Device -> Event .

op leave : User Device -> Event .

op pressButton : User Device -> Event .

op sendKey : Device User -> Event .

op callAPI : User Cloud Device Key -> Event .

op resetAPI : User Cloud Device -> Event .

op resetDevice : Cloud Device -> Event .

eq local(userA, deviceB) = true .

eq remote(userC, deviceB) = true .

eq noKey(userA) = true .

eq noKey(userC) = true .

eq cloudRecord(cloudA, deviceB, secret) = true .

eq noOwner(deviceB) = true .

eq offline(deviceB) = true .

eq owner(deviceB, empty) = true .

crl [approach] : remote(U, D) => local(U, D) if approach(U, D) .

crl [leave] : local(U, D) => remote(U, D) if leave(U, D) .

crl [pressButton] : local(U, D) => pressed(D) /\ online(D) /\ sendKey(D, U) if pressButton(U, D) .

crl [sendKey] : sendKey(D, U) /\ noKey(U) => hasKey(U, secret) .

crl [bindAPI] : cloudRecord(C, D, K) /\ callAPI(U, C, D, K) /\ online(D) => cloudOwner(C, D, U) /\ owner(D, U) .

crl [resetAPI] : cloudOwner(C, D, U) /\ resetAPI(U, C, D) => cloudOwner(C, D, empty) /\ resetDevice(C, D) .

crl [resetDevice] : online(D) /\ resetDevice(C, D) => offline(D) /\ owner(D, empty) .

rl [pressButtonEvent] : local(U, D) => pressButton(U, D) .

rl [bindAPIEvent] : hasKey(U, K) => callAPI(U, cloudA, D, K) .

rl [resetAPIEvent] : hasKey(U, K) => resetAPI(U, cloudA, D) .

rl [leaveEvent] : local(U, D) => leave(U, D) .

rl [approachEvent] : remote(U, D) => approach(U, D) .

endm