Reasoning timeout and dispose features

[htmai-880]

Reasoner timeout and dispose features

The issue

I noticed in my previous PR that the timeout feature for laconic justifications was poorly handled, mainly because on the side of owlexplanation there is no timeout support. Basically, one motivation for it is that it shouldn't take interrupting the code (and therefore stopping the whole JVM instance) to figure out that something has gone wrong with reasoning.

With that said, this PR attempts to implement a timeout feature for many reasoning features, and a dispose feature to free up the resources occupied by a reasoner once it is no longer needed.

Implementation

So one way to go about the timeout is to implement it Java-side directly (since it's where the reasoner is implemented), which is what this PR does with java.util.concurrent.CompletableFuture, java.util.concurrent.TimeUnit and java.util.concurrent.TimeoutException. Basically, we try to wrap the function calls with futures, and interrupt the run when the timeout is exceeded.

Regrettably, I have not found a straightforward implementation to achieve the goal, because reasoners can be destructive (i.e., if interrupted, they leave the ontology different from the one they ingested), which led to unit tests failing. So if a timeout or interrupt feature should be expected, then it should basically account for that destructive aspect. Hence, I chose to employ the rather inefficient approach of reasoning on a deep copy of the ontology (with a new instance of the reasoner) when timeout is required. Maybe this can be improved in the future, but I do not have a better approach in mind for now.

As an addition, I also made it possible to dispose of the reasoner once it is no longer needed (since either way, this has to be done if reasoning is carried out on a deep copy).

Feel free to play around this timeout feature and let me know your thoughts.

[htmai-880]

I can't see the log, but this probably failed due to testing on carcinogenesis (to enforce timeout). The Java-side logger is on, and it logs the whole signature, so it needs to be disabled (problem on OWLAPI's side). I'd suggest to set the logger off by forcing the environment variable:

export JAVA_TOOL_OPTIONS="-Dorg.slf4j.simpleLogger.defaultLogLevel=off"

[htmai-880]

The tests passed, but the action segfaulted, with no other log I can work with. If you have any ideas on how to debug this, please let me know.

For what it's worth, the tests did not segfault on my device.

[htmai-880]

Most likely either the environment variable enforcement, or the Java-side logging on huge ontologies makes the method for laconic justifications with timeout untestable in GitHub Actions. Feel free to propose better solutions.

[alkidbaci]

Hi, first thing first, thank you for the PR. I noticed that the timeout argument in create_laconic_axiom_justifications is not used at all. Now, as much as I believe the timeout feature is beneficial, implementing it in such a way where we use a copy of the ontology will introduce undesired runtime overhead when considering the optimal scenario where the timeout limit is not reached. Also these methods can be called multiple time consecutively emphasizing this inefficiency even more. So it is about finding the sweet spot in this trade-off. In the absence of a better idea for the moment, I would suggest the following options:

1. We perform the timeout check in the original ontology/reasoner (not the copy)
   • I was actually wondering were can it go wrong if using the original ontology? You say that the reasoner is destructive (i.e., if interrupted, they leave the ontology different from the one they ingested) but the reasoner does not modify the ontology. But maybe I am misunderstanding something here. Maybe this is something that happens with the java reasoners when, for example, doing inferences. I would appreciate a bit more clarification in this sense (you mentioned that the unit test fail but why?)
2. We remove the timeout feature all-together
   • If it comes to this, then I would say that having efficient code is a better trade-off than having the timeout feature. If, say for example, the consistency check can take a lot of time to finish processing in the first place, then a lot of other methods will also be very time consuming (like for example instances) because the problem is most likely the size of the ontology. So my point is that this feature is not very handy overall when comparing it with the fact that it comes bundled-up with the drawback of runtime overhead for the normal scenario.
3. Find a better solution (TODO for me :D)

That being said, I will spend some time to see if I can find a better solution to this because indeed there are specific scenarios when a timeout argument may come in handy but it would be very helpful to hear your input on option 1.

