{
* File: DualDeep_Part1.sml
* Author: Michael Schrefl, Bernd Neumayr, Manfred Jeusfeld, Christoph Schuetz
* Created: 10-Jun-2013/M.Jeusfeld (11-Dec-2013/M.Jeusfeld)
* ------------------------------------------------------
* Meta model and axiomatization for dual deep instantiation with
* generalization
*
* Part 1: Sorts and predicates
*
* requires ConceptBase 7.6 or later
*
* 14-Nov-2013: additional attributes for D and R; generalizing to link
* 25-Nov-2013: SPEC instead SUB
* 27-Nov-2013: link,predD,predR are all derived
*
* The Telos specifications in this file DualDeep_Part1.sml and in
* DualDeep_Part2.sml implement the DDI definitions in table 1
* of the paper
*   
* "Dual Deep Instantiation and its ConceptBase Implementation"
* by Bernd Neumayr, Manfred Jeusfeld, Michael Schrefl, and Christoph Schuetz
*
* The definitions and formulas marked by =(i)= refer to the respective entry in that
* table.
*
}

{*
  This source file is licensed under a
  Creative Commons Attribution-ShareAlike 3.0 license.
  You may use the files if you attribute your work to our work.
  And you may alter our work if you make it available under
  the same or similar license.
  http://creativecommons.org/licenses/by-sa/3.0/
*}



{* some useful definitions *}

RelationSemantics in Class with
  constraint
    singleConstraint :
        $ forall c,d/Proposition p/Proposition!single x,m/VAR
              P(p,c,m,d) and (x in c) ==>
                (
                  forall a1,a2/VAR
                    (a1 in p) and (a2 in p) and Ai(x,m,a1) and Ai(x,m,a2) ==>
                   (a1=a2)
                ) $;
    necConstraint:
          $ forall c,d/Proposition p/Proposition!necessary x,m/VAR
            P(p,c,m,d) and (x in c) ==>
             exists y/VAR (y in d) and (x m y) $
end



