2665d7759e63acff0bcd4135678f2cc6f2041d46Christian Maeder{- |

9658657e918981d91c8647ed8c220464f10a6235Christian MaederModule : $Header$

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederDescription : Gtk GUI for the consistency checker

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

d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

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

bdeddba30d29f413af1e1ae6b6bab275c017bd98Christian Maeder (showConsistencyChecker)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder where

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

ae35311385999d91f812155fe99439724d54063bChristian Maederimport Graphics.UI.Gtk

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport Graphics.UI.Gtk.Glade

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport GUI.GtkUtils

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport qualified GUI.Glade.NodeChecker as ConsistencyChecker

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport GUI.GraphTypes

52e573502bb19ca616ea63283d58ba73f39675d2Christian Maeder

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederimport Static.DevGraph

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederimport Static.PrintDevGraph ()

697e63e30aa3c309a1ef1f9357745111f8dfc5a9Christian Maederimport Static.GTheory

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Static.History

8e537a087207fb2ea9073ea66776c36b821a58c6Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Interfaces.GenericATPState (guiDefaultTimeLimit)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maederimport Logic.Grothendieck

520c5bce318eff52d9315f7c4491c3381a0c4336Christian Maederimport Logic.Comorphism (AnyComorphism (..))

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Prover

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder

411392046c2ba1752cde81eaa92a95a2c28b672dChristian Maederimport Comorphisms.LogicGraph (logicGraph)

f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport Common.DocUtils

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport Common.LibName (LibName)

46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport Common.Result

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport Common.Consistency

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowskiimport Control.Concurrent (forkIO, killThread)

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maederimport Control.Concurrent.MVar

c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maederimport Control.Monad (foldM_, join, when)

3986813db69106b9bb1b62faa77532af42512a0cChristian Maeder

3986813db69106b9bb1b62faa77532af42512a0cChristian Maederimport Proofs.AbstractState

3986813db69106b9bb1b62faa77532af42512a0cChristian Maederimport Proofs.InferBasic

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maeder

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

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maederimport qualified Data.Map as Map

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport Data.List (findIndex, partition, sort)

e982190515f83fe6615436530ebe89bb320770d6Christian Maederimport Data.Maybe

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder

f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichdata Finder = Finder { fName :: String

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder , finder :: G_cons_checker

d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian Maeder , comorphism :: [AnyComorphism]

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder , selected :: Int }

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulzinstance Eq Finder where

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz (==) (Finder { fName = n1, comorphism = c1 })

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz (Finder { fName = n2, comorphism = c2 }) = n1 == n2 && c1 == c2

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maederdata FNode = FNode { name :: String

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder , node :: LNode DGNodeLab

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder , sublogic :: G_sublogics

9b6a888fced92090f2f3d60f551b8bf38bf2eecbChristian Maeder , status :: ConsistencyStatus }

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder-- | Get a markup string containing name and color

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maederinstance Show FNode where

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder show FNode { name = n, status = s } =

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

961978c71545e0177683279f8b63358b3e3804b8Christian Maeder "</span>"

961978c71545e0177683279f8b63358b3e3804b8Christian Maeder

e4f0eaffd002e9e553ee113be33f9aa6e4181c43Christian Maederinstance Eq FNode where

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance (==) f1 f2 = compare f1 f2 == EQ

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksainstance Ord FNode where

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa compare (FNode { name = n1, status = s1 })

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa (FNode { name = n2, status = s2 }) = case compare s1 s2 of

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich EQ -> compare n1 n2

1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder c -> c

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

2dcec0e101ddd4169f5323462911e988337c2deeChristian MaedercStatusToColor :: ConsistencyStatus -> String

0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus LuettichcStatusToColor s = case sType s of

9f08800df9da91d444560875167fbf7acb8396edChristian Maeder CSUnchecked -> "black"

333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder CSConsistent -> "green"

bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder CSInconsistent -> "red"

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder CSTimeout -> "blue"

64c2422e1ba0691556a6639e959820add102315cChristian Maeder CSError -> "darkred"

938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz

4c8d3c5a9e938633f6147b5a595b9b93bfca99e6Christian MaedercStatusToPrefix :: ConsistencyStatus -> String

b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercStatusToPrefix s = case sType s of

63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz CSUnchecked -> "[ ] "

63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz CSConsistent -> "[+] "

f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz CSInconsistent -> "[-] "

b83ff3749d99d03b641adee264b781039a551addChristian Maeder CSTimeout -> "[t] "

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder CSError -> "[f] "

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

520c5bce318eff52d9315f7c4491c3381a0c4336Christian Maeder-- | Displays the consistency checker window

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

0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst SchulzshowConsistencyChecker mn (GInfo { libName = ln }) le = do

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz wait <- newEmptyMVar

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz showConsistencyCheckerAux wait mn ln le

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz le' <- takeMVar wait

0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz return $ Result [] $ Just le'

961978c71545e0177683279f8b63358b3e3804b8Christian Maeder

938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz-- | Displays the consistency checker window

0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst SchulzshowConsistencyCheckerAux

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

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian MaedershowConsistencyCheckerAux res mn ln le = postGUIAsync $ do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder xml <- getGladeXML ConsistencyChecker.get

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder -- get objects

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder window <- xmlGetWidget xml castToWindow "NodeChecker"

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

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

a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maeder -- get nodes view and buttons

d864f0a0e04e61b5f87963496765eafcf646ed7bChristian Maeder trvNodes <- xmlGetWidget xml castToTreeView "trvNodes"

72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz btnNodesAll <- xmlGetWidget xml castToButton "btnNodesAll"

5ca1fe655d7d4e35e59a082b5955b306643329d0Ewaryst Schulz btnNodesNone <- xmlGetWidget xml castToButton "btnNodesNone"

5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulz btnNodesInvert <- xmlGetWidget xml castToButton "btnNodesInvert"

5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulz btnNodesUnchecked <- xmlGetWidget xml castToButton "btnNodesUnchecked"

bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz btnNodesTimeout <- xmlGetWidget xml castToButton "btnNodesTimeout"

0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz cbInclThms <- xmlGetWidget xml castToCheckButton "cbInclThms"

5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulz -- get checker view and buttons

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder cbComorphism <- xmlGetWidget xml castToComboBox "cbComorphism"

4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder lblSublogic <- xmlGetWidget xml castToLabel "lblSublogic"

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder sbTimeout <- xmlGetWidget xml castToSpinButton "sbTimeout"

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski btnCheck <- xmlGetWidget xml castToButton "btnCheck"

aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian Maeder btnStop <- xmlGetWidget xml castToButton "btnStop"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder trvFinder <- xmlGetWidget xml castToTreeView "trvFinder"

aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian Maeder

53e165a53dfa59f717588d1f8236c9a763826525Christian Maeder windowSetTitle window "Consistency Checker"

53e165a53dfa59f717588d1f8236c9a763826525Christian Maeder spinButtonSetValue sbTimeout $ fromIntegral guiDefaultTimeLimit

1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder

aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian Maeder let widgets = [ toWidget sbTimeout

53e165a53dfa59f717588d1f8236c9a763826525Christian Maeder , toWidget cbComorphism

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder , toWidget lblSublogic ]

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder checkWidgets = widgets ++ [ toWidget btnClose

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder , toWidget btnNodesAll

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder , toWidget btnNodesNone

d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian Maeder , toWidget btnNodesInvert

d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian Maeder , toWidget btnNodesUnchecked

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder , toWidget btnNodesTimeout

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder , toWidget btnResults ]

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder switch b = do

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder widgetSetSensitive btnStop $ not b

074f8feaf71e0b71a95145e7439746f8eb8e2a7cChristian Maeder widgetSetSensitive btnCheck b

074f8feaf71e0b71a95145e7439746f8eb8e2a7cChristian Maeder

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz widgetSetSensitive btnStop False

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz widgetSetSensitive btnCheck False

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz threadId <- newEmptyMVar

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa wait <- newEmptyMVar

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder mView <- newEmptyMVar

e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder let dg = lookupDGraph ln le

074f8feaf71e0b71a95145e7439746f8eb8e2a7cChristian Maeder nodes = filter (maybe (const True) (==) mn . fst) $ labNodesDG dg

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

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

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder Nothing -> True)

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

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder n2CS n = case getNodeConsStatus n of

