# 
# File: test-SATEXAMPLESDB-Constraints.cbs
# Author: Manfred Jeusfeld, Thomas Kuehne
# Created: 2024-02-24 (2024-02-24/Manfred)
# -----------------------------------------------------
# Call: cbshell test-SATEXAMPLESDB-Constraints.cb
# This script test the MultiDim constarints formulated as constraints
#



# connect 
startServer -d SATEXAMPLESDB -t low -u nonpersistent 


cd MultiDim-SatelliteArtifacts


tell "
MultiDimRules with
  constraint

      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) $
end
"

#tell '
#GioveA1_v2 in Element,DigitalArtifact,GioveA1 with
#  owner owner: ESPAC 
#  embedded embedded1: SatCtrlcomm
#  potency Artifacts: 0
#  version version: "A1-v643.1.771"
#  lastupdate lastupdate: "2023-12-23 18:31"
#end
#'

#echo "-------------------------"




tell "
MultiDimRules with
  constraint

      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
"

tell "
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) $
end
"


tell "
MultiDimRules with
  constraint

      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) $
end
"

tell "
MultiDimRules with
  constraint

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

tell "
MultiDimRules with
  constraint
    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)) $
end
"


tell "
MultiDimRules with
  constraint

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

tell "
MultiDimRules with
  constraint

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



#      c3c: $ forall y/Element d/Dimension lab/Label (y in TopInDimension[d/dim]) and Label(d,lab) and
#                ( (not exists x0/Element (x0 instanceOf/lab y)) or
#                  (exists c/Element  (forall x/Element (x instanceOf/lab y) ==> (x instanceOf_trans/lab c)))
#                ) $


tell "
MultiDimRules with
  constraint
       c3c: $ forall lab/DimensionLabel exists c/Element 
                  (forall x,y/Element (x instanceOf/lab y)  ==>  (x instanceOf_trans/lab c)) $

end
"


tell "
MultiDimRules with
  constraint

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

tell "
MultiDimRules with
  constraint

      c4b: $ forall x,y/Element lab/Label 
                  (x specConnected/lab y)  ==>  (x orderNotInconsistent/lab y) $
end
"

tell "
MultiDimRules with
  constraint

      c4c: $ forall x,c1,c2/Element lab/Label
                  (x instanceOf/lab c1) and (x instanceOf/lab c2)  ==>  (c1 orderNotInconsistent/lab c2) $
end
"