LocalTop.hs revision eeaf0a8a1dc535d105904a2190f26c0835ecf429
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Id: StatAnaCSP.hs 9274 2007-11-29 20:55:26Z gimblett $
09249711700a6acbc40a2e337688b434d7aafa28Christian MaederDescription : Local top element analysis for CspCASL specifications
76647324ed70f33b95a881b536d883daccf9568dChristian MaederCopyright : (c) Andy Gimblett, Swansea University 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : a.m.gimblett@swan.ac.uk
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederStability : provisional
76647324ed70f33b95a881b536d883daccf9568dChristian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederAnalysis of relations for presence of local top elements. Used by
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederCspCASL static analysis.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder Obligation(..),
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport qualified Data.Set as S
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder-- A relation is a set of pairs.
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedertype Relation a b = S.Set (a, b)
0a39036fa485579a7b7c81cdd44a412392571927Christian Maedertype BinaryRelation a = Relation a a
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- We're interested in triples where two elements are both in relation
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- with some third object. We represent this as a Obligation, where
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- the first element is the shared one. It's important to note that
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- (Obligation x y z) == (Obligation x z y), which we encode here. For
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- every obligation, we look for any corresponding top elements.
d48085f765fca838c1d972d2123601997174583dChristian Maederdata Obligation a = Obligation a a a
05ae87b9efa19655024b0b6ac344d250b96567cdChristian Maederinstance Eq a => Eq (Obligation a) where
d48085f765fca838c1d972d2123601997174583dChristian Maeder (Obligation n m o) == (Obligation x y z) =
d48085f765fca838c1d972d2123601997174583dChristian Maeder (n==x) && ((m,o)==(y,z) || (m,o)==(z,y))
d48085f765fca838c1d972d2123601997174583dChristian Maederinstance Ord a => Ord (Obligation a) where
d48085f765fca838c1d972d2123601997174583dChristian Maeder compare (Obligation n m o) (Obligation x y z)
d48085f765fca838c1d972d2123601997174583dChristian Maeder | (Obligation n m o) == (Obligation x y z) = EQ
a39a820684c1974350f46593025e0bb279f41bc6Christian Maeder | otherwise = compare (n,m,o) (x,y,z)
a39a820684c1974350f46593025e0bb279f41bc6Christian Maederinstance Show a => Show (Obligation a) where
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder show (Obligation x y z) = show [x,y,z]
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder-- Turn a binary relation into a set mapping its obligation elements to
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- their corresponding local top elements (if any).
d48085f765fca838c1d972d2123601997174583dChristian MaederlocalTops :: Ord a => BinaryRelation a -> S.Set (Obligation a, S.Set a)
d48085f765fca838c1d972d2123601997174583dChristian MaederlocalTops r = S.map (\x -> (x, m x)) (obligations r)
d48085f765fca838c1d972d2123601997174583dChristian Maeder where m = findTops $ cartesian r
05ae87b9efa19655024b0b6ac344d250b96567cdChristian Maeder-- Find all the obligations in a binary relation, by searching its
d48085f765fca838c1d972d2123601997174583dChristian Maeder-- cartesian product for elements of the right form.
793945d4ac7c0f22760589c87af8e71427c76118Christian Maederobligations :: Ord a => BinaryRelation a -> S.Set (Obligation a)
a716971174535184da7713ed308423e355a4aa66Christian Maederobligations r = stripMaybe $ S.map isObligation (cartesian r)
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder where isObligation ((w,x),(y,z)) =
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder if (w==y) && (x /= z) && (w /= z) && (w /= x)
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder then Just (Obligation w x z)
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder-- Given a binary relation's cartesian product and a obligation, look
f2c2b420e386a90d940c758c631d16f12952d2b7Christian Maeder-- for corresponding top elements in that product.
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederfindTops :: Ord a => BinaryRelation (a,a) -> (Obligation a) -> S.Set a
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederfindTops c cand = S.map get_top (S.filter (is_top cand) c)
a716971174535184da7713ed308423e355a4aa66Christian Maeder where is_top (Obligation _ y z) ((m,n),(o,p))=((m==y)&&(o==z)&&(n==p))
a716971174535184da7713ed308423e355a4aa66Christian Maeder get_top ((_,_),(_,p)) = p
a716971174535184da7713ed308423e355a4aa66Christian Maeder-- Utility functions.
5e5c3fbbf8c22b883d551d83429b9f8d8041f1e0Christian Maeder-- Cartesian product of a set.
793945d4ac7c0f22760589c87af8e71427c76118Christian Maedercartesian :: Ord a => S.Set a -> S.Set (a,a)
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maedercartesian x = S.fromDistinctAscList [(i,j) | i <- xs, j <- xs]
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian Maeder -- fromDistinctAscList sorted precondition satisfied by construction
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder-- Given a set of Maybes, filter to keep only the Justs
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaederstripMaybe :: Ord a => S.Set (Maybe a) -> S.Set a
81d3d451a2543ca1f8ab00c229466c983bb08748Christian MaederstripMaybe x = S.fromList $ Maybe.catMaybes $ S.toList x
fd2dcd5c071e938c07338fd3a32296819b8a2333Christian Maeder-- Given a binary relation, compute its reflexive closure.
9884c7cef7e5a2c8595d5ef8c7d32b9b44a3fad8Christian MaederreflexiveClosure :: Ord a => BinaryRelation a -> BinaryRelation a
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian MaederreflexiveClosure r = S.fold add_refl r r
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder where add_refl (x, y) r' = (x, x) `S.insert` ((y, y) `S.insert` r')
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder-- Interface to hets for CspCASL LTE checks: given a
ee6c748be810b24e3c70ffd74f291c7394e389f5Christian Maeder-- transitively-closed subsort relation as a list of pairs, return a
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder-- list of unfulfilled LTE obligations.
d48085f765fca838c1d972d2123601997174583dChristian MaederunmetObs :: Ord a => [(a,a)] -> [Obligation a]
793945d4ac7c0f22760589c87af8e71427c76118Christian MaederunmetObs r = unmets
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder where l = S.toList $ localTops $ reflexiveClosure $ S.fromList r
793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder unmets = map fst $ filter (S.null . snd) l