lt_test.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.4.0 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Less-than constraint test 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;Less-than constraint test protocol&quot;
  (comment &quot;First and third skeletons should have a shape,&quot;
    &quot;second and fourth should be dead.&quot;))
(comment &quot;CPSA 3.4.0&quot;)
(comment &quot;All input read from lt_test.scm&quot;)</pre>

<p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t3">3</a> <a href="#t5">5</a>.</p>

<p id="t0">Tree <a href="#top">0</a>.</p>

<div>
 <svg
  class='diagram' width='129.840pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 129.840 79.920' font-size='12.000'>
  <text
   x='89.880' y='26.040'
   style='font-weight: bold; text-anchor: middle; fill: blue;'
   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 lttest basic
  (defrole init
    (vars (n1 n2 text) (k skey))
    (trace (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (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='79.920pt' height='229.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 229.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='39.960' y1='114.960' x2='39.960' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n2</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat n1 (enc n1 n2 k))</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960' style='text-anchor: middle;'>lttest 0</text>
  </svg></div>

<pre>(defskeleton lttest
  (vars (n1 n2 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n2) (k k))
  (non-orig k)
  (uniq-orig n1 n2)
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='79.920pt' height='229.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 229.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='39.960' y1='114.960' x2='39.960' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n1</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat n1 (enc n1 n1 k))</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n1) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960'
   style='text-anchor: middle;'>lttest 1 (realized)</text></svg></div>

<pre>(defskeleton lttest
  (vars (n1 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n1) (k k))
  (non-orig k)
  (uniq-orig n1)
  (operation nonce-test (displaced 1 0 init 1) n2 (0 1) (enc n1 n2 k))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((n1 n1) (n2 n1) (k k))))
  (origs (n1 (0 0))))</pre>

<p id="t2">Tree <a href="#top">2</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 79.920' font-size='12.000'>
  <text
   x='39.960' y='26.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k2&quot;, &quot;_self&quot;)'>2</text>
  </svg></div>

<pre>(defprotocol lttest basic
  (defrole init
    (vars (n1 n2 text) (k skey))
    (trace (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (uniq-orig n1 n2)))</pre>

<p id="k2">Item <a href="#t2">2</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='229.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 229.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='39.960' y1='114.960' x2='39.960' y2='189.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n2</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(cat n1 (enc n1 n2 k))</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960' style='text-anchor: middle;'>lttest 2</text>
  </svg></div>

<pre>(defskeleton lttest
  (vars (n1 n2 text) (k skey))
  (defstrand init 2 (n1 n1) (n2 n2) (k k))
  (lt (n1 n2))
  (non-orig k)
  (uniq-orig n1 n2)
  (label 2)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment &quot;empty cohort&quot;))</pre>

<p id="t3">Tree <a href="#top">3</a>.</p>

<div>
 <svg
  class='diagram' width='129.840pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 129.840 79.920' font-size='12.000'>
  <text
   x='89.880' 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='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;#k3&quot;, &quot;_self&quot;)'>3</text>
  </svg></div>

<pre>(defprotocol lttest2 basic
  (defrole init
    (vars (n1 n2 n text) (k skey))
    (trace (send n) (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (uniq-orig n1 n2)
    (lt (n2 n))))</pre>

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

<div>
 <svg
  class='diagram' width='79.920pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 304.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='39.960' y1='114.960' x2='39.960' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n2</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat n1 (enc n1 n2 k))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>n</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (n n) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960' style='text-anchor: middle;'>lttest2 3</text>
  </svg></div>

<pre>(defskeleton lttest2
  (vars (n1 n2 n text) (k skey))
  (defstrand init 3 (n1 n1) (n2 n2) (n n) (k k))
  (lt (n2 n))
  (non-orig k)
  (uniq-orig n1 n2)
  (label 3)
  (unrealized (0 2))
  (origs (n1 (0 1)) (n2 (0 1)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='79.920pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 304.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='39.960' y1='114.960' x2='39.960' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n1</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat n1 (enc n1 n1 k))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>n</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n1) (n n) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960'
   style='text-anchor: middle;'>lttest2 4 (realized)</text></svg></div>

<pre>(defskeleton lttest2
  (vars (n1 n text) (k skey))
  (defstrand init 3 (n1 n1) (n2 n1) (n n) (k k))
  (lt (n1 n))
  (non-orig k)
  (uniq-orig n1)
  (operation nonce-test (displaced 1 0 init 2) n2 (0 2) (enc n1 n2 k))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((n1 n1) (n2 n1) (n n) (k k))))
  (origs (n1 (0 1))))</pre>

<p id="t5">Tree <a href="#top">5</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 79.920' font-size='12.000'>
  <text
   x='39.960' y='26.040' style='text-anchor: middle; fill: red;'
   onclick='window.open(&quot;#k5&quot;, &quot;_self&quot;)'>5</text>
  </svg></div>

<pre>(defprotocol lttest2 basic
  (defrole init
    (vars (n1 n2 n text) (k skey))
    (trace (send n) (send (cat n1 (enc n1 n2 k))) (recv n2))
    (non-orig k)
    (uniq-orig n1 n2)
    (lt (n2 n))))</pre>

<p id="k5">Item <a href="#t5">5</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='304.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 304.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='39.960' y1='114.960' x2='39.960' y2='264.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>n2</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(cat n1 (enc n1 n2 k))</title>
   <circle cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>n</title><circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (n n) (k k))</title>
   <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>
   </g>
  <text
   x='39.960' y='39.960' style='text-anchor: middle;'>lttest2 5</text>
  </svg></div>

<pre>(defskeleton lttest2
  (vars (n n1 n2 text) (k skey))
  (defstrand init 3 (n1 n1) (n2 n2) (n n) (k k))
  (lt (n n1) (n2 n))
  (non-orig k)
  (uniq-orig n1 n2)
  (label 5)
  (unrealized (0 2))
  (origs (n1 (0 1)) (n2 (0 1)))
  (comment &quot;empty cohort&quot;))</pre>

</body>
</html>