{
* File: 02-constraints.sml.txt
* Author: Manfred Jeusfeld, Thomas Kuehne
* Created: 2023-03-01/M.Jeusfeld (2024-03-17/M.Jeusfeld)
* ------------------------------------------------------
* Constraints for multi-dimensional MLM
*
* 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) or (x isA c1)) and ((x instanceOf c2) or (x isA c2)) and
                  Pa(a1,c1,lab,t1) and Pa(a2,c2,lab,t2) and (x <> c1) and (x<>c2)  ==>  (c1 = c2) $; 
 
    c2a: $ forall x/Element p1,p2/Integer lab1,lab2/Label
                  (x potency/lab1 p1) and (x potency/lab2 p2) and (lab1 <> lab2) and (p1 > 0)  ==>  (p2 = 0) $;

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

    c2c: $ 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)) $;

    {* Constraint C3a was a much stronger version of the new C4c constraint, i.e., scenarios allowed under C4c would
     *  not be permitted under C3a. For this reason, constraint C3a is no longer enforced but still available as query C3a (see below). 
     *
     *  c3a: $ forall x,y1,y2/Element lab/Label 
     *                (x instanceOf/lab y1) and (x instanceOf/lab y2)  ==>  (y1 = y2) $; 
     *
     *}     

    {* Constraint C3b has been made optional, i.e., provided as a query, due to the change of handling C3a.
     *
     *  c3b: $ forall x,y1,y2/Element lab/Label 
     *                (x specializationOf/lab y1) and (x specializationOf/lab y2)  ==>  (y1 = y2) $; 
     *
     *}
    
    {* Constraint C3c has been made available in the form of a query (see below), to avoid enforcement with all models. 
     *
     *   c3c: $ forall lab/DimensionLabel (exists u,v/Element (u instanceOf/lab v))  ==>  
     *                (exists c/Element (forall x,y/Element (x instanceOf/lab y)  ==>  (x instanceOf_trans/lab c))) $; 
     *
     *}

    c4a: $ forall x/Element lab/Label 
                  not (x inIsa_trans/lab x) $;

    {* former (ER 2023) C4b version: 
     *
     *  c4b: $ forall x,y/Element lab/Label 
     *               (x instanceOf_trans/lab y)  ==>  not (x specConnected/lab y) $; 
     *
     *}
   
    c4b: $ forall x,y/Element lab/Label 
                  (x specConnected/lab y)  ==>  (x orderNotInconsistent/lab y) $; 

   {* Constraint C4c (level-respecting) replaces constraint C3a which enforced the same property but ruled out more models. *}
    c4c: $ forall x,c1,c2/Element lab/Label
                  (x instanceOf/lab c1) and (x instanceOf/lab c2)  ==>  (c1 orderNotInconsistent/lab c2) $
end


{*  Label/Dimension link and Characterization potency *}

MultiDimRules with
  constraint

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


    c0a: $ 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) $;


    c0b: $ 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) $
end


{* C3a: An element must not have more than one classifier in one dimension (no multiple classification). *}
C3a_MultipleClassification in QueryClass isA Element with
  constraint
   multipleClassifiers:  $ exists lab/Label c1,c2/Element 
                                          (this instanceOf/lab c1) and (this instanceOf/lab c2) and (c1 <> c2)  $
end 

{* C3b: An element must not have more than one supertype in one dimension (no multiple generalization). *}
C3b_MultipleGeneralization in QueryClass isA Element with
  constraint
   multipleSupertypes:  $ exists lab/Label s1,s2/Element 
                                           (this specializationOf/lab s1) and (this specializationOf/lab s2)  and  (s1 <> s2) $
end 

{* C3c: Within a dimension, all classification relationships must form a single cluster. *}
C3c_DisjointClusterRoots in GenericQueryClass isA Element with
  parameter,computed_attribute
    dim: Dimension
  constraint
    disjointRoots: $ exists lab/Label (this in TopInDimension[~dim/dim]) and Label(dim,lab) and
                                 exists x0/Element (x0 instanceOf/lab this) and  
                                 (not exists c/Element (forall x,y/Element (x instanceOf/lab y) ==>  (x instanceOf_trans/lab c))) $
end  

{---}

MultiDimRules!c1 with
  comment
    hint: "Elements that classify or generalize the same element, must not define features with the same name!"
end


MultiDimRules!c2a with
  comment
    hint: "Elements with potencies in more than one dimension must not have more than one non-zero potency value!"
end

MultiDimRules!c2b with
  comment
    hint: "All instantiations from a classifier must be into the same dimension!"
end

MultiDimRules!c2c with
  comment
    hint: "Elements participating in multiple dimensions must not entertain generalization relationships in their potency-zero dimensions!"
end

{* not used anymore due to use of query
MultiDimRules!c3a with
  comment
    hint: "Elements must not have more than one classifier within a dimension (no multiple classification within a dimension)!"
end
*}

{* not used anymore due to use of query
MultiDimRules!c3b with
  comment
    hint: "Elements must not have more than one supertype within a dimension (no multiple inheritance within a dimension)!"
end 
*}

{* not used anymore due to use of query
MultiDimRules!c3c with
  comment
    hint: "Within a dimension, all classification relationships must form a single cluster!"
end 
*}


MultiDimRules!c4a with
  comment
    hint: "The graph of instanceOf and specializationOf relations must be acyclic!"
end

MultiDimRules!c4b with
  comment
    hint: "Elements in a generalization hierarchy must not have inconsistent orders!"
end 

MultiDimRules!c4c with
  comment
    hint: "All instantiation paths between two elements must have the same length!"
end 


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


MultiDimRules!c0a 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!c0b with
  comment
    hint: "Subtypes must have an equal or higher potency than their supertypes!"
end