search

gsdlab / clafer

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

I74 #26

Closed Luke-Michael-Brown closed 11 years ago

Luke-Michael-Brown commented 11 years ago

see http://gsd.uwaterloo.ca:8888/question/338/problem-with-translation-of-abstract-clafers-in

mantkiew commented 11 years ago

This works nicely. There's one unexpected consequence though - when we change the cardinality of uninstantiated abstract clafers to 0, we get an UnSAT core and then IG tries to relax the cardinality 0 to * to produce a near-miss example. For example, 

abstract A

abstract B
    as ->> A 2..*

b : B

IG produces the following near miss:

No more instances found. Try increasing scope to get more instances.

The following set of constraints cannot be satisfied in the current scope.

(Hint: use the setUnsatCoreMinimization command to minimize the set of constraints below)

  1) A 0

Altering the following constraints produced the following near-miss example:

  1) A 0 changed to A *

A
b
  as$1 = A
  as$2 = A

Actually, the cardinality 0 on uninstantiated abstract clafers should not be considered as a removable constraint for the purpose of generating a near miss example.

We can merge this one and create a corresponding branch on IG to change the removable constraint behavior.