packages feed

cpsa 3.3.1 → 3.3.2

raw patch · 15 files changed

+140/−113 lines, 15 filesdep −array

Dependencies removed: array

Files

ChangeLog view
@@ -1,8 +1,18 @@+2016-06-22  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Extension): Add allow ambiguous types when compiling+	with GHC 8.0.0 or later.++2016-06-21  Moses D. Liskov <mliskov@mitre.org>++	* src/CPSA/DiffieHellman/Algebra.hs: Added code to implement the+	"tag" sort, which quoted string tags belong to.+ 2016-06-03  Moses D. Liskov <mliskov@mitre.org>  	* doc/examples/IKE_variants.tar.gz: Added this compressed archive 	of IKEv1 and IKEv2 variant input files.-	+ 2016-03-30  John D. Ramsdell  <ramsdell@mitre.org>  	* src/CPSA/SAS/SAS.hs: Added support for fringe skeletons so that@@ -222,4 +232,3 @@ 2013-02-06  John D. Ramsdell  <ramsdell@mitre.org>  	* cpet.cabal (Version): Tagged as 0.0.0.-
NEWS view
@@ -2,6 +2,12 @@    June, 2016: +* New feature: tag sort.  Introduced a new sort "tag" in both the basic and+  diffie-hellman algebras.  Quoted string constants are now considered to be+  of this sort rather than of least sort mesg.  This allows a user to specify+  a variable that may stand for a string constant, without forcing the user to+  use a variable of the mesg sort for that purpose.+ * New feature: depth limit.  When a depth limit is specified, analysis of   skeletons will proceed as long as the skeleton's depth in the search tree   is below the limit.  Skeletons not analyzed are marked as "(fringe)" to
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		3.3.1+Version:		3.3.2 Maintainer:		mliskov@mitre.org Cabal-Version:		>= 1.6 License:		BSD3@@ -98,9 +98,11 @@  Executable cpsa   Main-Is:		CPSA/Lib/Main.hs-  Build-Depends:	base >= 3 && < 5, containers, parallel, array+  Build-Depends:	base >= 3 && < 5, containers, parallel   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded -rtsopts+  if impl(ghc >= 8.0.0)+    Extensions: AllowAmbiguousTypes   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Vector CPSA.Lib.Utilities CPSA.Lib.Debug@@ -118,6 +120,8 @@   Build-Depends:	base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports+  if impl(ghc >= 8.0.0)+    Extensions: AllowAmbiguousTypes   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr@@ -134,6 +138,8 @@   Build-Depends:	base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports+  if impl(ghc >= 8.0.0)+    Extensions: AllowAmbiguousTypes   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr@@ -147,6 +153,8 @@   Build-Depends:	base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports+  if impl(ghc >= 8.0.0)+    Extensions: AllowAmbiguousTypes   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr@@ -162,6 +170,8 @@   Build-Depends:	base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports+  if impl(ghc >= 8.0.0)+    Extensions: AllowAmbiguousTypes   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr@@ -175,6 +185,8 @@   Build-Depends:	base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports+  if impl(ghc >= 8.0.0)+    Extensions: AllowAmbiguousTypes   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr@@ -198,6 +210,8 @@   Build-Depends:	base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports+  if impl(ghc >= 8.0.0)+    Extensions: AllowAmbiguousTypes   Hs-Source-Dirs:	src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr
doc/cpsamanual.pdf view

binary file changed (871671 → 872297 bytes)

