Coap option

 0   1   2   3   4   5   6   7

+---------------+---------------+ | | | | Option Delta | Option Length | 1 byte | | | +---------------+---------------+ \ / Option Delta / 0-2 bytes (extended) \ +-------------------------------+ \ / Option Length / 0-2 bytes (extended) \ +-------------------------------+ \ / / \ / Option Value / 0 or more bytes \ / / \ +-------------------------------+ Figure 8: Option Format

object coap_option_type = {
    type this = {
        critical : bool,   # [C] Critical
        unsafe : bool,     # [U] Unsafe
        nocachekey : bool, # [N] NoCacheKey
        repeatable : bool  # [R] Repeatable
    }
}

object option_name = {
    type this

    object if_match = { # [1] If-Match
        variant this of option_name = struct {
            opaque : stream_data, # opaque
        }
    }

    object uri_host = { # [3] Uri-Host
        variant this of option_name = struct {
            string : stream_data, # string
        }
    }

    object etag = { # [4] ETag
        variant this of option_name = struct {
            opaque : stream_data, # opaque
        }
    }

    object if_none_match = { # [5] If-None-Match
        variant this of option_name = struct {
        }
    }

    object uri_port = { # [7] Uri-Port
        variant this of option_name = struct {
            uint : stream_pos, # uint
        }
    }

    object location_path = { # [8] Location-Path
        variant this of option_name = struct {
            string : stream_data, # string
        }
    }

    object uri_path = { # [11] Uri-Path
        variant this of option_name = struct {
            string : stream_data, # string
        }
    }

    object content_format = { # [12] Content-Format
        variant this of option_name = struct {
            uint : stream_pos, # uint
        }
    }

    object max_age = { # [14] Max-Age
        variant this of option_name = struct {
            uint : stream_pos, # uint
        }
    }

    object uri_query = { # [15] Uri-Query
        variant this of option_name = struct {
            string : stream_data, # string
        }
    }

    object accept = { # [17] Accept
        variant this of option_name = struct {
            uint : stream_pos, # uint
        }
    }

    object location_query = { # [20] Location-Query
        variant this of option_name = struct {
            string : stream_data, # string
        }
    }

    object proxy_uri = { # [35] Proxy-Uri
        variant this of option_name = struct {
            string : stream_data, # string
        }
    }

    object proxy_scheme = { # [39] Proxy-Scheme
        variant this of option_name = struct {
            string : stream_data, # string
        }
    }

    object size1 = { # [60] Size1
        variant this of option_name = struct {
            uint : stream_pos, # uint
        }
    }

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

object coap_option = {
    type this = struct {
        option_number : stream_pos,   # [1] Option number
        option_length : stream_pos,   # [2] Length of the option value
        option_value  : stream_data    # [3] Option value
    }

    instance idx : unbounded_sequence
    instance arr : array(idx, this)
More definitions here, such as actions, invariants, etc.
}
+-----+---+---+---+---+----------------+--------+--------+----------+ | No. | C | U | N | R | Name | Format | Length | Default | +-----+---+---+---+---+----------------+--------+--------+----------+ | 1 | x | | | x | If-Match | opaque | 0-8 | (none) | | 3 | x | x | - | | Uri-Host | string | 1-255 | (see | | | | | | | | | | below) | | 4 | | | | x | ETag | opaque | 1-8 | (none) | | 5 | x | | | | If-None-Match | empty | 0 | (none) | | 7 | x | x | - | | Uri-Port | uint | 0-2 | (see | | | | | | | | | | below) | | 8 | | | | x | Location-Path | string | 0-255 | (none) | | 11 | x | x | - | x | Uri-Path | string | 0-255 | (none) | | 12 | | | | | Content-Format | uint | 0-2 | (none) | | 14 | | x | - | | Max-Age | uint | 0-4 | 60 | | 15 | x | x | - | x | Uri-Query | string | 0-255 | (none) | | 17 | x | | | | Accept | uint | 0-2 | (none) | | 20 | | | | x | Location-Query | string | 0-255 | (none) | | 35 | x | x | - | | Proxy-Uri | string | 1-1034 | (none) | | 39 | x | x | - | | Proxy-Scheme | string | 1-255 | (none) | | 60 | | | x | | Size1 | uint | 0-4 | (none) | +-----+---+---+---+---+----------------+--------+--------+----------+ C=Critical, U=Unsafe, N=NoCacheKey, R=Repeatable Table 4: Options