Conservativity.hs revision a604cbad8e2202147b5c6bb9f2e06ae61162d654
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Dominik Luecke, 2008
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : luecke@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : non-portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederThis module implements conservativity checks for OWL 2.0 based on the
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederthe syntactic locality checker written in Java from the OWL-Api.
08e5741dd8b6bf9b7419e89298e384e18bc57f64Christian Maeder ( localityJar
08e5741dd8b6bf9b7419e89298e384e18bc57f64Christian Maeder , conserCheck
c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport OWL2.FunctionalPrint (printOWLBasicTheory)
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till MossakowskilocalityJar :: String
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder-- | Conservativity Check for Propositional Logic
d67a33b40578beef2e255a274f89bb9c34aaf056Christian MaederconserCheck :: String -- ^ Conser type
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder -> (Sign, [Named Axiom]) -- ^ Initial sign and formulas
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder -> OWLMorphism -- ^ morphism between specs
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder -> [Named Axiom] -- ^ Formulas of extended spec
6e049108aa87dc46bcff96fae50a4625df1d9648Klaus Luettich -> IO (Result (Maybe (Conservativity, [Axiom])))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederconserCheck ct = uncurry $ doConservCheck localityJar ct
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian Maeder-- | Real conservativity check in IO Monad
c6fcd42c6d6d9dae8c7835c24fcb7ce8531a9050Christian MaederdoConservCheck :: String -- ^ Jar name
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski -> String -- ^ Conser Type
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus Luettich -> Sign -- ^ Signature of Onto 1
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> [Named Axiom] -- ^ Formulas of Onto 1
857992065be4ed40a72c6296b6c0aec62ab4c5b9Christian Maeder -> OWLMorphism -- ^ Morphism
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich -> [Named Axiom] -- ^ Formulas of Onto 2
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder -> IO (Result (Maybe (Conservativity, [Axiom])))
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederdoConservCheck jar ct sig1 sen1 mor sen2 =
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let ontoFile = printOWLBasicTheory (otarget mor, filter isAxiom sen2)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder sigFile = printOWLBasicTheory (sig1, filter isAxiom sen1)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder in runLocalityChecker jar ct (show ontoFile) (show sigFile)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder-- | Invoke the Java checker
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederrunLocalityChecker :: String -- ^ Jar name
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder -> String -- ^ Conser Type
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder -> String -- ^ Ontology
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder -> String -- ^ String
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder -> IO (Result (Maybe (Conservativity, [Axiom])))
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederrunLocalityChecker jar ct onto sig = do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (progTh, toolPath) <- check4HetsOWLjar jar
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder if progTh then withinDirectory toolPath $ do
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich sigFile <- getTempFile sig "ConservativityCheck.sig.owl"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let tLimit = 800
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder ontoFile = sigFile ++ ".onto.owl"
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich jargs = ["-jar", jar, "file://" ++ ontoFile, "file://" ++ sigFile, ct]
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich writeFile ontoFile onto
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich mExit <- timeoutCommand tLimit "java" jargs
5d4038657f6a63e131f5804af2f7957b69e15a43Klaus Luettich removeFile ontoFile
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder removeFile sigFile
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder return $ case mExit of
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just (cont, out, _) -> parseOutput out cont
77a65251ee036c6aaf09c2775315a4ee24259fbdJorina Freya Gerken Nothing -> fail $ "Timelimit " ++ show tLimit ++ " exceeded"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder else return $ fail $ jar ++ " not found"
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaederparseOutput :: String
97812b7ce9860bf514a8822a63503451795dbc65Klaus Luettich -> Result (Maybe (Conservativity, [Axiom]))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederparseOutput ls1 exit = do
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let ls = lines ls1
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ExitFailure 10 -> return $ Just (Cons, [])
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ExitFailure 20 -> fail $ unlines ls
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder x -> fail $ "Internal program error: " ++ show x ++ "\n" ++ unlines ls