f26489cf50364d60a14c9bf33ca2c91855ad438aChristian Maeder{- |

9658657e918981d91c8647ed8c220464f10a6235Christian MaederModule : $Header$

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederDescription : Gtk GUI for the consistency checker

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiCopyright : (c) Thiemo Wiedemeyer, Uni Bremen 2009

d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederMaintainer : raider@informatik.uni-bremen.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : portable

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederThis module provides a GUI for the consistency checker.

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski-}

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maedermodule GUI.GtkConsistencyChecker where

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Graphics.UI.Gtk

63719301448519453f66383f4e583d9fd5b89ecbChristian Maederimport Graphics.UI.Gtk.Glade

ae35311385999d91f812155fe99439724d54063bChristian Maeder

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport GUI.GtkUtils

3143271856dbf456bd7acc1c07193173f886d986Christian Maederimport qualified GUI.Glade.NodeChecker as ConsistencyChecker

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport GUI.GraphTypes

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport Static.DevGraph

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederimport Static.PrintDevGraph ()

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederimport Static.GTheory

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Static.History

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Interfaces.GenericATPState (guiDefaultTimeLimit)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maederimport Logic.Grothendieck

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Comorphism (AnyComorphism (..))

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport Logic.Prover

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport Comorphisms.LogicGraph (logicGraph)

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport Common.DocUtils

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport Common.LibName (LibName)

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowskiimport Common.Result

b4d51ce3a34a074859f5f34cf430307f5963f912Christian Maederimport Common.Consistency

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maederimport Control.Concurrent (forkIO, killThread)

c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maederimport Control.Concurrent.MVar

3986813db69106b9bb1b62faa77532af42512a0cChristian Maederimport Control.Monad (foldM_, join, when)

3986813db69106b9bb1b62faa77532af42512a0cChristian Maeder

3986813db69106b9bb1b62faa77532af42512a0cChristian Maederimport Proofs.AbstractState

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maederimport Proofs.ConsistencyCheck

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maeder

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maederimport Data.Graph.Inductive.Graph (LNode)

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport qualified Data.Map as Map

e982190515f83fe6615436530ebe89bb320770d6Christian Maederimport Data.List (findIndex, partition, sort)

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport Data.Maybe

f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maederdata Finder = Finder { fName :: String

d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian Maeder , finder :: G_cons_checker

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder , comorphism :: [AnyComorphism]

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder , selected :: Int }

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maederinstance Eq Finder where

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder (==) (Finder { fName = n1, comorphism = c1 })

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder (Finder { fName = n2, comorphism = c2 }) = n1 == n2 && c1 == c2

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maederdata FNode = FNode { name :: String

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder , node :: LNode DGNodeLab

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder , sublogic :: G_sublogics

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich , cStatus :: ConsistencyStatus }

1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | Get a markup string containing name and color

2dcec0e101ddd4169f5323462911e988337c2deeChristian Maederinstance Show FNode where

0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus Luettich show FNode { name = n, cStatus = s } =

9f08800df9da91d444560875167fbf7acb8396edChristian Maeder "<span color=\"" ++ cStatusToColor s ++ "\">" ++ cStatusToPrefix s ++ n ++

333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder "</span>"

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederinstance Eq FNode where

64c2422e1ba0691556a6639e959820add102315cChristian Maeder (==) f1 f2 = compare f1 f2 == EQ

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Ord FNode where

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder compare (FNode { name = n1, cStatus = s1 })

865ae561becd3cb451d6280125886b3e03ddf0a4Hendrik Iben (FNode { name = n2, cStatus = s2 }) = case compare s1 s2 of

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder EQ -> compare n1 n2

865ae561becd3cb451d6280125886b3e03ddf0a4Hendrik Iben c -> c

b83ff3749d99d03b641adee264b781039a551addChristian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian MaedercStatusToColor :: ConsistencyStatus -> String

63719301448519453f66383f4e583d9fd5b89ecbChristian MaedercStatusToColor s = case sType s of

c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maeder CSUnchecked -> "black"

