Generated Kodkod/Pardinus code in Alloy 6 - buggy?

1

Hi,

with the following spec:

abstract sig Super {
	to: set Super}
one sig Sub1 extends Super {}
sig Sub2 extends Super {}
run {}

Running and inspecting the predicate (in the reporter window of the analyzer) I see some lines like

Expression x8_upper = ((this/Sub1 + this/Sub2) -> (this/Sub1 + this/Sub2));
Expression x8_lower = (none -> none);

But I think it should be something like

TupleSet x8_upper = factory.noneOf(2);
x8_upper.add(factory.tuple("Sub1$0").product(factory.tuple("Sub1$0")));
x8_upper.add(factory.tuple("Sub1$0").product(factory.tuple("unused0")));
x8_upper.add(factory.tuple("Sub1$0").product(factory.tuple("Sub2$0")));
x8_upper.add(factory.tuple("unused0").product(factory.tuple("Sub1$0")));
x8_upper.add(factory.tuple("unused0").product(factory.tuple("unused0")));
x8_upper.add(factory.tuple("unused0").product(factory.tuple("Sub2$0")));
x8_upper.add(factory.tuple("Sub2$0").product(factory.tuple("Sub1$0")));
x8_upper.add(factory.tuple("Sub2$0").product(factory.tuple("unused0")));
x8_upper.add(factory.tuple("Sub2$0").product(factory.tuple("Sub2$0")));
bounds.bound(x8, x8_upper);

This snippet is from Alloy 5.1 with the same specification.

A bug in Alloy 6? At least I could not compile the generated code due to these lines.

– Burkhardt

2

Hi Burkhardt.

Yes, that’s a bug. Pardinus supports the definition of relation bounds as relational expressions rather than just tuple sets, but it seems that the translation to Java got broken along the way, will fix.