cpsa 2.0.3 → 2.0.4
raw patch · 42 files changed
+259/−127 lines, 42 filesdep ~base
Dependency ranges changed: base
Files
- ChangeLog +16/−0
- NEWS +8/−0
- cpsa.cabal +7/−7
- doc/Make.hs +19/−1
- doc/cpsaoverview.pdf binary
- doc/cpsaprimer.pdf binary
- doc/cpsaspec.tex +2/−2
- doc/macros.tex +1/−1
- src/CPSA/Annotations/Annotations.hs +2/−1
- src/CPSA/Graph/Loader.hs +3/−1
- src/CPSA/Lib/Cohort.hs +29/−21
- src/CPSA/Lib/Displayer.hs +4/−0
- src/CPSA/Lib/Strand.hs +119/−59
- src/CPSA/Lib/Utilities.hs +5/−6
- tst/Make.hs +17/−1
- tst/completeness-test.tst +1/−1
- tst/dass_simple.tst +1/−1
- tst/denning-sacco.tst +1/−1
- tst/dh.tst +1/−1
- tst/dy.tst +1/−1
- tst/encsig.tst +1/−1
- tst/epmo.tst +1/−1
- tst/epmo_acctnum.tst +1/−1
- tst/ffgg.tst +1/−1
- tst/isoreject.tst +1/−1
- tst/kelly1.tst +1/−1
- tst/kerberos.tst +1/−1
- tst/missing-contraction.tst +1/−1
- tst/neuman-stubblebine-reauth.tst +1/−1
- tst/neuman-stubblebine.tst +1/−1
- tst/ns.tst +1/−1
- tst/nsl3.tst +1/−1
- tst/nsl4cm1.tst +1/−1
- tst/nslsk.tst +1/−1
- tst/or.tst +1/−1
- tst/pca.tst +1/−1
- tst/sigenc.tst +1/−1
- tst/sorted_epmo_acctnum.tst +1/−1
- tst/weird.tst +1/−1
- tst/wmf.tst +1/−1
- tst/woolam.tst +1/−1
- tst/yahalom.tst +1/−1
ChangeLog view
@@ -1,3 +1,19 @@+2010-04-28 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Version): Tagged as version 2.0.4.++ * cpsa.cabal: Base versions are now base >= 3 &&< 5.++2010-04-20 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Strand.hs (acyclicOrder): Fix acyclic check by+ analyzing all edges in graph, not just communication edges.++2010-04-15 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Lib/Strand.hs (firstSkeleton): Input skeletons are no+ longer pruned.+ 2010-03-30 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as version 2.0.3.
NEWS view
@@ -1,5 +1,13 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.0.4++** Input skeletons are no longer pruned++** Bug in the acyclic graph checker fixed+In rare cases, the buggy checker allowed skeletons with circular+node orderings.+ * Changes in version 2.0.3 ** Generalization bug fixed
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 2.0.3+Version: 2.0.4 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.2 License: BSD3@@ -93,7 +93,7 @@ Executable cpsa Main-Is: CPSA/Lib/Main.hs- Build-Depends: base <= 4.2.0.0, containers+ Build-Depends: base >= 3 &&< 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports Hs-Source-Dirs: src@@ -113,7 +113,7 @@ Executable cpsagraph Main-Is: CPSA/Graph/Main.hs- Build-Depends: base <= 4.2.0.0, containers+ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports Hs-Source-Dirs: src@@ -130,7 +130,7 @@ Executable cpsashapes Main-Is: CPSA/Shapes/Main.hs- Build-Depends: base <= 4.2.0.0, containers+ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports Hs-Source-Dirs: src@@ -144,7 +144,7 @@ Executable cpsaannotations Main-Is: CPSA/Annotations/Main.hs- Build-Depends: base <= 4.2.0.0, containers+ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports Hs-Source-Dirs: src@@ -160,7 +160,7 @@ Executable cpsaparameters Main-Is: CPSA/Parameters/Main.hs- Build-Depends: base <= 4.2.0.0, containers+ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports Hs-Source-Dirs: src@@ -174,7 +174,7 @@ Executable cpsapp Main-Is: CPSA/Pretty/Main.hs- Build-Depends: base <= 4.2.0.0, containers+ Build-Depends: base >= 3 && < 5, containers GHC-Options: -Wall -fno-warn-name-shadowing -fwarn-unused-imports Hs-Source-Dirs: src
doc/Make.hs view
@@ -178,6 +178,19 @@ inputExt = shapesRoot ++ cpsaExt, outputExt = annosRoot ++ cpsaExt } +-- Parameters Rule++params :: FilePath -> IO ()+params root =+ do+ make cpsaparametersRule root++cpsaparametersRule :: Rule+cpsaparametersRule = + Rule { prog = "cpsaparameters",+ inputExt = sourceBasicExt,+ outputExt = paramsExt }+ -- Clean generated files cleanse :: FilePath -> IO ()@@ -211,6 +224,9 @@ graphExt :: String graphExt = ".xml" +paramsExt :: String+paramsExt = ".params"+ -- Rule Interpreters -- Make output for root using rule@@ -251,7 +267,9 @@ case code of ExitSuccess -> return () ExitFailure _ ->- fail "Command failed"+ do+ --rm output+ fail "Command failed" -- Remove a file
doc/cpsaoverview.pdf view
binary file changed (75334 → 75526 bytes)
doc/cpsaprimer.pdf view
binary file changed (177855 → 177854 bytes)
doc/cpsaspec.tex view
@@ -2520,7 +2520,7 @@ Let~$t_c$ be a critical message at~$n$ in~$k$, and~$i$ be an instance of a regular, non-listener role. Skeleton~$k_2$ is a \emph{regular augmentation} if-$k\reduction{\ops{A}_{i,n}}k_0\reduction{\ops{S}_\sigma}k_1+$k\reduction{\ops{S}_\sigma}k_0\reduction{\ops{A}_{i,n}}k_1 \reduction{\fn{skel}}k_2$ for some substitution~$\sigma$ and~$t_c$ is solved in~$k_2$ after~$k_0$ at~$n$. \end{defn}@@ -2579,7 +2579,7 @@ in skeleton~$k$. For each substitution-instance pair~$(\sigma,i)$ that satisfies some properties, there is a potential regular augmentation with~$\comp{\reduction{\fn{skel}}}%-{\comp{\reduction{\ops{S}_\sigma}}{\reduction{\ops{A}_{i,n}}}}$.+{\comp{\reduction{\ops{A}_{i,n}}}{\reduction{\ops{S}_\sigma}}}$. When successful, the message~$t$ in the last node of the added strand is outbound, carries~$\sigma(t_c)$, but~$\sigma(t_c)$ is not carried only within escape set~$\sigma(T_e)$ in~$t$. Moreover, for every
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.0.3}+\newcommand{\version}{2.0.4} \newcommand{\cpsacopying}{\begingroup \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2009 The MITRE Corporation. Permission to copy without fee all or part of
src/CPSA/Annotations/Annotations.hs view
@@ -422,10 +422,11 @@ before :: (Algebra t p g s e c, Monad m) => Pos -> Preskel t p g s e c -> m [(Node, [Node])] before pos k =- case isAcyclic graph (zip [0..] (replicate (length strands) 0)) of+ case isAcyclic graph nodes of False -> fail (shows pos "Cycle found") True -> return $ alist (traces k) $ orient (traces k) closure where+ nodes = [(s, p) | s <- nats $ length strands, p <- nats $ strands !! s] closure = close strands (orderings k) strands = map height (insts k) graph = adj strands (orderings k)
src/CPSA/Graph/Loader.hs view
@@ -222,7 +222,9 @@ let graph = adj heights pairs let pairs' = reduce graph pairs let strands = length insts- case isAcyclic graph (zip [0..] (replicate strands 0)) of+ let nodes = [(s, p) | s <- nats strands,+ p <- nats $ heights !! s]+ case isAcyclic graph nodes of False -> fail (shows pos "Cycle found") True -> return Preskel { protocol = name p,
src/CPSA/Lib/Cohort.hs view
@@ -57,6 +57,28 @@ context ts = addToContext emptyContext ts --} +-- Compile time switches for expermentation.++-- Filter a cohort for skeletons that solve the test. Turn off only+-- to debug the other parts of the test solving algorithm.+useSolvedFilter :: Bool+useSolvedFilter = True++-- Filter COWS function output so that it returns only MGUs. Turn off+-- to checking that an algebra's MGU filter is working.+useMguFilter :: Bool+useMguFilter = True++-- Solve encryption tests first when possible.+useEncryptionFirstOrder :: Bool+useEncryptionFirstOrder = True++-- Experiment: try adding orderings while contracting.+useContractionsWithOrdering :: Bool+useContractionsWithOrdering = False++-- Penetrator derivable predicate and checking for unrealized skeletons.+ derivable :: Algebra t p g s e c => Set t -> Set t -> t -> Bool derivable avoid sent term = let (knowns, unknowns) = decompose sent avoid in@@ -131,10 +153,6 @@ ts = S.map (evtTerm . event) vs -- Outbound predecessors (a, _) = avoid k --- This switch controls the use of solved filtering.-useSolvedFilter :: Bool-useSolvedFilter = True- maybeSolved :: Algebra t p g s e c => t -> Maybe t -> Set t -> Preskel t p g s e c -> Node -> s -> Bool maybeSolved ct ek escape k n subst =@@ -191,9 +209,6 @@ else Just $ testNode k u ts der (graphNode n) t -useEncryptionFirstOrder :: Bool-useEncryptionFirstOrder = True- -- Look for a critical term that makes this node a test node. testNode :: Algebra t p g s e c => Preskel t p g s e c -> [t] -> Set t -> (t -> Bool) -> Node -> t ->@@ -210,7 +225,7 @@ loop cts else solveNode k ct ek n t escape- cts = + cts = if useEncryptionFirstOrder then map g (filter h (encryptions t)) ++ map f (filter (flip carriedBy t) u)@@ -260,9 +275,6 @@ lsns = addListeners k ct ek n t escape cause cause = Cause (dir ek) n ct escape -useContractionsWithOrdering :: Bool-useContractionsWithOrdering = False- -- Contractions contractions :: Algebra t p g s e c => Preskel t p g s e c ->@@ -297,9 +309,6 @@ subst <- substs, s <- maybeToList $ unify a e subst ] -useMguFilter :: Bool-useMguFilter = True- -- Filter out non-most general unifiers mgus :: Algebra t p g s e c => [(g, s)] -> [(g, s)] mgus substs =@@ -352,8 +361,7 @@ Role t p g s e c -> [Preskel t p g s e c] roleAugs k ct ek n escape cause role = [ k' | (subst', inst) <- transformingNode ct escape role subst,- (k', n', subst'') <-- maybeToList $ augment k n cause role subst' inst,+ (k', n', subst'') <- augment k n cause role subst' inst, maybeSolved ct ek escape k' n' subst'' ] where subst = cloneRoleVars (gen k) role@@ -361,14 +369,14 @@ -- Generate a fresh set of role variables cloneRoleVars :: Algebra t p g s e c => g -> Role t p g s e c -> (g, s) cloneRoleVars gen role =- grow (rvars role) gen emptySubst+ grow (rvars role) gen emptyEnv where- grow [] gen subst = (gen, subst)- grow (t : ts) gen subst =+ grow [] gen env = (gen, substitution env)+ grow (t : ts) gen env = let (gen', t') = clone gen t in- case unify t t' (gen', subst) of+ case match t t' (gen', env) of Nothing -> error "Cohort.grow: Internal error"- Just (gen'', subst') -> grow ts gen'' subst'+ Just (gen'', env') -> grow ts gen'' env' transformingNode :: Algebra t p g s e c => t -> Set t -> Role t p g s e c -> (g, s) ->
src/CPSA/Lib/Displayer.hs view
@@ -133,6 +133,10 @@ displayCause (L () (S () "contracted" : substitution)) cause AddedOrdering node cause -> displayCause (L () [S () "added-ordering", displayNode node]) cause+ Displaced s s' role height cause ->+ displayCause+ (L () [S () "displaced", N () s, N () s', S () role, N () height])+ cause AddedStrand role height cause -> displayCause (L () [S () "added-strand", S () role, N () height]) cause
src/CPSA/Lib/Strand.hs view
@@ -63,6 +63,16 @@ context ts = addToContext emptyContext ts --} +-- Compile time switches for expermentation.++-- Sanity check: ensure no role variable occurs in a skeleton.+useCheckVars :: Bool+useCheckVars = False++-- Experiment: try adding displacements to the augmentation procedure.+useDisplacement :: Bool+useDisplacement = False+ -- Instances and Strand Identifiers -- An Instance is an instance of a role, in the sense that each@@ -237,6 +247,10 @@ graphPair :: GraphEdge e i -> Pair graphPair (n0, n1) = (graphNode n0, graphNode n1) +graphEdges :: [GraphStrand e i] -> [GraphEdge e i]+graphEdges strands =+ [ (dst, src) | s <- strands, src <- nodes s, dst <- preds src ]+ data Graph e i = Graph { gstrands :: [GraphStrand e i], gedges :: [GraphEdge e i] }@@ -366,6 +380,7 @@ = New | Contracted s (Cause t p g s e c) | AddedOrdering Node (Cause t p g s e c)+ | Displaced Int Int String Int (Cause t p g s e c) | AddedStrand String Int (Cause t p g s e c) | AddedListener t (Cause t p g s e c) | Generalized (Method t p g s e c)@@ -400,7 +415,7 @@ firstSkeleton k = do k <- wellFormedPreskel k- k' <- toSkeleton True k -- only k' should have pov = Nothing+ k' <- toSkeleton False k -- only k' should have pov = Nothing return $ k' { prob = strandids k', pov = Just k' } -- Create a preskeleton. The node ordering relation is put into the@@ -418,24 +433,38 @@ strands = gstrands g edges = gedges g orig = map (originationNodes strands) unique'- edges' = addSuccessors strands edges- tc = filter pairWellOrdered (graphClose edges') in- Preskel { gen = gen,- protocol = protocol,- insts = insts,- strands = strands,- orderings = orderings',- edges = edges,- knon = L.nub non,- kunique = unique',- kcomment = [],- korig = orig,- tc = map graphPair tc,- strandids = nats (length insts),- operation = oper,- prob = prob,- pov = pov }+ tc = filter pairWellOrdered (graphClose $ graphEdges strands)+ k = Preskel { gen = gen,+ protocol = protocol,+ insts = insts,+ strands = strands,+ orderings = orderings',+ edges = edges,+ knon = L.nub non,+ kunique = unique',+ kcomment = [],+ korig = orig,+ tc = map graphPair tc,+ strandids = nats (length insts),+ operation = oper,+ prob = prob,+ pov = pov } in+ if useCheckVars then+ checkVars k+ else k +checkVars :: Algebra t p g s e c => Preskel t p g s e c ->+ Preskel t p g s e c+checkVars k =+ foldl f k rolevars+ where+ skelvars = S.fromList $ kvars k+ rolevars = concatMap (rvars . role) (insts k)+ f k v+ | S.member v skelvars =+ error ("Strand.checkVars: role var in skel " ++ show k)+ | otherwise = k+ vertex :: Algebra t p g s e c => Preskel t p g s e c -> Node -> Vertex t p g s e c vertex k (s, p) =@@ -543,12 +572,13 @@ -- first search. acyclicOrder :: Algebra t p g s e c => Preskel t p g s e c -> Bool acyclicOrder k =- all (not . backEdge numbering) (edges k)+ all (not . backEdge numbering) edges where+ edges = graphEdges (strands k) -- The starting set contains the last node in every strand start = map (last . nodes) (strands k) -- Remove nodes that have non-zero indegree- start' = foldl (flip L.delete) start (map fst (edges k))+ start' = foldl (flip L.delete) start (map fst edges) numbering = dfs preds start' -- Variables in this preskeleton, excluding ones in roles, and ones@@ -560,18 +590,6 @@ f s i = foldl g s (reify (rvars (role i)) (env i)) g s (_, t) = foldVars (flip S.insert) s t -{---kvars :: Algebra t p g s e c => Preskel t p g s e c -> [t]-kvars k =- S.elems $ foldl addInstVars S.empty (insts k)--addInstVars :: Algebra t p g s e c => Set t -> Instance t p g s e c -> Set t-addInstVars vars inst =- foldl f vars (reify (rvars (role inst)) (env inst))- where- f s (_, t) = foldVars (flip S.insert) s t---}- -- Ensure each role unique origination assumption mapped by an -- instance originates in the instance's strand. roleOrigCheck :: Algebra t p g s e c => Preskel t p g s e c -> Bool@@ -587,21 +605,6 @@ Just ns -> any (\(s, p)-> sid strand == s && p == pos) ns | otherwise = True --- Support for preskeleton transitive closure computation---- Add the successor edges from a list of strands to another list of edges.-addSuccessors :: [GraphStrand e i] -> [GraphEdge e i] -> [GraphEdge e i]-addSuccessors strands edges =- foldl f edges strands- where- f edges strand =- successors edges (nodes strand)--successors :: [(a, a)] -> [a] -> [(a, a)]-successors z (x : y : xs) =- successors ((x, y) : z) (y : xs)-successors z _ = z- -- Isomorphism Check -- Are two skeletons equivalent? Two skeletons are equivalent if they@@ -805,7 +808,7 @@ k' <- wellFormedPreskel k' case validateSubst k subst k' of True -> return (k', n, compose subst hsubst)- False -> fail ""+ False -> Nothing -- Monad version of mapAccumR foldMapM :: Monad m => (a -> b -> m (a, c)) -> a -> [b] -> m (a, [c])@@ -829,6 +832,7 @@ Contracted (compose subst s) (substCause subst cause) substOper subst (AddedOrdering node cause) = AddedOrdering node (substCause subst cause)+substOper _ m@(Displaced _ _ _ _ _) = m substOper subst (AddedStrand role height cause) = AddedStrand role height (substCause subst cause) substOper subst (AddedListener t cause) =@@ -842,6 +846,7 @@ substCause subst (Cause dir n t escape) = Cause dir n (substitute subst t) (S.map (substitute subst) escape) +-- Ensure origination nodes a preserved as required to be a homomorphism validateSubst :: Algebra t p g s e c => Preskel t p g s e c -> s -> Preskel t p g s e c -> Bool validateSubst k subst k' =@@ -1176,8 +1181,22 @@ augment :: Algebra t p g s e c => Preskel t p g s e c -> Node -> Cause t p g s e c -> Role t p g s e c -> (g, s) ->- Instance t p g s e c -> Maybe (PRS t p g s e c)-augment k n cause role subst inst =+ Instance t p g s e c -> [PRS t p g s e c]+augment k0 n cause role subst inst =+ case substAndAugment k0 n cause role subst inst of+ Nothing -> []+ Just prs@(k, n, hsubst) ->+ case useDisplacement of+ False -> [prs]+ True ->+ case hull True prs of+ Nothing -> augDisplace k0 k n hsubst+ Just prs -> prs : augDisplace k0 k n hsubst++substAndAugment :: Algebra t p g s e c => Preskel t p g s e c -> Node ->+ Cause t p g s e c -> Role t p g s e c -> (g, s) ->+ Instance t p g s e c -> Maybe (PRS t p g s e c)+substAndAugment k n cause role subst inst = do let operation' = AddedStrand (rname role) (height inst) cause prs <- ksubst (k { operation = operation' }, n, emptySubst) subst@@ -1187,16 +1206,17 @@ Instance t p g s e c -> Maybe (PRS t p g s e c) aug (k, n, hsubst) inst = do- k' <- wellFormedPreskel k'- hull True (k', n, hsubst)- where- k' = newPreskel (gen k) (protocol k) insts'+ let insts' = (insts k) ++ [inst]+ let pair = ((length (insts k), height inst - 1), n)+ let orderings' = pair : orderings k+ let non' = inheritRnon inst ++ (knon k)+ let unique' = inheritRunique inst ++ (kunique k)+ let k' = newPreskel (gen k) (protocol k) insts' orderings' non' unique' (operation k) (prob k) (pov k)- insts' = (insts k) ++ [inst]- pair = ((length (insts k), height inst - 1), n)- orderings' = pair : orderings k- non' = inheritRnon inst ++ (knon k)- unique' = inheritRunique inst ++ (kunique k)+ k' <- wellFormedPreskel k'+ case useDisplacement of+ False -> hull True (k', n, hsubst)+ True -> return (k', n, hsubst) -- Inherit non-originating atoms if the traces is long enough inheritRnon :: Algebra t p g s e c => Instance t p g s e c -> [t]@@ -1213,6 +1233,46 @@ map (instantiate (env i) . fst) $ filter f rorigs where f (_, pos) = pos < height i++augDisplace :: Algebra t p g s e c => Preskel t p g s e c ->+ Preskel t p g s e c -> Node -> s -> [PRS t p g s e c]+augDisplace k0 k n hsubst =+ let s = nstrands k - 1 in+ [k' | s' <- [0..(s-1)],+ k' <- M.maybeToList $ augDisplaceStrands k0 k n hsubst s s']++augDisplaceStrands :: Algebra t p g s e c => Preskel t p g s e c ->+ Preskel t p g s e c -> Node -> s ->+ Sid -> Sid -> Maybe (PRS t p g s e c)+augDisplaceStrands k0 k n hsubst s s' =+ do+ (s, s', subst) <- unifyStrands k s s'+ let op = addedToDisplaced (operation k) s s'+ prs <- augSubst k0 (k { operation = op}, n, hsubst) subst+ prs <- compress prs s s'+ hull True prs++addedToDisplaced :: Algebra t p g s e c => Operation t p g s e c -> + Int -> Int -> Operation t p g s e c+addedToDisplaced (AddedStrand role height cause) s s' =+ Displaced s s' role height cause+addedToDisplaced _ _ _ = error "Strand.addedToDisplaced: Bad operation"++augSubst :: Algebra t p g s e c => Preskel t p g s e c ->+ PRS t p g s e c -> (g, s) -> Maybe (PRS t p g s e c)+augSubst k0 (k, n, hsubst) (gen, subst) =+ do+ (gen', insts') <- foldMapM (substInst subst) gen (insts k)+ let non' = map (substitute subst) (knon k)+ let unique' = map (substitute subst) (kunique k)+ let operation' = substOper subst (operation k)+ let k' = newPreskel gen' (protocol k) insts'+ (orderings k) non' unique' operation' (prob k) (pov k)+ k' <- wellFormedPreskel k'+ let hsubst' = compose subst hsubst+ case validateSubst k0 hsubst' k' of+ True -> return (k', n, hsubst')+ False -> Nothing -- Listener Augmentation
src/CPSA/Lib/Utilities.hs view
@@ -9,6 +9,7 @@ module CPSA.Lib.Utilities where import qualified Data.Set as S+import qualified Data.List as L import Data.List (foldl') adjoin :: Eq a => a -> [a] -> [a]@@ -48,14 +49,12 @@ -- Is graph acyclic? isAcyclic :: Ord a => (a -> [a]) -> [a] -> Bool isAcyclic adj nodes =- all (not . backEdge numbering) (S.toList edges)+ all (not . backEdge numbering) edges where- numbering = dfs adj (S.toList start)+ numbering = dfs adj start -- Remove nodes that have non-zero indegree- start = S.difference (S.fromList nodes) (S.map fst edges)- edges = foldl' f S.empty nodes- f edges src = foldl' (g src) edges (adj src)- g src edges dst = S.insert (dst, src) edges+ start = foldl' (flip L.delete) nodes (map fst edges)+ edges = [ (dst, src) | src <- nodes, dst <- adj src ] -- Compute a depth first search numbering of nodes using postorder. -- With postorder, only back edges go from a lower number to a higher
tst/Make.hs view
@@ -178,6 +178,19 @@ inputExt = shapesRoot ++ cpsaExt, outputExt = annosRoot ++ cpsaExt } +-- Parameters Rule++params :: FilePath -> IO ()+params root =+ do+ make cpsaparametersRule root++cpsaparametersRule :: Rule+cpsaparametersRule = + Rule { prog = "cpsaparameters",+ inputExt = sourceBasicExt,+ outputExt = paramsExt }+ -- Clean generated files cleanse :: FilePath -> IO ()@@ -211,6 +224,9 @@ graphExt :: String graphExt = ".xml" +paramsExt :: String+paramsExt = ".params"+ -- Rule Interpreters -- Make output for root using rule@@ -252,7 +268,7 @@ ExitSuccess -> return () ExitFailure _ -> do- rm output+ --rm output fail "Command failed" -- Remove a file
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol completeness-test basic
tst/dass_simple.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol dass basic
tst/denning-sacco.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol denning-sacco basic
tst/dh.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol dhke diffie-hellman
tst/dy.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol dy basic
tst/encsig.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol mult-keys-enc-sig basic
tst/epmo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol epmo basic
tst/epmo_acctnum.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol epmo_acctnum basic
tst/ffgg.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol ffgg basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol kerberos basic
tst/missing-contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol missing-contraction basic
tst/neuman-stubblebine-reauth.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol neuman-stubblebine basic
tst/neuman-stubblebine.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol neuman-stubblebine basic
tst/ns.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol ns basic
tst/nsl3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol nsl3 basic
tst/nsl4cm1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol nsl4cm basic
tst/nslsk.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol nslsk basic
tst/or.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol or basic
tst/pca.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol aic basic
tst/sigenc.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol mult-keys-sig-enc basic
tst/sorted_epmo_acctnum.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol epmo_acctnum basic
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol wierd basic
tst/wmf.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol wide-mouth-frog basic
tst/woolam.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol woolam basic
tst/yahalom.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.0.3")+(comment "CPSA 2.0.4") (comment "All input read") (defprotocol yahalom basic