c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maeder CSConsistent -> "green"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder CSInconsistent -> "red"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder CSTimeout -> "blue"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder CSError -> "darkred"

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian MaedercStatusToPrefix :: ConsistencyStatus -> String

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian MaedercStatusToPrefix s = case sType s of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder CSUnchecked -> "[ ] "

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder CSConsistent -> "[+] "

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder CSInconsistent -> "[-] "

fe4e6766a6e51cca3f8cc9632c25936af147d8b9Christian Maeder CSTimeout -> "[t] "

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder CSError -> "[f] "

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian MaedercInvert :: ConsistencyStatus -> ConsistencyStatus

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian MossakowskicInvert cs = case sType cs of

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder CSConsistent -> ConsistencyStatus CSInconsistent (sMessage cs)

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder CSInconsistent -> ConsistencyStatus CSConsistent (sMessage cs)

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder _ -> cs

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder-- | Displays the consistency checker window

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian MaedershowConsistencyChecker :: Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)

63719301448519453f66383f4e583d9fd5b89ecbChristian MaedershowConsistencyChecker mn gi@(GInfo { libName = ln }) le =

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder case mn of

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder Nothing -> showConsistencyCheckerMain mn gi le

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder Just n -> let

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder dg = lookupDGraph ln le

d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian Maeder lbl = labDG dg n

d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian Maeder in if case globalTheory lbl of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just (G_theory _ _ _ sens _) -> Map.null sens

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Nothing -> True

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder then do

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder infoDialogExt "No sentences" $ "Node " ++

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder getDGNodeName lbl

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder ++ " has no sentences and is thus trivially consistent"

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder return $ return le

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder else showConsistencyCheckerMain mn gi le

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder-- | Displays the consistency checker window

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian MaedershowConsistencyCheckerMain :: Maybe Int -> GInfo -> LibEnv -> IO (Result LibEnv)

63719301448519453f66383f4e583d9fd5b89ecbChristian MaedershowConsistencyCheckerMain mn (GInfo { libName = ln }) le = do

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder wait <- newEmptyMVar

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder showConsistencyCheckerAux wait mn ln le

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder le' <- takeMVar wait

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder return $ Result [] $ Just le'

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder-- | Displays the consistency checker window

63719301448519453f66383f4e583d9fd5b89ecbChristian MaedershowConsistencyCheckerAux

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder :: MVar LibEnv -> Maybe Int -> LibName -> LibEnv -> IO ()

63719301448519453f66383f4e583d9fd5b89ecbChristian MaedershowConsistencyCheckerAux res mn ln le = postGUIAsync $ do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder xml <- getGladeXML ConsistencyChecker.get

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -- get objects

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder window <- xmlGetWidget xml castToWindow "NodeChecker"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder btnClose <- xmlGetWidget xml castToButton "btnClose"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder btnResults <- xmlGetWidget xml castToButton "btnResults"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -- get nodes view and buttons

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder trvNodes <- xmlGetWidget xml castToTreeView "trvNodes"

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"

5382091fd2a705e6f026026e8a6adcd3607bdb9fChristian Maeder -- get checker view and buttons

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder btnCheck <- xmlGetWidget xml castToButton "btnCheck"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder btnStop <- xmlGetWidget xml castToButton "btnStop"

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder windowSetTitle window "Consistency Checker"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit

25662bf82f592e3268fddcc2c86e83c203b82e53Ewaryst Schulz

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder let widgets = [ toWidget sbTimeout

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu , toWidget cbComorphism

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu , toWidget lblSublogic ]

25662bf82f592e3268fddcc2c86e83c203b82e53Ewaryst Schulz checkWidgets = widgets ++ [ toWidget btnClose

21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder , toWidget btnNodesAll

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder , toWidget btnNodesNone

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder , toWidget btnNodesInvert

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder , toWidget btnNodesUnchecked

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder , toWidget btnNodesTimeout

25662bf82f592e3268fddcc2c86e83c203b82e53Ewaryst Schulz , toWidget btnResults ]

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu switch b = do

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu widgetSetSensitive btnStop $ not b

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder widgetSetSensitive btnCheck b

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder widgetSetSensitive btnStop False

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder widgetSetSensitive btnCheck False

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder threadId <- newEmptyMVar

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder wait <- newEmptyMVar

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder mView <- newEmptyMVar