Thank you!

[alkidbaci]

Regrading the segmentation fault, that's a long-lasting issue that although it has to do with SyncOntology initialization, I have not been able to find the exact cause. As you said it does not happen when testing locally so its not a issue worth spending much time investigating.

[htmai-880]

Hi @alkidbaci ,

First, thank you for looking into it!

To start you off, first set the environment to avoid getting the barrage of Java-side logging:

export JAVA_TOOL_OPTIONS="-Dorg.slf4j.simpleLogger.defaultLogLevel=off"

Then, you can try the following code, where I override the methods of the SyncReasoner with the "ideal" implementation where we wouldn't reason on a deep copy of the ontology:

import os
from typing import List, Set, Optional
from owlapy.owl_ontology import SyncOntology
from owlapy.owl_reasoner import SyncReasoner
from owlapy.owl_axiom import OWLClassAssertionAxiom, OWLAxiom
from owlapy.owl_individual import OWLNamedIndividual
from owlapy.iri import IRI
from owlapy.parser import manchester_to_owl_expression

from time import time

def initialize_reasoner_factory(reasoner: str):
    if reasoner == "HermiT":
        # noinspection PyUnresolvedReferences
        from org.semanticweb.HermiT import ReasonerFactory
        return ReasonerFactory()
    elif reasoner == "ELK":
        from org.semanticweb.elk.owlapi import ElkReasonerFactory
        return ElkReasonerFactory()
    elif reasoner == "JFact":
        # noinspection PyUnresolvedReferences
        from uk.ac.manchester.cs.jfact import JFactFactory
        return JFactFactory()
    elif reasoner == "Pellet":
        # noinspection PyUnresolvedReferences
        from openllet.owlapi import PelletReasonerFactory
        return PelletReasonerFactory.getInstance()
    elif reasoner == "Openllet":
        # noinspection PyUnresolvedReferences
        from openllet.owlapi import OpenlletReasonerFactory
        return OpenlletReasonerFactory().getInstance()
    elif reasoner == "Structural":
        # noinspection PyUnresolvedReferences
        from org.semanticweb.owlapi.reasoner.structural import StructuralReasonerFactory
        return StructuralReasonerFactory()
    else:
        raise NotImplementedError("Not implemented")


