Added a feature to ReasonOperation where an unsatisfiable module can be dumped (174) #324
Conversation
…be dumped for debugging purposes. Fixes #174 - Added documentation to reason.md - Added command (-D option) - Function is isolated n ReasonerHelper static class
|
The logic here is a little squirrely. The "core dump" only happens if the ontology is incoherent, which triggers an exception. Before the exception is thrown, the module is (optionally) dumped. See if it makes sense... |
|
I think I get it. The unit test loads |
There was a problem hiding this comment.
I tested it on the incoherent-tbox.owl file and it returned as expected (though that was the whole module, so I wasn't able to check if things are properly excluded).
Just out of curiosity I also ran it on inconsistent.owl - this one fails without any message, other than "use -vvv for stack trace". In the stack trace, you get a InconsistentOntologyException which is expected, but maybe we should add some ERROR logging to this as well?
|
@jamesaoverton I think you meant tbox not xbox? I usually often to add test files but I think I got them all this time. @rctauber - I'm not sure how to best make a module for inconsistent ontologies. I think we would need to use the explanation feature. Even if there is unsatisfiability at the root of the inconsistency, Elk will not let you ask for unsats if the ontology is inconsistent. But yes the reporting should be better. I just pushed a change that (a) reports if the ontology is inconsistent in all cases (b) apologizes for not being able to make an unsat dump if this was asked for |
|
Ok. I love my Xbox. |
Fixes #174