added dependency sorting definitions

git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@14220 cec4b9c1-7d33-0410-9eda-942365e851bb

CSL/Analysis.hs

@@ -18,7 +18,10 @@ module CSL.Analysis
     , Guard(..)
     , Guarded(..)
     , dependencySortAS
+    , getDependencyRelation
     , epElimination
+    , topsortDirect
+    , topsort
 -- basicCSLAnalysis
 -- ,mkStatSymbItems
 -- ,mkStatSymbMapItem
@@ -248,7 +251,13 @@ addAssignment n (Op (OpString s) epl al _) def m =
 
 addAssignment _ x _ _ = error $ "unexpected assignment " ++ show x
 
--- | Splits the Commands into the AssignmentStore
+{-  TODO:
+    1. analysis for missing definitions and undeclared extparams
+    2. Integrating extparam domain definitions
+    3. check for each constant if the Guards exhaust the extparam domain (in splitAS)
+-}
+
+-- | Splits the Commands into the AssignmentStore and a program sequence
 splitAS :: [Named CMD] -> (GuardedMap EPRange, [Named CMD])
 splitAS cl =
     let f nc (m,l) = case sentence nc of
@@ -286,8 +295,56 @@ foldForest :: (b -> a -> Tr.Forest a -> b) -> b -> Tr.Forest a -> b
 foldForest f = foldl g where g x tr = f x (Tr.rootLabel tr) $ Tr.subForest tr
 
 
+-- ** Dependency Sorting
+
 dependencySortAS :: GuardedMap EPRange -> [(String, Guarded EPRange)]
