diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,63 @@ +2010-12-20 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.2.1. + +2010-12-16 John D. Ramsdell + + * 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 + + * 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 + + * 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 + + * 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 + + * 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 + + * 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 + + * 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 * cpsa.cabal (Version): Tagged as version 2.2.0. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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. diff --git a/README b/README --- a/README +++ b/README @@ -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 diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -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. diff --git a/doc/Make.hs b/doc/Make.hs --- a/doc/Make.hs +++ b/doc/Make.hs @@ -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 diff --git a/doc/cpsa.mk b/doc/cpsa.mk --- a/doc/cpsa.mk +++ b/doc/cpsa.mk @@ -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 diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ 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/cpsaprimer.tex b/doc/cpsaprimer.tex --- a/doc/cpsaprimer.tex +++ b/doc/cpsaprimer.tex @@ -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 diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ diff --git a/doc/cpsatheory.pdf b/doc/cpsatheory.pdf Binary files a/doc/cpsatheory.pdf and b/doc/cpsatheory.pdf differ diff --git a/doc/cpsatheory.tex b/doc/cpsatheory.tex --- a/doc/cpsatheory.tex +++ b/doc/cpsatheory.tex @@ -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 diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -42,7 +42,7 @@ provides a visualization of answers using Scalable Vector Graphics (SVG). The cpsashapes program removes intermediate results -from analyzer runs making the shapes easy to identify. +from analyzer runs making the shapes easy to identify. The cpsadiff program compares CPSA output files S-expression by S-expression, and prints the first skeleton @@ -67,16 +67,16 @@ 
$ cpsa +RTS -M512m -RTS -o prob.txt prob.scm
-$ cpsagraph -o prob.xml prob.txt
-$ firefox -remote "openFile(`pwd`/prob.xml)"
+$ cpsagraph -o prob.xhtml prob.txt +$ firefox -remote "openFile(`pwd`/prob.xhtml)"

Often a summary of the analysis is more enlightening.

$ cpsashapes -o prob_shapes.txt prob.txt
-$ cpsagraph -o prob_shapes.xml prob_shapes.txt
-$ firefox -remote "openFile(`pwd`/prob_shapes.xml)"
+$ cpsagraph -o prob_shapes.xhtml prob_shapes.txt +$ firefox -remote "openFile(`pwd`/prob_shapes.xhtml)"

The distribution comes with the file cpsa.mk @@ -87,18 +87,14 @@ 

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
+ -rm *.txt *.xhtml

For platforms without GNU make, the Haskell program

After running the analysis, you will note files with the extension -.xml. These are XHTML/SVG compound documents that can be viewed by +.xhtml. These are XHTML/SVG compound documents that can be viewed by standards compliant browsers such as Firefox or Safari.

New users should study CPSA's analysis of the following protocols in order, -Needham-Schroeder (ns.xml), Woo-Lam (woolam.xml), Yahalom -(yahalom.xml), ffgg (ffgg.xml), and finally Otway-Rees -(or.xml). When studying the full output, simultaneously display the -extracted shapes. The shapes file has an extension of _shapes.xml.

+Needham-Schroeder (ns.xhtml), Woo-Lam (woolam.xhtml), Yahalom +(yahalom.xhtml), ffgg (ffgg.xhtml), and finally Otway-Rees +(or.xhtml). When studying the full output, simultaneously display the +extracted shapes. The shapes file has an extension of _shapes.xhtml.

