Variant2

type t

type a
type b

individual v : t


variant v1 of t = struct {
    foo : a
}

variant v2 of t = struct {
    bar : b
}

after init {
    var w : v1;
    w.foo := 2;
    v := w;
}

action act (inp: t) = {
}

before act {
    assume inp = v;
}

export act

interpret a->bv[2]
interpret b->bv[3]