{
* Author: Michael Schrefl, Bernd Neumayr, Manfred Jeusfeld, Christoph Schuetz
* Created: 23-Oct-2013/M.Jeusfeld (25-Oct-2013/M.Jeusfeld)
* ------------------------------------------------------
* negative example for axiom a30 (= formula (30) in table 1 of the paper)
*
* The LHS of the axiom is true but vc has no suitable attribute to vd1,vd2
*
}

a in ALABEL end
ab in ALABEL end

{* vC is needed for axiom i2 (unique definition of attributes) *}

vC in OBJECT with
 linkDR m: vD
end

vD in OBJECT end

vC!m with
  sourcelevel e: 4
  targetlevel f: 3
  label l: a
end



{* the example starts here *}

vc in OBJECT with
   IN c: vC
   linkDR m1: vd1
   linkDR m2: vd2
end

vd1 in OBJECT with
  IN c: vD
end

vd2 in OBJECT with
 IN c: vD
end

vc!m1 with
  sourcelevel e: 3
  targetlevel f: 2
  label l: a
end

vc!m2 with
  sourcelevel e: 3
  targetlevel f: 2
  label l: a
end


vc1 in OBJECT with
 IN cl: vc
end

vc2 in OBJECT with
 IN cl: vc1
end

vx in OBJECT with  
 IN cl: vc2  {* (vx ISA_RT vc) is true *}
 linkDR m: vy
end

ve2 in OBJECT with
  IN c: vD  {* to satisfy i4 *}
end

vy1 in OBJECT with
 IN cl: ve2
end

vy in OBJECT with  {* 2 levels below vd *}
 IN cl: vy1
end

vx!m with
  sourcelevel s: 0
  targetlevel t: 0
  label l: a
end