Fix role unsafety check

We now check that the existential expression in the axiom of type T3 is
not top.

2 files changed, 8 insertions, 7 deletions

diff --git a/src/main/scala/rsacomb/RSAAxiom.scala b/src/main/scala/rsacomb/RSAAxiom.scala
index 588c72a..9e9a016 100644
--- a/src/main/scala/rsacomb/RSAAxiom.scala
+++ b/src/main/scala/rsacomb/RSAAxiom.scala
@@ -16,9 +16,10 @@ trait RSAAxiom {
    */
   private sealed trait RSAAxiomType
   private object RSAAxiomType {
-    case object T3 extends RSAAxiomType // ∃R.A ⊑ B
-    case object T4 extends RSAAxiomType // A ⊑ ≤1R.B
-    case object T5 extends RSAAxiomType // A ⊑ ∃R.B
+    case object T3    extends RSAAxiomType // ∃R.A ⊑ B
+    case object T3top extends RSAAxiomType // ∃R.⊤ ⊑ B
+    case object T4    extends RSAAxiomType // A ⊑ ≤1R.B
+    case object T5    extends RSAAxiomType // A ⊑ ∃R.B
   }
 
   /* Implements additional features on top of `OWLAxiom` from
@@ -43,6 +44,8 @@ trait RSAAxiom {
         val sub = axiom.getSubClass().getClassExpressionType()
         val sup = axiom.getSuperClass().getClassExpressionType()
         t match {
+          case RSAAxiomType.T3top => // ∃R.⊤ ⊑ B
+            axiom.isT5 && axiom.getSubClass().asInstanceOf[OWLObjectSomeValuesFrom].getFiller.isOWLThing
           case RSAAxiomType.T3 => // ∃R.A ⊑ B
             sub == ClassExpressionType.OBJECT_SOME_VALUES_FROM && sup == ClassExpressionType.OWL_CLASS
           case RSAAxiomType.T4 => // A ⊑ ≤1R.B
@@ -67,6 +70,7 @@ trait RSAAxiom {
     }
 
     /* Exposed methods */
+    def isT3top: Boolean = isOfType(RSAAxiomType.T3top)
     def isT3: Boolean = isOfType(RSAAxiomType.T3)
     def isT4: Boolean = isOfType(RSAAxiomType.T4)
     def isT5: Boolean = isOfType(RSAAxiomType.T5)
diff --git a/src/main/scala/rsacomb/RSAOntology.scala b/src/main/scala/rsacomb/RSAOntology.scala
index 92be118..3b08e61 100644
--- a/src/main/scala/rsacomb/RSAOntology.scala
+++ b/src/main/scala/rsacomb/RSAOntology.scala
@@ -108,9 +108,6 @@ trait RSAOntology {
        *    For all roles r1 appearing in an axiom of type T5, r1 is unsafe
        *    if there exists a role r2 (different from top) appearing in an axiom
        *    of type T3 and r1 is a subproperty of the inverse of r2.
-       * 
-       * TODO: We are not checking whether the class expression on the right in T3
-       * is top. For now we can assume it is always the case.
        */
       val unsafe1 = for {
         axiom <- tbox
@@ -119,7 +116,7 @@ trait RSAOntology {
         roleSuper = role1 +: reasoner.superObjectProperties(role1).collect(Collectors.toList()).asScala
         roleSuperInv = roleSuper.map(_.getInverseProperty)
         axiom <- tbox
-        if axiom.isT3
+        if axiom.isT3 && !axiom.isT3top
         role2 <- axiom.objectPropertyExpressionsInSignature 
         if roleSuperInv.contains(role2)
       } yield role1