packages feed

cpsa-3.5.0: doc/examples/ffgg.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.5.0 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>The ffgg Protocol</title>
 <meta http-equiv="content-type" content="application/xhtml+xml; charset=UTF-8" />
 <style>
  svg.diagram { border-width: 1px; border-style: solid }
 </style>
</head>
<body>

<pre>(herald &quot;The ffgg Protocol&quot;
  (comment &quot;From A Necessarily Parallel Attack by Jon K. Millen&quot;))
(comment &quot;CPSA 3.5.0&quot;)
(comment &quot;All input read from ffgg.scm&quot;)</pre>

<p id="t0">Tree 0.</p>

<div>
 <svg
  class='diagram' width='279.600pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.600 79.920' font-size='12.000'>
  <text
   x='239.640' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   onclick='window.open(&quot;#k4&quot;, &quot;_self&quot;)'>4</text>
  <line
   x1='189.720' y1='39.960' x2='239.640' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='189.720' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k3&quot;, &quot;_self&quot;)'>3</text>
  <line
   x1='139.800' y1='39.960' x2='189.720' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='139.800' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k2&quot;, &quot;_self&quot;)'>2</text>
  <line
   x1='89.880' y1='39.960' x2='139.800' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='89.880' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k1&quot;, &quot;_self&quot;)'>1</text>
  <line
   x1='39.960' y1='39.960' x2='89.880' y2='39.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <text
   x='39.960' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k0&quot;, &quot;_self&quot;)'>0</text>
  </svg></div>

<pre>(defprotocol ffgg basic
  (defrole init
    (vars (a b name) (n1 n2 m x y text))
    (trace (send a) (recv (cat b n1 n2))
      (send (cat a (enc n1 n2 m (pubk b))))
      (recv (cat n1 x (enc x y n1 (pubk b))))))
  (defrole resp
    (vars (b a name) (n1 n2 x y text))
    (trace (recv a) (send (cat b n1 n2))
      (recv (cat a (enc n1 x y (pubk b))))
      (send (cat n1 x (enc x y n1 (pubk b)))))
    (uniq-orig n1 n2)))</pre>

