# 
# File: add-positiveExamples.cbs
# Author: Manfred Jeusfeld, Thomas Kuehne
# Created: 2023-03-01 (2023-03-09/Manfred)
# -----------------------------------------------------
# Call: cbshell -v add-positiveExamples.cbs
#

# parameter -e controls the maximum number of errors messages generated for a transaction


connect



cd MultiDim

tell '
MultiDimRules with
  constraint
    c1: $ forall x,c1,c2/Element t1,t2/DataType a1,a2/ElementAttribute lab/Label
                :(x in c1): and :(x in 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 inst1,inst2/InstanceOfWithDim dim1,dim2/Dimension
              From(inst1,x) and To(inst1,c1) and From(inst2,x) and To(inst2,c2) and 
              (inst1 dimension dim1) and (inst2 dimension dim2) and (dim1 <> dim2) and
              Label(dim1,lab1) and Label(dim2,lab2) and 
              (x potency/lab1 p1) and (x potency/lab2 p2) and (p1 > 0) ==> (p2 = 0) $;
    c5: $ forall c/Element inst1,inst2/InstanceOfWithDim dim1,dim2/Dimension
              (inst1 dimension dim1) and (inst2 dimension dim2) and To(inst1,c) and To(inst2,c) 
          ==> (dim1 = dim2) $
end

{* additional constraints  *}
{* ac1: Elements can have multiple potencies but their local label must
        the the label of a known dimension
   ac2: Instances must have a strictly lower potency than their classes within a given dimension
   ac3: Subclasses must have a lower or equal potency than their superclasses within a given dimension
   ac4: Specialization or generalizations of a given object may not have different dimension, i.e. within
        a dimension, one can use only the specialization that belongs to the dimension (adapted from Thomas).
 *}

 
MultiDimRules with
  constraint
    ac1: $ forall x/Element lab/Label n/Integer (x potency/lab n) ==> exists dim/Dimension Label(dim,lab) $;
    ac2: $ forall inst/InstanceOfWithDim dim/Dimension x,c/Element px,pc/Integer lab/Label
               (inst dimension dim) and From(inst,x) and To(inst,c) and Label(dim,lab) and
               (c potency/lab pc) and (x potency/lab px)  ==> (px < pc) $;
    ac3: $ forall spec/IsAWithDim dim/Dimension c,d/Element pc,pd/Integer lab/Label
               (spec dimension dim) and From(spec,c) and To(spec,d) and Label(dim,lab) and
               (c potency/lab pc) and (d potency/lab pd) ==>  (pc <= pd) $;
    ac4 : $ forall spec1,spec2/IsAWithDim x/Element dim1/Dimension dim2/Dimension (spec1 dimension dim1) and (spec2 dimension dim2) and ((From(spec1,x) and From(spec2,x)) or (To(spec1,x) and To(spec2,x)))  ==> (dim1 = dim2) $ 
end

MultiDimRules!c1 with
  comment
    hint: "Classifiers in different dimensions that (potentially deeply) classify the same elements, must not define the same feature!"
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!c5 with
  comment
    hint: "Dimensional instantiations to the same class must use the same dimension!"
end

MultiDimRules!ac1 with
  comment
    hint: "Elements can have multiple potencies but their local label must the the label of a known dimension!"
end

MultiDimRules!ac2 with
  comment
    hint: "Instances must have a strictly lower potency than their classes within a given dimension!"
end

MultiDimRules!ac3 with
  comment
    hint: "Subclasses must have a lower or equal potency than their superclasses within a given dimension!"
end

MultiDimRules!ac4 with
  comment
    hint: "Specialization or generalizations of a given object may not have different dimension, i.e. within a dimension, one can use only the specialization that belongs to the dimension!"
end


'

cd MultiDim
mkdir TestC1
cd TestC1

# should fail:
tellModel c1-neg1.sml.txt
showAnswer
why

# should not fail:
tellModel c1-pos1.sml.txt
showAnswer


cd MultiDim
mkdir TestC2
cd TestC2

# should fail:
tellModel c2-neg1.sml.txt
showAnswer
why

# should not fail:
tellModel c2-pos1.sml.txt
showAnswer


cd MultiDim
mkdir TestC5
cd TestC5

# should fail:
tellModel c5-neg1.sml.txt
showAnswer
why


# should not fail:
tellModel c5-pos1.sml.txt
showAnswer