Added a feature to ReasonOperation where an unsatisfiable module can …

…be dumped

for debugging purposes.
Fixes #174

 - Added documentation to reason.md
 - Added command (-D option)
 - Function is isolated n ReasonerHelper static class

docs/reason.md

@@ -35,6 +35,22 @@ If no `--reasoner` is provided, ROBOT will default to ELK. The following other r
   * `emr` - [Expression Materializing Reasoner](http://static.javadoc.io/org.geneontology/expression-materializing-reasoner/0.1.3/org/geneontology/reasoner/ExpressionMaterializingReasoner.html)
   * `structural` - [Structural Reasoner](http://owlcs.github.io/owlapi/apidocs_4/org/semanticweb/owlapi/reasoner/structural/StructuralReasoner.html)
 
+## Logical Validation
+
+ROBOT will always perform a logical validation check prior to reasoning. Formally, this is known as testing for *incoherency*, i.e. the presence of either a logical inconsistency or unsatisfiable classes. If either of these hold true, the reason operation will fail and robot will exit with a non-zero code, after reporting the problematic classes.
+
+You can perform detailed debugging using an environment like Protege - load the ontology, switch on the reasoner and use the explain feature. For example, if you have unsatisfiable classes, find one of them (they should show up red) and click on the `?` where it says `EquivalentTo Nothing`.
+
+If you are working on a large complex ontology with multiple imports and you encounter unsatisfiable classes during the release, you can make a minimal ontology for debugging purposes using the `-D` (`--dump-unsatisfiable`) option folled by an output file path. This will find all unsatisfiable classes and use the [extract](extract) operation to create a debug module.
+
+```
+robot reason --reasoner ELK \
+  --input incoherent-tbox.owl \
+  -D results/debug.owl
+```
+
+If the input module contains at least one import, axioms in the debug module will be tagged with the source ontology, to assist in debugging.
+
 ---
 
 ## Error Messages

robot-command/src/main/java/org/obolibrary/robot/ReasonCommand.java

@@ -33,6 +33,11 @@ public class ReasonCommand implements Command {
   public ReasonCommand() {
     Options o = CommandLineHelper.getCommonOptions();
     o.addOption("r", "reasoner", true, "reasoner to use: ELK, HermiT, JFact");
+    o.addOption(
+        "D",
+        "dump-unsatisfiable",
+        true,
+        "if specified and ontology is incoherent, dump minimal explanatory module here");
     o.addOption(
         "s", "remove-redundant-subclass-axioms", true, "if true, remove redundant subclass axioms");
     o.addOption(

robot-core/src/main/java/org/obolibrary/robot/OptionsHelper.java

@@ -12,7 +12,7 @@ public class OptionsHelper {
    * @param key the name of the option to get
    * @return the value, if set, otherwise null
    */
-  private static String getOption(Map<String, String> options, String key) {
+  public static String getOption(Map<String, String> options, String key) {
     return getOption(options, key, null);
   }
 
@@ -25,7 +25,7 @@ private static String getOption(Map<String, String> options, String key) {
    * @param defaultValue the value to return if the key is not set
    * @return the value, if set, otherwise the default value
    */
-  private static String getOption(Map<String, String> options, String key, String defaultValue) {
+  public static String getOption(Map<String, String> options, String key, String defaultValue) {
     if (options == null) {
       return defaultValue;
     }

robot-core/src/main/java/org/obolibrary/robot/ReasonOperation.java

@@ -72,6 +72,7 @@ public static Map<String, String> getDefaultOptions() {
     options.put("equivalent-classes-allowed", ALL.written());
     options.put("prevent-invalid-references", "false");
     options.put("preserve-annotated-axioms", "false");
+    options.put("dump-unsatisfiable", null);
 
     return options;
   }
@@ -146,7 +147,9 @@ public static void reason(
 
     logger.info("Starting reasoning...");
     OWLReasoner reasoner = reasonerFactory.createReasoner(ontology);
-    ReasonerHelper.validate(reasoner);
+
+    String dumpFilePath = OptionsHelper.getOption(options, "dump-unsatisfiable", null);
+    ReasonerHelper.validate(reasoner, dumpFilePath, new IOHelper());
 
     logger.info("Precomputing class hierarchy...");
     reasoner.precomputeInferences(InferenceType.CLASS_HIERARCHY);

robot-core/src/main/java/org/obolibrary/robot/ReasonerHelper.java

@@ -1,24 +1,31 @@
 package org.obolibrary.robot;
 
+import java.io.IOException;
 import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Map;
 import java.util.Set;
 import java.util.UUID;
+import java.util.stream.Collectors;
 import org.obolibrary.robot.exceptions.IncoherentRBoxException;
 import org.obolibrary.robot.exceptions.IncoherentTBoxException;
 import org.obolibrary.robot.exceptions.InconsistentOntologyException;
 import org.semanticweb.owlapi.model.IRI;
+import org.semanticweb.owlapi.model.OWLAnnotation;
+import org.semanticweb.owlapi.model.OWLAnnotationProperty;
 import org.semanticweb.owlapi.model.OWLAxiom;
 import org.semanticweb.owlapi.model.OWLClass;
 import org.semanticweb.owlapi.model.OWLDataFactory;
 import org.semanticweb.owlapi.model.OWLObjectProperty;
 import org.semanticweb.owlapi.model.OWLOntology;
+import org.semanticweb.owlapi.model.OWLOntologyCreationException;
+import org.semanticweb.owlapi.model.OWLOntologyID;
 import org.semanticweb.owlapi.model.OWLOntologyManager;
 import org.semanticweb.owlapi.model.parameters.Imports;
 import org.semanticweb.owlapi.reasoner.OWLReasoner;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
+import uk.ac.manchester.cs.owlapi.modularity.ModuleType;
 
 /**
  * Provides convenience methods for working with OWL reasoning.
@@ -40,12 +47,29 @@ public class ReasonerHelper {
    */
   public static void validate(OWLReasoner reasoner)
       throws IncoherentTBoxException, InconsistentOntologyException, IncoherentRBoxException {
+    validate(reasoner, null, null);
+  }
+
+  /**
+   * Validates ontology, writes unsatisfiable module
+   *
+   * @param reasoner
+   * @param unsatisfiableModulePath
+   * @param ioHelper
+   * @throws IncoherentTBoxException
+   * @throws InconsistentOntologyException
+   * @throws IncoherentRBoxException
+   */
+  public static void validate(
+      OWLReasoner reasoner, String unsatisfiableModulePath, IOHelper ioHelper)
+      throws IncoherentTBoxException, InconsistentOntologyException, IncoherentRBoxException {
 
     OWLOntology ont = reasoner.getRootOntology();
     OWLOntologyManager manager = ont.getOWLOntologyManager();
     OWLDataFactory dataFactory = manager.getOWLDataFactory();
     OWLClass nothing = dataFactory.getOWLNothing();
     OWLClass thing = dataFactory.getOWLThing();
+
     logger.info("Checking for inconsistencies");
     if (!reasoner.isConsistent()) {
       throw new InconsistentOntologyException();
@@ -60,9 +84,22 @@ public static void validate(OWLReasoner reasoner)
       for (OWLClass cls : unsatisfiableClasses) {
         logger.error("    unsatisfiable: " + cls.getIRI());
       }
+      if (unsatisfiableModulePath != null) {
+        // normally we would not catch an exception and carry on,
+        // but in this case the primary exception is IncoherentTBoxException,
+        // we want to ensure this is thrown
+        try {
+          saveIncoherentModule(ont, unsatisfiableClasses, unsatisfiableModulePath, ioHelper);
+        } catch (OWLOntologyCreationException e) {
+          e.printStackTrace();
+        } catch (IOException e) {
+          e.printStackTrace();
+        }
+      }
       throw new IncoherentTBoxException(unsatisfiableClasses);
     }
 
+    // TODO: can this be done by checking for equivalence to bottomObjectProperty?
     logger.info("Checking for unsatisfiable object properties...");
 
     Set<OWLAxiom> tempAxioms = new HashSet<>();
@@ -100,4 +137,77 @@ public static void validate(OWLReasoner reasoner)
       throw new IncoherentRBoxException(unsatPs);
     }
   }
+
+  /**
+   * @param reasoner
+   * @param outputIRI
+   * @return minimal incoherent module
+   * @throws OWLOntologyCreationException
+   */
+  public static OWLOntology createIncoherentModule(OWLReasoner reasoner, IRI outputIRI)
+      throws OWLOntologyCreationException {
+    OWLOntology ontology = reasoner.getRootOntology();
+    OWLClass nothing = ontology.getOWLOntologyManager().getOWLDataFactory().getOWLNothing();
+    Set<OWLClass> unsatisfiableClasses =
+        reasoner.getUnsatisfiableClasses().getEntitiesMinus(nothing);
+    return createIncoherentModule(ontology, unsatisfiableClasses, outputIRI);
+  }
+
+  private static OWLOntology createIncoherentModule(
+      OWLOntology ontology, Set<OWLClass> unsatisfiableClasses, IRI outputIRI)
+      throws OWLOntologyCreationException {
+    if (outputIRI == null) {
+      outputIRI = IRI.generateDocumentIRI();
+    }
+    Set<IRI> terms = unsatisfiableClasses.stream().map(x -> x.getIRI()).collect(Collectors.toSet());
+    OWLOntology module = ExtractOperation.extract(ontology, terms, outputIRI, ModuleType.BOT);
+
+    if (ontology.getImportsClosure().size() > 1) {
+      logger.info("Tagging axioms in unsatisfiable module with their source");
+      // create an index of where each axiom comes from -
+      // this will be useful for debugging
+      OWLOntologyManager manager = ontology.getOWLOntologyManager();
+      OWLDataFactory dataFactory = manager.getOWLDataFactory();
+      OWLAnnotationProperty isDefinedBy = dataFactory.getRDFSIsDefinedBy();
+      Map<OWLAxiom, Set<OWLOntologyID>> axiomToOntologyMap = new HashMap<>();
+      for (OWLOntology subont : ontology.getImportsClosure()) {
+        OWLOntologyID ontid = subont.getOntologyID();
+        for (OWLAxiom axiom : module.getAxioms()) {
+          OWLAxiom axiomWithoutAnns = axiom.getAxiomWithoutAnnotations();
+          if (!axiomToOntologyMap.containsKey(axiomWithoutAnns)) {
+            axiomToOntologyMap.put(axiomWithoutAnns, new HashSet<>());
+          }
+          axiomToOntologyMap.get(axiomWithoutAnns).add(ontid);
+        }
+      }
+      Set<OWLAxiom> newAxioms = new HashSet<>();
+      Set<OWLAxiom> rmAxioms = new HashSet<>();
+      for (OWLAxiom axiom : module.getAxioms()) {
+        OWLAxiom axiomWithoutAnns = axiom.getAxiomWithoutAnnotations();
+
+        Set<OWLAnnotation> anns = new HashSet<>();
+        if (!axiomToOntologyMap.containsKey(axiomWithoutAnns)) {
+          logger.warn("Unexpected: module has axiom not in source ontologies: " + axiomWithoutAnns);
+        } else {
+          for (OWLOntologyID ontid : axiomToOntologyMap.get(axiomWithoutAnns)) {
+            anns.add(
+                dataFactory.getOWLAnnotation(
+                    isDefinedBy, dataFactory.getOWLLiteral(ontid.toString())));
+          }
+        }
+        newAxioms.add(axiom.getAnnotatedAxiom(anns));
+        rmAxioms.add(axiom);
+      }
+      manager.removeAxioms(module, rmAxioms);
+      manager.addAxioms(module, newAxioms);
+    }
+    return module;
+  }
+
+  private static void saveIncoherentModule(
+      OWLOntology ontology, Set<OWLClass> unsatisfiableClasses, String path, IOHelper ioHelper)
+      throws OWLOntologyCreationException, IOException {
+    OWLOntology module = createIncoherentModule(ontology, unsatisfiableClasses, null);
+    ioHelper.saveOntology(module, path);
+  }
 }

robot-core/src/main/java/org/obolibrary/robot/ReduceOperation.java

@@ -15,13 +15,11 @@
 import org.semanticweb.owlapi.model.OWLClass;
 import org.semanticweb.owlapi.model.OWLClassExpression;
 import org.semanticweb.owlapi.model.OWLDataFactory;
-import org.semanticweb.owlapi.model.OWLEquivalentClassesAxiom;
 import org.semanticweb.owlapi.model.OWLObjectPropertyCharacteristicAxiom;
 import org.semanticweb.owlapi.model.OWLOntology;
 import org.semanticweb.owlapi.model.OWLOntologyCreationException;
 import org.semanticweb.owlapi.model.OWLOntologyManager;
 import org.semanticweb.owlapi.model.OWLSubClassOfAxiom;
-import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom;
 import org.semanticweb.owlapi.model.parameters.Imports;
 import org.semanticweb.owlapi.reasoner.Node;
 import org.semanticweb.owlapi.reasoner.OWLReasoner;

robot-core/src/test/java/org/obolibrary/robot/ReasonerHelperTest.java

@@ -3,11 +3,17 @@
 import static org.junit.Assert.assertTrue;
 
 import java.io.IOException;
+import java.util.Set;
 import org.junit.Test;
 import org.obolibrary.robot.exceptions.IncoherentRBoxException;
 import org.obolibrary.robot.exceptions.IncoherentTBoxException;
 import org.obolibrary.robot.exceptions.InconsistentOntologyException;
+import org.semanticweb.owlapi.model.AddImport;
+import org.semanticweb.owlapi.model.AxiomType;
+import org.semanticweb.owlapi.model.IRI;
 import org.semanticweb.owlapi.model.OWLOntology;
+import org.semanticweb.owlapi.model.OWLOntologyCreationException;
+import org.semanticweb.owlapi.model.OWLSubClassOfAxiom;
 import org.semanticweb.owlapi.reasoner.OWLReasoner;
 import org.semanticweb.owlapi.reasoner.OWLReasonerFactory;
 
@@ -70,6 +76,44 @@ public void testIncoherentTBox()
     assertTrue(isCaughtException);
   }
 
+  /**
+   * Test creating an unsatisfiable module
+   *
+   * @throws IOException if file error
+   * @throws IncoherentTBoxException if has unsatisfiable classes
+   * @throws InconsistentOntologyException if has inconsistencies
+   * @throws IncoherentRBoxException if has unsatisfiable properties
+   * @throws OWLOntologyCreationException
+   */
+  @Test
+  public void testCreateUnsatisfiableModule()
+      throws IOException, IncoherentTBoxException, InconsistentOntologyException,
+          IncoherentRBoxException, OWLOntologyCreationException {
+    OWLOntology ontologyMain = loadOntology("/incoherent-tbox.owl");
+    IRI iri = ontologyMain.getOntologyID().getOntologyIRI().get();
+    OWLOntology ontology = ontologyMain.getOWLOntologyManager().createOntology();
+    AddImport ai =
+        new AddImport(
+            ontology,
+            ontology.getOWLOntologyManager().getOWLDataFactory().getOWLImportsDeclaration(iri));
+    ontology.getOWLOntologyManager().applyChange(ai);
+    OWLReasonerFactory reasonerFactory = new org.semanticweb.elk.owlapi.ElkReasonerFactory();
+    OWLReasoner reasoner = reasonerFactory.createReasoner(ontology);
+    boolean isCaughtException = false;
+    IOHelper ioHelper = new IOHelper();
+    String PATH = "target/unsat.owl";
+    try {
+      ReasonerHelper.validate(reasoner, PATH, ioHelper);
+    } catch (IncoherentTBoxException e) {
+      isCaughtException = true;
+      IOHelper ioh = new IOHelper();
+      OWLOntology unsatisfiableOntology = ioh.loadOntology(PATH);
+      Set<OWLSubClassOfAxiom> scas = unsatisfiableOntology.getAxioms(AxiomType.SUBCLASS_OF);
+      assertTrue(scas.size() == 2);
+    }
+    assertTrue(isCaughtException);
+  }
+
   /**
    * Test checking for inconsistencies.
    *

robot-core/src/test/java/org/obolibrary/robot/ReduceOperationTest.java

@@ -120,7 +120,7 @@ public void testReduceWithEquiv() throws IOException, OWLOntologyCreationExcepti
     assertIdentical("/equiv_reduce_test_reduced.obo", reasoned);
   }
 
- /**
+  /**
    * Edge case, taken from GO
    *
    * <p>See: 'central nervous system development' in the test file
@@ -135,15 +135,14 @@ public void testReduceEdgeCase() throws IOException, OWLOntologyCreationExceptio
 
     Map<String, String> options = new HashMap<String, String>();
     options.put("remove-redundant-subclass-axioms", "true");
- 
+
     ReduceOperation.reduce(reasoned, reasonerFactory, options);
     assertIdentical("/reduce-edgecase-cnd-reduced.obo", reasoned);
   }
-  
+
   /**
    * Domain case, see https://github.com/ontodev/robot/issues/321
    *
-   * 
    * @throws IOException
    * @throws OWLOntologyCreationException
    */
@@ -153,7 +152,7 @@ public void testReduceDomainCase() throws IOException, OWLOntologyCreationExcept
     OWLReasonerFactory reasonerFactory = new org.semanticweb.elk.owlapi.ElkReasonerFactory();
 
     Map<String, String> options = new HashMap<String, String>();
- 
+
     ReduceOperation.reduce(reasoned, reasonerFactory, options);
     assertIdentical("/reduce-domain-test.owl", reasoned);
   }