priority_test.xhtml

<?xml version="1.0"?>
<!-- CPSA 3.6.0 -->
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
 <title>Receive priority 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;Receive priority test protocol&quot;)
(comment &quot;CPSA 3.6.0&quot;)
(comment &quot;All input read from priority_test.scm&quot;)</pre>

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

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

<div>
 <svg
  class='diagram' width='179.760pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.760 79.920' font-size='12.000'>
  <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 priority_test basic
  (defrole init
    (vars (n1 n2 n3 n4 text) (k skey))
    (trace (send (enc n1 n1 k)) (recv (enc n1 n2 k))
      (recv (enc n1 n3 k)) (recv (enc n1 n4 k)))
    (non-orig k)
    (uniq-orig n1)
    (priority (2 0) (3 10))))</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='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n1 n4 k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n1 n3 k)</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n1 n2 k)</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 n1 k)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (n3 n3) (n4 n4) (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;'>priority_test 0</text></svg></div>

<pre>(defskeleton priority_test
  (vars (n1 n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n1) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 0) ((0 3) 10))
  (non-orig k)
  (uniq-orig n1)
  (label 0)
  (unrealized (0 1) (0 2) (0 3))
  (origs (n1 (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>, Child: <a href="#k2">2</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n4 n4 k)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n4 n3 k)</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n4 n2 k)</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n4 n4 k)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n4) (n2 n2) (n3 n3) (n4 n4) (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;'>priority_test 1</text></svg></div>

<pre>(defskeleton priority_test
  (vars (n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n4) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 0) ((0 3) 10))
  (non-orig k)
  (uniq-orig n4)
  (operation encryption-test (displaced 1 0 init 1) (enc n4 n4 k) (0 3))
  (label 1)
  (parent 0)
  (unrealized (0 1) (0 2))
  (origs (n4 (0 0)))
  (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>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n2 n2 k)</title>
   <circle style='fill: blue;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n2 n3 k)</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n2 n2 k)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n2 n2 k)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n2) (n2 n2) (n3 n3) (n4 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;'>priority_test 2</text></svg></div>

<pre>(defskeleton priority_test
  (vars (n2 n3 text) (k skey))
  (defstrand init 4 (n1 n2) (n2 n2) (n3 n3) (n4 n2) (k k))
  (priority ((0 2) 0) ((0 3) 10))
  (non-orig k)
  (uniq-orig n2)
  (operation encryption-test (displaced 1 0 init 1) (enc n2 n2 k) (0 1))
  (label 2)
  (parent 1)
  (unrealized (0 2))
  (origs (n2 (0 0))))</pre>

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

<div>
 <svg
  class='diagram' width='179.760pt' height='79.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 179.760 79.920' font-size='12.000'>
  <text
   x='139.800' y='26.040' style='text-anchor: middle; fill: black;'
   onclick='window.open(&quot;#k5&quot;, &quot;_self&quot;)'>5</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;#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 priority_test basic
  (defrole init
    (vars (n1 n2 n3 n4 text) (k skey))
    (trace (send (enc n1 n1 k)) (recv (enc n1 n2 k))
      (recv (enc n1 n3 k)) (recv (enc n1 n4 k)))
    (non-orig k)
    (uniq-orig n1)
    (priority (2 0) (3 10))))</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='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n1 n4 k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n1 n3 k)</title>
   <circle style='fill: red;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n1 n2 k)</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n1 n1 k)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n1) (n2 n2) (n3 n3) (n4 n4) (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;'>priority_test 3</text></svg></div>

<pre>(defskeleton priority_test
  (vars (n1 n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n1) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 10) ((0 3) 0))
  (non-orig k)
  (uniq-orig n1)
  (label 3)
  (unrealized (0 1) (0 2) (0 3))
  (origs (n1 (0 0)))
  (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>, Child: <a href="#k5">5</a>.</p>

<div>
 <svg
  class='diagram' width='79.920pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n3 n4 k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n3 n3 k)</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n3 n2 k)</title>
   <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n3 n3 k)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n3) (n2 n2) (n3 n3) (n4 n4) (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;'>priority_test 4</text></svg></div>

<pre>(defskeleton priority_test
  (vars (n2 n3 n4 text) (k skey))
  (defstrand init 4 (n1 n3) (n2 n2) (n3 n3) (n4 n4) (k k))
  (priority ((0 2) 10) ((0 3) 0))
  (non-orig k)
  (uniq-orig n3)
  (operation encryption-test (displaced 1 0 init 1) (enc n3 n3 k) (0 2))
  (label 4)
  (parent 3)
  (unrealized (0 1) (0 3))
  (origs (n3 (0 0)))
  (comment &quot;1 in cohort - 1 not yet seen&quot;))</pre>

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

<div>
 <svg
  class='diagram' width='79.920pt' height='379.920pt'
  xmlns='http://www.w3.org/2000/svg' version='1.1'
  viewBox='0 0 79.920 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='39.960' y1='114.960' x2='39.960' y2='339.960'
   style='stroke-width: 0.960; stroke: gray;'/>
  <g><title>(enc n2 n4 k)</title>
   <circle style='fill: red;' cx='39.960' cy='339.960' r='6.000'/></g>
  <g><title>(enc n2 n2 k)</title>
   <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>
  <g><title>(enc n2 n2 k)</title>
   <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>
  <g><title>(enc n2 n2 k)</title>
   <circle cx='39.960' cy='114.960' r='6.000'/></g>
  <g><title>((n1 n2) (n2 n2) (n3 n2) (n4 n4) (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;'>priority_test 5</text></svg></div>

<pre>(defskeleton priority_test
  (vars (n2 n4 text) (k skey))
  (defstrand init 4 (n1 n2) (n2 n2) (n3 n2) (n4 n4) (k k))
  (priority ((0 2) 10) ((0 3) 0))
  (non-orig k)
  (uniq-orig n2)
  (operation encryption-test (displaced 1 0 init 1) (enc n2 n2 k) (0 1))
  (label 5)
  (parent 4)
  (unrealized (0 3))
  (origs (n2 (0 0))))</pre>

</body>
</html>