Struct1

type q
type r

type t = struct {
    first : q,
    second : r
}

individual v:t

action a(c:q,d:r) = {
    first(v) := c;
    second(v) := d;
    assert first(v) = c & second(v) = d
}

action b returns (x:q) = {
    x := first(v)
}

action c returns (x:r) = {
    x := second(v)
}

action d(x:t) = {
    v := x
}

action e returns (x:t) = {
    x := v
}

interpret q -> bv[16]
interpret r -> bv[16]

export a
export b
export c
export d
export e