<p id="k0">Item <a href="#t0">0</a>, Child: <a href="#k1">1</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='114.960' x2='139.920' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>m</title><circle cx='139.920' cy='189.960' r='6.000'/></g>
  <g><title>m</title>
   <circle style='fill: red;' cx='139.920' cy='114.960' r='6.000'/></g>
  <g><title>(cat n1 x (enc x y n1 (pubk b)))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(cat a (enc n1 n2 m (pubk b)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b n1 n2)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>a</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text x='89.940' y='39.960' style='text-anchor: middle;'>ffgg 0</text>
  </svg></div>

<pre>(defskeleton ffgg
  (vars (m n1 n2 x y text) (b a name))
  (defstrand init 4 (n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))
  (deflistener m)
  (non-orig (privk b))
  (uniq-orig m)
  (label 0)
  (unrealized (1 0))
  (preskeleton)
  (comment &quot;Not a skeleton&quot;))</pre>

<p id="k1">Item <a href="#t0">1</a>, Parent: <a href="#k0">0</a>, Child: <a href="#k2">2</a>.</p>

<div>
 <svg
  class='diagram' width='179.880pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.880 379.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='139.920' y1='264.960' x2='139.920' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>m</title><circle cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>m</title>
   <circle style='fill: red;' cx='139.920' cy='264.960' r='6.000'/></g>
  <g><title>(cat n1 x (enc x y n1 (pubk b)))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 86.940 264.960 133.920 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat a (enc n1 n2 m (pubk b)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b n1 n2)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>a</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text x='89.940' y='39.960' style='text-anchor: middle;'>ffgg 1</text>
  </svg></div>

<pre>(defskeleton ffgg
  (vars (m n1 n2 x y text) (b a name))
  (defstrand init 4 (n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))
  (deflistener m)
  (precedes ((0 2) (1 0)))
  (non-orig (privk b))
  (uniq-orig m)
  (label 1)
  (parent 0)
  (unrealized (1 0))
  (origs (m (0 2)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k2">Item <a href="#t0">2</a>, Parent: <a href="#k1">1</a>, Child: <a href="#k3">3</a>.</p>

<div>
 <svg
  class='diagram' width='279.840pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 279.840 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='239.880' y1='114.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='339.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat n1 n2 (enc n2 m n1 (pubk b)))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(cat a-0 (enc n1 n2 m (pubk b)))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 239.880 189.960 Q 142.920 152.460 45.960 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b n1 n2-0)</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>a-0</title>
   <circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
  <g><title>m</title><circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>m</title>
   <circle style='fill: red;' cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(cat n1 x (enc x y n1 (pubk b)))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 136.920 227.460 233.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat a (enc n1 n2 m (pubk b)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b n1 n2)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>a</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2-0) (x n2) (y m) (b b) (a a-0))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='139.920' y='39.960' style='text-anchor: middle;'>ffgg 2</text>
  </svg></div>

<pre>(defskeleton ffgg
  (vars (m n1 n2 x y n2-0 text) (b a a-0 name))
  (defstrand init 4 (n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))
  (deflistener m)
  (defstrand resp 4 (n1 n1) (n2 n2-0) (x n2) (y m) (b b) (a a-0))
  (precedes ((0 2) (2 2)) ((2 1) (0 1)) ((2 3) (1 0)))
  (non-orig (privk b))
  (uniq-orig m n1 n2-0)
  (operation nonce-test (added-strand resp 4) m (1 0)
    (enc n1 n2 m (pubk b)))
  (label 2)
  (parent 1)
  (unrealized (1 0))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k3">Item <a href="#t0">3</a>, Parent: <a href="#k2">2</a>, Child: <a href="#k4">4</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='454.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 454.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='339.840' y1='114.960' x2='339.840' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='114.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='339.960' x2='139.920' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 339.960 Q 242.880 302.460 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat n2 m (enc m n1 n2 (pubk b)))</title>
   <circle cx='339.840' cy='339.960' r='6.000'/></g>
  <g><title>(cat a-1 (enc n2 m n1 (pubk b)))</title>
   <circle style='fill: red;' cx='339.840' cy='264.960' r='6.000'/></g>
  <path
   d='M 339.840 189.960 Q 192.900 152.460 45.960 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b n2 n2-1)</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>a-1</title>
   <circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 192.900 339.960 145.920 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat n1 n2 (enc n2 m n1 (pubk b)))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(cat a-0 (enc n1 n2 m (pubk b)))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 239.880 189.960 Q 142.920 152.460 45.960 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b n1 n2-0)</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>a-0</title>
   <circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
  <g><title>m</title><circle cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>m</title>
   <circle style='fill: blue;' cx='139.920' cy='339.960' r='6.000'/></g>
  <g><title>(cat n1 x (enc x y n1 (pubk b)))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 136.920 227.460 233.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <path
   d='M 39.960 264.960 Q 186.900 227.460 333.840 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat a (enc n1 n2 m (pubk b)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b n1 n2)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>a</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n2) (n2 n2-1) (x m) (y n1) (b b) (a a-1))</title>
   <text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n1 n1) (n2 n2-0) (x n2) (y m) (b b) (a a-0))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='189.900' y='39.960' style='text-anchor: middle;'>ffgg 3</text>
  </svg></div>