class SyncReasonerWithTimeout(SyncReasoner):


    def create_axiom_justifications(self,
                                    axiom_to_explain: OWLAxiom,
                                    n_max_justifications: Optional[int] = 10,
                                    timeout: Optional[int] = 1000,
                                    save: bool = False,
    ) -> List[Set[OWLAxiom]]:
        """For brievety, I removed the documentation.
        """
        # First verify that the axiom is even entailed
        if not self.is_entailed(axiom_to_explain):
            raise ValueError(
                f"The axiom {axiom_to_explain} is not entailed by the ontology. No justifications to create."
            )
        from com.clarkparsia.owlapi.explanation import (
            BlackBoxExplanation,
            HSTExplanationGenerator,
            SatisfiabilityConverter
        )
        from java.util.concurrent import CompletableFuture, TimeUnit, TimeoutException
  
        j_ontology = self._owlapi_ontology
        j_reasoner = self._owlapi_reasoner
        j_data_factory = self._owlapi_manager.getOWLDataFactory()
        j_reasoner_factory = initialize_reasoner_factory(self.reasoner_name)
        j_reasoner = self._owlapi_reasoner
        j_manager = self._owlapi_manager
            
        j_axiom = self.mapper.map_(axiom_to_explain)
        j_data_factory = j_manager.getOWLDataFactory()

        # Following the internal implementation of DefaultExplanationGenerator to circumvent the need for a progress monitor

        converter = SatisfiabilityConverter(j_data_factory)
        try:
            j_axiom_ce = converter.convert(j_axiom)
        except Exception as e:
            if "not implemented" in str(e).lower():
                raise NotImplementedError(
                    f"Failed to convert the axiom {axiom_to_explain} into a class expression. "
                    f"This most likely means that the axiom type {type(axiom_to_explain)} is not supported for justification generation.\n{str(e)}"
                )
            raise e
        blackbox_exp = BlackBoxExplanation(j_ontology, j_reasoner_factory, j_reasoner)
        explanation_gen = HSTExplanationGenerator(blackbox_exp)

        justifications = []
        if n_max_justifications is not None and not isinstance(
            n_max_justifications, int
        ):
            raise ValueError(
                f"n_max_justifications must be an integer or None, but got {n_max_justifications}"
            )
    
        if n_max_justifications is not None and n_max_justifications > 0:
            time_start = time()
            try:
                if timeout is None:
                    j_explanations = explanation_gen.getExplanations(
                        j_axiom_ce, n_max_justifications
                    )
                else:
                    future = CompletableFuture.supplyAsync(
                        lambda: explanation_gen.getExplanations(j_axiom_ce, n_max_justifications)
                    )
                    j_explanations = future.get(timeout, TimeUnit.SECONDS)
            except Exception as e:
                time_end = time()
                if isinstance(e, TimeoutException) and (timeout is not None):
                    raise TimeoutError(
                        f"Justification generation exceeded the timeout of {timeout} seconds. (Elapsed time: {time_end - time_start:.2f} seconds). "
                        f"Consider increasing the timeout or reducing the number of justifications to generate."
                    )
                if "not implemented" in str(e).lower():
                    raise ValueError(
                        f"Justification failed most likely because the axiom type {type(axiom_to_explain)} is not supported for justification generation.\n{str(e)}"
                    )
                raise e
        else:
            time_start = time()
            try:
                if timeout is None:
                    j_explanations = explanation_gen.getExplanations(j_axiom_ce)
                else:
                    future = CompletableFuture.supplyAsync(
                        lambda: explanation_gen.getExplanations(j_axiom_ce)
                    )
                    j_explanations = future.get(timeout, TimeUnit.SECONDS)
                    
            except Exception as e:
                time_end = time()
                if isinstance(e, TimeoutException) and (timeout is not None):
                    future.cancel(True)  # Attempt to cancel the task if it's still running
                    raise TimeoutError(
                        f"Justification generation exceeded the timeout of {timeout} seconds (elapsed: {time_end - time_start:.2f} seconds). "
                        f"Consider increasing the timeout or reducing the number of justifications to generate."
                    )
                if "not implemented" in str(e).lower():
                    raise ValueError(
                        f"Justification failed most likely because the axiom type {type(axiom_to_explain)} is not supported for justification generation.\n{str(e)}"
                    )
                raise e
            

        for j_expl in j_explanations:
            py_axioms = {self.mapper.map_(ax) for ax in j_expl}
            justifications.append(py_axioms)

        # Save to justifications.owl if requested
        if save:
            from owlapy.owl_ontology import SyncOntology
            from owlapy.iri import IRI

            # Create a new in-memory ontology to store justifications
            just_iri = IRI.create("http://example.org/justifications")
            just_ontology = SyncOntology(path=just_iri, load=False)

            for axiom_set in justifications:
                for axiom in axiom_set:
                    just_ontology.add_axiom(axiom)

            # Save to file
            save_path = "justifications.owl"
            just_ontology.save(save_path)
            print(f"Justifications saved to {os.path.abspath(save_path)}")

        return justifications



    def create_laconic_axiom_justifications(self,
        axiom_to_explain: OWLAxiom,
        n_max_justifications: Optional[int] = 10,
        timeout: Optional[int] = 1000,
        save: bool = False,
    ) -> List[Set[OWLAxiom]]:
        """For brievety, I removed the documentation.
        """
        # First verify that the axiom is even entailed
        if not self.is_entailed(axiom_to_explain):
            raise ValueError(
                f"The axiom {axiom_to_explain} is not entailed by the ontology. No justifications to create."
            )
        from com.clarkparsia.owlapi.explanation import (
            BlackBoxExplanation,
            HSTExplanationGenerator,
            SatisfiabilityConverter
        )
        from java.util.concurrent import CompletableFuture, TimeUnit, TimeoutException

        j_ontology = self._owlapi_ontology
        j_reasoner = self._owlapi_reasoner
        j_data_factory = self._owlapi_manager.getOWLDataFactory()
        j_reasoner_factory = initialize_reasoner_factory(self.reasoner_name)
        j_reasoner = self._owlapi_reasoner
        j_manager = self._owlapi_manager
            
        j_axiom = self.mapper.map_(axiom_to_explain)
        j_data_factory = j_manager.getOWLDataFactory()

        # Following the internal implementation of DefaultExplanationGenerator to circumvent the need for a progress monitor

        converter = SatisfiabilityConverter(j_data_factory)
        try:
            j_axiom_ce = converter.convert(j_axiom)
        except Exception as e:
            if "not implemented" in str(e).lower():
                raise NotImplementedError(
                    f"Failed to convert the axiom {axiom_to_explain} into a class expression. "
                    f"This most likely means that the axiom type {type(axiom_to_explain)} is not supported for justification generation.\n{str(e)}"
                )
            raise e
        
        blackbox_exp = BlackBoxExplanation(j_ontology, j_reasoner_factory, j_reasoner)
        explanation_gen = HSTExplanationGenerator(blackbox_exp)

        justifications = []
        if n_max_justifications is not None and not isinstance(
            n_max_justifications, int
        ):
            raise ValueError(
                f"n_max_justifications must be an integer or None, but got {n_max_justifications}"
            )
    
        if n_max_justifications is not None and n_max_justifications > 0:
            time_start = time()
            try:
                if timeout is None:
                    j_explanations = explanation_gen.getExplanations(
                        j_axiom_ce, n_max_justifications
                    )
                else:
                    future = CompletableFuture.supplyAsync(
                        lambda: explanation_gen.getExplanations(j_axiom_ce, n_max_justifications)
                    )
                    j_explanations = future.get(timeout, TimeUnit.SECONDS)
            except Exception as e:
                time_end = time()
                if isinstance(e, TimeoutException) and (timeout is not None):
                    future.cancel(True)  # Attempt to cancel the task if it's still running
                    raise TimeoutError(
                        f"Justification generation exceeded the timeout of {timeout} seconds. (Elapsed time: {time_end - time_start:.2f} seconds). "
                        f"Consider increasing the timeout or reducing the number of justifications to generate."
                    )
                if "not implemented" in str(e).lower():
                    raise ValueError(
                        f"Justification failed most likely because the axiom type {type(axiom_to_explain)} is not supported for justification generation.\n{str(e)}"
                    )
                raise e
        else:
            time_start = time()
            try:
                if timeout is None:
                    j_explanations = explanation_gen.getExplanations(j_axiom_ce)
                else:
                    future = CompletableFuture.supplyAsync(
                        lambda: explanation_gen.getExplanations(j_axiom_ce)
                    )
                    j_explanations = future.get(timeout, TimeUnit.SECONDS)
                    
            except Exception as e:
                time_end = time()
                if isinstance(e, TimeoutException) and (timeout is not None):
                    future.cancel(True)  # Attempt to cancel the task if it's still running
                    raise TimeoutError(
                        f"Justification generation exceeded the timeout of {timeout} seconds (elapsed: {time_end - time_start:.2f} seconds). "
                        f"Consider increasing the timeout or reducing the number of justifications to generate."
                    )
                if "not implemented" in str(e).lower():
                    raise ValueError(
                        f"Justification failed most likely because the axiom type {type(axiom_to_explain)} is not supported for justification generation.\n{str(e)}"
                    )
                raise e
            

        for j_expl in j_explanations:
            py_axioms = {self.mapper.map_(ax) for ax in j_expl}
            justifications.append(py_axioms)

        # Save to justifications.owl if requested
        if save:
            from owlapy.owl_ontology import SyncOntology
            from owlapy.iri import IRI

            # Create a new in-memory ontology to store justifications
            just_iri = IRI.create("http://example.org/justifications")
            just_ontology = SyncOntology(path=just_iri, load=False)

            for axiom_set in justifications:
                for axiom in axiom_set:
                    just_ontology.add_axiom(axiom)

            # Save to file
            save_path = "justifications.owl"
            just_ontology.save(save_path)
            print(f"Justifications saved to {os.path.abspath(save_path)}")

        return justifications
    