b4d51ce3a34a074859f5f34cf430307f5963f912Christian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder let dg = lookupDGraph ln le

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder nodes = labNodesDG dg

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder selNodes = partition (\ (FNode { node = (_, l)}) -> case globalTheory l of

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder Just (G_theory _ _ _ sens _) -> Map.null sens

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Nothing -> True)

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder sls = map sublogicOfTh $ mapMaybe (globalTheory . snd) nodes

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder n2CS n = case getNodeConsStatus n of

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder ConsStatus _ pc thmls ->

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder let t = showDoc thmls "" in case pc of

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder Inconsistent -> ConsistencyStatus CSInconsistent t

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder Cons -> ConsistencyStatus CSConsistent t

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder _ -> ConsistencyStatus CSUnchecked t

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder (emptyNodes, others) = selNodes

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder $ map (\ (n@(_, l), s) -> FNode (getDGNodeName l) n s $ n2CS l)

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder $ zip nodes sls

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder -- setup data

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder listNodes <- setListData trvNodes show $ sort others

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder listFinder <- setListData trvFinder fName []

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder -- setup comorphism combobox

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder comboBoxSetModelText cbComorphism

b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder shC <- after cbComorphism changed

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder $ setSelectedComorphism trvFinder listFinder cbComorphism

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder -- setup view selection actions

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let update = do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder mf <- getSelectedSingle trvFinder listFinder

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder updateComorphism trvFinder listFinder cbComorphism shC

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder widgetSetSensitive btnCheck $ isJust mf

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder setListSelectorSingle trvFinder update

b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let upd = updateNodes trvNodes listNodes

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder (\ b s -> do

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski labelSetLabel lblSublogic $ show s

8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder updateFinder trvFinder listFinder b s)

8865728716566f42fa73e7e0bc080ba3225df764Christian Maeder (do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder labelSetLabel lblSublogic "No sublogic"

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder listStoreClear listFinder

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder activate widgets False

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder widgetSetSensitive btnCheck False)

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder (activate widgets True >> widgetSetSensitive btnCheck True)

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder shN <- setListSelectorMultiple trvNodes btnNodesAll btnNodesNone

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder btnNodesInvert upd

36f69d35e01d2d6b6bdc165b49661f2a80af8687Mihai Codescu

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -- bindings

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder let selectWithAux f u = do

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder signalBlock shN

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder sel <- treeViewGetSelection trvNodes

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder treeSelectionSelectAll sel

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder rs <- treeSelectionGetSelectedRows sel

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder mapM_ ( \ ~p@(row : []) -> do

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder fn <- listStoreGetValue listNodes row

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder (if f fn then treeSelectionSelectPath else treeSelectionUnselectPath)

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder sel p) rs

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder signalUnblock shN

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder u

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder selectWith f = selectWithAux $ f . cStatus

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder onClicked btnNodesUnchecked

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $ selectWith (== ConsistencyStatus CSUnchecked "") upd

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder onClicked btnNodesTimeout $ selectWith (== ConsistencyStatus CSTimeout "") upd

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder onClicked btnResults $ showModelView mView "Models" listNodes emptyNodes

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder onClicked btnClose $ widgetDestroy window

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder onClicked btnCheck $ do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder activate checkWidgets False

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder timeout <- spinButtonGetValueAsInt sbTimeout

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder inclThms <- toggleButtonGetActive cbInclThms

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder (updat, pexit) <- progressBar "Checking consistency" "please wait..."

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder nodes' <- getSelectedMultiple trvNodes listNodes

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder mf <- getSelectedSingle trvFinder listFinder

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder f <- case mf of

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder Nothing -> error "Consistency checker: internal error"

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder Just (_, f) -> return f

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder switch False

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder tid <- forkIO $ do

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder check False inclThms ln le dg f timeout listNodes updat nodes'

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder putMVar wait ()

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder putMVar threadId tid

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder forkIO_ $ do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder takeMVar wait

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder postGUIAsync $ do

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder switch True