e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder ConsStatus _ pc thmls ->

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

e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder Inconsistent -> ConsistencyStatus CSInconsistent t

e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder Cons -> ConsistencyStatus CSConsistent t

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder _ -> ConsistencyStatus CSUnchecked t

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder (emptyNodes, others) = selNodes

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

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $ zip nodes sls

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -- setup data

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder listNodes <- setListData trvNodes show $ sort others

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder listFinder <- setListData trvFinder fName []

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -- setup comorphism combobox

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder comboBoxSetModelText cbComorphism

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder shC <- after cbComorphism changed

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder $ setSelectedComorphism trvFinder listFinder cbComorphism

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder

a7b34c1a61dabe150288424d90389d5988bf9d7aChristian Maeder -- setup view selection actions

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa let update = do

a7b34c1a61dabe150288424d90389d5988bf9d7aChristian Maeder mf <- getSelectedSingle trvFinder listFinder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder updateComorphism trvFinder listFinder cbComorphism shC

52e573502bb19ca616ea63283d58ba73f39675d2Christian Maeder widgetSetSensitive btnCheck $ isJust mf

5382091fd2a705e6f026026e8a6adcd3607bdb9fChristian Maeder setListSelectorSingle trvFinder update

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder let upd = updateNodes trvNodes listNodes

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder (\ b s -> do

074f8feaf71e0b71a95145e7439746f8eb8e2a7cChristian Maeder labelSetLabel lblSublogic $ show s

e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder updateFinder trvFinder listFinder b s)

aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian Maeder (do

aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian Maeder labelSetLabel lblSublogic "No sublogic"

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder listStoreClear listFinder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder activate widgets False

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder widgetSetSensitive btnCheck False)

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder (activate widgets True >> widgetSetSensitive btnCheck True)

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder shN <- setListSelectorMultiple trvNodes btnNodesAll btnNodesNone

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu btnNodesInvert upd

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu

25662bf82f592e3268fddcc2c86e83c203b82e53Ewaryst Schulz -- bindings

21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder let selectWith f u = do

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder signalBlock shN

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder sel <- treeViewGetSelection trvNodes

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder treeSelectionSelectAll sel

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder rs <- treeSelectionGetSelectedRows sel

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder mapM_ ( \ p@(row : []) -> do

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu (FNode { status = s }) <- listStoreGetValue listNodes row

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu (if f s then treeSelectionSelectPath else treeSelectionUnselectPath)

7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder sel p) rs

154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu signalUnblock shN

486db0a875bcdd0b80cf0d447d14c9c00a92ae94Simon Ulbricht u

486db0a875bcdd0b80cf0d447d14c9c00a92ae94Simon Ulbricht

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder onClicked btnNodesUnchecked

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder $ selectWith (== ConsistencyStatus CSUnchecked "") upd

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder onClicked btnNodesTimeout $ selectWith (== ConsistencyStatus CSTimeout "") upd

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

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

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder onClicked btnClose $ widgetDestroy window

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder onClicked btnStop $ takeMVar threadId >>= killThread >>= putMVar wait

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder onClicked btnCheck $ do

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder activate checkWidgets False

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder timeout <- spinButtonGetValueAsInt sbTimeout

706201451843aa76b8d862de800570c9838c9910Christian Maeder inclThms <- toggleButtonGetActive cbInclThms

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder (updat, pexit) <- progressBar "Checking consistency" "please wait..."

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder nodes' <- getSelectedMultiple trvNodes listNodes

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder mf <- getSelectedSingle trvFinder listFinder

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder f <- case mf of

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder Nothing -> error "Consistency checker: internal error"

9b6a888fced92090f2f3d60f551b8bf38bf2eecbChristian Maeder Just (_, f) -> return f

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder switch False

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder tid <- forkIO $ do

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder check inclThms ln le dg f timeout listNodes updat nodes'

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder putMVar wait ()

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder putMVar threadId tid

21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder forkIO_ $ do

ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder takeMVar wait

e4f0eaffd002e9e553ee113be33f9aa6e4181c43Christian Maeder postGUIAsync $ do

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance switch True

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance tryTakeMVar threadId

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance showModelView mView "Results of consistency check" listNodes emptyNodes

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance signalBlock shN

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance sortNodes trvNodes listNodes

c4076ff1721f8901a30e4b7aa004479ecb2631e0Felix Gabriel Mance signalUnblock shN

e4f0eaffd002e9e553ee113be33f9aa6e4181c43Christian Maeder upd

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa activate checkWidgets True

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa pexit

961978c71545e0177683279f8b63358b3e3804b8Christian Maeder

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa onDestroy window $ do

961978c71545e0177683279f8b63358b3e3804b8Christian Maeder nodes' <- listStoreToList listNodes

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa let changes = foldl (\ cs (FNode { node = (i, l), status = s }) ->

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa if (\ st -> st /= CSConsistent && st /= CSInconsistent)

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa $ sType s then cs

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa else

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa let n = (i, if sType s == CSInconsistent then

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder markNodeInconsistent "" l

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder else markNodeConsistent "" l)

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa in SetNodeLab l n : cs

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ) [] nodes'

b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder dg' = changesDGH dg changes

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

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder selectWith (== ConsistencyStatus CSUnchecked "") upd

c1168d10047d2c1394b82953158747775a9b4556Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder widgetShow window

c1168d10047d2c1394b82953158747775a9b4556Christian Maeder

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian MaedersortNodes :: TreeView -> ListStore FNode -> IO ()

1937dccb04b363364f7a7de17fdaae1d70583af9Christian MaedersortNodes trvNodes listNodes = do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder sel <- getSelectedMultiple trvNodes listNodes