# Load ontology and reasoner
ontology = SyncOntology(
    "XXX/KGs/Carcinogenesis/carcinogenesis.owl"
)
# JVM is started from here
reasoner = SyncReasonerWithTimeout(ontology)

# Get some ontology statistics (e.g., signature size)
# Check number of axioms
print(f"Ontology contains {len(ontology.get_tbox_axioms())} TBox axioms")
print(f"Ontology contains {len(ontology.get_rbox_axioms())} RBox axioms")
print(f"Ontology contains {len(ontology.get_abox_axioms())} ABox axioms")

# The axiom to prove
manchester_expr = "Compound and hasAtom some Carbon"
owl_expr = manchester_to_owl_expression(
    manchester_expr, namespace="http://dl-learner.org/carcinogenesis#"
)
d100 = OWLNamedIndividual(
    IRI.create("http://dl-learner.org/carcinogenesis#d100")
)
axiom_to_prove = OWLClassAssertionAxiom(d100, owl_expr)

# Entailment check

t_0 = time()
is_entailed = reasoner.is_entailed(axiom_to_prove)
t_1 = time()
print(f"Time taken to check entailment: {t_1 - t_0} seconds")
print(f"Is the axiom {axiom_to_prove} entailed by the ontology? {is_entailed}")


try:
    t_0 = time()
    justifications = reasoner.create_axiom_justifications(
        axiom_to_prove, n_max_justifications=10, timeout=1
    )
    t_1 = time()
    print(
        f"Time taken to compute standard justifications: {t_1 - t_0} seconds. Justifications:"
    )
    print("Number of justifications generated before timeout:", len(justifications))