{* now define the base sort O (here labelled OBJECT *}

OBJECT with
  attribute

    link: OBJECT;   {* =(6)= generic link; corresponds to the predicate A in the paper *}

    linkDR: OBJECT;  {* =(4)= explicit attribute implying both range and domain constraints *}
    linkD: OBJECT;  {* =(3)= explicit attribute implying domain constraints *}
    linkR: OBJECT;  {* =(2)= explicit attribute implying range constraints *}
    predD: OBJECT;  {* =(8)= derived domain attribute (either from linkDR or linkD) *}
    predR: OBJECT;  {* =(7)= derived range attribute (either from linkDR or linkR) *}

    IN: OBJECT;      {* =(5)= *}
    SPEC: OBJECT;    {* =(17)= (c SPEC d): c is explicit subclass of d *}
    ISIN: OBJECT;
    MEMBER: OBJECT;  {* =(9)= (x MEMBER c): c is the 'class' side *}
    ISA: OBJECT;     {* =(11)=,=(20)= *}
    ORTHO: OBJECT;

    SPEC_t: OBJECT;  {* for transitive closure of SPEC *}
    MEMBER_t: OBJECT;
    ISA_t: OBJECT; 
    IN_t: OBJECT;

    SPEC_rt: OBJECT;  {* for reflexive&transitive closure of SPEC *}
    MEMBER_rt: OBJECT;
    ISA_rt: OBJECT;
    IN_rt: OBJECT

end

{* OBJECT!link corresponds to A(x,i,a,j,y); below are its specializations D,R,DR *}
OBJECT!linkD isA OBJECT!link end      {* =(6)= *}
OBJECT!linkR isA OBJECT!link end      {* =(6)= *} 
OBJECT!linkDR isA OBJECT!link end     {* =(6)= *} 


{* realize the derivation of predD,predR via Telos isA;       *}
{* so an instance of linkDR is also an instance of predD etc.  *}
OBJECT!linkDR isA OBJECT!predR end  {*  =(7)= DR(x,s,a,t,y) ==> R'(x,s,a,t,y) *}
OBJECT!linkR isA OBJECT!predR end   {*  =(7)= R(x,s,a,t,y) ==> R'(x,s,a,t,y) *}
OBJECT!linkDR isA OBJECT!predD end  {*  =(8)= DR(x,s,a,t,y) ==> D'(x,s,a,t,y) *}
OBJECT!linkD isA OBJECT!predD end   {*  =(8)= D(x,s,a,t,y) ==> D(x,s,a,t,y) *}


{* link,predR,predD have no explicit solution; all are stemming from their respective subclasses *}
{* implements the :<==> of =(6)=,=(7)=,=(8)= *}
AbstractnessConstraints in Class with
  constraint
    ac1: $ forall x,y/OBJECT (x link y) ==> (x linkD y) or (x linkR y) or (x linkDR y) $;
    ac2: $ forall x,y/OBJECT (x predR y) ==> (x linkR y) or (x linkDR y) $;
    ac3: $ forall x,y/OBJECT (x predD y) ==> (x linkD y) or (x linkDR y) $
end




{* closures of the extensional predicates *}
ClosureRules in Class with
  rule

    c1: $ forall x,y/OBJECT (x SPEC y) ==> (x SPEC_t y) $;
    c2: $ forall x,y/OBJECT (x MEMBER y) ==> (x MEMBER_t y) $;
    c3: $ forall x,y/OBJECT (x ISA y) ==> (x ISA_t y) $;
    c4: $ forall x,y/OBJECT (x IN y) ==> (x IN_t y) $;

    t1: $ forall x,y,z/OBJECT (x SPEC z) and (z SPEC_t y) ==> (x SPEC_t y) $;
    t2: $ forall x,y,z/OBJECT (x MEMBER z) and (z MEMBER_t y) ==> (x MEMBER_t y) $;
    t3: $ forall x,y,z/OBJECT (x ISA z) and (z ISA_t y) ==> (x ISA_t y) $;
    t4: $ forall x,y,z/OBJECT (x IN z) and (z IN_t y) ==> (x IN_t y) $;

    rt1: $ forall x,y/OBJECT (x SPEC_t y) ==> (x SPEC_rt y) $;
    rt2: $ forall x,y/OBJECT (x MEMBER_t y) ==> (x MEMBER_rt y) $;
    rt3: $ forall x,y/OBJECT (x ISA_t y) ==> (x ISA_rt y) $;
    rt4: $ forall x,y/OBJECT (x IN_t y) ==> (x IN_rt y) $;

    r1: $ forall x/OBJECT (x SPEC_rt x) $;
    r2: $ forall x/OBJECT (x MEMBER_rt x) $;
    r3: $ forall x/OBJECT (x ISA_rt x) $;
    r4: $ forall x/OBJECT (x IN_rt x) $

end



{* links are attributes that have both a source and a target level *}
{* We use it for modeling the A(x,sl,a,tl,y) predicate as well as  *}
{* R(x,sl,a,tl,y) and D(x,sl,a,tl,y)                               *}
{*  =(1)=,=(6)= *}
OBJECT!link with
  attribute
    sourcelevel: Integer;
    targetlevel: Integer;
    label: ALABEL
end


{* =(1)= *}
ALABEL end  {* just for labels of the attributes/relationships *}


DerivedPredicateDefinitions in Class with
   rule
     {* =(9)=,=(18)= *}
     MEMBER_rule: $ forall x,c,s,d/OBJECT (x SPEC_rt s) and (s IN d) and (d SPEC_rt c) ==> (x MEMBER c) $;
     {* =(20)= *}  
     ISA_rule: $ forall x,y/OBJECT (x SPEC y) or (x IN y)  ==> (x ISA y) $;
    {* not used *}  
     ORTHO_rule : $ forall x,y/OBJECT not (x SPEC_rt y) and not (y SPEC_rt x) ==> (x ORTHO y) $
end


{* an object is concrete if it has no explicit subclass/subobject *}
{* =(22)= *}
CONCRETE in QueryClass,MSFOLrule isA OBJECT with
  constraint
     isConcrete: $ not exists y/OBJECT (y SPEC this) $
end


{* NMEMBER is virtually a distance functions that counts the
   explicit instantiation links (IN) on the path from p1_x to p2_c;
   SPECs are overread via the MEMBER predicate
*}
{* =(19)= *}
NMEMBER in Function isA Integer with
  parameter
    p1_x: OBJECT;
    p2_c: OBJECT
  constraint
    nmember_rule:
        $ ((this=0) and (p1_x SPEC_rt p2_c)) or
          (exists d/OBJECT (d MEMBER p2_c) and (this = NMEMBER(p1_x,d) + 1)
          )
        $
end



{* to characterize link multiplicities *}
{* not used in the paper *}
Functional end
Injective end
Total end
Surjective end





{* Inheritance of attributes *}
{* As we have no general predicates in ConceptBase, we use queries to realize them: *}
{*   A^r*(x,i,a,j,y) <=> (yes in ARstar[x,i,a,j,y])                                 *}

{* not used in the paper *}
ARstar in GenericQueryClass isA YesClass with
  parameter,computed_attribute
     a1_x: OBJECT;
     a2_i: Integer;
     a3_a: ALABEL;
     a4_j: Integer;
     a5_y: OBJECT
  constraint
      c1: $ 
            (exists m1/OBJECT!link From(m1,a1_x) and (m1 sourcelevel a2_i) and (m1 label a3_a) and (m1 targetlevel a4_j) and To(m1,a5_y)
            ) or
            (exists s/OBJECT (a1_x SPEC s) and (yes in ARstar[s,a2_i,a3_a,a4_j,a5_y]) and 
              not exists y1/OBJECT (yes in ARstar[a1_x,a2_i,a3_a,a4_j,y1])
            )
          $
end

ADstar in GenericQueryClass isA YesClass with
  parameter,computed_attribute
     a1_x: OBJECT;
     a2_i: Integer;
     a3_a: ALABEL;
     a4_j: Integer;
     a5_y: OBJECT
  constraint
      c1: $ 
            (exists m1/OBJECT!link From(m1,a1_x) and (m1 sourcelevel a2_i) and (m1 label a3_a) and (m1 targetlevel a4_j) and To(m1,a5_y)
            ) or
            (exists t/OBJECT (a5_y SPEC t) and (yes in ADstar[a1_x,a2_i,a3_a,a4_j,t]) and 
              not exists x1/OBJECT (yes in ARstar[x1,a2_i,a3_a,a4_j,a5_y])
            )
          $
end

Astar in GenericQueryClass isA YesClass with
  parameter,computed_attribute
     a1_x: OBJECT;
     a2_i: Integer;
     a3_a: ALABEL;
     a4_j: Integer;
     a5_y: OBJECT
  constraint
      c1: $ 
            (yes in ARstar[a1_x,a2_i,a3_a,a4_j,a5_y]) or
            (yes in ADstar[a1_x,a2_i,a3_a,a4_j,a5_y])
          $
end