Navigation.jrag

aspect Navigation {

  /** Tests if A is a A1.
  *  @return 'true' if this is a A1, otherwise 'false'
  */
  syn A A.isA1() = false;
  eq A1.isA1() = true;

  /** Tests if A is a A2.
  *  @return 'true' if this is a A2, otherwise 'false'
  */
  syn A A.isA2() = false;
  eq A2.isA2() = true;

  /** casts a A into a A1 if possible.
   *  @return an Optional of 'this' cast to a A1 or an empty Optional
   */
  syn A A.asA1();
  eq A.asA1() = java.util.Optional.empty();
  eq .asA1() = java.util.Optional.of(this);

  /** casts a A into a A2 if possible.
   *  @return an Optional of 'this' cast to a A2 or an empty Optional
   */
  syn A A.asA2();
  eq A.asA2() = java.util.Optional.empty();
  eq .asA2() = java.util.Optional.of(this);

}