Bug in BDD difference

[jclark]

There's a bug in the last line of figure 21. It's currently:

n1 \ n2 = <a(n1), l(n1) \  n2, m(n1) \ n2, r(n1) \ n2>

but it should be:

n1 \ n2 = <a(n1), l(n1) \ l(n2), m(n1) \ m(n2), r(n1) \ r(n2)>

as in the Castagna paper (https://arxiv.org/pdf/1809.01427.pdf, at the bottom of page 15:35) where the corresponding formula is

a1? C1 \ C2 : U1 \ U2 : D1 \ D2

The way you have it does not preserve the invariant that on every path the order of the labels strictly increases.

BTW, thanks very much for your tutorial: I found it very helpful for getting started with my project (https://github.com/jclark/semtype).

[pnwamk]

Thank you for the issue; I believe I've addressed it here, and I've rerendered the tutorial and the fix should be live.

I'm glad the tutorial was useful! I wrote it originally so I could understand what on earth I was trying to do, so it's awesome to hear it had a benefit outside of that limited use =)

[jclark]

I think there's actually a bug here in the Castagna paper: ballerina-platform/nballerina#757 (comment)

I have reported it, so we will see what he says.

[jclark]

Castagna confirmed the bug and the fix, so I made a new issue #5.