except TimeoutError as e:
    t_1 = time()
    print(
        f"Justification generation timed out after {t_1 - t_0} seconds. Error message: {str(e)}"
    )

# Check number of axioms again
print(f"Ontology contains {len(ontology.get_tbox_axioms())} TBox axioms")
print(f"Ontology contains {len(ontology.get_rbox_axioms())} RBox axioms")
print(f"Ontology contains {len(ontology.get_abox_axioms())} ABox axioms")
# Check if axiom is still entailed
is_entailed_after = reasoner.is_entailed(axiom_to_prove)
print(f"Is the axiom still entailed after justification attempts? {is_entailed_after}")

t_0 = time()
justifications = reasoner.create_axiom_justifications(
    axiom_to_prove, n_max_justifications=2, timeout=None
)
t_1 = time()
print(
    f"Time taken to compute standard justifications: {t_1 - t_0} seconds"
)
# How many justifications were generated?
print("Number of justifications generated:", len(justifications))

The output I get:

Picked up JAVA_TOOL_OPTIONS: -Dorg.slf4j.simpleLogger.defaultLogLevel=off
WARNING: A restricted method in java.lang.System has been called
WARNING: java.lang.System::load has been called by org.jpype.JPypeContext in an unnamed module (file:/home/XXX/owlapy-current/lib/python3.11/site-packages/org.jpype.jar)
WARNING: Use --enable-native-access=ALL-UNNAMED to avoid a warning for callers in this module
WARNING: Restricted methods will be blocked in a future release unless native access is enabled

