NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations
MIT License
31 stars 2 forks source link

Records that are used as map keys are printed as tuples #60

Closed nickgian closed 4 years ago

nickgian commented 4 years ago

When I use a record type as a map key, if it's printed as part of the solutions it's printed as a tuple instead of a record, actual MWE:

type r = {a:int; b:int}
type attr = set[r]

let nodes = 1
let edges ={}

let init u =
  let d = createDict false in
  d[{a=1;b=1} := true]

let trans e x = x

let merge u x y = x

let x = solution { init=init; trans=trans; merge=merge}
nickgian commented 4 years ago

A related problem is that sometimes the order of the fields is not preserved, i.e. they are printed as tuples but 'b' comes first and 'a' second. This is fine, if they are printed as records, but otherwise it's a big hassle. The example above doesn't exhibit this behavior though.

DKLoehr commented 4 years ago

This is caused by a combination of our BDD library and the fact that record unrolling happens before map unrolling (we weren't seeing this issue for e.g. edges because they're unrolled afterwards, so during mapback they get turned back into edges before we create any bdd values). Will push a fix momentarily.