Files

39 lines
6.1 KiB
XML
Raw Permalink Blame History

This file contains invisible Unicode characters
This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
<?xml version="1.0" encoding="UTF-8" standalone="no"?><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" contentScriptType="application/ecmascript" contentStyleType="text/css" height="378px" preserveAspectRatio="none" style="width:324px;height:378px;" version="1.1" viewBox="0 0 324 378" width="324px" zoomAndPan="magnify"><defs/><g><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="303" x="9.5" y="12.8281">A4 APPLICATION — behavior parity is part of the proof</text><!--MD5=[2fdd58fa1f9dca7f678b1591ba5c253a]
entity dyn--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="129" x="6" y="23.9041"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="106" x="16" y="46.7322">01 dynamic worker</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="16" y="63.0763">receive 0xCAFE</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="109" x="16" y="79.4204">start dynamic timer</text><!--MD5=[299d1c4a2ba6184a4b2319b3d939ce68]
entity stat--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="112" x="191.5" y="23.9041"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="89" x="201.5" y="46.7322">02 static worker</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="201.5" y="63.0763">receive 0xCAFE</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="92" x="201.5" y="79.4204">start static timer</text><!--MD5=[995a46705506099b563611b182911a66]
entity daemon--><rect fill="#EDF6FA" height="69.0323" style="stroke: #2C7794; stroke-width: 1.5;" width="135" x="81" y="152.9341"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="96" x="91" y="175.7622">03 timer daemon</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="115" x="91" y="192.1063">dynamic callback = 1</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="98" x="91" y="208.4504">static callback = 1</text><!--MD5=[43277b5e5915b8aad291fb6c6bd0e270]
entity verify--><rect fill="#EDF6FA" height="85.3765" style="stroke: #2C7794; stroke-width: 1.5;" width="106" x="95.5" y="281.9641"/><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="57" x="105.5" y="304.7922">04 verifier</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="86" x="105.5" y="321.1363">message parity</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="80" x="105.5" y="337.4804">callback parity</text><text fill="#000000" font-family="Monospace" font-size="12" lengthAdjust="spacingAndGlyphs" textLength="78" x="105.5" y="353.8245">distinct stacks</text><!--MD5=[bea346f714fb01cb80d7f2e7dbd64f2b]
link dyn to daemon--><path d="M91.2,93.1241 C101.42,109.7841 113.82,129.9741 124.46,147.3041 " fill="none" id="dyn-&gt;daemon" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="126.91,151.2941,125.5852,141.5348,124.2831,147.0397,118.7782,145.7377,126.91,151.2941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[455cce1656bdd5dce2f89c06f912f1d1]
link stat to daemon--><path d="M221.23,93.1241 C208.14,109.9241 192.25,130.3141 178.66,147.7541 " fill="none" id="stat-&gt;daemon" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="175.82,151.3941,184.5064,146.7522,178.8927,147.4497,178.1952,141.836,175.82,151.3941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[55f9ed2204fe7b44e8df8666194ec3de]
link dyn to verify--><path d="M61.71,93.2441 C54.63,126.9441 48.13,179.6141 63.5,221.9641 C70.76,241.9641 83.85,260.7741 97.63,276.6541 " fill="none" id="dyn-&gt;verify" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="100.92,280.3541,97.9304,270.97,97.5982,276.6171,91.9511,276.2849,100.92,280.3541" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[0b779b9021da6d81f69dcc0e6137211d]
link stat to verify--><path d="M250.36,93.1741 C251.93,127.0441 250.78,180.0741 233.5,221.9641 C225.31,241.8241 211.8,260.7241 197.92,276.7141 " fill="none" id="stat-&gt;verify" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="194.62,280.4541,203.5812,276.3679,197.9347,276.7108,197.5918,271.0643,194.62,280.4541" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[97dcfe194a7fdfb828de87be35f0eec1]
link daemon to verify--><path d="M148.5,222.2241 C148.5,238.2441 148.5,257.6841 148.5,275.2341 " fill="none" id="daemon-&gt;verify" style="stroke: #A80036; stroke-width: 1.0;"/><polygon fill="#A80036" points="148.5,280.0941,152.5,271.0941,148.5,275.0941,144.5,271.0941,148.5,280.0941" style="stroke: #A80036; stroke-width: 1.0;"/><!--MD5=[a8a1b31c45c5f222072643cce2cd8c96]
@startuml
skinparam backgroundColor transparent
skinparam shadowing false
skinparam defaultFontName Monospace
skinparam defaultFontSize 12
skinparam rectangleBorderColor #2c7794
skinparam rectangleBackgroundColor #edf6fa
title A4 APPLICATION — behavior parity is part of the proof
rectangle "01 dynamic worker\nreceive 0xCAFE\nstart dynamic timer" as dyn
rectangle "02 static worker\nreceive 0xCAFE\nstart static timer" as stat
rectangle "03 timer daemon\ndynamic callback = 1\nstatic callback = 1" as daemon
rectangle "04 verifier\nmessage parity\ncallback parity\ndistinct stacks" as verify
dyn - -> daemon
stat - -> daemon
dyn - -> verify
stat - -> verify
daemon - -> verify
@enduml
PlantUML version 1.2020.02(Sun Mar 01 11:22:07 CET 2020)
(GPL source distribution)
Java Runtime: OpenJDK Runtime Environment
JVM: OpenJDK 64-Bit Server VM
Java Version: 25.0.4-ea+4-1-Debian
Operating System: Linux
Default Encoding: UTF-8
Language: en
Country: null
--></g></svg>