7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder tryTakeMVar threadId

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder showModelView mView "Results of consistency check" listNodes emptyNodes

9f08800df9da91d444560875167fbf7acb8396edChristian Maeder signalBlock shN

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder sortNodes trvNodes listNodes

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder signalUnblock shN

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder upd

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder activate checkWidgets True

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder pexit

efb44558d78b59ea6ce8c16cb5eb1ac0a2604c84Christian Maeder

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder onDestroy window $ do

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder nodes' <- listStoreToList listNodes

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder let changes = foldl (\ cs (FNode { node = (i, l), cStatus = s }) ->

7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder if (\ st -> st /= CSConsistent && st /= CSInconsistent)

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder $ sType s then cs

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder else

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder let n = (i, if sType s == CSInconsistent then

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder markNodeInconsistent "" l

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder else markNodeConsistent "" l)

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder in SetNodeLab l n : cs

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder ) [] nodes'

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder dg' = changesDGH dg changes

putMVar res $ Map.insert ln (groupHistory dg (DGRule "Consistency") dg') le

selectWithAux (maybe ((== ConsistencyStatus CSUnchecked "") . cStatus)

(\ n -> (== n) . fst . node) mn) upd

widgetShow window

sortNodes :: TreeView -> ListStore FNode -> IO ()

sortNodes trvNodes listNodes = do

sel <- getSelectedMultiple trvNodes listNodes

nodes <- listStoreToList listNodes

let sn = sort nodes

updateListData listNodes sn

selector <- treeViewGetSelection trvNodes

mapM_ (\ (_, FNode { name = n }) -> treeSelectionSelectPath selector

[fromMaybe (error "Node not found!") $ findIndex ((n ==) . name) sn]

) sel

-- | Called when node selection is changed. Updates finder list

updateNodes :: TreeView -> ListStore FNode -> (Bool -> G_sublogics -> IO ())

-> IO () -> IO () -> IO ()

updateNodes view listNodes update lock unlock = do

nodes <- getSelectedMultiple view listNodes

if null nodes then lock

else let sls = map (sublogic . snd) nodes in

maybe lock (\ sl -> unlock >> update (length nodes == 1) sl)

$ foldl (\ ma b -> case ma of

Just a -> joinSublogics b a

Nothing -> Nothing) (Just $ head sls) $ tail sls

-- | Update the list of finder

updateFinder :: TreeView -> ListStore Finder -> Bool -> G_sublogics -> IO ()

updateFinder view list useNonBatch sl = do

old <- listStoreToList list

let new = Map.elems $ foldr (\ (cc, c) m ->

let n = getCcName cc

f = Map.findWithDefault (Finder n cc [] 0) n m

in Map.insert n (f { comorphism = c : comorphism f}) m) Map.empty

$ filter (\ (G_cons_checker _ cc, _) -> useNonBatch || ccBatch cc)

$ getConsCheckers $ findComorphismPaths logicGraph sl

when (old /= new) $ do

-- update list and try to select previous finder

selected' <- getSelectedSingle view list

sel <- treeViewGetSelection view

listStoreClear list

mapM_ (listStoreAppend list) $ mergeFinder old new

maybe (selectFirst view)

(\ (_, f) -> let i = findIndex ((fName f ==) . fName) new in

maybe (selectFirst view) (treeSelectionSelectPath sel . (: [])) i

) selected'

-- | Try to select previous selected comorphism if possible

mergeFinder :: [Finder] -> [Finder] -> [Finder]

mergeFinder old new = let m' = Map.fromList $ map (\ f -> (fName f, f)) new in

Map.elems $ foldl (\ m (Finder { fName = n, comorphism = cc, selected = i}) ->

case Map.lookup n m of

Nothing -> m

Just f@(Finder { comorphism = cc' }) -> let c = cc !! i in

Map.insert n (f { selected = fromMaybe 0 $ findIndex (== c) cc' }) m

) m' old

check :: Bool -> Bool -> LibName -> LibEnv -> DGraph -> Finder -> Int

-> ListStore FNode -> (Double -> String -> IO ()) -> [(Int, FNode)]

-> IO ()

check dispr inclThms ln le dg (Finder _ cc cs i) timeout listNodes update

nodes = let

count' = fromIntegral $ length nodes

c = cs !! i in

foldM_ (\ count (row, fn@(FNode { name = n', node = n })) -> do

postGUISync $ update (count / count') n'

res <- consistencyCheck inclThms cc c ln le dg n timeout

let res' = if dispr then cInvert res else res

postGUISync $ listStoreSetValue listNodes row fn { cStatus = res' }

return $ count + 1) 0 nodes

updateComorphism :: TreeView -> ListStore Finder -> ComboBox

-> ConnectId ComboBox -> IO ()

updateComorphism view list cbComorphism sh = do

signalBlock sh

model <- comboBoxGetModelText cbComorphism

listStoreClear model

mfinder <- getSelectedSingle view list

case mfinder of

Just (_, f) -> do

mapM_ (comboBoxAppendText cbComorphism) $ expand f

comboBoxSetActive cbComorphism $ selected f

Nothing -> return ()

signalUnblock sh

expand :: Finder -> [String]

expand = map show . comorphism

setSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()

setSelectedComorphism view list cbComorphism = do

mfinder <- getSelectedSingle view list

case mfinder of

Just (i, f) -> do

sel <- comboBoxGetActive cbComorphism

listStoreSetValue list i f { selected = sel }

Nothing -> return ()

-- | Displays the model view window

showModelViewAux :: MVar (IO ()) -> String -> ListStore FNode -> [FNode]

-> IO ()

showModelViewAux lock title list other = do

xml <- getGladeXML ConsistencyChecker.get

-- get objects

window <- xmlGetWidget xml castToWindow "ModelView"

btnClose <- xmlGetWidget xml castToButton "btnResClose"

frNodes <- xmlGetWidget xml castToFrame "frResNodes"

trvNodes <- xmlGetWidget xml castToTreeView "trvResNodes"

tvModel <- xmlGetWidget xml castToTextView "tvResModel"

windowSetTitle window title

-- setup text view

buffer <- textViewGetBuffer tvModel

textBufferInsertAtCursor buffer ""

tagTable <- textBufferGetTagTable buffer

font <- textTagNew Nothing

set font [ textTagFont := "FreeMono" ]

textTagTableAdd tagTable font

start <- textBufferGetStartIter buffer

end <- textBufferGetEndIter buffer

textBufferApplyTag buffer font start end

-- setup list view

let filterNodes = filter ((/= ConsistencyStatus CSUnchecked "") . cStatus)

nodes <- listStoreToList list

listNodes <- setListData trvNodes show $ sort $ filterNodes $ other ++ nodes

setListSelectorSingle trvNodes $ do

mn <- getSelectedSingle trvNodes listNodes

case mn of

Nothing -> textBufferSetText buffer ""

Just (_, n) -> textBufferSetText buffer $ show $ cStatus n

-- setup actions

onClicked btnClose $ widgetDestroy window

onDestroy window $ takeMVar lock >>= const (return ())

putMVar lock $ do

sel' <- getSelectedSingle trvNodes listNodes

sel <- treeViewGetSelection trvNodes

nodes'' <- listStoreToList list

let nodes' = sort $ filterNodes nodes''

updateListData listNodes $ sort (other ++ nodes')

maybe (selectFirst trvNodes) (treeSelectionSelectPath sel . (: []))

$ maybe Nothing (\ (_, n) -> findIndex ((name n ==) . name) nodes') sel'

selectFirst trvNodes

widgetSetSizeRequest window 800 600

widgetSetSizeRequest frNodes 250 (-1)

widgetShow window

-- | Displays the model view window

showModelView :: MVar (IO ()) -> String -> ListStore FNode -> [FNode] -> IO ()

showModelView lock title list other = do

isNotOpen <- isEmptyMVar lock

if isNotOpen then showModelViewAux lock title list other

else join (readMVar lock)