{
* File: 02-constraints.sml.txt
* Author: Manfred Jeusfeld, Thomas Kuehne
* Modified: 2023-09-07/M.Jeusfeld/T.Kuehne  
* ------------------------------------------------------
* Constraints of MDM
* Version as published for ER 2023 paper
* 
* Thomas Kuehne, Manfred Jeusfeld: Sanity-Checking Multiple Levels of Classification -
* A Formal Approach with a ConceptBase Implementation. 
* In: Proceedings 42nd Intl. Conf. on Conceptual Modeling (ER 2023), Springer-Verlag
* 
*
* License: Creative Commons license
   Attribution-NonCommercial 4.0 International
   http://creativecommons.org/licenses/by-nc/4.0/
   http://creativecommons.org/licenses/by-nc/4.0/legalcode
*
}

MultiDimRules with
  constraint

    c1: $ forall x,c1,c2/Element t1,t2/DataType a1,a2/ElementAttribute lab/Label
            (x instanceOf c1) and (x instanceOf c2) and (c1 < c2) and Pa(a1,c1,lab,t1) and Pa(a2,c2,lab,t2) ==> (a1 = a2) $;

    c2: $ forall x,c1,c2/Element p1,p2/Integer lab1,lab2/Label
            (x potency/lab1 p1) and (x potency/lab2 p2) and (lab1 < lab2) and (p1 > 0) ==> (p2 = 0) $;

    c3a: $ forall x,y1,y2/Element lab/Label (x instanceOf/lab y1) and (x instanceOf/lab y2) ==> (y1 = y2) $;

    c3b: $ forall x,y1,y2/Element lab/Label (x specializationOf/lab y1) and (x specializationOf/lab y2) ==> (y1 = y2) $; 

    c4a: $ forall x/Element lab/Label not (x inIsa_trans/lab x) $;
    
    c4b: $ forall x,y/Element lab/Label (x instanceOf_trans/lab y) ==> not (x specConnected/lab y) $; 

    c5: $ forall x1,x2,c/Element lab1,lab2/Label (x1 instanceOf/lab1 c) and (x2 instanceOf/lab2 c) ==> (lab1 = lab2) $

   {* candidate constraint to exclude mixed generalizations; not used in this paper however
    c5b: $ forall x1,x2,c/Element lab1,lab2/Label
              (x1 specializationOf/lab1 c) and (x2 specializationOf/lab2 c)
          ==> (lab1 = lab2) $ 
   *}

end



MultiDimRules with
  constraint

    ac1: $ forall x/Element lab/Label n/Integer (x potency/lab n) ==> exists dim/Dimension Label(dim,lab) $;

   {* requires existence of instance potency *}
   {* = c2c }
    ac2: $ forall x,c/Element pc/Integer lab/Label
               (x instanceOf/lab c) and (c potency/lab pc) ==>
               exists px/Integer (x potency/lab px) and (px < pc) and (pc > 0) $;

    ac3: $ forall c,d/Element pc,pd/Integer lab/Label
               (c specializationOf/lab d) and
               (c potency/lab pc) and (d potency/lab pd) ==>  (pd <= pc) $;

    ac4: $ forall x,c/Element lab/Label dim/Dimension
             (x specializationOf/lab c) and
             (x memberOf dim) and not Label(dim,lab) ==>
             (exists p/Integer (x potency/lab p) and (p > 0)) $

end


{* The following query class replaces the old c3b constraint *}
{* If there are two different top objects in a given dimension, then there are unconnected components in the dimension graph *}

C3_DisjointDimensions in GenericQueryClass isA Element with
  parameter,computed_attribute
    dim: Dimension
  computed_attribute
    otherTop: Element
  constraint
    disjointDim: $ exists lab/Label (this in TopInDimension[~dim/dim]) and (~otherTop in TopInDimension[~dim/dim]) and 
                  (this <> ~otherTop) and Label(~dim,lab) and 
                      (not exists commonDesc/Element (commonDesc inIsa_trans/lab this) and (commonDesc inIsa_trans/lab ~otherTop)) $
end 


C3c_ClusterRoots in QueryClass isA Element with
  computed_attribute
    dim: Dimension
  constraint
    disjointDim: $ exists x0/Element lab/Label (x0 instanceOf/lab this) and Label(dim,lab) and 
                  not (exists c/Element 
                      (forall x,y/Element (x instanceOf/lab y)  ==>  (x instanceOf_trans/lab c))) $
end



{---} 

{* ConceptBase ignores this hint for some reason and generates instead an error message using the partially evaluated formula *}
MultiDimRules!c1 with
  comment
    hint: "Classifiers that (potentially deeply) classify the same elements, must not define features with the same name!"
end


MultiDimRules!c2 with
  comment
    hint: "Elements that are classified by more than one dimension must have a potency value of zero for all but possibly one dimension!"
end


MultiDimRules!c3a with
  comment
    hint: "Elements may only have one classifier within a dimension (no multiple classification within a dimension)!"
end

MultiDimRules!c3b with
  comment
    hint: "Elements may only have one superclass within a dimension (no multiple inheritance within a dimension)!"
end 


MultiDimRules!c4a with
  comment
    hint: "The graph of instanceOf and specializationOf relations may not contain cycles!"
end

MultiDimRules!c4b with
   comment
     hint: "An element's classifier cannot share the same generalization hierarchy with the element!"
end 


MultiDimRules!c5 with
  comment
    hint: "All instantiations to a classifier must be in the same dimension!"
end


MultiDimRules!ac1 with
  comment
    hint: "Elements can have multiple potencies but their potency labels must be the labels of known dimensions!"
end

MultiDimRules!ac2 with
  comment
    hint: "Instances must have a potency that is strictly lower than that of their classifiers and classifiers must have potencies greater than zero!"
end

MultiDimRules!ac3 with
  comment
    hint: "Subclasses must have an equal or higher potency than their superclasses!"
end

MultiDimRules!ac4 with
  comment
    hint: "An element which is in multiple dimensions may only entertain specializations relationships in the one dimension where its potency is greater than zero!"
end