WARNING: A terminally deprecated method in sun.misc.Unsafe has been called
WARNING: sun.misc.Unsafe::objectFieldOffset has been called by com.github.benmanes.caffeine.base.UnsafeAccess (file:/home/XXX/owlapy-current/lib/python3.11/site-packages/owlapy/jar_dependencies/caffeine-2.6.1.jar)
WARNING: Please consider reporting this to the maintainers of class com.github.benmanes.caffeine.base.UnsafeAccess
WARNING: sun.misc.Unsafe::objectFieldOffset will be removed in a future release
Ontology contains 182 TBox axioms
Ontology contains 0 RBox axioms
Ontology contains 74223 ABox axioms
Time taken to check entailment: 0.37525486946105957 seconds
Is the axiom OWLClassAssertionAxiom(individual=OWLNamedIndividual(IRI('http://dl-learner.org/carcinogenesis#', 'd100')),class_expression=OWLObjectIntersectionOf((OWLClass(IRI('http://dl-learner.org/carcinogenesis#', 'Compound')), OWLObjectSomeValuesFrom(property=OWLObjectProperty(IRI('http://dl-learner.org/carcinogenesis#', 'hasAtom')),filler=OWLClass(IRI('http://dl-learner.org/carcinogenesis#', 'Carbon'))))),annotations=[]) entailed by the ontology? True
Justification generation timed out after 1.418541669845581 seconds. Error message: Justification generation exceeded the timeout of 1 seconds. (Elapsed time: 1.00 seconds). Consider increasing the timeout or reducing the number of justifications to generate.
Ontology contains 179 TBox axioms
Ontology contains 0 RBox axioms
Ontology contains 74222 ABox axioms
Is the axiom still entailed after justification attempts? True
Traceback (most recent call last):
  File "HSTExplanationGenerator.java", line 200, in com.clarkparsia.owlapi.explanation.HSTExplanationGenerator.getExplanations