-dependencySortAS = Map.toList
+dependencySortAS grdm = map f $ topsortDirect $ getDependencyRelation grdm
+    where f x = (x, Map.findWithDefault (err x) x grdm)
+          err x = error $ "dependencySortAS: impossible lookup error at " ++ x
+
+
+type Rel2 a = Map.Map a (Set.Set a)
+type BackRef a = Map.Map a [a]
+
+getDependencyRelation :: GuardedMap a -> Rel2 String
+getDependencyRelation = Map.map g where
+    g grdd = Set.unions $ map (setOfUserDefined . definition) $ guards grdd
+
+getBackRef :: Ord a => Rel2 a -> BackRef a
+getBackRef d =
+    let uf k n m  = Map.insertWith (++) n [k] m
+        -- for each entry in the set insert k into the list
+        f k s m = Set.fold (uf k) m s
+    -- from each entry in d add entries in the map
+    in Map.foldWithKey f Map.empty d
+
+
+topsortDirect :: (Show a, Ord a) => Rel2 a -> [a]
+topsortDirect d = topsort d $ getBackRef d
+
+-- | This function is based on the Kahn-algorithm. It requires a representation
+-- of a relation which has for each entry of the domain an entry in the map.
+-- 
+-- E.g., 1 |-> {2}, 2 |-> {3, 4} is not allowed because the entries
+-- 3 |-> {}, 4 |-> {} are missing
+topsort :: (Show a, Ord a) => Rel2 a -> BackRef a -> [a]
+topsort d br =
+ let f d' acc []
+         | Map.null d' = acc
+         | otherwise =
+             let (s, v) = Map.findMin d'
+             in error $ "contains cycles: " ++ concat [ show s, " -> ", show v ]
+     f d' acc (n:l) =
+         let cl = Map.findWithDefault [] n br
+             (nl, d'') = foldl (remEdge n) ([], d') cl
+         in f d'' (n:acc) $ l ++ nl
+     uf n a = let b = Set.delete n a in if Set.null b then Nothing else Just b
+     -- returns a new list of empty-nodes and a new def-map
+     remEdge n (nl, m) s = let c = Map.size m
+                               m' = Map.update (uf n) s m
+                           in (if Map.size m' < c then s:nl else nl, m')
+     (me, mne) = Map.partition Set.null d
+ in f mne [] $ Map.keys me
 
 
 -- ** Extended Parameter Elimination
@@ -334,7 +391,7 @@ eliminateGuard m grd = do
         fldOp _ v _ _ _ _ = v
         h pim = foldTerm passRecord{ foldOp = fldOp pim } $ definition grd
         g (er, pim) = grd{ range = er, definition = h pim }
-    partMap <- extractUserDefined f $ definition grd
+    partMap <- mapUserDefined f $ definition grd
     rePart <- refineDefPartitions partMap
     case rePart of
       AllPartition _ -> error $ "eliminateGuard: AllPartition " ++ show grd
@@ -365,9 +422,9 @@ mkPIConst s epl = (s, if null epl then Nothing else Just $ toEPExps epl)
 
 -- | Returns a map of user defined (partially instantiated) constants
 -- to the result of this constant under the given function.
-extractUserDefined :: Monad m => (String -> [EXTPARAM] -> [EXPRESSION] -> m a)
+mapUserDefined :: Monad m => (String -> [EXTPARAM] -> [EXPRESSION] -> m a)
                    -> EXPRESSION -> m (Map.Map PIConst a)
-extractUserDefined f e = g Map.empty e
+mapUserDefined f e = g Map.empty e
     where
       g m x =
        case x of
@@ -379,6 +436,16 @@ extractUserDefined f e = g Map.empty e
          -- ignoring lists (TODO: they should be removed soon anyway)
          _ -> return m
 
+-- | Returns a set of user defined constants ignoring instantiation.
+setOfUserDefined :: EXPRESSION -> Set.Set String
+setOfUserDefined e = g Set.empty e
+    where
+      g s x =
+       case x of
+         Op (OpString n) _ al _ -> foldl g (Set.insert n s) al 
+         -- ignoring lists (TODO: they should be removed soon anyway)
+         _ -> s
+
 {- |
    Given a map holding for each constant, probably partly instantiated,
    a partition labeled by the corresponding elim-constants we build a

CSL/EPRelation.hs

@@ -280,14 +280,6 @@ compareEPs eps1 eps2 =
 -- * SMT based comparison - utility functions
 -- ----------------------------------------------------------------------
 
--- | Generates from a list of Extended Parameter names an id-mapping
-varMapFromList :: [String] -> VarMap
-varMapFromList l = Map.fromList $ zip l $ [1 .. length l]
-
--- | Generates from a list of Extended Parameter names an id-mapping
-varMapFromSet :: Set.Set String -> VarMap
-varMapFromSet = varMapFromList . Set.toList
-
 -- | Builds a Boolean representation from the extended parameter expression.
 -- Variable names are composed from the string "x" together with an integer.
 boolExps :: VarMap -> EPExps -> BoolRep
@@ -390,6 +382,9 @@ rangeCmp x y = liftM tripleFst $ rangeFullCmp x y
 
 type SmtComparer = ReaderT VarEnv IO
 
+execSMTComparer :: VarEnv -> SmtComparer a -> IO a
+execSMTComparer ve smt = runReaderT smt ve
+
 instance CompareIO SmtComparer where
     rangeFullCmp r1 r2 = do
       ve <- ask

CSL/InteractiveTests.hs

@@ -181,6 +181,21 @@ sl <- sens (-3)
 fst $ splitAS sl
 -}
 
+-- TODO: build a tester for the ep-elimination proc
+-- testSMTComparer :: [String] ->
+
+varEnvFromList :: [String] -> VarEnv
+varEnvFromList l = error ""
+
+-- | Generates from a list of Extended Parameter names an id-mapping
+varMapFromList :: [String] -> VarMap
+varMapFromList l = Map.fromList $ zip l $ [1 .. length l]
+
+-- | Generates from a list of Extended Parameter names an id-mapping
+varMapFromSet :: Set.Set String -> VarMap
+varMapFromSet = varMapFromList . Set.toList
+
+
 epList :: [EPRange]
 epList =
     let l = map (Atom . toEPs)
@@ -486,57 +501,3 @@ extractOps = extr Map.empty
 -- -- ----------------------------------------------------------------------
 
 
--- TODO: move this to analysis!
-toDef :: [String] -> Def
-toDef l = Map.fromList $ map (\ x -> (head x, Set.fromList $ tail x)) $ map (map (:[])) l
-
--- toDef ["043", "124", "23", "34", "4"] -- entnommen spec Test1011
-
-type Def = Map.Map String (Set.Set String)
-type BackRef = Map.Map String [String]
-
-buildDBR :: Guarded a -> (Def, BackRef)
-buildDBR = error ""
-
-getBackRef :: Def -> BackRef
-getBackRef d =
-    let uf k n m  = Map.insertWith (++) n [k] m
-        -- for each entry in the set insert k into the list
-        f k s m = Set.fold (uf k) m s
-    -- from each entry in d add entries in the map
-    in Map.foldWithKey f Map.empty d
-
-{-
-Set.fold :: (a -> b -> b) -> b -> Set a -> b
-
-Map.foldWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
--}
--- Kahn-algorithm
-topsort :: Def -> BackRef -> [String]
-topsort d br =
- let f d' [] = if Map.null d' then [] else error $ "contains cycles: " ++ let (s, v) = Map.findMin d' in concat [ s, " -> ", show v ]
-     f d' (n:l) =
-         let cl = Map.findWithDefault [] n br
-             (nl, d'') = foldl (remEdge n) ([], d') cl
-         in n : (f d'' $ l ++ nl)
-     uf n a = let b = Set.delete n a in if Set.null b then Nothing else Just b
-     -- returns a new list of empty-nodes and a new def-map
-     remEdge n (nl, m) s = let c = Map.size m
-                               m' = Map.update (uf n) s m
-                           in (if Map.size m' < c then s:nl else nl, m')
-     (me, mne) = Map.partition Set.null d
- in f mne $ Map.keys me
-
--- L ← Empty list that will contain the sorted elements
--- S ← Set of all nodes with no incoming edges
--- while S is non-empty do
---     remove a node n from S
---     insert n into L
---     for each node m with an edge e from n to m do
---         remove edge e from the graph
---         if m has no other incoming edges then
---             insert m into S
--- if graph has edges then
---     output error message (graph has at least one cycle)
--- else 
---     output message (proposed topologically sorted order: L)