1. 7
    1. 3

      this is what I came up with on my own attempt, and I may well be doing something fairly silly by the standards of “real” Alloy users.

      I haven’t read the whole thing yet, but I think you could simplify things by combining positiveFlags and negativeFlags into a single multirelation:

      abstract sig Valence {}
      one sig Pos, Neg extends Valence {}
      sig Bitfield {
          flags: Valence lone -> Flag

      To get just the positive flags, write b.flags[Pos]. If you instead do Flag -> lone Valence, you can write b.flags.Pos, which I guess is a bit nicer.

      The main reason to do this is it simplifies your other predicates. For example, here’s the new bitfieldSubset:

      pred bitfieldSubset[b, b": Bitfield] {
        b.flags in b".flags
      1. 1

        Thanks, I’ll try it out! Also, thank you for reading, and for writing about Alloy in the first place – it was your blog post that made me aware of the tool.