src/CPSA/Annotations/Annotations.hs view
@@ -246,8 +246,7 @@       return (gen', Instance { pos = pos, role = Just r,                                env = env, height = height }) -lookupRole :: (Algebra t p g s e c, Monad m) => Pos ->-              Prot t g -> String -> m (Role t)+lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t) lookupRole pos prot role =     case L.find (\r -> role == rname r) (roles prot) of       Nothing ->@@ -426,8 +425,7 @@ successors strands =     [((s, p), (s, p + 1)) | (s, n) <- zip [0..] strands, p <- nats (n - 1)] -before :: (Algebra t p g s e c, Monad m) => Pos ->-          Preskel t g e -> m [(Node, [Node])]+before :: Monad m => Pos -> Preskel t g e -> m [(Node, [Node])] before pos k =     case isAcyclic graph nodes of       False -> fail (shows pos "Cycle found")
src/CPSA/DiffieHellman/Algebra.hs view
@@ -22,7 +22,7 @@  -- The Diffie-Hellman Order-Sorted Signature is --- Sorts: mesg, text, data, name, skey, akey,+-- Sorts: mesg, text, data, name, skey, akey, tag, --        string, base, expr, and expn -- -- Subsorts: text, data, name, skey, akey,@@ -339,6 +339,7 @@     | Name                      -- Principal atom     | Skey                      -- Symmetric key atom     | Base                      -- Base of an exponentiated atom+    | Tag                       -- Tag atom     | Ltk                       -- Long term shared symmetric key     | Bltk                      -- Bidirectional ltk     | Akey                      -- Asymmetric key atom@@ -426,6 +427,7 @@ forceVar (F Text y) = (F Text y) forceVar (F Data y) = (F Data y) forceVar (F Name y) = (F Name y)+forceVar (F Tag [(I x)]) = (F Tag [(I x)]) forceVar (F Skey [(I x)]) = (F Skey [(I x)]) forceVar (F Skey [(F Ltk ns@(_:_))]) = forceVar (head ns) forceVar (F Skey [(F Bltk ns@(_:_))]) = forceVar (head ns)@@ -539,7 +541,8 @@ isVar (I _) = True           -- Sort: mesg isVar (F s [I _]) =     -- Sorts: text, data, name, skey, and akey-    s == Text || s == Data || s == Name || s == Skey || s == Akey || s == Base+    s == Text || s == Data || s == Name || s == Skey ||+      s == Akey || s == Base || s == Tag isVar (G t) = isGroupVar t isVar _ = False @@ -557,6 +560,7 @@ varId (F Skey [I x]) = x varId (F Akey [I x]) = x varId (F Base [I x]) = x+varId (F Tag [I x]) = x varId (G t) | isGroupVar t = getGroupVar t varId (D x) = x varId _ = C.assertError "Algebra.varId: term not a variable with its sort"@@ -603,6 +607,8 @@     extendVarEnv xts x t        -- Name variable termWellFormed xts t@(F Skey [I x]) =     extendVarEnv xts x t        -- Symmetric key variable+termWellFormed xts t@(F Tag [I x]) =+    extendVarEnv xts x t        -- Tag variable termWellFormed xts (F Skey [F Ltk [I x, I y]]) =     -- Long term shared symmetric key     doubleTermWellFormed xts (F Name [I x]) (F Name [I y])@@ -635,7 +641,7 @@     where       expnVarEnv xts (x, (be, _)) =           extendVarEnv xts x (groupVar be x)-termWellFormed xts (C _) =+termWellFormed xts (F Tag [(C _)]) =     Just xts                    -- Tags termWellFormed xts (F Cat [t0, t1]) =     doubleTermWellFormed xts t0 t1  -- Concatenation@@ -661,9 +667,9 @@ -- Is the sort of the term a base sort? isAtom :: Term -> Bool isAtom (I _) = False-isAtom (C _) = False+isAtom (C _) = True isAtom (F s _) =-    s == Text || s == Data || s == Name || s == Skey || s == Akey+    s == Text || s == Data || s == Name || s == Skey || s == Akey || s == Tag isAtom (G x) = isBasisVar x isAtom (D _) = False isAtom (P _) = False@@ -696,6 +702,7 @@ foldVars :: (a -> Term -> a) -> a -> Term -> a foldVars f acc t@(I _) = f acc t          -- Mesg variable foldVars f acc t@(F Text [I _]) = f acc t -- Text variable+foldVars f acc t@(F Tag [I _]) = f acc t -- Tag variable foldVars f acc t@(F Data [I _]) = f acc t -- Data variable foldVars f acc t@(F Name [I _]) = f acc t -- Name variable foldVars f acc t@(F Skey [I _]) =@@ -727,7 +734,7 @@     where       expnAddVars acc x (be, _) =           f acc (groupVar be x)-foldVars _ acc (C _) = acc        -- Tags+foldVars _ acc (F Tag [(C _)]) = acc        -- Tags foldVars f acc (F Cat [t0, t1]) = -- Concatenation     foldVars f (foldVars f acc t0) t1 foldVars f acc (F Enc [t0, t1]) = -- Encryption@@ -783,8 +790,7 @@     ba term     where       ba (I _) = True           -- A mesg sorted variable is always buildable---      ba (F Genr _) = True      -- as is the generator-      ba (C _) = True           -- So is a tag+--      ba (C _) = True           -- Tags are now atoms.       ba (F Cat [t0, t1]) =           ba t0 && ba t1       ba t@(F Enc [t0, t1]) =@@ -2075,6 +2081,8 @@           | x == y = (F Akey [I x], F Akey [t])       loop (F Base [I x] : _) (y, t)           | x == y = (F Base [I x], F Base [t])+      loop (F Tag [I x] : _) (y, t)+          | x == y = (F Tag [I x], F Tag [t])       loop (G x : _) (y, G t)           | isGroupVar x && varId (G x) == y = (G x, G t)       loop (D x : _) (y, t)@@ -2192,6 +2200,7 @@             "skey" -> return $ F Skey [t]             "akey" -> return $ F Akey [t]             "base" -> return $ F Base [t]+            "tag" -> return $ F Tag [t]             "expr" -> return $ groupVar False x             "expn" -> return $ groupVar True x             "node" -> return (D x)@@ -2227,7 +2236,7 @@ loadTerm vars strict (S pos s) =     either fail return (loadLookup pos vars strict s) loadTerm _ _ (Q _ t) =-    return (C t)+    return (F Tag [(C t)]) loadTerm vars strict (L pos (S _ s : l)) =     case lookup s loadDispatch of       Nothing -> fail (shows pos "Keyword " ++ s ++ " unknown")@@ -2415,6 +2424,7 @@ displayVar ctx (F Skey [I x]) = displaySortId "skey" ctx x displayVar ctx (F Akey [I x]) = displaySortId "akey" ctx x displayVar ctx (F Base [I x]) = displaySortId "base" ctx x+displayVar ctx (F Tag [I x]) = displaySortId "tag" ctx x displayVar ctx t@(G x)     | isBasisVar x = displaySortId "expn" ctx (varId t)     | isGroupVar x = displaySortId "expr" ctx (varId t)@@ -2454,6 +2464,7 @@       F Invk [F Pubk [C c, I x]] ->           L () [S () "privk", Q () c, displayId ctx x]       _ -> error ("Algebra.displayAkey: Bad term " ++ show t)+displayTerm ctx (F Tag [I x]) = displayId ctx x displayTerm ctx (F Base [t]) =     displayBase t     where@@ -2475,6 +2486,7 @@       displayFactor (x, (_, n))           | n >= 0 = displayId ctx x           | otherwise = L () [S () "rec", displayId ctx x]+displayTerm _ (F Tag [(C t)]) = Q () t displayTerm _ (C t) = Q () t displayTerm ctx (F Cat [t0, t1]) =     L () (S () "cat" : displayTerm ctx t0 : displayList ctx t1)
src/CPSA/Lib/Cohort.hs view
@@ -196,8 +196,7 @@   if visitOldStrandsFirst mode then (compare s0 s1)   else (compare s1 s0) -compareNodeOrder :: Algebra t p g s e c => Mode -> Strand t e ->-                    Int -> Int -> Ordering+compareNodeOrder :: Mode -> Strand t e -> Int -> Int -> Ordering compareNodeOrder mode s i0 i1 =   if (reverseNodeOrder mode == rsearch (role $ inst s)) then (compare i0 i1)   else (compare i1 i0)
src/CPSA/Lib/Declaration.hs view
@@ -138,45 +138,39 @@            Declarations t l mkDecls dl = declsNub Declarations { dlist = dl } -dnon :: (Algebra t p g s e c, Loc l) => Declarations t l ->-        DeclInstList t l+dnon :: Declarations t l -> DeclInstList t l dnon decls = tagDecls "non-orig" decls -dpnon :: (Algebra t p g s e c, Loc l) => Declarations t l ->-         DeclInstList t l+dpnon :: Declarations t l -> DeclInstList t l dpnon decls = tagDecls "pen-non-orig" decls -dunique :: (Algebra t p g s e c, Loc l) => Declarations t l ->-           DeclInstList t l+dunique :: Declarations t l -> DeclInstList t l dunique decls = tagDecls "uniq-orig" decls -duniqgen :: (Algebra t p g s e c, Loc l) => Declarations t l ->-           DeclInstList t l+duniqgen :: Declarations t l -> DeclInstList t l duniqgen decls = tagDecls "uniq-gen" decls  -- Exported-dknon :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t]+dknon :: Declarations t l -> [t] dknon d = map head $ map dterms (dnon d)  -- Exported-dkpnon :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t]+dkpnon :: Declarations t l -> [t] dkpnon d = map head $ map dterms (dpnon d)  -- Exported-dkunique :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t]+dkunique :: Declarations t l -> [t] dkunique d = map head $ map dterms (dunique d) -dkuniqgen :: (Algebra t p g s e c, Loc l) => Declarations t l -> [t]+dkuniqgen :: Declarations t l -> [t] dkuniqgen d = map head $ map dterms (duniqgen d)  -- Exported-dkuniqFull :: (Algebra t p g s e c, Loc l) => Declarations t l ->-              [(t,l)]+dkuniqFull :: Declarations t l -> [(t,l)] dkuniqFull d = map (\x -> (head $ dterms x, head $ dlocs x)) (dunique d)  -- Exported-dkugenFull :: (Algebra t p g s e c, Loc l) => Declarations t l ->-              [(t, Maybe l)]+dkugenFull :: Declarations t l -> [(t, Maybe l)] dkugenFull d = map (\x -> foo x) (duniqgen d)                where                  foo x@@ -247,19 +241,17 @@  -- Exported -- Classifies the declaration tags used in the given Declarations according to format.-declarationTags :: (Algebra t p g s e c, Loc l) => Declarations t l ->-                   [(String, (DeclOutFormat, Bool))]+declarationTags :: Declarations t l -> [(String, (DeclOutFormat, Bool))] declarationTags d = nub $ declarationTagsCore d declFormats  -- Exported-declarationRoleTags :: (Algebra t p g s e c, Loc l) => Declarations t l ->-                       [(String, (DeclOutFormat, Bool))]+declarationRoleTags :: Declarations t l -> [(String, (DeclOutFormat, Bool))] declarationRoleTags d = nub $ declarationTagsCore d declRFormats  -- Common code for declarationRoleTags and declarationTags. -- Looks up the format associated each declaration and pairs the tag with its format. -- Since subtags are subsequent words in the tag string, we look up by the first word.-declarationTagsCore :: (Algebra t p g s e c, Loc l) => Declarations t l ->+declarationTagsCore :: Declarations t l ->                    [(String, (Int, Int))] -> [(String, (DeclOutFormat, Bool))] declarationTagsCore d fmts =    map (\ tag -> (tag, declOutputFormats !! (getOutFormat tag))) dtags@@ -270,18 +262,15 @@                           Just (_,out) -> out  -- Exported-tagDeclsTermsOnly :: (Algebra t p g s e c, Loc l) => String ->-                     Declarations t l -> [t]+tagDeclsTermsOnly :: String -> Declarations t l -> [t] tagDeclsTermsOnly tag decls = map head $ map dterms $ tagDecls tag decls  -- Exported-tagDeclsLocsOnly :: (Algebra t p g s e c, Loc l) => String ->-                    Declarations t l -> [l]+tagDeclsLocsOnly :: String -> Declarations t l -> [l] tagDeclsLocsOnly tag decls = map head $ map dlocs $ tagDecls tag decls  -- Exported-tagDecls :: (Algebra t p g s e c, Loc l) => String -> Declarations t l ->-            DeclInstList t l+tagDecls :: String -> Declarations t l -> DeclInstList t l tagDecls tag decls =     case lookup tag (dlist decls) of       Nothing -> []@@ -325,7 +314,7 @@     g dinst = declInstAux (map f $ dterms dinst) (dlocs dinst) (daux dinst)  -- Exported-declsMapLocations :: (Algebra t p g s e c, Loc l, Loc l') => (l -> l') ->+declsMapLocations :: (Algebra t p g s e c, Loc l') => (l -> l') ->                      Declarations t l -> Declarations t l' declsMapLocations f decls =   mkDecls (map fdecls (dlist decls))@@ -353,7 +342,7 @@     f dinst = declInstAux (map (instantiate env) $ dterms dinst)                        (map locmap $ dlocs dinst) (daux dinst) -avoidTerms :: (Algebra t p g s e c, Loc l) => Declarations t l -> Set t+avoidTerms :: Algebra t p g s e c => Declarations t l -> Set t avoidTerms decls =   S.unions [ns, as, uos, ugs]     where@@ -363,8 +352,7 @@       ugs = S.fromList (dkuniqgen decls)  -------------------------- Constraint checking, where possible ---------------declCheck :: (Algebra t p g s e c, Loc l) => Declarations t l ->-             (Bool, String)+declCheck :: Algebra t p g s e c => Declarations t l -> (Bool, String) declCheck d =    case doDeclCheck d of      Return _ -> (True, "")@@ -377,10 +365,10 @@          failwith "subsort requirements violated" $ subsortCheck d          failwith "[ASSERT FAILED] inst limit requirements violated" $ instlimitCheck d -instlimitCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool+instlimitCheck :: Declarations t l -> Bool instlimitCheck _ = True -neqCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool+neqCheck :: Algebra t p g s e c => Declarations t l -> Bool neqCheck decls =    null failures    where@@ -393,7 +381,7 @@       dts = map dterms ((tagDecls "neq" decls) ++                         (tagDecls "neqlist" decls)) -ltCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool+ltCheck :: Algebra t p g s e c => Declarations t l -> Bool ltCheck decls =    checkAll pairs pairs ((length pairs)-1)    where@@ -405,7 +393,7 @@      evlv x y = [[(ts1 !! 0),(ts2 !! 1)]| ts1 <- y, ts2 <- x, ts1 !! 1 == ts2 !! 0]      pairs = map dterms (tagDecls "lt" decls) -subsortCheck :: (Algebra t p g s e c, Loc l) => Declarations t l -> Bool+subsortCheck :: Algebra t p g s e c => Declarations t l -> Bool subsortCheck decls =    null failures    where
src/CPSA/Lib/Loader.hs view
@@ -571,8 +571,7 @@               (gen', env') <- foldM (loadMaplet kvars vars) (gen, emptyEnv) env               return (mkInstance gen' r env' height) -lookupRole :: (Algebra t p g s e c, Monad m) => Pos ->-              Prot t g -> String -> m (Role t)+lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t) lookupRole _ p role  | role == "" =     return $ listenerRole p lookupRole pos p role =
src/CPSA/Lib/Main.hs view
@@ -105,6 +105,21 @@            | otherwise ->                abort ("Bad algebra: " ++ name) +{--+-- name the algebra and go.+select :: [String] -> Maybe (SExpr Pos) -> Options -> [SExpr Pos] -> IO ()+select files herald opts sexprs =+    case optAlg opts of+      name | name == CPSA.Algebra.Basic.name ->+               go name (CPSA.Algebra.Algebra.origin CPSA.Algebra.Basic.origin)+                  files herald opts sexprs+           | name == CPSA.Algebra.DiffieHellman.name ->+               go name (CPSA.Algebra.Algebra.origin CPSA.Algebra.DiffieHellman.origin)+                  files herald opts sexprs+           | otherwise ->+               abort ("Bad algebra: " ++ name)+--}+ -- Load protocols and preskeletons and print run time information go :: Algebra t p g s e c => String -> g -> [String] ->       Maybe (SExpr Pos) -> Options -> [SExpr Pos] -> IO ()
src/CPSA/Lib/Reduction.hs view
@@ -42,8 +42,7 @@                  parent :: Maybe (LPreskel t g s e) }       deriving Show -withParent :: Algebra t p g s e c => Preskel t g s e ->-              Int ->  LPreskel t g s e -> LPreskel t g s e+withParent :: Preskel t g s e -> Int ->  LPreskel t g s e -> LPreskel t g s e withParent k label parent =     LPreskel k label (1 + depth parent) (Just parent) @@ -65,26 +64,24 @@ newtype Seen t g s e = Seen [IPreskel t g s e]  -- Create a singleton seen history-hist :: Algebra t p g s e c => IPreskel t g s e -> Seen t g s e+hist :: IPreskel t g s e -> Seen t g s e hist ik = Seen [ik]  -- Add an element to the seen history.-remember :: Algebra t p g s e c => IPreskel t g s e ->-            Seen t g s e -> Seen t g s e+remember :: IPreskel t g s e -> Seen t g s e -> Seen t g s e remember ik (Seen seen) = Seen (ik : seen)  -- Find an element of the seen history that satisfies a predicate.-recall :: Algebra t p g s e c => (IPreskel t g s e -> Bool) ->+recall :: (IPreskel t g s e -> Bool) ->           Seen t g s e -> Maybe (IPreskel t g s e) recall f (Seen seen) = L.find f seen  -- Create an empty seen history-void :: Algebra t p g s e c => Seen t g s e+void :: Seen t g s e void = Seen []  -- Merge two seen histories.-merge :: Algebra t p g s e c => Seen t g s e ->-         Seen t g s e -> Seen t g s e+merge :: Seen t g s e -> Seen t g s e -> Seen t g s e merge (Seen xs) (Seen ys) = Seen (xs ++ ys)  -- Contains the result of applying the cohort reduction rule.  The@@ -277,7 +274,7 @@       Nothing -> (kid : unseen, dups)  -- Make a todo list for dump-mktodo :: Algebra t p g s e c => [Reduct t g s e] ->+mktodo :: [Reduct t g s e] ->           [LPreskel t g s e] -> [LPreskel t g s e] ->           [LPreskel t g s e] mktodo reducts todo tobig =@@ -328,8 +325,7 @@       let (n', todo') = foldl (children lk) (n, []) ks'       fast p h ks m n' (todo ++ reverse todo') -children :: Algebra t p g s e c => LPreskel t g s e ->-            (Int, [LPreskel t g s e]) ->+children :: LPreskel t g s e -> (Int, [LPreskel t g s e]) ->             Preskel t g s e -> (Int, [LPreskel t g s e]) children p (n, todo) k =        -- Label a preskeleton here     (n + 1, withParent k n p : todo)
src/CPSA/Lib/State.hs view
@@ -17,14 +17,14 @@ -- label :: Tran t -> Maybe t -- label (Tran (_, _, t)) = t -observer :: Eq t => Tran t -> Bool+observer :: Tran t -> Bool observer (Tran (_, Nothing, _)) = True observer _ = False -path :: Eq t => Tran t -> Bool+path :: Tran t -> Bool path x = not (observer x) -transition :: Eq t => Tran t -> Bool+transition :: Tran t -> Bool transition (Tran (Just _, Just _, _)) = True transition _ = False
src/CPSA/Lib/Strand.hs view
@@ -200,7 +200,7 @@     where       g s (_, t) = foldVars (flip S.insert) s t -listenerTerm :: Algebra t p g s e c => Instance t e -> Maybe t+listenerTerm :: Instance t e -> Maybe t listenerTerm inst =     case rname (role inst) of       "" -> recvTerm (trace inst !! 0) -- Get first term in trace@@ -495,11 +495,10 @@  -- Strand functions -strandInst :: Algebra t p g s e c => Preskel t g s e ->-              Sid -> Instance t e+strandInst :: Preskel t g s e -> Sid -> Instance t e strandInst k strand = insts k !! strand -nstrands :: Algebra t p g s e c => Preskel t g s e -> Int+nstrands :: Preskel t g s e -> Int nstrands k = length (strandids k)  -- Convert the preskeleton made by the loader into the first skeleton@@ -559,8 +558,7 @@             error ("Strand.checkVars: role var in skel " ++ show k)         | otherwise = k -vertex  :: Algebra t p g s e c => Preskel t g s e -> Node ->-           Vertex t e+vertex  :: Preskel t g s e -> Node -> Vertex t e vertex k (s, i) =     nodes (strands k !! s) !! i @@ -579,11 +577,11 @@           p <- M.maybeToList $ generationPos u (trace (inst strand)) ])  -- Do the nodes in the orderings have the right direction?-wellOrdered :: Algebra t p g s e c => Preskel t g s e -> Bool+wellOrdered :: Preskel t g s e -> Bool wellOrdered k =     all pairWellOrdered (edges k) -pairWellOrdered :: Algebra t p g s e c => Edge t e -> Bool+pairWellOrdered :: Edge t e -> Bool pairWellOrdered (n0, n1) =     case (event n0, event n1) of       (Out _, In _) -> True@@ -593,11 +591,11 @@       _ -> False  -- Do transitively reduced orderings have the right direction?-reducedWellOrdered :: Algebra t p g s e c => Preskel t g s e -> Bool+reducedWellOrdered :: Preskel t g s e -> Bool reducedWellOrdered k =     all reducedPairWellOrdered (edges k) -reducedPairWellOrdered :: Algebra t p g s e c => Edge t e -> Bool+reducedPairWellOrdered :: Edge t e -> Bool reducedPairWellOrdered (n0, n1) =     case (event n0, event n1) of       (Out _, In _) -> True@@ -636,7 +634,7 @@ -- Use depth first search to detect cycles.  A graph with no node with -- an indegree of zero is cyclic and must not be checked with depth -- first search.-acyclicOrder :: Algebra t p g s e c => Preskel t g s e -> Bool+acyclicOrder :: Preskel t g s e -> Bool acyclicOrder k =     all (not . backEdge numbering) edges     where@@ -828,7 +826,7 @@                         s)      -- Substition part of homomorphism  -- Extract the protential cohort member from a PRS.-skel :: Algebra t p g s e c => PRS t p g s e c -> Preskel t g s e+skel :: PRS t p g s e c -> Preskel t g s e skel (_, k, _, _, _) = k  -- Returns the preskeletons that result from applying a substitution.@@ -945,7 +943,7 @@     map (\ (n,i) -> (nodeMap mapping n, i)) kpriority  -- Provide a list of nodes with non-default priorities-kpriorities :: Algebra t p g s e c => Preskel t g s e -> [(Node,Int)]+kpriorities :: Preskel t g s e -> [(Node,Int)] kpriorities k =   [((s,i),priority k (s,i)) | s <- [0..(length (insts k) - 1)],                i <- [0..(height ((insts k) !! s) -1)],@@ -958,7 +956,7 @@         In _ -> True         Sync _ -> False -priority :: Algebra t p g s e c => Preskel t g s e -> Node -> Int+priority :: Preskel t g s e -> Node -> Int priority k (s,i) =   case lookup (s,i) (kpriority k) of     Just p -> p@@ -1089,8 +1087,7 @@  -- Ensure that if (s, p) precedes (s", p"), then (s', p) precedes (s", p") -- and if (s", p") precedes (s, p), then (s", p") precedes (s', p)-precedesCheck :: Algebra t p g s e c => Preskel t g s e ->-                 Sid -> Sid -> Edge t e -> Bool+precedesCheck :: Preskel t g s e -> Sid -> Sid -> Edge t e -> Bool precedesCheck k s s' (gn0, gn1)     | s == sid (strand gn0) = graphPrecedes (vertex k (s', pos gn0)) gn1     | s == sid (strand gn1) = graphPrecedes gn0 (vertex k (s', pos gn1))@@ -1360,7 +1357,7 @@ -- Answers for cohorts type Ans t p g s e c = (Preskel t g s e, Node, [Sid], s) -ans :: Algebra t p g s e c => PRS t p g s e c -> [Ans t p g s e c]+ans :: PRS t p g s e c -> [Ans t p g s e c] ans (_, k, n, phi, subst) = [(k, n, phi, subst)]  -- Returns the skeleton associated with a preskeleton or nothing when@@ -1568,8 +1565,7 @@  type Candidate t p g s e c = (Preskel t g s e, [Sid]) -addIdentity :: Algebra t p g s e c => Preskel t g s e ->-               Candidate t p g s e c+addIdentity :: Preskel t g s e -> Candidate t p g s e c addIdentity k = (k, strandids k)  separateVariablesLimit :: Int@@ -1675,7 +1671,7 @@              (declsMapStrands mapping decls0)     terms = iterms insts' -nodeInSkel :: Algebra t p g s e c => Preskel t g s e -> Node -> Bool+nodeInSkel :: Preskel t g s e -> Node -> Bool nodeInSkel k (s, i) =   s >= 0 && s < nstrands k && i >= 0 &&   i < height (strandInst k s)@@ -1997,27 +1993,27 @@      deriving Show  -- Exported-knon :: Algebra t p g s e c => Preskel t g s e -> [t]+knon :: Preskel t g s e -> [t] knon = dknon . decls  -- Exported-kpnon :: Algebra t p g s e c => Preskel t g s e -> [t]+kpnon :: Preskel t g s e -> [t] kpnon = dkpnon . decls  -- Exported-kunique :: Algebra t p g s e c => Preskel t g s e -> [t]+kunique :: Preskel t g s e -> [t] kunique = dkunique . decls  -- Exported-korig :: Algebra t p g s e c => Preskel t g s e -> [(t, [Node])]+korig :: Preskel t g s e -> [(t, [Node])] korig = dkorig . cInfo  -- Exported-kugen :: Algebra t p g s e c => Preskel t g s e -> [(t, [Node])]+kugen :: Preskel t g s e -> [(t, [Node])] kugen = dkugen . cInfo  -- Exported-kuniqgen :: Algebra t p g s e c => Preskel t g s e -> [t]+kuniqgen :: Preskel t g s e -> [t] kuniqgen k = map head $ filter (\ts -> not $ null ts) $ map dterms $ tagDecls "uniq-gen" $ decls k  {-- Exported@@ -2026,7 +2022,7 @@ --}  -- Exported-nsdecls :: (Algebra t p g s e c, Loc l) => Declarations t l -> [Int]+nsdecls :: Declarations t l -> [Int] nsdecls decls =   [length (dknon decls), length (dkpnon decls), length (dkunique decls)] @@ -2133,16 +2129,14 @@           (null ts)  -- Do notation friendly preskeleton well formed check.-reducedWellFormed :: (Monad m, Algebra t p g s e c) =>-                     Preskel t g s e -> m ()+reducedWellFormed :: Monad m => Preskel t g s e -> m () reducedWellFormed k   | reducedWellOrdered k = return ()   | otherwise = fail "reduced preskeleton not well formed"  -- A transition or an observer node should have at most one transition -- node immediately after it.-noStateSplit :: (Monad m, Algebra t p g s e c) =>-                     Preskel t g s e -> m ()+noStateSplit :: Monad m => Preskel t g s e -> m () noStateSplit k   | loop (leadsto k) S.empty = return ()   | otherwise = fail "reduced preskeleton has a state split"@@ -2307,7 +2301,7 @@  -- Determine if a given PRS has a multiple origination of a -- non-numeric fresh value.-hasMultipleOrig :: Algebra t p g s e c => PRS t p g s e c -> Bool+hasMultipleOrig :: PRS t p g s e c -> Bool hasMultipleOrig prs =   any (\(_, l) -> length l > 1) (korig (skel prs)) ||   any (\(_, l) -> length l > 1) (kugen (skel prs))@@ -2318,7 +2312,7 @@   declCheckOrigs (declsMapLocations (permuteNode perm) $ gdecls g) (gdecls g') env  -- Exported-declsOrig :: (Algebra t p g s e c, Loc l) => [Strand t e] ->+declsOrig :: Algebra t p g s e c => [Strand t e] ->              Declarations t l -> ConstInfo t declsOrig strands d =   ConstInfo { dkorig = map (originationNodes strands) (dkunique d),@@ -2577,7 +2571,7 @@     t' <- dkuniqgen $ decls k     match t t' e -inSkel :: Algebra t p g s e c => Preskel t g s e -> (Int, Int) -> Bool+inSkel :: Preskel t g s e -> (Int, Int) -> Bool inSkel k (s, i) =   s >= 0 && s < nstrands k && i >= 0 && i < height (insts k !! s)
src/CPSA/SAS/Main.hs view
@@ -48,7 +48,7 @@                abort ("Bad algebra: " ++ alg)  -- Continue and ignore header if one was found-next :: Algebra t p g s e c => PosHandle -> Handle -> Int ->+next :: PosHandle -> Handle -> Int ->         Maybe (SExpr Pos) -> (State t g c -> Maybe (SExpr Pos)                               -> IO (State t g c)) -> IO () next p h margin Nothing f = -- Found header@@ -103,7 +103,7 @@         Left err ->             abort (show err) -after :: Algebra t p g s e c => Handle -> Int -> State t g c ->+after :: Handle -> Int -> State t g c ->          Maybe (SExpr Pos) -> IO (State t g c) after output margin state (Just sexpr@(L _ (S _ "defprotocol" : _))) =     do
src/CPSA/SAS/SAS.hs view
@@ -215,8 +215,7 @@  -- Find a protocol -findProt :: (Algebra t p g s e c, Monad m) => Pos ->-            [Prot t g c] -> [SExpr Pos] -> m (Prot t g c)+findProt :: Monad m => Pos -> [Prot t g c] -> [SExpr Pos] -> m (Prot t g c) findProt pos ps (S _ name : _) =     case L.find (\p -> name == pname p) ps of       Nothing -> fail (shows pos $ "Protocol " ++ name ++ " unknown")@@ -317,8 +316,7 @@       return (Instance { pos = pos, role = r,                          env = env, height = height }) -lookupRole :: (Algebra t p g s e c, Monad m) => Pos ->-              Prot t g c -> String -> m (Role t c)+lookupRole :: Monad m => Pos -> Prot t g c -> String -> m (Role t c) lookupRole pos prot role =     case L.find (\r -> role == rname r) (roles prot) of       Nothing ->@@ -461,8 +459,7 @@  -- Applies a strand permutation to a node. -- Hope the strand map is valid, or !! will blow up.-loadNodeEq :: Algebra t p g s e c => Preskel t g c ->-              [Int] -> (Node, t) -> (t, t)+loadNodeEq :: Preskel t g c -> [Int] -> (Node, t) -> (t, t) loadNodeEq k perm ((s, i), v) =   (v, nlookup (perm !! s, i) (varmap k))