Exception: Java Exception

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/home/XXX/test_owlapy_justifications_timeout.py", line 443, in <module>
    justifications = reasoner.create_axiom_justifications(
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/XXX/test_owlapy_justifications_timeout.py", line 153, in create_axiom_justifications
    raise e
  File "/home/XXX/test_owlapy_justifications_timeout.py", line 134, in create_axiom_justifications
    j_explanations = explanation_gen.getExplanations(
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
java.util.java.util.ConcurrentModificationException: java.util.ConcurrentModificationException

Now, if I try to get laconic axiom justifications instead,

Picked up JAVA_TOOL_OPTIONS: -Dorg.slf4j.simpleLogger.defaultLogLevel=off
WARNING: A restricted method in java.lang.System has been called
WARNING: java.lang.System::load has been called by org.jpype.JPypeContext in an unnamed module (file:/home/XXX/owlapy-current/lib/python3.11/site-packages/org.jpype.jar)
WARNING: Use --enable-native-access=ALL-UNNAMED to avoid a warning for callers in this module
WARNING: Restricted methods will be blocked in a future release unless native access is enabled

WARNING: A terminally deprecated method in sun.misc.Unsafe has been called
WARNING: sun.misc.Unsafe::objectFieldOffset has been called by com.github.benmanes.caffeine.base.UnsafeAccess (file:/home/XXX/owlapy-current/lib/python3.11/site-packages/owlapy/jar_dependencies/caffeine-2.6.1.jar)
WARNING: Please consider reporting this to the maintainers of class com.github.benmanes.caffeine.base.UnsafeAccess
WARNING: sun.misc.Unsafe::objectFieldOffset will be removed in a future release
Ontology contains 182 TBox axioms
Ontology contains 0 RBox axioms
Ontology contains 74223 ABox axioms
Time taken to check entailment: 0.35181188583374023 seconds
Is the axiom OWLClassAssertionAxiom(individual=OWLNamedIndividual(IRI('http://dl-learner.org/carcinogenesis#', 'd100')),class_expression=OWLObjectIntersectionOf((OWLClass(IRI('http://dl-learner.org/carcinogenesis#', 'Compound')), OWLObjectSomeValuesFrom(property=OWLObjectProperty(IRI('http://dl-learner.org/carcinogenesis#', 'hasAtom')),filler=OWLClass(IRI('http://dl-learner.org/carcinogenesis#', 'Carbon'))))),annotations=[]) entailed by the ontology? True
Justification generation timed out after 1.6446363925933838 seconds. Error message: Justification generation exceeded the timeout of 1 seconds. (Elapsed time: 1.00 seconds). Consider increasing the timeout or reducing the number of justifications to generate.
Ontology contains 181 TBox axioms
Ontology contains 0 RBox axioms
Ontology contains 74222 ABox axioms
Is the axiom still entailed after justification attempts? True
Traceback (most recent call last):
  File "HSTExplanationGenerator.java", line 200, in com.clarkparsia.owlapi.explanation.HSTExplanationGenerator.getExplanations
Exception: Java Exception

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/home/XXX/test_owlapy_justifications_timeout.py", line 359, in <module>
    justifications = reasoner.create_laconic_axiom_justifications(
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/XXX/test_owlapy_justifications_timeout.py", line 250, in create_laconic_axiom_justifications
    raise e
  File "/home/XXX/test_owlapy_justifications_timeout.py", line 230, in create_laconic_axiom_justifications
    j_explanations = explanation_gen.getExplanations(
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
java.util.java.util.ConcurrentModificationException: java.util.ConcurrentModificationException

Now, notice that except for the glaringly obvious ConcurrentModificationException that is raised, the ontology signature has changed during the reasoning process.

[alkidbaci]

Hi @htmai-880, thanks for the details on the issue.

It seems like the reasoner modifies the ontology when trying to find justifications so if interrupted we deal with the ConcurrentModificationException.

Spent some time on it and I found a more optimal solution to avoid this error. For now, I have implemented it only for create_laconic_axiom_justifications. Instead of using the CompletableFuture.supplyAsync which will run a one-shot fire-and-forget thread I use a dedicated SingleThreadExecutor (from java.util.concurrent.Executors) with a daemon ThreadFactory, initialized on __init__. This executor is shared and reused across calls, serializing reasoning tasks to prevent concurrency issues (e.g. HermiT's non-reentrant ExtensionManager). Note that this can also be used for other methods to implement the timeout feature (like i have done with instances method).

Code for these changes can be found here.

Until now, I didn't find a weak point for this implementation but it may be early to say that it does not have any. If you got some time to test with your datasets and see for yourself, it would be a great feedback.

---

TL;DR
Also instead of using ExplanationManager to create the GeneratorFactory I used another class SatisfiabilityEntailmentCheckerFactory (combined with BlackBoxExplanationGeneratorFactory and Configuration) in order to pass the timeout argument to the cheker so that the checker itself is aware of the budget.
In the LaconicExplenationGeneratorFactory I pass a custom monitor _TimeoutProgressMonitor, that collects justifications as they're found (this has to be rethinked because I noticed that the list may be too long and not very worthy) and exposes an isCancelled() hook checked cooperatively by the explanation library. So basically the cancellation may be triggered by either the reasoning library finding out that the timeout limit has been passed or if that does not happen (because of some deep internal process) then the cancellation will be triggered by future.cancel(True), the harder fallback which will not cause the thread to stop because we are using SingleThreadExecutor.

[htmai-880]

Thanks a lot for looking into this! I'll run more tests on my end next week when I have the time. However, I would be greatly interested if such a feature could also be implemented for standard axiom justifications.

[alkidbaci]

Timeout arg is now added for the create_axiom_justifications method as well.
Same branch as before: https://github.com/dice-group/owlapy/blob/timeout-feature/owlapy/owl_reasoner.py