informalsystems/itf-rs

Support traces with sum types

Closed this issue · 2 comments

hvanz commented

Since v0.17, Quint supports sum types, which are encoded in a specific way in ITF trace files. For example, for

type T = None | Some(int)
var x: T

variable x will be appear in traces as {"tag": "None", value: {}} or {"tag": "Some", value: 123}.

romac commented

Done in #12.

@hvanz See the test here for an example: https://github.com/informalsystems/itf-rs/pull/12/files#diff-5235d25ffd085a52564b84d521e5e301742d2858fc3c9b24024b2fef4928f890

Basically you just need to annotate the enum with:

#[serde(tag = "tag", content = "value")]
  • ❤️1
romac commented

Released in v0.2.2