Coap message method

import coap_uri

object coap_message_method = {
    type this = {
        GET,
        POST,
        DELETE,
        PUT
    }
}

object coap_message_code_class = {
    type this = {
        SUCCESS,
        CLIENT_ERROR,
        SERVER_ERROR
    }
}

object coap_message_code_definition = {
    type this = {

SUCCESS

        CREATED,
        DELETED,
        VALID,
        CHANGED,
        CONTENT,

CLIENT_ERROR

        BAD_REQUEST,
        UNAUTHORIZED,
        BAD_OPTION,
        FORBIDDEN,
        NOT_FOUND,
        METHOD_NOT_ALLOWED,
        NOT_ACCEPTABLE,
        REQUEST_ENTITY_INCOMPLETE,
        PRECONDITION_FAILED,
        REQUEST_ENTITY_TOO_LARGE,
        UNSUPPORTED_CONTENT_FORMAT,

SERVER_ERROR

        INTERNAL_SERVER_ERROR,
        NOT_IMPLEMENTED,
        BAD_GATEWAY,
        SERVICE_UNAVAILABLE,
        GATEWAY_TIMEOUT,
        PROXYING_NOT_SUPPORTED
    }
}

object message_method = {

    type this

A CoAP request consists of the method to be applied to the resource, the identifier of the resource, a payload and Internet media type (if any), and optional metadata about the request.

    object request = {
        variant this of message_method = struct {
            req_type : coap_message_method
            res_id   : stream_data
            payload  : stream_data
            metadata : stream_data
        }
    }

0 1 2 3 4 5 6 7 +-+-+-+-+-+-+-+-+ |class| detail | +-+-+-+-+-+-+-+-+

              Figure 9: Structure of a Response Code

The upper three bits of the 8-bit Response Code number define the class of response. The lower five bits do not have any categorization role; they give additional detail to the overall class (Figure 9).

As a human-readable notation for specifications and protocol diagnostics, CoAP code numbers including the Response Code are documented in the format "c.dd", where "c" is the class in decimal, and "dd" is the detail as a two-digit decimal. For example, "Forbidden" is written as 4.03 -- indicating an 8-bit code value of hexadecimal 0x83 (40x20+3) or decimal 131 (432+3).

There are 3 classes of Response Codes:

2 - Success: The request was successfully received, understood, and accepted.

4 - Client Error: The request contains bad syntax or cannot be fulfilled.

5 - Server Error: The server failed to fulfill an apparently valid request.

    object response = {
        variant this of message_method = struct {
            code_class   : coap_message_code_class
            code_detail  : coap_message_code_definition
            payload      : stream_data
        }
    }

    instance idx : unbounded_sequence
    instance arr : array(idx, this)

    action handle(r: this, src:ip.endpoint,dst:ip.endpoint, i:id)  = {
        require false;
    }
}

relation is_idempotent

object message_method = {
    ...
    object request = {
        ...
        action handle(r: message_method.request, src:ip.endpoint,dst:ip.endpoint, i:id)

        around handle {

            ...

        }
    }
}


object message_method = {
    ...
    object response = {
        ...
        action handle(r: message_method.response, src:ip.endpoint,dst:ip.endpoint, i:id)

        around handle {

            ...

        }
    }
}