b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder nodes <- listStoreToList listNodes

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let sn = sort nodes

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder updateListData listNodes sn

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski selector <- treeViewGetSelection trvNodes

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

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

1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder ) sel

bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder

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

bb9642ff292545658dc11251b83a7b7af3c1fccbChristian MaederupdateNodes :: TreeView -> ListStore FNode -> (Bool -> G_sublogics -> IO ())

bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder -> IO () -> IO () -> IO ()

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian MaederupdateNodes view listNodes update lock unlock = do

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder nodes <- getSelectedMultiple view listNodes

6c08e47c4275556c18f4f89521bf21fe94c28dd5Christian Maeder if null nodes then lock

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

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

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder $ foldl (\ ma b -> case ma of

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder Just a -> joinSublogics b a

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder Nothing -> Nothing) (Just $ head sls) $ tail sls

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder-- | Update the list of finder

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian MaederupdateFinder :: TreeView -> ListStore Finder -> Bool -> G_sublogics -> IO ()

63719301448519453f66383f4e583d9fd5b89ecbChristian MaederupdateFinder view list useNonBatch sl = do

f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder old <- listStoreToList list

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

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let n = getPName cc

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

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

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

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $ getConsCheckers $ findComorphismPaths logicGraph sl

a7b34c1a61dabe150288424d90389d5988bf9d7aChristian Maeder when (old /= new) $ do

bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder -- update list and try to select previous finder

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder selected' <- getSelectedSingle view list

e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder sel <- treeViewGetSelection view

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder listStoreClear list

938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz mapM_ (listStoreAppend list) $ mergeFinder old new

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder maybe (selectFirst view)

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

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

00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder ) selected'

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder-- | Try to select previous selected comorphism if possible

3143271856dbf456bd7acc1c07193173f886d986Christian MaedermergeFinder :: [Finder] -> [Finder] -> [Finder]

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

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

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder case Map.lookup n m of

bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder Nothing -> m

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

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

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder ) m' old

56440c7ae61e7277a3494452d0165ee52e677b29Christian Maeder

3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksacheck :: Bool -> LibName -> LibEnv -> DGraph -> Finder -> Int -> ListStore FNode

53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz -> (Double -> String -> IO ()) -> [(Int, FNode)] -> IO ()

3143271856dbf456bd7acc1c07193173f886d986Christian Maedercheck inclThms ln le dg (Finder { finder = cc, comorphism = cs, selected = i})

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder timeout listNodes update nodes = let

c30231257d9116b514dce02703a515fe21cd427dTill Mossakowski count' = fromIntegral $ length nodes

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder c = cs !! i in

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

00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder postGUISync $ update (count / count') n'

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

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder postGUISync $ listStoreSetValue listNodes row fn { status = res }

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder return $ count + 1) 0 nodes

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder

ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian MaederupdateComorphism :: TreeView -> ListStore Finder -> ComboBox

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -> ConnectId ComboBox -> IO ()

1937dccb04b363364f7a7de17fdaae1d70583af9Christian MaederupdateComorphism view list cbComorphism sh = do

1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder signalBlock sh

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder model <- comboBoxGetModelText cbComorphism

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa listStoreClear model

00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder mfinder <- getSelectedSingle view list

52e573502bb19ca616ea63283d58ba73f39675d2Christian Maeder case mfinder of

88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder Just (_, f) -> do

ef4c609cebc5260771dae6e4f3a54a8959e81ed9Christian Maeder mapM_ (comboBoxAppendText cbComorphism) $ expand f

180ab8c3df8cb0c88f0e881bca93354df6b5d560Christian Maeder comboBoxSetActive cbComorphism $ selected f

00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Nothing -> return ()

52e573502bb19ca616ea63283d58ba73f39675d2Christian Maeder signalUnblock sh

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maederexpand :: Finder -> [String]

ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksaexpand = map show . comorphism

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder

3143271856dbf456bd7acc1c07193173f886d986Christian MaedersetSelectedComorphism :: TreeView -> ListStore Finder -> ComboBox -> IO ()

3143271856dbf456bd7acc1c07193173f886d986Christian MaedersetSelectedComorphism view list cbComorphism = do

ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder mfinder <- getSelectedSingle view list

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder case mfinder of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just (i, f) -> do

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder sel <- comboBoxGetActive cbComorphism

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder listStoreSetValue list i f { selected = sel }

fb37a248ebad4696bbc9d9b94ce1cfc6497a9160Christian Maeder Nothing -> return ()

fb37a248ebad4696bbc9d9b94ce1cfc6497a9160Christian Maeder

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder-- | Displays the model view window

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

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder -> IO ()

ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian MaedershowModelViewAux 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 "") . status)

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 $ status 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)