<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
<svg xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns:xl="http://www.w3.org/1999/xlink" xmlns="http://www.w3.org/2000/svg" viewBox="81.316 84.276 559.1417 205.724" width="559.1417" height="205.724">
  <defs>
    <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -3 7 6" markerWidth="7" markerHeight="6" color="black">
      <g>
        <path d="M 4.8 0 L 0 -1.8 L 0 1.8 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
      </g>
    </marker>
    <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -2 4 4" markerWidth="4" markerHeight="4" color="black">
      <g>
        <path d="M 1.584 0 L 0 -.594 L 0 .594 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
      </g>
    </marker>
  </defs>
  <g id="Canvas_1" fill-opacity="1" stroke-opacity="1" stroke-dasharray="none" fill="none" stroke="none">
    <title>Canvas 1</title>
    <g id="Canvas_1_Layer_1">
      <title>Layer 1</title>
      <g id="Graphic_2">
        <text transform="translate(86.316 104.5)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="3907985e-19" y="15">Specification</tspan>
        </text>
      </g>
      <g id="Graphic_4">
        <text transform="translate(377.5 146.5)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="4369838e-19" y="15">Invariant</tspan>
        </text>
      </g>
      <g id="Graphic_6">
        <ellipse cx="249.86258" cy="99.724" rx="15.3008842768261" ry="14.2240217519925" fill="white"/>
        <ellipse cx="249.86258" cy="99.724" rx="15.3008842768261" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        <text transform="translate(242.6219 93.584)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K1</tspan>
        </text>
      </g>
      <g id="Graphic_7">
        <ellipse cx="215.80086" cy="150.724" rx="15.300884276826" ry="14.2240217519925" fill="white"/>
        <ellipse cx="215.80086" cy="150.724" rx="15.300884276826" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        <text transform="translate(208.56017 144.584)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K0</tspan>
        </text>
      </g>
      <g id="Graphic_8">
        <ellipse cx="288.36258" cy="150.724" rx="15.300884276826" ry="14.2240217519925" fill="white"/>
        <ellipse cx="288.36258" cy="150.724" rx="15.300884276826" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        <text transform="translate(281.1219 144.584)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.8656878" y="10">k2</tspan>
        </text>
      </g>
      <g id="Line_9">
        <line x1="241.2334" y1="112.64433" x2="231.59467" y2="127.07622" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
      </g>
      <g id="Line_10">
        <line x1="259.25724" y1="112.16888" x2="271.19565" y2="127.9834" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
      </g>
      <g id="Graphic_11">
        <text transform="translate(302.06172 107)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="3161915e-19" y="15">k1 &lt; k2</tspan>
        </text>
      </g>
      <g id="Graphic_17">
        <ellipse cx="530.3626" cy="99.5" rx="15.3008842768261" ry="14.2240217519925" fill="white"/>
        <ellipse cx="530.3626" cy="99.5" rx="15.3008842768261" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        <text transform="translate(523.1219 93.36)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K1</tspan>
        </text>
      </g>
      <g id="Graphic_16">
        <ellipse cx="496.30086" cy="150.5" rx="15.3008842768261" ry="14.2240217519925" fill="white"/>
        <ellipse cx="496.30086" cy="150.5" rx="15.3008842768261" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        <text transform="translate(489.0602 144.36)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K0</tspan>
        </text>
      </g>
      <g id="Graphic_15">
        <ellipse cx="568.8626" cy="150.5" rx="15.3008842768262" ry="14.2240217519925" fill="white"/>
        <ellipse cx="568.8626" cy="150.5" rx="15.3008842768262" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        <text transform="translate(561.6219 144.36)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.8656878" y="10">k2</tspan>
        </text>
      </g>
      <g id="Line_14">
        <line x1="521.7334" y1="112.42033" x2="512.09467" y2="126.85222" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
      </g>
      <g id="Line_13">
        <line x1="539.75724" y1="111.94488" x2="551.69565" y2="127.7594" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
      </g>
      <g id="Graphic_12">
        <text transform="translate(582.5617 106.776)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="3161915e-19" y="15">k1 &lt; k2</tspan>
        </text>
      </g>
      <g id="Graphic_21">
        <path d="M 387 130.25 L 387 119.75 L 406.6017 119.75 L 406.6017 114.5 L 417.6017 125 L 406.6017 135.5 L 406.6017 130.25 Z" fill="white"/>
        <path d="M 387 130.25 L 387 119.75 L 406.6017 119.75 L 406.6017 114.5 L 417.6017 125 L 406.6017 135.5 L 406.6017 130.25 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
      </g>
      <g id="Group_40">
        <g id="Graphic_38">
          <rect x="206.06663" y="198" width="244.88618" height="91" fill="white"/>
          <rect x="206.06663" y="198" width="244.88618" height="91" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Graphic_27">
          <ellipse cx="255.32134" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" fill="white"/>
          <ellipse cx="255.32134" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Graphic_26">
          <ellipse cx="238.52125" cy="245.46008" rx="7.54677761079225" ry="7.01564216493943" fill="white"/>
          <ellipse cx="238.52125" cy="245.46008" rx="7.54677761079225" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Graphic_25">
          <ellipse cx="274.3105" cy="245.46008" rx="7.54677761079228" ry="7.01564216493943" fill="white"/>
          <ellipse cx="274.3105" cy="245.46008" rx="7.54677761079228" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Line_24">
          <line x1="250.78322" y1="227.10045" x2="246.65168" y2="233.28653" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Line_23">
          <line x1="260.26097" y1="226.849" x2="265.4739" y2="233.75445" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Graphic_32">
          <ellipse cx="326.89984" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" fill="white"/>
          <ellipse cx="326.89984" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Graphic_31">
          <ellipse cx="310.09975" cy="245.46008" rx="7.54677761079224" ry="7.01564216493943" fill="white"/>
          <ellipse cx="310.09975" cy="245.46008" rx="7.54677761079224" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Graphic_30">
          <ellipse cx="345.889" cy="245.46008" rx="7.54677761079227" ry="7.01564216493943" fill="white"/>
          <ellipse cx="345.889" cy="245.46008" rx="7.54677761079227" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Line_29">
          <line x1="322.36172" y1="227.10045" x2="318.23018" y2="233.28653" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Line_28">
          <line x1="331.83947" y1="226.849" x2="337.0524" y2="233.75445" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Graphic_34">
          <ellipse cx="364.87816" cy="270.61455" rx="7.54677761079224" ry="7.0156421649394" fill="white"/>
          <ellipse cx="364.87816" cy="270.61455" rx="7.54677761079224" ry="7.0156421649394" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
        <g id="Line_36">
          <line x1="350.82863" y1="252.00347" x2="356.04156" y2="258.90892" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/>
        </g>
      </g>
      <g id="Graphic_39">
        <text transform="translate(93.564 173)" fill="black">
          <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="8029133e-19" y="15">Denotation</tspan>
        </text>
      </g>
    </g>
  </g>
</svg>