search

gsdlab / clafer

Clafer is a lightweight modeling language
http://clafer.org
MIT License
45 stars 13 forks source link

incorrect choco output for reference to a constant #89

Open mantkiew opened 8 years ago

mantkiew commented 8 years ago

For a model

abstract ASIL -> integer
A : ASIL -> 1
B : ASIL -> 2
C : ASIL -> 3
D : ASIL -> 4

the compiler produces

...
c0_ASIL.refToUnique(Int);
c0_A.extending(c0_ASIL).refTo(Int);
c0_B.extending(c0_ASIL).refTo(Int);
c0_C.extending(c0_ASIL).refTo(Int);
c0_D.extending(c0_ASIL).refTo(Int);

whereas the correct output should be

...
c0_ASIL.refToUnique(Int);
c0_A.extending(c0_ASIL).refToUnique(1);
c0_B.extending(c0_ASIL).refToUnique(2);
c0_C.extending(c0_ASIL).refToUnique(3);
c0_D.extending(c0_ASIL).refToUnique(4);
JLiangWaterloo commented 8 years ago

That's not supported right now by the backend (the refToUnique(1) part), but can't it be encoded easily with constraints like the following?

c0_A.extending(c0_ASIL); c0_A.addConstraint(equal(joinRef($this()), 1)); c0_B.extending(c0_ASIL); c0_B.addConstraint(equal(joinRef($this()), 2)); c0_C.extending(c0_ASIL); c0_C.addConstraint(equal(joinRef($this()), 3)); c0_D.extending(c0_ASIL); c0_D.addConstraint(equal(joinRef($this()), 4));

There would be no loss of efficiency since the backend has very good static analysis for these types of constraints and it will easily figure out that A/B/C/D must refer to 1/2/3/4 respectively.

mantkiew commented 8 years ago

Ok, I'll do it this way for int literals.