Mon Jul 30 16:23:27 WEST 2007 Miguel Vilaca <jmvilaca@di.uminho.pt>
* Valid IN System
Checks if a document is a valid Interaction Nets System.
{
hunk ./Makefile 258
+src/INChecks.o : src/Shape.hi
hunk ./Makefile 260
+src/INChecks.o : src/Palette.hi
hunk ./src/INChecks.hs 31
+import Palette hiding (join)
hunk ./src/INChecks.hs 33
+import Shape
hunk ./src/INChecks.hs 38
+import Data.List
hunk ./src/INChecks.hs 44
+ | MultiDef String Int -- ^ Symbol is defined multiple times in palette
+ | UndefAgent (Node n) -- ^ Undefined agent
+ | BadInterfaceSymbol Shape (Maybe Ports) -- ^ Bad interface symbol definition
+ | BadInterfaceAgent (Node n) -- ^ Bad interface agent
+ | SymbolNoPorts String -- ^ Symbol without ports
+ | AgentNoPorts (Node n) -- ^ Agent without ports
+ | MappingNoDom Mapping NodeNr -- ^ Bad mapping which refers one element in domain that do not exist.
+ | MappingNoRang Mapping NodeNr -- ^ Bad mapping which refers one element in range that do not exist.
+ | MappingNotInj Mapping NodeNr -- ^ Mapping is not injective with respect to LHS node given.
+ | MappingNotFunc Mapping NodeNr -- ^ Mapping is not a function with respect to RHS node given.
+ | UnMappedInterface (Node n) -- ^ Interface agent is not mapped to another.
+ | Not2Agents [Node n] -- ^ rule LHS don't have exactly 2 agents.
+ | NoActivePair (Node n) (Node n) -- ^ No active pair between the nodes given
+ | ExtraEdge EdgeNr (NodeNr, Port) (NodeNr, Port) -- ^ Edge other than edge between principal ports found between agents in LHS.
+ | InterfaceBadConnected NodeNr (EdgeNr) -- ^ Interface agent is not connected to free ports of active pair.
+ | MultRulesSameLHS String String [String] -- ^ Multiple rules with same LHS active pair, i.e. between shape1 and shape2.
+
hunk ./src/INChecks.hs 67
+ showsPrec _ (MultiDef symb reps) =
+ showString "Symbol \"" . showString symb . showString "\" is defined "
+ . shows reps . showString " times in palette of symbols."
+ showsPrec _ (UndefAgent node) =
+ showString "Agent \"" . showString (Network.getName node)
+ . showString "\" @ " . shows (getPosition node)
+ . showString " is not defined in the palette of symbols."
+ showsPrec _ (BadInterfaceSymbol shape ports) =
+ showString ("A symbol called interface is defined, so its definition should be :\n"
+ ++ "\tshape = Circle { shapeStyle = ShapeStyle { styleStrokeWidth = 2\n"
+ ++ "\t , styleStrokeColour = RGB 255 255 255\n"
+ ++ "\t , styleFill = RGB 255 255 255 }\n"
+ ++ "\t , shapeRadius = 0.25 }\n"
+ ++ "\tports = Just [(\"interface\", DoublePoint 0.0 0.25)]\n"
+ ++ "but something different were found:")
+ . showString "\tshape = " . shows shape
+ . showString "\tports = " . shows ports
+ showsPrec _ (BadInterfaceAgent node) =
+ showString "Agent \"" . showString (Network.getName node)
+ . showString "\" @ " . shows (getPosition node)
+ . showString " is a bad interface agent."
+ showsPrec _ (SymbolNoPorts symb) =
+ showString "Symbol \"" . showString symb . showString "\" don't have ports."
+ showsPrec _ (AgentNoPorts node) =
+ showString "Agent \"" . showString (Network.getName node)
+ . showString "\" @ " . shows (getPosition node)
+ . showString " don't have ports."
+ showsPrec _ (MappingNoDom mapping nNr) =
+ showString "Interface node " . shows nNr
+ . showString " do not exist in LHS but is referred in domain of mapping\n"
+ . showsMapping mapping
+ showsPrec _ (MappingNoRang mapping nNr) =
+ showString "Interface node " . shows nNr
+ . showString" do not exist in RHS but is referred in range of mapping\n"
+ . showsMapping mapping
+ showsPrec _ (MappingNotInj mapping nNr) =
+ showString "Mapping is not injective with respect to LHS interface node "
+ . shows nNr
+ . showChar '\n'
+ . showsMapping mapping
+ showsPrec _ (MappingNotFunc mapping nNr) =
+ showString "Mapping is not a function with respect to RHS interface node "
+ . shows nNr
+ . showChar '\n'
+ . showsMapping mapping
+ showsPrec _ (UnMappedInterface node) =
+ showString "Interface \"" . showString (Network.getName node)
+ . showString "\" @ " . shows (getPosition node)
+ . showString " is not mapped to other interface in the other side of the rule."
+ showsPrec _ (Not2Agents lNs) =
+ showString "The rule LHS should have exactly 2 agents but those "
+ . shows (length lNs) . showString " were found:" . showsAgents lNs
+ showsPrec _ (NoActivePair node1 node2) =
+ showString "No active pair between agent \"" . showString (Network.getName node1)
+ . showString "\" @ " . shows (getPosition node1)
+ . showString "\nand agent \"" . showString (Network.getName node2)
+ . showString "\" @ " . shows (getPosition node2)
+ showsPrec _ (ExtraEdge edgeNr (nNr1, port1) (nNr2, port2)) =
+ showString "Edge " . shows edgeNr
+ . showString "is not the edge between principal ports but also found between agents \"Node "
+ . shows nNr1 . showString "\" at port " . showString (fst port1)
+ . showString " and \"Node " . shows nNr2 . showString "\" at port "
+ . showString (fst port2)
+ showsPrec _ (InterfaceBadConnected nNr edgeNr) =
+ showString "Interface \"Node " . shows nNr
+ . showString "\" should be connected to one of the free ports of active pair \"Edge "
+ . shows edgeNr . showString "\" but it isn't."
+ showsPrec _ (MultRulesSameLHS shape1 shape2 rules) =
+ showString "There should be at most one rule for pair of agents but for agents \""
+ . showString shape1 . showString "\" and \"" . showString shape2
+ . showString "\" there are this rules whose LHS is an active pair between such agents :"
+ . showString (commasAnd rules)
+
hunk ./src/INChecks.hs 142
+showsAgent :: Node n -> ShowS
+showsAgent node =
+ showString "Agent \"" . showString (Network.getName node)
+ . showString "\" of symbol \""
+ . showString (either id (const "UNDEFINED SYMBOL") $ getShape node)
+ . showString "\" @ " . shows (getPosition node)
+ where err = error ""
hunk ./src/INChecks.hs 150
+showsAgents :: [Node n] -> ShowS
+showsAgents [] = showString ""
+showsAgents (x:xs) = showsAgent x . showChar '\n' . showsAgents xs
hunk ./src/INChecks.hs 159
-data ErrorLoc = PALETTE | NET | RULE RuleName (Maybe Side) deriving (Eq, Ord)
+data ErrorLoc = PALETTE | NET | RULES | RULE RuleName (Maybe Side) deriving (Eq, Ord)
hunk ./src/INChecks.hs 164
+ show RULES = "RULES"
hunk ./src/INChecks.hs 191
+ , iNCheck
hunk ./src/INChecks.hs 265
+------------------------------------------------------------------------------------------------------------------
+
+
+-- valid IN system ------------------------------------------------------------------------------------------------
+iNCheck :: Check g n e
+iNCheck =
+ ( "Valid IN system"
+ , unlines
+ [ "Check if it is a valid IN system.\n"
+ , "An IN system is valid in INblobs if:"
+ , " * every port is connected exactly once in net and in LHS and RHS of every rule"
+ , " * the LHS of every rule is one active pair, plus interface agents"
+ , " * every interface agent in the LHS (respectively RHS) of a rule is mapped to one interface agent in the RHS (respectively LHS)"
+ , " * there are at most one rule per pair of agents"
+ , " * every agent mentioned in the net or any rule is declared in the palette of symbols"
+ ]
+ , "Valid IN system"
+ , "Invalid IN system"
+ , validIN
+ )
+
+{- | An IN system is valid in INblobs if:
+
+ * every port is connected exactly once in net and in LHS and RHS of every rule
+
+ * the LHS of every rule is one active pair, plus interface agents
+
+ * every interface agent in the LHS (respectively RHS) of a rule is mapped to
+ one interface agent in the RHS (respectively LHS)
+
+ * there are at most one rule per pair of agents
+
+ * every agent mentioned in the net or any rule is declared in the palette of symbols
+
+-}
+validIN :: CheckOp g n e
+validIN = joins [
+ pureBadPorts
+ , checkAgents
+ , checkEachRule
+ , checkNoRepeatedRules
+ ]
+
+sepInterface :: Network g n e -> ( [(NodeNr,Node n)] -- interface nodes
+ , [(NodeNr,Node n)] -- none interface nodes
+ )
+sepInterface = partition isInterfaceNode . getNodeAssocs
+
+-- | 'checkLHS' and 'checkMapping'
+checkEachRule :: CheckOp g n e
+checkEachRule = doc2Errors funcNet funcRule
+ where funcNet :: Network g n e -> [INError g n e]
+ funcNet = const []
+
+ funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
+ funcRule rule = (Just Lhs, checkLHS lhs)
+ : checkMapping (getMapping rule)
+ (fst $ sepInterface lhs)
+ (fst . sepInterface $ getRHS rule)
+ where lhs = getLHS rule
+
+-- | LHS should be exactly two agents different from interface connected trough their
+-- principal ports with the rest of the ports connected to one interface agent.
+checkLHS :: Network g n e -> [INError g n e]
+checkLHS = either (const []) id . checkLHS'
+
+checkLHS' :: Network g n e -> Either (String, String) [INError g n e]
+checkLHS' net =
+ case sepInterface net of
+ (iNs, [(xNr,x), (yNr,y)]) ->
+ case (getPorts x, getPorts y) of
+ (Just (px:pxs), Just (py:pys)) ->
+ case findEdge xNr (Just px) yNr (Just py) net of
+ Nothing -> Right [NoActivePair x y]
+ Just ed ->
+ let mINs = map (otherExtremeOfEdgeConnectedOnPort net xNr) pxs
+ ++ map (otherExtremeOfEdgeConnectedOnPort net yNr) pys
+ in if all isJust mINs
+ then
+ let iNs' = map (id >< head . fromJust . getPorts) iNs
+ cons = map fromJust mINs
+ dif1 = cons \\ iNs' -- multiple edges between agents x and y
+ dif2 = iNs' \\ cons -- interface nodes not connected to agent x or y
+ in if null dif1 && null dif2
+ then case (getShape x, getShape y) of
+ (Left shape1, Left shape2) -> Left (shape1,shape2)
+ _ -> Right []
+ else Right $ toError1 dif1 ++ map (toError2 ed) dif2
+ else Right [] -- disconnected ports checked in another piece of code
+
+
+
+ (psx, psy) -> Right . map (AgentNoPorts . snd) $ filter (maybe True null . fst) [(psx,x),(psy,y)]
+ (_, lAs) -> Right [Not2Agents $ map snd lAs]
+ where
+ toError1 = map aux3 . groupBy aux2 . map aux
+ aux = id /\ fromJust . uncurry (edgeConnectedOnPort net)
+ aux2 a b = snd a == snd b
+ aux3 :: [((NodeNr,Port),EdgeNr)] -> INError g n e
+ aux3 [(from,edge), (to,_)] = ExtraEdge edge from to
+ aux3 _ = error "unexpected situation"
+ toError2 ed (nNr,_) = InterfaceBadConnected nNr ed
+
+
+-- | Every interface agent in the LHS (respectively RHS) of a rule is mapped to
+-- one interface agent in the RHS (respectively LHS).
+checkMapping :: Mapping -> [(NodeNr,Node n)] -> [(NodeNr,Node n)] -> [(Maybe Side, [INError g n e])]
+checkMapping mapR lhsI rhsI =
+ [ (Just Lhs, map errL $ lhs \\ domMap )
+ , (Just Rhs, map errR $ rhs \\ rangeMap)
+ , (Nothing, (uncurry (++) . (map errNotInj >< map errNoDom ) . partition (`elem` lhs) $ domMap \\ lhs )
+ ++
+ (uncurry (++) . (map errNotFunc >< map errNoRang) . partition (`elem` rhs) $ rangeMap \\ rhs )
+
+ )
+ ]
+ where
+ aux :: (NodeNr,Node n) -> (NodeNr, Maybe Port)
+ aux = id >< (Just . head . fromJust . getPorts)
+
+ (domMap, rangeMap) = unzip mapR
+ lhs = map aux lhsI
+ rhs = map aux rhsI
+
+ errL (nNr,_) = UnMappedInterface . fromJust $ lookup nNr lhsI
+ errR (nNr,_) = UnMappedInterface . fromJust $ lookup nNr rhsI
+ errNotInj = MappingNotInj mapR . fst
+ errNoDom = MappingNoDom mapR . fst
+ errNotFunc = MappingNotFunc mapR . fst
+ errNoRang = MappingNoRang mapR . fst
+
+insertIf :: Ord k => k -> [a] -> Map k [a] -> Map k [a]
+insertIf k a mapp | null a = mapp
+ | otherwise = Map.insertWith (++) k a mapp
+
+checkAgents :: CheckOp g n e
+checkAgents doc =
+ insertIf PALETTE (map toError3 . filter badInterface $ shaps)
+ . insertIf PALETTE (map toError2 $ filter noPorts shaps)
+ . insertIf PALETTE (map toError . repeateds $ symbs)
+ $ undefinedAgents symbs doc
+ where
+ shaps = shapes $ getPalette doc
+ symbs = map fst shaps
+ toError (symb, i) = MultiDef symb i
+ toError2 = SymbolNoPorts . fst
+ toError3 (_, (shape, mPorts, _)) = BadInterfaceSymbol shape mPorts
+ noPorts = maybe True null . snd3 . snd
+ fstsnd (a,b,_) = (a,b)
+
+ badInterface ("interface", (_, Just [("interface",_)], _)) = False
+ badInterface ("interface", _) = True
+ badInterface _ = False
+
+-- | Check if there are undefined agents.
+undefinedAgents :: [String] -> CheckOp g n e
+undefinedAgents symbols = doc2Errors funcNet funcRule
+ where funcNet :: Network g n e -> [INError g n e]
+ funcNet = undefinedAgentNet symbols
+
+ funcRule :: INRule g n e -> [(Maybe Side, [INError g n e])]
+ funcRule rule =
+ [ (Just Lhs, undefinedAgentNet symbols $ getLHS rule)
+ , (Just Rhs, undefinedAgentNet symbols $ getRHS rule)
+ ]
+
+undefinedAgentNet :: [String] -> Network g n e -> [INError g n e]
+undefinedAgentNet symbols = uncurry (++)
+ . ( (map UndefAgent . filter undefs) /\ (map BadInterfaceAgent . filter badInterfaceNode) )
+ . getNodes
+ where
+ undefs = either (`notElem` symbols) (const True) . getShape
+ badInterfaceNode node = either (\str -> str == "interface" && not (isInterfaceNode (0,node)) )
+ (const False)
+ $ getShape node
+
+
+-- | Filter repeated elements only, mentioning the number of repetitions.
+repeateds :: Ord a => [a] -> [(a, Int)]
+repeateds = Map.toList . Map.filter (>1) . Map.fromListWith (+) . map (\x -> (x,1))
+
+-- | Checks if there are at most one rule per pair of agents.
+checkNoRepeatedRules :: CheckOp g n e
+checkNoRepeatedRules =
+ (\lErrors -> insertIf RULES lErrors Map.empty)
+ . map toError . filter dups . groupBy activePair
+ . map left . filter isLeft
+ . map (INRule.getName /\ checkLHS' .getLHS) . getRules
+ where
+ isLeft = either (const True) (const False) . snd
+ left = id >< either id (error "This shouldn't happen")
+ activePair :: (RuleName, (String,String)) -> (RuleName, (String,String)) -> Bool
+ activePair (_,shapes1) (_,shapes2) = shapes1 == shapes2 || shapes1 == swap shapes2
+ dups = (> 1) . length
+ toError :: [(RuleName, (String,String))] -> INError g n e
+ toError ( (ruleName,(shape1,shape2)):xs) = MultRulesSameLHS shape1 shape2 $ ruleName : map fst xs
hunk ./src/INRule.hs 26
+ , showsMapping
hunk ./src/INRule.hs 50
+showsMapping :: Mapping -> ShowS
+showsMapping [] = showString "{}"
+showsMapping (x:xs) =
+ showChar '{' . showsE x . showl xs
+ where showl [] = showChar '}'
+ showl (x:xs) = showChar ',' . showsE x . showl xs
+ showsE ((from,_),(to,_)) = shows from . showString " |-> " . shows to
hunk ./src/INRule.hs 141
-isInterfaceNode (_, node) = case getShape node of
- Left "interface" -> True
+isInterfaceNode (_, node) = case (getShape node, getPorts node) of
+ (Left "interface", Just [("interface",_)]) -> True
}