diff --git a/ChangeLog b/ChangeLog
--- a/ChangeLog
+++ b/ChangeLog
@@ -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.
diff --git a/NEWS b/NEWS
--- a/NEWS
+++ b/NEWS
@@ -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
diff --git a/cpsa.cabal b/cpsa.cabal
--- a/cpsa.cabal
+++ b/cpsa.cabal
@@ -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
diff --git a/doc/Make.hs b/doc/Make.hs
--- a/doc/Make.hs
+++ b/doc/Make.hs
@@ -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
 
diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf
Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ
diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf
Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ
diff --git a/doc/cpsaspec.tex b/doc/cpsaspec.tex
--- a/doc/cpsaspec.tex
+++ b/doc/cpsaspec.tex
@@ -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
diff --git a/doc/macros.tex b/doc/macros.tex
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -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
diff --git a/src/CPSA/Annotations/Annotations.hs b/src/CPSA/Annotations/Annotations.hs
--- a/src/CPSA/Annotations/Annotations.hs
+++ b/src/CPSA/Annotations/Annotations.hs
@@ -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)
diff --git a/src/CPSA/Graph/Loader.hs b/src/CPSA/Graph/Loader.hs
--- a/src/CPSA/Graph/Loader.hs
+++ b/src/CPSA/Graph/Loader.hs
@@ -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,
diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs
--- a/src/CPSA/Lib/Cohort.hs
+++ b/src/CPSA/Lib/Cohort.hs
@@ -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) ->
diff --git a/src/CPSA/Lib/Displayer.hs b/src/CPSA/Lib/Displayer.hs
--- a/src/CPSA/Lib/Displayer.hs
+++ b/src/CPSA/Lib/Displayer.hs
@@ -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
diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs
--- a/src/CPSA/Lib/Strand.hs
+++ b/src/CPSA/Lib/Strand.hs
@@ -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
 
diff --git a/src/CPSA/Lib/Utilities.hs b/src/CPSA/Lib/Utilities.hs
--- a/src/CPSA/Lib/Utilities.hs
+++ b/src/CPSA/Lib/Utilities.hs
@@ -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
diff --git a/tst/Make.hs b/tst/Make.hs
--- a/tst/Make.hs
+++ b/tst/Make.hs
@@ -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
diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst
--- a/tst/completeness-test.tst
+++ b/tst/completeness-test.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol completeness-test basic
diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst
--- a/tst/dass_simple.tst
+++ b/tst/dass_simple.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol dass basic
diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst
--- a/tst/denning-sacco.tst
+++ b/tst/denning-sacco.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol denning-sacco basic
diff --git a/tst/dh.tst b/tst/dh.tst
--- a/tst/dh.tst
+++ b/tst/dh.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol dhke diffie-hellman
diff --git a/tst/dy.tst b/tst/dy.tst
--- a/tst/dy.tst
+++ b/tst/dy.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol dy basic
diff --git a/tst/encsig.tst b/tst/encsig.tst
--- a/tst/encsig.tst
+++ b/tst/encsig.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol mult-keys-enc-sig basic
diff --git a/tst/epmo.tst b/tst/epmo.tst
--- a/tst/epmo.tst
+++ b/tst/epmo.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol epmo basic
diff --git a/tst/epmo_acctnum.tst b/tst/epmo_acctnum.tst
--- a/tst/epmo_acctnum.tst
+++ b/tst/epmo_acctnum.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol epmo_acctnum basic
diff --git a/tst/ffgg.tst b/tst/ffgg.tst
--- a/tst/ffgg.tst
+++ b/tst/ffgg.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol ffgg basic
diff --git a/tst/isoreject.tst b/tst/isoreject.tst
--- a/tst/isoreject.tst
+++ b/tst/isoreject.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol isoreject basic
diff --git a/tst/kelly1.tst b/tst/kelly1.tst
--- a/tst/kelly1.tst
+++ b/tst/kelly1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol kelly1 basic
diff --git a/tst/kerberos.tst b/tst/kerberos.tst
--- a/tst/kerberos.tst
+++ b/tst/kerberos.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol kerberos basic
diff --git a/tst/missing-contraction.tst b/tst/missing-contraction.tst
--- a/tst/missing-contraction.tst
+++ b/tst/missing-contraction.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol missing-contraction basic
diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst
--- a/tst/neuman-stubblebine-reauth.tst
+++ b/tst/neuman-stubblebine-reauth.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol neuman-stubblebine basic
diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst
--- a/tst/neuman-stubblebine.tst
+++ b/tst/neuman-stubblebine.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol neuman-stubblebine basic
diff --git a/tst/ns.tst b/tst/ns.tst
--- a/tst/ns.tst
+++ b/tst/ns.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol ns basic
diff --git a/tst/nsl3.tst b/tst/nsl3.tst
--- a/tst/nsl3.tst
+++ b/tst/nsl3.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol nsl3 basic
diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst
--- a/tst/nsl4cm1.tst
+++ b/tst/nsl4cm1.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol nsl4cm basic
diff --git a/tst/nslsk.tst b/tst/nslsk.tst
--- a/tst/nslsk.tst
+++ b/tst/nslsk.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol nslsk basic
diff --git a/tst/or.tst b/tst/or.tst
--- a/tst/or.tst
+++ b/tst/or.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol or basic
diff --git a/tst/pca.tst b/tst/pca.tst
--- a/tst/pca.tst
+++ b/tst/pca.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol aic basic
diff --git a/tst/sigenc.tst b/tst/sigenc.tst
--- a/tst/sigenc.tst
+++ b/tst/sigenc.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol mult-keys-sig-enc basic
diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst
--- a/tst/sorted_epmo_acctnum.tst
+++ b/tst/sorted_epmo_acctnum.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol epmo_acctnum basic
diff --git a/tst/weird.tst b/tst/weird.tst
--- a/tst/weird.tst
+++ b/tst/weird.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol wierd basic
diff --git a/tst/wmf.tst b/tst/wmf.tst
--- a/tst/wmf.tst
+++ b/tst/wmf.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol wide-mouth-frog basic
diff --git a/tst/woolam.tst b/tst/woolam.tst
--- a/tst/woolam.tst
+++ b/tst/woolam.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol woolam basic
diff --git a/tst/yahalom.tst b/tst/yahalom.tst
--- a/tst/yahalom.tst
+++ b/tst/yahalom.tst
@@ -1,4 +1,4 @@
-(comment "CPSA 2.0.3")
+(comment "CPSA 2.0.4")
 (comment "All input read")
 
 (defprotocol yahalom basic