RELATION SCHEMA Bidirectional_3 
[Class1;Class2; role1:String;role2;String;mult1:Multiplicity;mult2:multiplicity; visibility1:Visi1:Visibility1; visi2:Visibility2; AddOnly: Boolean]
IMPORTS Class1, Class2, Integer, String, Set [elem:ANY] rename create as createSet
BASIC CONSTRUCTORS create, addLink
EFFECTIVE 
TYPE
Bidirectional_3
OPERATIONS
create: -> Bidirectional_3;
addLink: Bidirectional_3 (b) * Class1(c1) * Class2 (c2)
 -> Bidirectional_3
  pre:  not isRelated (b, c1, c2);
isFrozen: Bidirectional_3 ->  Boolean;
isChangeable: Bidirectional_3 ->  Boolean;
isAddOnly: Bidirectional_3 ->  Boolean;
role1: Bidirectional_3 ->  String;
role2: Bidirectional_3 -> String;
mult1: Bidirectional_3 ->  Multiplicity;
mult2: Bidirectional_3->  Multiplicity;
visibility1: Bidirectional_3 ->  Visibility;
visibility2: Bidirectional_3->  Visibility;
isEmpty: Bidirectional_3 -> Boolean;
isRightLinked: Bidirectional_3 * Class1 -> Boolean;
isLeftLinked: Bidirectional_3 * Class2 -> Boolean;
rightCardinality: Bidirectional_3 * Class1 -> Integer;
leftCardinality: Bidirectional_3  * Class2 -> Integer;
get_role2: Bidirectional_3 (a) * Class1 (c1) -> Set[Class2]
   pre: isRightLinked (a, c1);
get_role1: Bidirectional_3 (a) * Class2 (c2)->  Set[Class1] 
   pre: isLeftLinked (a, c2);
remove: Bidirectional_3 (a)  * Class1 (c1)  * Class2 (c2) ->
  Bidirectional_3
   pre: isRelated (a, c1, c2);
isRelated: Bidirectional_3 * Class1 (c1) * Class2 (c2) ->  Boolean;
AXIOMS a: Bidirectional_3; c1,cc1: Class1; c2,cc2:Class2; 
 isFrozen(create ()) = False; 
 isFrozen(addLink (a, c1, c2)) = isFrozen (a);
 isChangeable(create ()) = True;
   isChangeable(addLink (a, c1, c2)) = isChangeable (a);
   isEmpty(create ()) = True;
   isEmpty(addLink (a, c1, c2)) = False;
role1 (create()) = <role name>; 
role1(addLink (a, c1, c2)) = role1 (a);
role2 (create()) = role2 (a);
role2 (addLink (a, c1, c2)) = role2 (a);	
visibility1 (create()) = <visibility>;
visibility1 (addLink (a, c1, c2)) = visibility1 (a);
visibility2 (create()) = <visibility>;
visibility2 (addLink (a, c1, c2)) = visibility2 (a);
isAddOnly (create ()) = <True or False>;
isAddOnly (addLink (a, c1, c2)) = isAddOnly (a);
mult1(create()) = <mult1>;
mult1(addLink (a, c1, c2)) = mult1 (a);
mult2 (create()) = <mult2>;
mult2 (addLink (a, c1, c2)) = mult2 (a);
isRelated (create (), c1, c2) = False;
isRelated (addLink (a, c1, c2), cc1, cc2) = 
   ((c1 = cc1) and (c2 = cc2)) or isRelated(a, cc1, cc2) ;
isRightLinked (create (), c1) = False;
isRightLinked (addLink(a, c1, c2), cc1) =
   if (c1 = cc1) then True 
                        else isRightLinked (a, cc1) 
   endif;
isLeftLinked (create ( ), c2) = False;
isLeftLinked (addLink (a, c1, c2), cc2) =
   if (c2 = cc2) then True 
                        else isLeftLinked (a, cc2) 
   endif;
rightCardinality (create (), c1) = 0;
rightCardinality  (addLink (a, c1, c2), cc1) = 
   if (c1 = cc1) then 1 + rightCardinality (a, cc1) 
                        else rightCardinality (a, cc1) 
    endif;
leftCardinality (create (), c2) = 0;
leftCardinality (addLink (a, c1, c2), cc2) = 
   if (c2 = cc2) then 1 + leftCardinality (a, cc2)
                       else leftCardinality(a, cc2) 
   endif;
get_role2 (create( ), cc1) = createSet();
get_role2 (addLink (a, c1, c2), cc1) = 
  if (c1 = cc1) then  addSet (get_role2 (a, cc1), c2)
                       else get_role2 (a, cc1) 
  endif;
get_role1 (create( ), cc2) = createSet()
get_role1 (addLink (a, c1, c2), cc2) = 
      if (c2 = cc2) then  add (get_role1(a, cc2), c1)
                          else get_role1 (a, cc2) 
      endif;
remove (addLink (a, c1, c2), cc1, cc2) = 
   if ((c1 = cc1) and (c2 = cc2)) then a 
                                                  else remove (a, cc1, cc2) 
   endif;

END-CLASS