search

gsdlab / clafer

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

Cyclic containment problem #2

Closed kbak closed 11 years ago

kbak commented 13 years ago

For the following code:

abstract AttributeToColumn
  ComplexAttributeToColumn
    atc : AttributeToColumn ?

k : AttributeToColumn

Generated Alloy code contains a cycle between ComplexAttributeToColumn and AttributeToColumn, so that they might exist without any instance of k.

kbak commented 12 years ago

the same problem with (mutually recursive declarations):

abstract AttributeToColumn
  cat
  bab
    test
      g : gtc ?

abstract gtc
  test
    atc : AttributeToColumn ?

k : AttributeToColumn

A solution is to analyze each containment path and and disallow recursive declarations:

fact { no iden & ^(r_child1.r_child2...) }
mantkiew commented 12 years ago

Running the first example in ClaferIG v0.3.0.1 produces correct instances. For example,

k
  ComplexAttributeToColumn4
    atc3
      ComplexAttributeToColumn3
        atc2
          ComplexAttributeToColumn2
            atc1
              ComplexAttributeToColumn1
mantkiew commented 12 years ago

Running the first example in ClaferIG v0.3.0.1 produces only empty instances, regardless of the set scope.

mantkiew commented 11 years ago

With the current (in develop)

Clafer v0.3.3.29-5-2013 ClaferIG v0.3.3.3-6-2013

There are no problems at all. Both examples instantiate just fine with different scopes.