cpsa 2.2.0 → 2.2.1
raw patch · 37 files changed
+1169/−397 lines, 37 files
Files
- ChangeLog +60/−0
- NEWS +24/−1
- README +16/−4
- cpsa.cabal +4/−3
- doc/Make.hs +16/−10
- doc/cpsa.mk +5/−1
- doc/cpsadesign.pdf binary
- doc/cpsaoverview.pdf binary
- doc/cpsaprimer.pdf binary
- doc/cpsaprimer.tex +1/−1
- doc/cpsaspec.pdf binary
- doc/cpsatheory.pdf binary
- doc/cpsatheory.tex +4/−4
- doc/cpsauser.html +9/−12
- doc/index.html +5/−5
- doc/macros.tex +1/−1
- src/CPSA/Annotations/Main.hs +1/−1
- src/CPSA/Diff/Main.hs +5/−4
- src/CPSA/DiffieHellman/Algebra.hs +1/−1
- src/CPSA/Graph/CompactView.hs +11/−1
- src/CPSA/Graph/ExpandedView.hs +89/−112
- src/CPSA/Graph/LaTeXView.hs +15/−9
- src/CPSA/Graph/Loader.hs +49/−26
- src/CPSA/Graph/Main.hs +81/−33
- src/CPSA/Graph/Preskeleton.hs +4/−7
- src/CPSA/Graph/SVG.hs +14/−6
- src/CPSA/Graph/Tree.hs +80/−62
- src/CPSA/Lib/Reduction.hs +1/−7
- src/CPSA/Lib/Strand.hs +3/−3
- src/CPSA/Lib/Utilities.hs +7/−0
- src/ghcmemlimit +15/−0
- src/sliders.js +0/−70
- src/zoom.js +7/−0
- tst/Make.hs +15/−9
- tst/Makefile +4/−4
- tst/tor.scm +41/−0
- tst/tor.tst +581/−0
ChangeLog view
@@ -1,3 +1,63 @@+2010-12-20 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Version): Tagged as version 2.2.1.++2010-12-16 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Diff/Main.hs (showDiff): Closed output handle when a+ difference is found so as to ensure the output is flushed before+ exiting signaling failure.++2010-12-15 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Graph/ExpandedView.hs (treelessView): Added+ treelessView, an output format that just prints the skeletons.+ It's meant to be used on cpsagraph input that is too large to+ handle otherwise.++2010-12-14 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Graph/Loader.hs (loadFirst, loadNext): The loader+ returns one preskeleton per call, rather than returning the list+ of all preskeletons in the input. This allows modes of operation+ in which only a small portion of the input is in memory at any one+ time.++2010-12-10 John D. Ramsdell <ramsdell@mitre.org>++ * doc/cpsa.mk, doc/Make.hs: Changed the extension associated with+ cpsagraph output from .xml to .xhtml.++ * doc/cpsa.mk, doc/Make.hs: Changed the extension associated with+ cpsaparameters output from .params to _parameters.txt.++2010-12-09 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Graph/Tree.hs: Dump commented out copy of the old+ algorithm.++ * src/CPSA/Graph/ExpandedView.hs (kdrawer): Replaced tree+ sorting with a queue to produce a breadth first ordering of the+ tree on output. This change has a big impact on performance on+ large inputs.++2010-12-08 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Graph/ExpandedView.hs (zoomControl): Omit need to run a+ script at load time by adding the attribute onchange="zoom(event)".++2010-12-07 John D. Ramsdell <ramsdell@mitre.org>++ * src/CPSA/Graph/ExpandedView.hs: Changed the scripting to better+ support very large documents. Instead of running a script to+ insert the new control, this version builds the controls into the+ document. The script run a load time just registers event+ handlers.++ * src/CPSA/Graph/Tree.hs (forest): Changed data structures used to+ form the forest so as to replace linear searches on lists with+ binary searches on maps and sets.+ 2010-12-01 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as version 2.2.0.
NEWS view
@@ -1,5 +1,28 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.1++** Web graph output extension changed from .xml to .xhtml+ Firefox works better with this file extension.++** No HTML5 sliders+ The zoom option for cpsagraph no longer generates HTML5 sliders due+ to changes designed to make large documents load faster.++** Program cpsagraph tree construction algorithm improved+ The time and space used to form derivation trees has been reduced.++** Treeless option added to cpsagraph+ For input too large to process otherwise, option --treeless+ generates an XHTML document without trees, and therefore uses less+ memory. It works as long as each skeleton in the input fits into+ memory. The default XHTML generator requires that all skeletons+ fit in memory simultaneously.++** Output bug in cpsadiff fixed+ A bug in cpsadiff that caused it to fail to print all of its output+ before it exited has been fixed.+ * Changes in version 2.2.0 ** Pruning reverted to CPSA 2.1.0 behavior@@ -35,7 +58,7 @@ warning message. This change makes it easier to analyze runs that fail to terminate. -** Green marks realized reception nodes+** Blue marks realized reception nodes The program cpsagraph uses the color blue to distinguish realized reception nodes from transmission nodes.
README view
@@ -13,8 +13,8 @@ : To analyze a protocol in prob.scm type: $ cpsa -o prob.txt prob.scm-$ cpsagraph -x -o prob.xml prob.txt-$ firefox -remote "openFile(`pwd`/prob.xml)"+$ cpsagraph -o prob.xhtml prob.txt+$ firefox -remote "openFile(`pwd`/prob.xhtml)" : To view the user guide: $ firefox -remote "openFile($HOME/share/cpsa-X.Y.Z/doc/cpsauser.html)"@@ -28,8 +28,8 @@ : To analyze a protocol in prob.scm type: $ cpsa -o prob.txt prob.scm-$ cpsagraph -c -o prob.svg prob.txt-$ open prob.svg+$ cpsagraph -o prob.xhtml prob.txt+$ open prob.xhtml : To view the user guide: $ open $HOME/share/cpsa-X.Y.Z/doc/cpsauser.html@@ -107,6 +107,18 @@ Don't develop your protocols in the tst directory. The Makefile is optimized for testing the cpsa program, not analyzing protocols.++ADDITIONAL PROGRAMS++The src directory of the source distributions includes programs+written in Scheme, Prolog, and Elisp for performing tasks. Use them+as templates for your special perpose CPSA analysis and transformation+needs.++On Linux, the GHC runtime can request so much memory that thrashing+results. The script in src/ghcmemlimit sets an environment variable+that limits memory to the amount of free and reclaimable memory on+your machine. WEB CPSA
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 2.2.0+Version: 2.2.1 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3@@ -55,7 +55,7 @@ doc/SDAG.lhs doc/cpsatheory.pdf doc/cpsaspec.pdf doc/cpsadesign.pdf src/index.html src/cpsacgi src/cpsacgi.py src/cpsa2svg src/cpsa.el src/httpd_allow_execmem.te src/cpsaops.scm src/preskel- src/cpsa.pl src/pp.pl src/sexpr.pl src/sliders.js src/js2hs+ src/cpsa.pl src/pp.pl src/sexpr.pl src/zoom.js src/js2hs src/ghcmemlimit tst/README tst/Makefile tst/Make.hs tst/checktst tst/cpsagraphall tst/cpsashapesall tst/blanchet.scm tst/blanchet.tst tst/completeness-test.scm@@ -89,7 +89,8 @@ tst/wide-mouth-frog.tst tst/wonthull2.scm tst/wonthull2.tst tst/wonthull3.scm tst/wonthull3.tst tst/wonthull.scm tst/wonthull.tst tst/woolam.scm tst/woolam.tst tst/yahalom-6.3.6.scm- tst/yahalom-6.3.6.tst tst/yahalom.scm tst/yahalom.tst+ tst/yahalom-6.3.6.tst tst/yahalom.scm tst/yahalom.tst tst/tor.scm+ tst/tor.tst -- Disable with -f-par option during configuration.
doc/Make.hs view
@@ -14,7 +14,7 @@ *Make> cpsa "prob" -If successful, the analysis is in the file prob.xml, which can be+If successful, the analysis is in the file prob.xhtml, which can be viewed with a standards-compliant browser. To analyze a problem in prob.sch using the Diffie-Hellman algebra, type:@@ -25,13 +25,13 @@ *Make> shapes "prob" -If successful, the shapes are in the file prob_shapes.xml.+If successful, the shapes are in the file prob_shapes.xhtml. When the protocol is annotated with rely-guarantee formulas, type: *Make> annos "prob" -If successful, the annotated shapes are in the file prob_annotations.xml.+If successful, the annotated shapes are in the file prob_annotations.xhtml. To remove the files generated from source files, type: @@ -70,6 +70,11 @@ initialCpsaFlags :: String initialCpsaFlags = "+RTS -M512m -RTS" +graphFlags :: String+graphFlags = ""+-- To enable zooming, use:+-- graphFlags = " -z"+ -- A mutable location for CPSA flags cpsaFlags :: IORef String cpsaFlags = unsafePerformIO $ newIORef initialCpsaFlags@@ -99,7 +104,7 @@ graphRule :: Rule graphRule =- Rule { prog = "cpsagraph -x",+ Rule { prog = "cpsagraph" ++ graphFlags, inputExt = cpsaExt, outputExt = graphExt } @@ -186,10 +191,10 @@ make cpsaparametersRule root cpsaparametersRule :: Rule-cpsaparametersRule = +cpsaparametersRule = Rule { prog = "cpsaparameters", inputExt = sourceBasicExt,- outputExt = paramsExt }+ outputExt = paramsRoot ++ cpsaExt } -- Clean generated files @@ -202,6 +207,7 @@ rm $ root ++ shapesRoot ++ graphExt rm $ root ++ annosRoot ++ cpsaExt rm $ root ++ annosRoot ++ graphExt+ rm $ root ++ paramsRoot ++ cpsaExt -- File Extensions @@ -221,11 +227,11 @@ annosRoot :: String annosRoot = "_annotations" -graphExt :: String-graphExt = ".xml"+paramsRoot :: String+paramsRoot = "_parameters" -paramsExt :: String-paramsExt = ".params"+graphExt :: String+graphExt = ".xhtml" -- Rule Interpreters
doc/cpsa.mk view
@@ -23,8 +23,12 @@ %_annotations.txt: %_shapes.txt cpsaannotations $(ANNOTATIONSFLAGS) -o $@ $< +# Compute protocol parameters+%_parameters.txt: %_shapes.txt+ cpsaparameters $(PARAMETERSFLAGS) -o $@ $<+ # Visualize output using the expanded format (default)-%.xml: %.txt+%.xhtml: %.txt cpsagraph $(GRAPHFLAGS) -o $@ $< # Visualize output using the compact format
doc/cpsadesign.pdf view
binary file changed (205755 → 205754 bytes)
doc/cpsaoverview.pdf view
binary file changed (77952 → 77952 bytes)
doc/cpsaprimer.pdf view
binary file changed (192265 → 192274 bytes)
doc/cpsaprimer.tex view
@@ -108,7 +108,7 @@ problem statement. The \texttt{cpsagraph} program is applied to the output to produce a-more readable, hyperlinked \textsc{xml} document that can be displayed+more readable, hyperlinked \textsc{xhtml} document that can be displayed in a standards-compliant web browser. The {\cpsa} User Guide contains the up-to-date description of \texttt{cpsagraph} generated documents. The guide is also the place to find command-line usage information for
doc/cpsaspec.pdf view
binary file changed (348307 → 348310 bytes)
doc/cpsatheory.pdf view
binary file changed (291421 → 291419 bytes)
doc/cpsatheory.tex view
@@ -865,9 +865,9 @@ \item $\anc(t,p) \cap E(S,t \termat p) = \emptyset$. \end{enumerate} \end{defn} -\begin{conj}+\begin{thm} $S\vdash t$ iff $\critpos(S,t)=\emptyset$.-\end{conj}+\end{thm} A critical message is $t \termat p$ where $p$ is a critical position. A critical message that is an atom is called a \emph{nonce test}, and@@ -1347,8 +1347,8 @@ \end{defn} \begin{defn}-Let $k$ be an unrealized skeleton with unrealized node $n$ and critical position $p$. Let $k'$ be a realized,-pruned skeleton, and let $k \homomorphism{\phi,\sigma} k'$. Then $(r,i,pp,tt)$ is a {\em solving augmentation+Let $k$ be an unrealized skeleton with unrealized node $n$ and critical position $p$. Let $k'$ be a realized +skeleton, and let $k \homomorphism{\phi,\sigma} k'$. Then $(r,i,pp,tt)$ is a {\em solving augmentation candidate} for $(k,k',n,p,\phi,\sigma)$ if $(r,i,pp,tt)$ is an augmentation candidate for $(k,n,p)$, and \begin{enumerate} \item There is a send of a message $t'$ at a node $n' = (s, i)$ in $k'$ such
doc/cpsauser.html view
@@ -42,7 +42,7 @@ provides a visualization of answers using Scalable Vector Graphics (<a href="http://www.w3.org/Graphics/SVG/">SVG</a>). The <a href="#cpsashapes"><tt>cpsashapes</tt></a> program removes intermediate results-from analyzer runs making the shapes easy to identify. +from analyzer runs making the shapes easy to identify. The <a href="#cpsafiff"><tt>cpsadiff</tt></a> program compares CPSA output files S-expression by S-expression, and prints the first skeleton@@ -67,16 +67,16 @@ <blockquote> <pre>$ cpsa +RTS -M512m -RTS -o prob.txt prob.scm-$ cpsagraph -o prob.xml prob.txt-$ firefox -remote "openFile(`pwd`/prob.xml)"</pre>+$ cpsagraph -o prob.xhtml prob.txt+$ firefox -remote "openFile(`pwd`/prob.xhtml)"</pre> </blockquote> <p>Often a summary of the analysis is more enlightening.</p> <blockquote> <pre>$ cpsashapes -o prob_shapes.txt prob.txt-$ cpsagraph -o prob_shapes.xml prob_shapes.txt-$ firefox -remote "openFile(`pwd`/prob_shapes.xml)"</pre>+$ cpsagraph -o prob_shapes.xhtml prob_shapes.txt+$ firefox -remote "openFile(`pwd`/prob_shapes.xhtml)"</pre> </blockquote> <p>The distribution comes with the file <a href="cpsa.mk"><tt>cpsa.mk</tt></a>@@ -87,18 +87,14 @@ <blockquote> <pre>CPSAFLAGS = +RTS -M512m -RTS -BASIC_SRC := $(wildcard *.scm)-DH_SRC := $(wildcard *.sch)--BASIC = $(BASIC_SRC:%.scm=%_shapes.xml) $(BASIC_SRC:%.scm=%.xml)-DH = $(DH_SRC:%.sch=%_shapes.xml) $(DH_SRC:%.sch=%.xml)+SRCS := $(wildcard *.scm) include cpsa.mk -all: $(BASIC) $(DH)+all: $(SRCS:%.scm=%_shapes.xhtml) $(SRCS:%.scm=%.xhtml) clean:- -rm *.txt *.xml</pre>+ -rm *.txt *.xhtml</pre> </blockquote> <p>For platforms without GNU <tt>make</tt>, the Haskell program <a@@ -396,6 +392,7 @@ -o FILE --output=FILE output FILE -x --expanded use expanded format (default) -z --zoom enable diagram scaling+ -t --treeless use treeless expanded format -c --compact use compact format -l --latex use LaTeX format -m INT --margin=INT set output margin (default 72)
doc/index.html view
@@ -36,14 +36,14 @@ protocols when GNU Make is available.</p> <p>After running the analysis, you will note files with the extension-<tt>.xml</tt>. These are XHTML/SVG compound documents that can be viewed by+<tt>.xhtml</tt>. These are XHTML/SVG compound documents that can be viewed by standards compliant browsers such as Firefox or Safari.</p> <p>New users should study CPSA's analysis of the following protocols in order,-Needham-Schroeder (<tt>ns.xml</tt>), Woo-Lam (<tt>woolam.xml</tt>), Yahalom-(<tt>yahalom.xml</tt>), ffgg (<tt>ffgg.xml</tt>), and finally Otway-Rees-(<tt>or.xml</tt>). When studying the full output, simultaneously display the-extracted shapes. The shapes file has an extension of <tt>_shapes.xml</tt>.</p>+Needham-Schroeder (<tt>ns.xhtml</tt>), Woo-Lam (<tt>woolam.xhtml</tt>), Yahalom+(<tt>yahalom.xhtml</tt>), ffgg (<tt>ffgg.xhtml</tt>), and finally Otway-Rees+(<tt>or.xhtml</tt>). When studying the full output, simultaneously display the+extracted shapes. The shapes file has an extension of <tt>_shapes.xhtml</tt>.</p> <p>Choose a small, simple protocol for your first analysis task. When analyzing complex protocols, analyze small parts of the protocol first, and then enrich
doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.2.0}+\newcommand{\version}{2.2.1} \newcommand{\cpsacopying}{\begingroup \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The MITRE Corporation. Permission to copy without fee all or part of
src/CPSA/Annotations/Main.hs view
@@ -40,7 +40,7 @@ | alg == CPSA.DiffieHellman.Algebra.name -> go (step h alg CPSA.DiffieHellman.Algebra.origin margin) p [] | alg == CPSA.SimpleDiffieHellman.Algebra.name ->- go (step h alg CPSA.SimpleDiffieHellman.Algebra.origin margin) + go (step h alg CPSA.SimpleDiffieHellman.Algebra.origin margin) p [] | otherwise -> abort ("Bad algebra: " ++ alg)
src/CPSA/Diff/Main.hs view
@@ -28,11 +28,11 @@ [oldName, newName] -> do oldFile <- openFile oldName ReadMode- old <- posHandle oldName oldFile + old <- posHandle oldName oldFile newFile <- openFile newName ReadMode- new <- posHandle newName newFile + new <- posHandle newName newFile go params old new- _ -> + _ -> do msg <- use options [] abort msg@@ -67,6 +67,7 @@ hPutStrLn out ">>>" _ -> return ()+ hClose out exitFailure writeSkel :: Params -> Handle -> SExpr a -> IO ()@@ -83,7 +84,7 @@ Nothing -> return input Just x -> case x of- L _ (S _ "defskeleton" : _) -> + L _ (S _ "defskeleton" : _) -> return input _ -> readSkel p
src/CPSA/DiffieHellman/Algebra.hs view
@@ -674,7 +674,7 @@ -- application on the path to the named subterm. The integer is the -- index of the subterm in the application's list of terms. --- The places and replace code fail to find the variable +-- The places and replace code fail to find the variable -- (F Akey [I x]) in (F Akey [Invk [I x]]). newtype Place = Place [Int] deriving Show
src/CPSA/Graph/CompactView.hs view
@@ -82,7 +82,7 @@ tdraw conf x y t = (w, h, ec "svg" attrs (rect conf 0 0 tw th : contents)) where- attrs = [("id", "t" ++ show (label (vertex t))),+ attrs = [("id", tid (show (label (vertex t)))), ("x", showL x), ("y", showL y), ("width", showL w), ("height", showL h), ("visibility", "hidden")]@@ -98,3 +98,13 @@ foldl (body conf x y) (max w w', max h h', e:es) (children t) where (w', h', e) = kdraw conf x y (vertex t)++-- Draw a preskeleton+kdraw :: Config -> Float -> Float -> Preskel -> (Float, Float, Element)+kdraw conf x y k =+ (w, h, ec "svg" attrs (rect conf 0 0 w h : lines))+ where+ attrs = [("id", kid (show (label k))), ("x", showL x),+ ("y", showL y), ("width", showL w), ("height", showL h)] +++ if compact conf then [("visibility", "hidden")] else []+ (w, h, lines) = skel conf k
src/CPSA/Graph/ExpandedView.hs view
@@ -7,9 +7,8 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -module CPSA.Graph.ExpandedView (expandedView) where+module CPSA.Graph.ExpandedView (expandedView, treelessView) where -import qualified Data.Set as S import Data.List (intersperse) import System.IO import CPSA.Lib.CPSA@@ -23,16 +22,15 @@ type Printer a = Int -> Int -> SExpr a -> String expandedView :: Handle -> Config -> Int -> [SExpr Pos] -> [Preskel] -> IO ()-expandedView h conf margin cmts ps =+expandedView h conf margin cmts ks = do- hPutList h (header (scripts conf) cmts ps)+ hPutList h (header (scripts conf) cmts ks) let pp = printer conf comments h margin pp cmts- let f = forest ps- case f of+ case forest ks of [t] -> tdrawer h conf margin pp False t- _ ->+ f -> do toc h f mapM_ (tdrawer h conf margin pp True) f@@ -40,32 +38,32 @@ hClose h header :: Bool -> [SExpr Pos] -> [Preskel] -> [String]-header False cmts ps =+header addScript cmts ks = ["<html xmlns=\"http://www.w3.org/1999/xhtml\">", "<head>",+ " <title>" ++ title cmts ks ++ "</title>", " <meta http-equiv=\"content-type\"" ++ " content=\"application/xhtml+xml; charset=UTF-8\" />",- " <title>" ++ title cmts ps ++ "</title>",- "</head>",+ " <style>",+ " svg.diagram { border-width: 1px; border-style: solid }",+ " </style>"]+ ++ maybeScript addScript +++ ["</head>", "<body>"]-header True cmts ps =- ["<html xmlns=\"http://www.w3.org/1999/xhtml\">",- "<head>",- " <meta http-equiv=\"content-type\"" ++- " content=\"application/xhtml+xml; charset=UTF-8\" />",- " <title>" ++ title cmts ps ++ "</title>",- " <script>"]- ++ sliders ++- [" </script>",- "</head>",- "<body onload=\"init()\">"] +maybeScript :: Bool -> [String]+maybeScript False = []+maybeScript True =+ [ " <script>"]+ ++ javascript +++ [" </script>"]+ -- Find title in a herald form, but if absent use a protocol name. title :: [SExpr Pos] -> [Preskel] -> String-title [] ps = protocolTitle ps+title [] ks = protocolTitle ks title ((L _ (S _ "herald" : S _ title : _)) : _) _ = title title ((L _ (S _ "herald" : Q _ title : _)) : _) _ = title-title (_ : cmts) ps = title cmts ps+title (_ : cmts) ks = title cmts ks protocolTitle :: [Preskel] -> String protocolTitle [] = "CPSA"@@ -102,14 +100,15 @@ anchor h id n = hPutStr h $ " <a href=\"#" ++ id n ++ "\">" ++ show n ++ "</a>" --- Generates an SVG document root and puts in into a div element.+-- Generates an SVG document root and puts it into a div element. -- When scripting is enabled, it places all elements into a g element -- that is used as the target of scaling actions. docRoot :: Config -> Float -> Float -> [Element] -> Element docRoot conf w h es =- ec "div" dattrs [ec "svg" attrs elems]+ ec "div" [] div where- attrs = [("width", showL w ++ units conf),+ attrs = [("class", "diagram"),+ ("width", showL w ++ units conf), ("height", showL h ++ units conf), ("xmlns", "http://www.w3.org/2000/svg"), ("xmlns:xlink", "http://www.w3.org/1999/xlink"),@@ -117,9 +116,19 @@ ("viewBox", viewbox), ("font-size", showL (font conf))] viewbox = "0 0 " ++ showL w ++ " " ++ showL h- dattrs = if scripts conf then [("class", "scalable")] else []- elems = if scripts conf then [ec "g" [] es] else es+ svg = ec "svg" attrs (if scripts conf then [ec "g" [] es] else es)+ div = if scripts conf then [zoomControl, br, svg] else [svg]+ br = ec "br" [] [] +zoomControl :: Element+zoomControl =+ ec "select" [("onchange", "zoom(event)")]+ [mc "option" [("value", "1.0")] "1.0",+ mc "option" [("value", "0.8")] "0.8",+ mc "option" [("value", "0.6")] "0.6",+ mc "option" [("value", "0.4")] "0.4",+ mc "option" [("value", "0.2")] "0.2"]+ -- Draws one tree tdrawer :: Handle -> Config -> Int -> Printer Pos -> Bool -> Tree -> IO () tdrawer h conf margin pp toc t =@@ -133,24 +142,17 @@ hPutStrLn h ".</p>" hPutStrLn h "" let (width, height, es) = tree conf t- hPutStrLn h $ show $ docRoot conf width height $- rect conf 0 0 width height : es+ hPutStrLn h $ show $ docRoot conf width height es hPutSExpr h margin pp (protSrc (vertex t))- mapM_ (kdrawer h conf margin pp id) (collectPreskels t)+ kdrawer h conf margin pp id [t] treeid :: Int -> String-treeid label = "t" ++ show label---- Collects the preskeletons within a tree and sorts them by label.-collectPreskels :: Tree -> [Tree]-collectPreskels t =- S.toAscList $ f S.empty t- where- f s t = foldl f (S.insert t s) (children t)+treeid label = tid (show label) --- Draws one item in the tree--a preskeleton.-kdrawer :: Handle -> Config -> Int -> Printer Pos -> Int -> Tree -> IO ()-kdrawer h conf margin pp tid t =+-- Draws the first item in the queue+kdrawer :: Handle -> Config -> Int -> Printer Pos -> Int -> [Tree] -> IO ()+kdrawer _ _ _ _ _ [] = return ()+kdrawer h conf margin pp tid (t:ts) = do hPutStrLn h "" let k = vertex t@@ -167,12 +169,14 @@ titledList h "Seen Child" "Seen Children" $ seen k hPutStrLn h ".</p>" hPutStrLn h ""- let (width, height, e) = kdraw conf 0 0 k- hPutStrLn h $ show $ docRoot conf width height [defs conf, e]+ let (width, height, es) = skel conf k+ hPutStrLn h $ show $ docRoot conf width height (defs conf : es) hPutSExpr h margin pp (preskelSrc k)+ -- Use a breadth first ordering by appending children to the queue+ kdrawer h conf margin pp tid (ts ++ children t) itemid :: Int -> String-itemid label = "i" ++ show label+itemid label = kid (show label) -- Handle singular vs. plural. titledList :: Handle -> String -> String -> [Int] -> IO ()@@ -197,74 +201,11 @@ indent :: Int indent = 2 --- Encoded from src/sliders.js using src/js2hs-sliders :: [String]-sliders =+-- Encoded from src/zoom.js using src/js2hs+javascript :: [String]+javascript = ["<![CDATA[",- "// Slider support for use with cpsagraph and option --scalers",- "",- "// Check to see if HTML5 sliders are available.",- "function have_input_type(t) {",- " var ns = document.documentElement.namespaceURI;",- " var i = document.createElementNS(ns, \"input\");",- " i.setAttribute(\"type\", t);",- " return i.type !== \"text\";",- "}",- "",- "var have_sliders = have_input_type(\"range\");",- "",- "// Create an element that controls scaling",- "function scaler(ns) {",- " if (have_sliders) ",- " return slider(ns);",- " else",- " return selector(ns);",- "}",- "",- "// Create an HTML5 slider for scaling",- "function slider(ns) {",- " var i = document.createElementNS(ns, \"input\");",- " i.setAttribute(\"type\", \"range\");",- " i.setAttribute(\"min\", 0.2);",- " i.setAttribute(\"max\", 1.0);",- " i.setAttribute(\"step\", 0.2);",- " i.setAttribute(\"value\", 1.0);",- " i.addEventListener(\"change\", zoom, false);",- " return i;",- "}",- "",- "// Create an old style select element for scaling",- "function selector(ns) {",- " var s = document.createElementNS(ns, \"select\");",- " s.appendChild(option(ns, \"1.0\"));",- " s.appendChild(option(ns, \"0.8\"));",- " s.appendChild(option(ns, \"0.6\"));",- " s.appendChild(option(ns, \"0.4\"));",- " s.appendChild(option(ns, \"0.2\"));",- " s.addEventListener(\"change\", zoom, false);",- " return s;",- "}",- "",- "// Create one option for use within a select element",- "function option(ns, val) {",- " var o = document.createElementNS(ns, \"option\");",- " o.setAttribute(\"value\", val);",- " o.appendChild(document.createTextNode(val));",- " return o;",- "}",- "",- "// At load time, insert browser appropriate scaler",- "function init() {",- " var ns = document.documentElement.namespaceURI;",- " var nodes = document.getElementsByClassName(\"scalable\");",- " var i;",- " for (i = 0; i < nodes.length; i++) {",- " var n = nodes.item(i);",- " var b = document.createElementNS(ns, \"br\");",- " n.insertBefore(b, n.firstChild);",- " n.insertBefore(scaler(ns), n.firstChild);",- " }",- "}",+ "// Zoom support for use with cpsagraph and option --zoom", "", "// Find the g element within a near by svg element and apply a transform", "function zoom(evt) {",@@ -272,3 +213,39 @@ " g.setAttribute(\"transform\", \"scale(\"+evt.target.value+\")\");", "}", "]]>"]++-- Treeless View -- fast because we don't generated derivation trees.++treelessView :: Handle -> Config -> Int -> [SExpr Pos] ->+ Preskel -> State -> IO ()+treelessView h conf margin cmts k s =+ do+ hPutList h (header (scripts conf) cmts [k])+ let pp = printer conf+ comments h margin pp cmts+ body h conf margin pp k s++body :: Handle -> Config -> Int -> Printer Pos -> Preskel -> State -> IO ()+body h conf margin pp k s =+ do+ case parent k of+ Nothing ->+ do+ hPutStrLn h ""+ hPutStrLn h $ show $ mc "p" [] ("Tree " ++ show (label k))+ hPutSExpr h margin pp (protSrc k)+ Just _ -> return ()+ hPutStrLn h ""+ hPutStrLn h $ show $ mc "p" [] ("Item " ++ show (label k))+ hPutStrLn h ""+ let (width, height, es) = skel conf k+ hPutStrLn h $ show $ docRoot conf width height (defs conf : es)+ hPutSExpr h margin pp (preskelSrc k)+ n <- loadNext s+ case n of+ Nothing -> -- EOF+ do+ hPutList h closer+ hClose h+ Just (k, s) ->+ body h conf margin pp k s
src/CPSA/Graph/LaTeXView.hs view
@@ -16,22 +16,20 @@ type Printer a = Int -> Int -> SExpr a -> String -- Main entry point-latexView :: Handle -> Int -> Printer Pos ->- [SExpr Pos] -> [Preskel] -> IO ()-latexView h margin pp cmts ps =+latexView :: Handle -> Int -> Printer Pos -> [SExpr Pos] ->+ Preskel -> State -> IO ()+latexView h margin pp cmts k s = do hPutStrLn h "\\usepackage[matrix,arrow,curve]{xy}" hPutStrLn h "\\begin{document}" hPutStrLn h "\\begin{verbatim}" mapM_ (writeItem h margin pp) cmts hPutStrLn h "\\end{verbatim}"- mapM_ (writeLnPreskel h margin pp) ps- hPutStrLn h "\n\\end{document}"- hClose h- return ()+ writeLnPreskel h margin pp k s -writeLnPreskel :: Handle -> Int -> Printer Pos -> Preskel -> IO ()-writeLnPreskel h m pp k =+-- Write each preskeleton+writeLnPreskel :: Handle -> Int -> Printer Pos -> Preskel -> State -> IO ()+writeLnPreskel h m pp k s = do case parent k of -- Write protocol with first preskeleton Nothing ->@@ -47,6 +45,14 @@ hPutStrLn h "\n\\begin{verbatim}" writeItem h m pp (preskelSrc k) hPutStrLn h "\\end{verbatim}"+ n <- loadNext s+ case n of+ Nothing -> -- EOF+ do+ hPutStrLn h "\n\\end{document}"+ hClose h+ Just (k, s) ->+ writeLnPreskel h m pp k s -- XY-pic output
src/CPSA/Graph/Loader.hs view
@@ -15,12 +15,14 @@ part, lastVertex, vertices, Node, vnode, strands, label, parent, seen, unrealized, protSrc, preskelSrc, initial, strand, pos,- prev, next, msg, out, succs, preds, loadDefs)+ prev, next, msg, out, succs, preds,+ State, loadFirst, loadNext) where import qualified Data.List as L import Control.Monad import CPSA.Lib.CPSA+import CPSA.Lib.Entry (gentlyReadSExpr) -- A view of protocols and preskeletons designed for display. @@ -116,39 +118,60 @@ type Pair = (Node, Node) -- An ordering of nodes --- Load the initial comments and top-level defs or return an error--- message+-- Loader -loadDefs :: Monad m => [SExpr Pos] -> m ([SExpr Pos], [Preskel])-loadDefs xs =- do- let (cmts, xs') = loadComments [] xs- (_, ks, _) <- foldM loadSExpr ([], [], 0) xs'- return (reverse cmts, reverse ks)+-- Load one preskeleton at a time from the input. The state of+-- loading follows. -loadComments :: [SExpr Pos] -> [SExpr Pos] -> ([SExpr Pos], [SExpr Pos])-loadComments cmts (cmt@(L _ (S _ "comment" : _)): xs) =- loadComments (cmt:cmts) xs-loadComments cmts (cmt@(L _ (S _ "herald" : _)): xs) =- loadComments (cmt:cmts) xs-loadComments cmts xs = (cmts, xs)+newtype State = State (PosHandle, Int, [(String, Protocol)]) --- The integer is used to add a label to preskeleton without one.-type LoadSExpr = ([(String, Protocol)], [Preskel], Int)+-- Load the initial comments and the first preskeleton. It's an error+-- if there is no preskeleton in the input. -loadSExpr :: Monad m => LoadSExpr -> SExpr Pos -> m LoadSExpr-loadSExpr (ps, ks, tag) x@(L pos (S _ "defprotocol" : xs)) =+loadFirst :: PosHandle -> IO ([SExpr Pos], Preskel, State)+loadFirst h =+ loadComments h []++loadComments :: PosHandle -> [SExpr Pos] -> IO ([SExpr Pos], Preskel, State)+loadComments h cmts = do+ x <- gentlyReadSExpr h+ case x of+ Nothing -> fail "Empty input"+ Just x ->+ case x of+ cmt@(L _ (S _ "comment" : _)) ->+ loadComments h (cmt:cmts)+ cmt@(L _ (S _ "herald" : _)) ->+ loadComments h (cmt:cmts)+ _ ->+ do+ n <- loadSExpr (State (h, 0, [])) x+ case n of+ Nothing -> fail "Empty input"+ Just (p, s) -> return (reverse cmts, p, s)++-- Load the next preskeleton or return Nothing on EOF+loadNext :: State -> IO (Maybe (Preskel, State))+loadNext s@(State (h, _, _)) =+ do+ x <- gentlyReadSExpr h+ case x of+ Nothing -> return Nothing+ Just x -> loadSExpr s x++-- Load from one S-expression+loadSExpr :: State -> SExpr Pos -> IO (Maybe (Preskel, State))+loadSExpr (State (h, tag, ps)) x@(L pos (S _ "defprotocol" : xs)) =+ do p <- loadProt x pos xs- return (p : ps, ks, tag)-loadSExpr (ps, ks, tag) x@(L pos (S _ "defskeleton" : xs)) =+ loadNext (State (h, tag, p:ps)) -- Add protocol to state+loadSExpr (State (h, tag, ps)) x@(L pos (S _ "defskeleton" : xs)) = do k <- loadPreskel x pos ps tag xs- -- Ensure labels are unique- case any ((== (label k)) . label) ks of- True -> fail (shows pos ("Duplicate label " ++ show (label k)))- False -> return (ps, k : ks, tag + 1)-loadSExpr le (L _ (S _ "comment" : _)) = return le+ return (Just (k, State (h, 1 + max tag (label k), ps)))+loadSExpr s (L _ (S _ "comment" : _)) =+ loadNext s loadSExpr _ x = fail (shows (annotation x) "Malformed input") -- Protocols
src/CPSA/Graph/Main.hs view
@@ -30,57 +30,101 @@ margin :: Int } -- Output line length deriving Show -data Format = XML | SVG | LaTeX deriving Show+data Format = XHTML | TreelessXHTML | SVG | LaTeX deriving Show main :: IO () main = do (p, params) <- start options interp- sexprs <- readSExprs p- preskels <- try (loadDefs sexprs)+ case format params of+ TreelessXHTML -> treeless p params+ LaTeX -> latex p params+ _ -> loadAll p params++-- Load all preskeletons before generating any output.+-- Don't use these graphing methods if your input is large.+loadAll :: PosHandle -> Params -> IO ()+loadAll p params =+ do+ preskels <- try (loadDefs p) case preskels of Left err -> abort (ioeGetErrorString err)- Right (_, []) ->- abort "Empty input" Right (cmts, preskels) -> do h <- outputHandle (file params)+ hPutStrLn h "<?xml version=\"1.0\"?>"+ hPutStrLn h ("<!-- " ++ cpsaVersion ++ " -->") let conf = config (prefix params) (scripted params) case format params of- LaTeX ->- do- hPutStrLn h "\\documentclass[12pt]{article}"- hPutStrLn h ("% " ++ cpsaVersion)- let pp = printer $ conf False- latexView h (margin params) pp cmts preskels- _ ->- do- hPutStrLn h "<?xml version=\"1.0\"?>"- hPutStrLn h ("<!-- " ++ cpsaVersion ++ " -->")- case format params of- XML -> expandedView h (conf False)- (margin params) cmts preskels- SVG -> compactView h (conf True) preskels- LaTeX -> error "Bad case in main"+ XHTML -> expandedView h (conf False)+ (margin params) cmts preskels+ SVG -> compactView h (conf True) preskels+ _ -> error "Bad case in main" -readSExprs :: PosHandle -> IO [SExpr Pos]-readSExprs p =- loop []+-- Load comments and preskeletons+loadDefs :: PosHandle -> IO ([SExpr Pos], [Preskel])+loadDefs h =+ do+ (cmts, k, s) <- loadFirst h+ ks <- loop [k] s+ return (cmts, ks) where- loop xs =+ loop ks s = do- x <- gentlyReadSExpr p- case x of- Nothing ->- return $ reverse xs- Just x ->- loop (x:xs)+ n <- loadNext s+ case n of+ Nothing -> -- EOF+ return $ reverse ks+ Just (k, s) ->+ loop (k:ks) s +-- XHTML graphing for very large files.+-- Treeless loads one S-expression at a time, processes it, prints the+-- results, and makes the S-expression available for garbage+-- collection before reading the next S-expression.+treeless :: PosHandle -> Params -> IO ()+treeless p params =+ do+ preskel <- try (loadFirst p)+ case preskel of+ Left err -> abort (ioeGetErrorString err)+ Right (cmts, preskel, state) ->+ do+ h <- outputHandle (file params)+ hPutStrLn h "<?xml version=\"1.0\"?>"+ hPutStrLn h ("<!-- " ++ cpsaVersion ++ " -->")+ let conf = config (prefix params) (scripted params) False+ ans <- try (treelessView h conf (margin params)+ cmts preskel state)+ case ans of+ Left err -> abort (ioeGetErrorString err)+ Right () -> return ()++-- LaTeX graphing.+latex :: PosHandle -> Params -> IO ()+latex p params =+ do+ preskel <- try (loadFirst p)+ case preskel of+ Left err -> abort (ioeGetErrorString err)+ Right (cmts, preskel, state) ->+ do+ h <- outputHandle (file params)+ hPutStrLn h "\\documentclass[12pt]{article}"+ hPutStrLn h ("% " ++ cpsaVersion)+ let conf = config (prefix params) (scripted params) False+ let pp = printer conf+ ans <- try (latexView h (margin params) pp cmts preskel state)+ case ans of+ Left err -> abort (ioeGetErrorString err)+ Right () -> return ()+ -- Command line option flags data Flag = Help -- Help | Info -- Version information- | Expanded -- Select expanded format in XML+ | Expanded -- Select expanded format in XHTML+ | Treeless -- Select treeless expanded format in XHTML | Scripted -- Ensable scripting | Compact -- Select compact format in SVG | Text -- Select text format in LaTeX@@ -99,6 +143,8 @@ "use expanded format (default)", Option ['z'] ["zoom"] (NoArg Scripted) "enable diagram scaling",+ Option ['t'] ["treeless"] (NoArg Treeless)+ "use treeless expanded format", Option ['c'] ["compact"] (NoArg Compact) "use compact format", Option ['l'] ["latex"] (NoArg Text) "use LaTeX format", Option ['m'] ["margin"] (ReqArg Margin "INT")@@ -111,7 +157,7 @@ interp :: [Flag] -> IO Params interp flags = loop flags (Params { file = Nothing, -- By default, no output file- format = XML, -- and use expanded format+ format = XHTML, -- and use expanded format prefix = True, scripted = False, margin = defaultMargin })@@ -121,7 +167,9 @@ | file params == Nothing = loop flags $ params { file = Just name } loop (Expanded : flags) params =- loop flags $ params { format = XML }+ loop flags $ params { format = XHTML }+ loop (Treeless : flags) params =+ loop flags $ params { format = TreelessXHTML } loop (Scripted : flags) params = loop flags $ params { scripted = True } loop (Compact : flags) params =
src/CPSA/Graph/Preskeleton.hs view
@@ -6,7 +6,7 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -module CPSA.Graph.Preskeleton (kdraw) where+module CPSA.Graph.Preskeleton (skel) where import CPSA.Lib.CPSA (SExpr, printMsg, printEnv) import CPSA.Graph.XMLOutput@@ -115,13 +115,10 @@ _ -> "" -- Draw a preskeleton-kdraw :: Config -> Float -> Float -> Preskel -> (Float, Float, Element)-kdraw conf x y k =- (w, h, ec "svg" attrs (rect conf 0 0 w h : lines))+skel :: Config -> Preskel -> (Float, Float, [Element])+skel conf k =+ (w, h, lines) where- attrs = [("id", "k" ++ show (label k)), ("x", showL x),- ("y", showL y), ("width", showL w), ("height", showL h)] ++- if compact conf then [("visibility", "hidden")] else [] (w, h) = dim conf (strands k) (maxRank k rank) circs = foldl (addNode conf k rank) (title conf k) (initial k) lines = foldl (addStrand conf rank) circs (initial k)
src/CPSA/Graph/SVG.hs view
@@ -15,8 +15,8 @@ -- Show a coordinate as a length showsL :: Float -> ShowS-showsL len s =- N.showFFloat (Just 3) len s+showsL len =+ N.showFFloat (Just 3) len showL :: Float -> String showL len = showsL len []@@ -123,9 +123,9 @@ onclick :: Config -> Int -> String onclick conf label = if compact conf then- showString "showk(evt, \"k" $ shows label "\")"+ showString "showk(evt, \"" $ kid $ shows label "\")" else- showString "window.open(\"#i" $ shows label "\", \"_self\")"+ showString "window.open(\"#" $ kid $ shows label "\", \"_self\")" -- A button that displays a tree and its first preskeleton tbutton :: Config -> Float -> Float -> Int -> Element@@ -135,9 +135,17 @@ attrs = [("x", showL x), ("y", showL y), ("style", style), ("onclick", script)] style = props [("text-anchor", "middle")]- script = showString "showt(evt, \"t" $ content $- showString "\", \"k" $ content "\")"+ script = showString "showt(evt, \"" $ tid $ content $+ showString "\", \"" $ kid $ content "\")" content = shows label++-- Tree identifier+tid :: ShowS+tid = showChar 't'++-- Skeleton identifier+kid :: ShowS+kid = showChar 'k' -- The script for the buttons ecmascript :: String
src/CPSA/Graph/Tree.hs view
@@ -9,6 +9,11 @@ module CPSA.Graph.Tree (Tree (..), Forest, forest, tree) where import qualified Data.Map as M+import Data.Map (Map)+import Data.List (foldl')+import qualified Data.Set as S+import Data.Set (Set)+import CPSA.Lib.CPSA (seqList) import CPSA.Graph.XMLOutput import CPSA.Graph.Config import CPSA.Graph.SVG@@ -23,12 +28,12 @@ -- display. data Tree = Tree- { vertex :: Preskel,- duplicates :: Forest, -- Preskeletons already seen- children :: Forest, -- Freshly discovered preskeletons- alive :: Bool, -- Is preskeleton alive?- width :: Int, -- Number of leaf nodes- height :: Int } -- Longest distance to a leaf plus one+ { vertex :: !Preskel,+ children :: !Forest, -- Freshly discovered preskeletons+ duplicates :: !Forest, -- Preskeletons already seen+ alive :: !Bool, -- Is preskeleton alive?+ width :: !Int, -- Number of leaf nodes+ height :: !Int } -- Longest distance to a leaf plus one deriving Show instance Eq Tree where@@ -38,53 +43,67 @@ compare t0 t1 = compare (vertex t0) (vertex t1) makeTree :: Preskel -> [Tree] -> [Tree] -> Tree-makeTree k dups kids =- Tree { vertex = k, duplicates = dups, children = kids,- alive = True, -- The correct value is set later- width = x (dups ++ kids), height = y (dups ++ kids) }+makeTree k kids dups =+ Tree { vertex = k,+ children = seqList kids,+ duplicates = seqList dups,+ alive = live kids dups,+ width = x kids dups,+ height = y kids dups } where- x [] = 1 -- Compute the width and height- x kids = sum (map width kids)- y kids = 1 + foldl max 0 (map height kids)+ live kids dups =+ maybe True null (unrealized k) ||+ any alive kids || any alive dups+ x [] [] = 1+ -- The width of a duplicate is one+ x kids dups = sum (map width kids) + length dups+ -- The height of a duplicate is one+ y kids dups = 1 + foldl max (dupsHeight dups) (map height kids)+ dupsHeight [] = 0+ dupsHeight _ = 1 type Forest = [Tree] -- Assemble preskeletons into a forest and then set the alive flag forest :: [Preskel] -> Forest-forest ks = map setLiveness (assemble ks)+forest ks =+ map setLiveness (reverse (foldl' f [] ks))+ where+ f ts k+ | parent k == Nothing = -- Found tree root+ assemble (childMap ks) k : ts+ | otherwise = ts -- Otherwise skip k --- Assemble preskeletons into a forest-assemble :: [Preskel] -> Forest-assemble ks =- map loops (spanning ks)+-- A child map maps a label to a preskeleton and a list of its+-- childnen. The map is derived by looking at the parent field. The+-- code assumes a parent precedes its children in the input list.+childMap :: [Preskel] -> Map Int (Preskel, [Preskel])+childMap ks =+ foldl' child M.empty ks where- loops t = -- Add in the other edges- let k = vertex t in -- in the forest- makeTree k (duplicates k) (map loops (children t))- duplicates k =- [ makeTree k' [] []- | tag <- seen k,- k' <- maybe [] (:[]) (M.lookup tag table) ]- table = M.fromList $ map (\k -> (label k, k)) ks+ child cm k =+ case parent k of+ Nothing -> cm'+ Just p ->+ M.adjust addChild p cm'+ where+ cm' = M.insert (label k) (k, []) cm+ addChild (k', children) =+ (k', k : children) --- Compute the spanning forest of the preskeletons-spanning :: [Preskel] -> Forest-spanning [] = []-spanning (k:ks) =- makeTree k [] kids : rest+-- Assemble preskeletons into a tree+assemble :: Map Int (Preskel, [Preskel]) -> Preskel -> Tree+assemble table k =+ makeTree k (kids k) (dups k) where- (kids, rest) = partition (label k) (assemble ks)- partition _ [] = ([], [])- partition tag (t:ts) =- let (kids, rest) = partition tag ts in- case parent (vertex t) of- Just parent' ->- if parent' == tag then- (t:kids, rest)- else- (kids, t:rest)- Nothing ->- (kids, t:rest)+ kids k =+ case M.lookup (label k) table of+ Nothing -> [] -- This should never happen+ Just (_, ks) -> map (assemble table) (reverse ks)+ dups k =+ [ makeTree k' [] [] -- Make an empty tree for a duplicate+ | tag <- seen k,+ k' <- maybe [] (\(k, _) -> [k]) (M.lookup tag table) ] -- Set the alive flag in each preskeleton. setLiveness :: Tree -> Tree@@ -94,38 +113,37 @@ -- dead if it is known to be unrealized, and all of its children are -- unrealized. Because of duplicates, process of computing the list -- must be iterated.-live :: Tree -> [Preskel]+live :: Tree -> Set Preskel live t =- loop []+ loop (init S.empty t) where decend ks t =- let ks' = foldl decend ks (kids t) in- if contain ks' (vertex t) || dead ks' t then+ let ks' = foldl' decend ks (kids t) in+ if S.member (vertex t) ks' || dead ks' t then ks' else- vertex t : ks'+ S.insert (vertex t) ks' dead ks t =- maybe False (not . null) (unrealized (vertex t))- && all (not . contain ks . vertex) (kids t)+ all (not . (flip S.member ks) . vertex) (kids t)+ kids t = duplicates t ++ children t loop old = let new = decend old t in- if length new == length old then+ if S.size new == S.size old then old else loop new- kids t = duplicates t ++ children t+ init ks t =+ foldl' init (live ks t) (children t)+ where+ live ks t+ | alive t = S.insert (vertex t) ks+ | otherwise = ks -updateLiveness :: [Preskel] -> Tree -> Tree+updateLiveness :: Set Preskel -> Tree -> Tree updateLiveness live t =- t { duplicates = map (updateLiveness live) (duplicates t),- children = map (updateLiveness live) (children t),- alive = contain live (vertex t) }---- Does list contain a given preskeleton?-contain :: [Preskel] -> Preskel -> Bool-contain [] _ = False-contain (k:ks) k' =- label k == label k' || contain ks k'+ t { children = map (updateLiveness live) (children t),+ duplicates = map (updateLiveness live) (duplicates t),+ alive = S.member (vertex t) live } -- Draw tree view of preskeleton relations tree :: Config -> Tree -> (Float, Float, [Element])
src/CPSA/Lib/Reduction.hs view
@@ -18,6 +18,7 @@ import Control.Parallel #endif import qualified Data.List as L+import CPSA.Lib.Utilities import CPSA.Lib.SExpr import CPSA.Lib.Entry import CPSA.Lib.Algebra@@ -82,13 +83,6 @@ -- seen children data Algebra t p g s e c => Reduct t p g s e c = Reduct !(LPreskel t p g s e c) !Int !Bool ![Preskel t p g s e c] ![Int]--seqList :: [a] -> [a]-seqList xs =- loop xs- where- loop [] = xs- loop (y : ys) = seq y (loop ys) #if defined HAVE_PAR
src/CPSA/Lib/Strand.hs view
@@ -1180,7 +1180,7 @@ ((s0, i0), n1) <- pairs, s0 == s ] -unboundCheck :: Algebra t p g s e c => Preskel t p g s e c -> +unboundCheck :: Algebra t p g s e c => Preskel t p g s e c -> Sid -> Sid -> e -> Bool unboundCheck k s s' env = all (flip S.member unbound) (map (instantiate env) (S.elems unbound))@@ -1191,13 +1191,13 @@ others = kvarsBut k s s' unbound = S.difference this others -kvarsBut :: Algebra t p g s e c => Preskel t p g s e c -> +kvarsBut :: Algebra t p g s e c => Preskel t p g s e c -> Sid -> Sid -> Set t kvarsBut k s s' = loop S.empty (insts k) 0 where loop xs [] _ = xs- loop xs (i:is) s'' + loop xs (i:is) s'' | s'' == s || s'' == s' = loop xs is (s'' + 1) | otherwise =
src/CPSA/Lib/Utilities.hs view
@@ -46,6 +46,13 @@ | pred x = return x | otherwise = fail "assertion failed" +seqList :: [a] -> [a]+seqList xs =+ loop xs+ where+ loop [] = xs+ loop (y : ys) = seq y (loop ys)+ -- Is graph acyclic? isAcyclic :: Ord a => (a -> [a]) -> [a] -> Bool isAcyclic adj nodes =
+ src/ghcmemlimit view
@@ -0,0 +1,15 @@+#! /bin/sh+# Compute the free memory on a Linux system with /proc/meminfo.+# Set GHCRTS accordingly.+# Source this file or pass it a command to run in the extended environment.++GHCRTS=-M`awk '+/^MemFree:/ { free += $2 }+/^Buffers:/ { free += $2 }+/^Cached:/ { free += $2 }+END { print free "k" }' /proc/meminfo`+export GHCRTS+if [ -n "$1" ]+then+ "$@"+fi
− src/sliders.js
@@ -1,70 +0,0 @@-// Slider support for use with cpsagraph and option --scalers--// Check to see if HTML5 sliders are available.-function have_input_type(t) {- var ns = document.documentElement.namespaceURI;- var i = document.createElementNS(ns, "input");- i.setAttribute("type", t);- return i.type !== "text";-}--var have_sliders = have_input_type("range");--// Create an element that controls scaling-function scaler(ns) {- if (have_sliders) - return slider(ns);- else- return selector(ns);-}--// Create an HTML5 slider for scaling-function slider(ns) {- var i = document.createElementNS(ns, "input");- i.setAttribute("type", "range");- i.setAttribute("min", 0.2);- i.setAttribute("max", 1.0);- i.setAttribute("step", 0.2);- i.setAttribute("value", 1.0);- i.addEventListener("change", zoom, false);- return i;-}--// Create an old style select element for scaling-function selector(ns) {- var s = document.createElementNS(ns, "select");- s.appendChild(option(ns, "1.0"));- s.appendChild(option(ns, "0.8"));- s.appendChild(option(ns, "0.6"));- s.appendChild(option(ns, "0.4"));- s.appendChild(option(ns, "0.2"));- s.addEventListener("change", zoom, false);- return s;-}--// Create one option for use within a select element-function option(ns, val) {- var o = document.createElementNS(ns, "option");- o.setAttribute("value", val);- o.appendChild(document.createTextNode(val));- return o;-}--// At load time, insert browser appropriate scaler-function init() {- var ns = document.documentElement.namespaceURI;- var nodes = document.getElementsByClassName("scalable");- var i;- for (i = 0; i < nodes.length; i++) {- var n = nodes.item(i);- var b = document.createElementNS(ns, "br");- n.insertBefore(b, n.firstChild);- n.insertBefore(scaler(ns), n.firstChild);- }-}--// Find the g element within a near by svg element and apply a transform-function zoom(evt) {- var g = evt.target.parentNode.lastElementChild.firstElementChild;- g.setAttribute("transform", "scale("+evt.target.value+")");-}
+ src/zoom.js view
@@ -0,0 +1,7 @@+// Zoom support for use with cpsagraph and option --zoom++// Find the g element within a near by svg element and apply a transform+function zoom(evt) {+ var g = evt.target.parentNode.lastElementChild.firstElementChild;+ g.setAttribute("transform", "scale("+evt.target.value+")");+}
tst/Make.hs view
@@ -14,7 +14,7 @@ *Make> cpsa "prob" -If successful, the analysis is in the file prob.xml, which can be+If successful, the analysis is in the file prob.xhtml, which can be viewed with a standards-compliant browser. To analyze a problem in prob.sch using the Diffie-Hellman algebra, type:@@ -25,13 +25,13 @@ *Make> shapes "prob" -If successful, the shapes are in the file prob_shapes.xml.+If successful, the shapes are in the file prob_shapes.xhtml. When the protocol is annotated with rely-guarantee formulas, type: *Make> annos "prob" -If successful, the annotated shapes are in the file prob_annotations.xml.+If successful, the annotated shapes are in the file prob_annotations.xhtml. To remove the files generated from source files, type: @@ -70,6 +70,11 @@ initialCpsaFlags :: String initialCpsaFlags = "+RTS -M512m -RTS" +graphFlags :: String+graphFlags = ""+-- To enable zooming, use:+-- graphFlags = " -z"+ -- A mutable location for CPSA flags cpsaFlags :: IORef String cpsaFlags = unsafePerformIO $ newIORef initialCpsaFlags@@ -99,7 +104,7 @@ graphRule :: Rule graphRule =- Rule { prog = "cpsagraph -x",+ Rule { prog = "cpsagraph" ++ graphFlags, inputExt = cpsaExt, outputExt = graphExt } @@ -189,7 +194,7 @@ cpsaparametersRule = Rule { prog = "cpsaparameters", inputExt = sourceBasicExt,- outputExt = paramsExt }+ outputExt = paramsRoot ++ cpsaExt } -- Clean generated files @@ -202,6 +207,7 @@ rm $ root ++ shapesRoot ++ graphExt rm $ root ++ annosRoot ++ cpsaExt rm $ root ++ annosRoot ++ graphExt+ rm $ root ++ paramsRoot ++ cpsaExt -- File Extensions @@ -221,11 +227,11 @@ annosRoot :: String annosRoot = "_annotations" -graphExt :: String-graphExt = ".xml"+paramsRoot :: String+paramsRoot = "_parameters" -paramsExt :: String-paramsExt = ".params"+graphExt :: String+graphExt = ".xhtml" -- Rule Interpreters
tst/Makefile view
@@ -40,13 +40,13 @@ ../dist/build/cpsagraph/cpsagraph -c -o $@ $< # Visualize output using the expanded format-%.xml: %.txt+%.xhtml: %.txt ../dist/build/cpsagraph/cpsagraph $(GRAPHFLAGS) -o $@ $< .PRECIOUS: %.txt %_shapes.txt %_annotations.txt -all: $(TSTS) $(patsubst %.txt,%.xml,$(TSTS)) \- $(patsubst %.txt,%_shapes.xml,$(TSTS))+all: $(patsubst %.txt,%.xhtml,$(TSTS)) \+ $(patsubst %.txt,%_shapes.xhtml,$(TSTS)) clean:- -rm *.txt *.xml+ -rm *.txt *.xhtml
+ tst/tor.scm view
@@ -0,0 +1,41 @@+(herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman)+ (comment "Achieves unilateral authentication"))++;; Hashing--the key no one has is (invk kh)++(defmacro (hash x)+ (enc "hash" x kh))++(defprotocol tor diffie-hellman+ (defrole init+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace + (send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (hash (cat (exp (exp (gen) x) y)))))+ (send (enc n (exp (exp (gen) y) x))))+ (uniq-orig x n)+ (non-orig (invk kh)))+ (defrole resp+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace + (recv (enc (exp (gen) x) (pubk b)))+ (send (cat (exp (gen) y) (hash (cat (exp (exp (gen) x) y)))))+ (recv (enc n (exp (exp (gen) x) y))))+ (uniq-orig y)+ (non-orig (invk kh))))++(defskeleton tor+ (vars (b name) (n text))+ (defstrand init 2 (b b))+ (non-orig (privk b)))++(defskeleton tor+ (vars (b name) (n text))+ (defstrand resp 3 (b b))+ (non-orig (privk b)))++(defskeleton tor+ (vars (b name) (n text))+ (defstrand init 3 (b b) (n n))+ (deflistener n)+ (non-orig (privk b)))
+ tst/tor.tst view
@@ -0,0 +1,581 @@+(herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman)+ (comment "Achieves unilateral authentication"))++(comment "CPSA 2.2.0")+(comment "All input read")++(defprotocol tor diffie-hellman+ (defrole init+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace (send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y))))+ (non-orig (invk kh))+ (uniq-orig n x))+ (defrole resp+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace (recv (enc (exp (gen) x) (pubk b)))+ (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (recv (enc n (exp (exp (gen) x) y))))+ (non-orig (invk kh))+ (uniq-orig y)))++(defskeleton tor+ (vars (b name) (x y expn) (kh akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (non-orig (invk kh) (privk b))+ (uniq-orig x)+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))))+ (label 0)+ (unrealized (0 1))+ (comment "2 in cohort - 2 not yet seen"))++(defskeleton tor+ (vars (b b-0 name) (x y expn) (kh kh-0 akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))+ (precedes ((0 0) (1 0)) ((1 1) (0 1)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig x y)+ (operation encryption-test (added-strand resp 2) (exp (exp (gen) x) y)+ (0 1))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv (enc (exp (gen) x) (pubk b-0)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))+ (label 1)+ (parent 0)+ (unrealized (0 1) (1 0))+ (comment "2 in cohort - 2 not yet seen"))++(defskeleton tor+ (vars (b name) (x y expn) (kh akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (deflistener x)+ (precedes ((0 0) (1 0)) ((1 1) (0 1)))+ (non-orig (invk kh) (privk b))+ (uniq-orig x)+ (operation encryption-test (added-listener x) (exp (exp (gen) x) y)+ (0 1))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv x) (send x)))+ (label 2)+ (parent 0)+ (unrealized (1 0))+ (comment "1 in cohort - 1 not yet seen"))++(defskeleton tor+ (vars (b name) (x y expn) (kh kh-0 akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))+ (precedes ((0 0) (1 0)) ((1 1) (0 1)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig x y)+ (operation encryption-test (contracted (b-0 b)) (exp (gen) x) (1 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))+ (label 3)+ (parent 1)+ (unrealized (0 1))+ (comment "2 in cohort - 2 not yet seen"))++(defskeleton tor+ (vars (b b-0 name) (x y expn) (kh kh-0 akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))+ (deflistener x)+ (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig x y)+ (operation encryption-test (added-listener x) (exp (gen) x) (1 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv (enc (exp (gen) x) (pubk b-0)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv x) (send x)))+ (label 4)+ (parent 1)+ (unrealized (2 0))+ (comment "1 in cohort - 1 not yet seen"))++(defskeleton tor+ (vars (b name) (x y y-0 expn) (kh kh-0 akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (deflistener x)+ (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-0))+ (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig x y-0)+ (operation nonce-test (added-strand resp 2) x (1 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv x) (send x))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y-0)+ (enc "hash" (exp (exp (gen) x) y-0) kh-0)))))+ (label 5)+ (parent 2)+ (unrealized (1 0))+ (comment "empty cohort"))++(defskeleton tor+ (vars (b name) (x y expn) (kh akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh))+ (precedes ((0 0) (1 0)) ((1 1) (0 1)))+ (non-orig (invk kh) (privk b))+ (uniq-orig x y)+ (operation encryption-test (contracted (kh-0 kh))+ (exp (exp (gen) x) y) (0 1) (enc "hash" (exp (exp (gen) x) y) kh))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))))+ (label 6)+ (parent 3)+ (unrealized)+ (shape))++(defskeleton tor+ (vars (b name) (x y expn) (kh kh-0 akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))+ (deflistener y)+ (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig x y)+ (operation encryption-test (added-listener y) (exp (exp (gen) x) y)+ (0 1) (enc "hash" (exp (exp (gen) x) y) kh-0))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv y) (send y)))+ (label 7)+ (parent 3)+ (unrealized (0 1) (2 0))+ (comment "1 in cohort - 1 not yet seen"))++(defskeleton tor+ (vars (b b-0 name) (x y y-0 expn) (kh kh-0 kh-1 akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))+ (deflistener x)+ (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-1))+ (precedes ((0 0) (3 0)) ((1 1) (0 1)) ((2 1) (1 0)) ((3 1) (2 0)))+ (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))+ (uniq-orig x y y-0)+ (operation nonce-test (added-strand resp 2) x (2 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv (enc (exp (gen) x) (pubk b-0)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv x) (send x))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y-0)+ (enc "hash" (exp (exp (gen) x) y-0) kh-1)))))+ (label 8)+ (parent 4)+ (unrealized (2 0))+ (comment "empty cohort"))++(defskeleton tor+ (vars (b b-0 name) (x y y-0 expn) (kh kh-0 kh-1 akey))+ (defstrand init 2 (b b) (x x) (y y) (kh kh))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))+ (deflistener y)+ (defstrand resp 2 (b b-0) (x y) (y y-0) (kh kh-1))+ (precedes ((0 0) (1 0)) ((1 1) (3 0)) ((2 1) (0 1)) ((3 1) (2 0)))+ (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))+ (uniq-orig x y y-0)+ (operation nonce-test (added-strand resp 2) y (2 0) (exp (gen) y)+ (enc "hash" (exp (exp (gen) x) y) kh-0))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh))))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv y) (send y))+ ((recv (enc (exp (gen) y) (pubk b-0)))+ (send+ (cat (exp (gen) y-0)+ (enc "hash" (exp (exp (gen) y) y-0) kh-1)))))+ (label 9)+ (parent 7)+ (unrealized (0 1) (2 0))+ (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol tor diffie-hellman+ (defrole init+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace (send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y))))+ (non-orig (invk kh))+ (uniq-orig n x))+ (defrole resp+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace (recv (enc (exp (gen) x) (pubk b)))+ (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (recv (enc n (exp (exp (gen) x) y))))+ (non-orig (invk kh))+ (uniq-orig y)))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh akey))+ (defstrand resp 3 (n n) (b b) (x x) (y y) (kh kh))+ (non-orig (invk kh) (privk b))+ (uniq-orig y)+ (traces+ ((recv (enc (exp (gen) x) (pubk b)))+ (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (recv (enc n (exp (exp (gen) x) y)))))+ (label 10)+ (unrealized)+ (shape))++(comment "Nothing left to do")++(defprotocol tor diffie-hellman+ (defrole init+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace (send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y))))+ (non-orig (invk kh))+ (uniq-orig n x))+ (defrole resp+ (vars (x y expn) (b name) (n text) (kh akey))+ (trace (recv (enc (exp (gen) x) (pubk b)))+ (send (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (recv (enc n (exp (exp (gen) x) y))))+ (non-orig (invk kh))+ (uniq-orig y)))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (non-orig (invk kh) (privk b))+ (uniq-orig n x)+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))+ (label 11)+ (unrealized (0 1) (1 0)))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (precedes ((0 2) (1 0)))+ (non-orig (invk kh) (privk b))+ (uniq-orig n x)+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n)))+ (label 12)+ (parent 11)+ (unrealized (0 1) (1 0))+ (comment "1 in cohort - 1 not yet seen"))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (1 0)))+ (non-orig (invk kh) (privk b))+ (uniq-orig n x)+ (operation nonce-test (added-listener (exp (exp (gen) x) y)) n (1 0)+ (enc n (exp (exp (gen) x) y)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y))))+ (label 13)+ (parent 12)+ (seen 14)+ (unrealized (0 1) (2 0))+ (comment "3 in cohort - 2 not yet seen"))++(defskeleton tor+ (vars (n text) (b b-0 name) (x y expn) (kh kh-0 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))+ (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))+ ((3 1) (2 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig n x y)+ (operation encryption-test (added-strand resp 2) (exp (exp (gen) x) y)+ (2 0))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv (enc (exp (gen) x) (pubk b-0)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))+ (label 14)+ (parent 13)+ (seen 16)+ (unrealized (0 1) (2 0) (3 0))+ (comment "3 in cohort - 2 not yet seen"))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (deflistener x)+ (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0)))+ (non-orig (invk kh) (privk b))+ (uniq-orig n x)+ (operation encryption-test (added-listener x) (exp (exp (gen) x) y)+ (2 0))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv x) (send x)))+ (label 15)+ (parent 13)+ (seen 18)+ (unrealized (0 1) (3 0))+ (comment "2 in cohort - 1 not yet seen"))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh kh-0 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))+ (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))+ ((3 1) (2 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig n x y)+ (operation encryption-test (contracted (b-0 b)) (exp (gen) x) (3 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0)))))+ (label 16)+ (parent 14)+ (unrealized (0 1) (2 0))+ (comment "1 in cohort - 1 not yet seen"))++(defskeleton tor+ (vars (n text) (b b-0 name) (x y expn) (kh kh-0 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))+ (deflistener x)+ (precedes ((0 0) (4 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))+ ((3 1) (2 0)) ((4 1) (3 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig n x y)+ (operation encryption-test (added-listener x) (exp (gen) x) (3 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv (enc (exp (gen) x) (pubk b-0)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv x) (send x)))+ (label 17)+ (parent 14)+ (seen 20)+ (unrealized (4 0))+ (comment "2 in cohort - 1 not yet seen"))++(defskeleton tor+ (vars (n text) (b name) (x y y-0 expn) (kh kh-0 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (deflistener x)+ (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-0))+ (precedes ((0 0) (4 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0))+ ((4 1) (3 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig n x y-0)+ (operation nonce-test (added-strand resp 2) x (3 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv x) (send x))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y-0)+ (enc "hash" (exp (exp (gen) x) y-0) kh-0)))))+ (label 18)+ (parent 15)+ (unrealized (0 1) (3 0))+ (comment "empty cohort"))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh kh-0 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))+ (deflistener x)+ (precedes ((0 0) (3 0)) ((0 0) (4 0)) ((0 2) (1 0)) ((2 1) (1 0))+ ((3 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig n x y)+ (operation encryption-test (added-listener x) (exp (exp (gen) x) y)+ (2 0) (enc "hash" (exp (exp (gen) x) y) kh-0))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv x) (send x)))+ (label 19)+ (parent 16)+ (seen 21 22)+ (unrealized (0 1) (4 0))+ (comment "6 in cohort - 2 not yet seen"))++(defskeleton tor+ (vars (n text) (b b-0 name) (x y y-0 expn) (kh kh-0 kh-1 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (defstrand resp 2 (b b-0) (x x) (y y) (kh kh-0))+ (deflistener x)+ (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-1))+ (precedes ((0 0) (5 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))+ ((3 1) (2 0)) ((4 1) (3 0)) ((5 1) (4 0)))+ (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))+ (uniq-orig n x y y-0)+ (operation nonce-test (added-strand resp 2) x (4 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv (enc (exp (gen) x) (pubk b-0)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv x) (send x))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y-0)+ (enc "hash" (exp (exp (gen) x) y-0) kh-1)))))+ (label 20)+ (parent 17)+ (unrealized (4 0))+ (comment "empty cohort"))++(defskeleton tor+ (vars (n text) (b name) (x y y-0 expn) (kh kh-0 kh-1 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))+ (deflistener x)+ (defstrand resp 2 (b b) (x x) (y y-0) (kh kh-1))+ (precedes ((0 0) (3 0)) ((0 0) (5 0)) ((0 2) (1 0)) ((2 1) (1 0))+ ((3 1) (0 1)) ((3 1) (2 0)) ((4 1) (2 0)) ((5 1) (4 0)))+ (non-orig (invk kh) (invk kh-0) (invk kh-1) (privk b))+ (uniq-orig n x y y-0)+ (operation nonce-test (added-strand resp 2) x (4 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv x) (send x))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y-0)+ (enc "hash" (exp (exp (gen) x) y-0) kh-1)))))+ (label 21)+ (parent 19)+ (unrealized (0 1) (4 0))+ (comment "empty cohort"))++(defskeleton tor+ (vars (n text) (b name) (x y expn) (kh kh-0 akey))+ (defstrand init 3 (n n) (b b) (x x) (y y) (kh kh))+ (deflistener n)+ (deflistener (exp (exp (gen) x) y))+ (defstrand resp 2 (b b) (x x) (y y) (kh kh-0))+ (deflistener x)+ (precedes ((0 0) (3 0)) ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (0 1))+ ((3 1) (4 0)) ((4 1) (2 0)))+ (non-orig (invk kh) (invk kh-0) (privk b))+ (uniq-orig n x y)+ (operation nonce-test (displaced 5 3 resp 2) x (4 0)+ (enc (exp (gen) x) (pubk b)))+ (traces+ ((send (enc (exp (gen) x) (pubk b)))+ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh)))+ (send (enc n (exp (exp (gen) x) y)))) ((recv n) (send n))+ ((recv (exp (exp (gen) x) y)) (send (exp (exp (gen) x) y)))+ ((recv (enc (exp (gen) x) (pubk b)))+ (send+ (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y) kh-0))))+ ((recv x) (send x)))+ (label 22)+ (parent 19)+ (unrealized (0 1) (4 0))+ (comment "empty cohort"))++(comment "Nothing left to do")