Choose a small, simple protocol for your first analysis task. When analyzing complex protocols, analyze small parts of the protocol first, and then enrich 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.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 diff --git a/src/CPSA/Annotations/Main.hs b/src/CPSA/Annotations/Main.hs --- a/src/CPSA/Annotations/Main.hs +++ b/src/CPSA/Annotations/Main.hs @@ -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) diff --git a/src/CPSA/Diff/Main.hs b/src/CPSA/Diff/Main.hs --- a/src/CPSA/Diff/Main.hs +++ b/src/CPSA/Diff/Main.hs @@ -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 diff --git a/src/CPSA/DiffieHellman/Algebra.hs b/src/CPSA/DiffieHellman/Algebra.hs --- a/src/CPSA/DiffieHellman/Algebra.hs +++ b/src/CPSA/DiffieHellman/Algebra.hs @@ -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 diff --git a/src/CPSA/Graph/CompactView.hs b/src/CPSA/Graph/CompactView.hs --- a/src/CPSA/Graph/CompactView.hs +++ b/src/CPSA/Graph/CompactView.hs @@ -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 diff --git a/src/CPSA/Graph/ExpandedView.hs b/src/CPSA/Graph/ExpandedView.hs --- a/src/CPSA/Graph/ExpandedView.hs +++ b/src/CPSA/Graph/ExpandedView.hs @@ -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 = ["", "", + " " ++ title cmts ks ++ "", " ", - " " ++ title cmts ps ++ "", - "", + " "] + ++ maybeScript addScript ++ + ["", ""] -header True cmts ps = - ["", - "", - " ", - " " ++ title cmts ps ++ "", - " ", - "", - ""] +maybeScript :: Bool -> [String] +maybeScript False = [] +maybeScript True = + [ " "] + -- 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 $ " " ++ show n ++ "" --- 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 ".

" 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 ".

" 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 = [""] + +-- 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 diff --git a/src/CPSA/Graph/LaTeXView.hs b/src/CPSA/Graph/LaTeXView.hs --- a/src/CPSA/Graph/LaTeXView.hs +++ b/src/CPSA/Graph/LaTeXView.hs @@ -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 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 @@ -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 diff --git a/src/CPSA/Graph/Main.hs b/src/CPSA/Graph/Main.hs --- a/src/CPSA/Graph/Main.hs +++ b/src/CPSA/Graph/Main.hs @@ -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 "" + hPutStrLn h ("") 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 "" - hPutStrLn h ("") - 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 "" + hPutStrLn h ("") + 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 = diff --git a/src/CPSA/Graph/Preskeleton.hs b/src/CPSA/Graph/Preskeleton.hs --- a/src/CPSA/Graph/Preskeleton.hs +++ b/src/CPSA/Graph/Preskeleton.hs @@ -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) diff --git a/src/CPSA/Graph/SVG.hs b/src/CPSA/Graph/SVG.hs --- a/src/CPSA/Graph/SVG.hs +++ b/src/CPSA/Graph/SVG.hs @@ -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 diff --git a/src/CPSA/Graph/Tree.hs b/src/CPSA/Graph/Tree.hs --- a/src/CPSA/Graph/Tree.hs +++ b/src/CPSA/Graph/Tree.hs @@ -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]) diff --git a/src/CPSA/Lib/Reduction.hs b/src/CPSA/Lib/Reduction.hs --- a/src/CPSA/Lib/Reduction.hs +++ b/src/CPSA/Lib/Reduction.hs @@ -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 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 @@ -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 = 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 @@ -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 = diff --git a/src/ghcmemlimit b/src/ghcmemlimit new file mode 100644 --- /dev/null +++ b/src/ghcmemlimit @@ -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 diff --git a/src/sliders.js b/src/sliders.js deleted file mode 100644 --- a/src/sliders.js +++ /dev/null @@ -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+")"); -} diff --git a/src/zoom.js b/src/zoom.js new file mode 100644 --- /dev/null +++ b/src/zoom.js @@ -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+")"); +} diff --git a/tst/Make.hs b/tst/Make.hs --- a/tst/Make.hs +++ b/tst/Make.hs @@ -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 diff --git a/tst/Makefile b/tst/Makefile --- a/tst/Makefile +++ b/tst/Makefile @@ -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 diff --git a/tst/tor.scm b/tst/tor.scm new file mode 100644 --- /dev/null +++ b/tst/tor.scm @@ -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))) diff --git a/tst/tor.tst b/tst/tor.tst new file mode 100644 --- /dev/null +++ b/tst/tor.tst @@ -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")