<pre>(defskeleton ffgg
  (vars (m n1 n2 x y n2-0 n2-1 text) (b a a-0 a-1 name))
  (defstrand init 4 (n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))
  (deflistener m)
  (defstrand resp 4 (n1 n1) (n2 n2-0) (x n2) (y m) (b b) (a a-0))
  (defstrand resp 4 (n1 n2) (n2 n2-1) (x m) (y n1) (b b) (a a-1))
  (precedes ((0 2) (2 2)) ((0 2) (3 2)) ((2 1) (0 1)) ((2 3) (1 0))
    ((3 1) (0 1)) ((3 3) (1 0)))
  (non-orig (privk b))
  (uniq-orig m n1 n2 n2-0 n2-1)
  (operation nonce-test (added-strand resp 4) m (1 0)
    (enc n1 n2 m (pubk b)) (enc n2 m n1 (pubk b)))
  (label 3)
  (parent 2)
  (unrealized (3 2))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

<p id="k4">Item <a href="#t0">4</a>, Parent: <a href="#k3">3</a>.</p>

<div>
 <svg
  class='diagram' width='379.800pt' height='529.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 379.800 529.920' font-size='12.000'>
  <defs>
   <marker
    id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'
    refY='5'>
    <path
     d='M 0 0 5 5 0 10'
     style='stroke-width: 2; fill: none; stroke: black;'/></marker>
   </defs>
  <line
   x1='339.840' y1='114.960' x2='339.840' y2='414.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='239.880' y1='114.960' x2='239.880' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='139.920' y1='414.960' x2='139.920' y2='489.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <line
   x1='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <path
   d='M 339.840 414.960 Q 242.880 377.460 145.920 414.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat n2 m (enc m n1 n2 (pubk b)))</title>
   <circle cx='339.840' cy='414.960' r='6.000'/></g>
  <g><title>(cat a-1 (enc n2 m n1 (pubk b)))</title>
   <circle style='fill: blue;' cx='339.840' cy='339.960' r='6.000'/></g>
  <path
   d='M 339.840 189.960 Q 192.900 152.460 45.960 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b n2 n2-1)</title>
   <circle cx='339.840' cy='189.960' r='6.000'/></g>
  <g><title>a-1</title>
   <circle style='fill: blue;' cx='339.840' cy='114.960' r='6.000'/></g>
  <path
   d='M 239.880 339.960 Q 286.860 339.960 333.840 339.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat n1 n2 (enc n2 m n1 (pubk b)))</title>
   <circle cx='239.880' cy='339.960' r='6.000'/></g>
  <g><title>(cat a-0 (enc n1 n2 m (pubk b)))</title>
   <circle style='fill: blue;' cx='239.880' cy='264.960' r='6.000'/></g>
  <path
   d='M 239.880 189.960 Q 142.920 152.460 45.960 189.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat b n1 n2-0)</title>
   <circle cx='239.880' cy='189.960' r='6.000'/></g>
  <g><title>a-0</title>
   <circle style='fill: blue;' cx='239.880' cy='114.960' r='6.000'/></g>
  <g><title>m</title><circle cx='139.920' cy='489.960' r='6.000'/></g>
  <g><title>m</title>
   <circle style='fill: blue;' cx='139.920' cy='414.960' r='6.000'/></g>
  <g><title>(cat n1 x (enc x y n1 (pubk b)))</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <path
   d='M 39.960 264.960 Q 136.920 227.460 233.880 264.960'
   style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>
  <g><title>(cat a (enc n1 n2 m (pubk b)))</title>
   <circle cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat b n1 n2)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>a</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n2) (n2 n2-1) (x m) (y n1) (b b) (a a-1))</title>
   <text x='339.840' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n1 n1) (n2 n2-0) (x n2) (y m) (b b) (a a-0))</title>
   <text x='239.880' y='77.460' style='text-anchor: middle;'>resp</text>
   </g>
  <g><title>((n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='189.900' y='39.960'
   style='text-anchor: middle;'>ffgg 4 (realized)</text></svg></div>

<pre>(defskeleton ffgg
  (vars (m n1 n2 x y n2-0 n2-1 text) (b a a-0 a-1 name))
  (defstrand init 4 (n1 n1) (n2 n2) (m m) (x x) (y y) (a a) (b b))
  (deflistener m)
  (defstrand resp 4 (n1 n1) (n2 n2-0) (x n2) (y m) (b b) (a a-0))
  (defstrand resp 4 (n1 n2) (n2 n2-1) (x m) (y n1) (b b) (a a-1))
  (precedes ((0 2) (2 2)) ((2 1) (0 1)) ((2 3) (3 2)) ((3 1) (0 1))
    ((3 3) (1 0)))
  (non-orig (privk b))
  (uniq-orig m n1 n2 n2-0 n2-1)
  (operation nonce-test (displaced 4 2 resp 4) m (3 2)
    (enc n1 n2 m (pubk b)))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0 1) ((b b) (m m) (a a) (n1 n1) (n2 n2) (x x) (y y))))
  (origs (n1 (2 1)) (n2-0 (2 1)) (n2 (3 1)) (n2-1 (3 1)) (m (0 2))))</pre>

</body>
</html>