X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=docs%2Fgraphics%2Fsw-model-checking-2.svg;fp=docs%2Fgraphics%2Fsw-model-checking-2.svg;h=a0575f7b4743ff7e11475a799752c7da79eb3ca9;hp=0000000000000000000000000000000000000000;hb=3f0145e38039475a1654974a45ad89c58e2e91e7;hpb=eb4888bdc6128a112847f8c8b93f94efc2bb9f54

diff --git a/docs/graphics/sw-model-checking-2.svg b/docs/graphics/sw-model-checking-2.svg
new file mode 100644
index 0000000..a0575f7
--- /dev/null
+++ b/docs/graphics/sw-model-checking-2.svg
@@ -0,0 +1,3 @@
+<?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="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="34 236 374 190" width="374pt" height="190pt" xmlns:dc="http://purl.org/dc/elements/1.1/"><metadata> Produced by OmniGraffle 6.1 <dc:date>2015-01-05 22:19:29 +0000</dc:date></metadata><defs><font-face font-family="Courier" font-size="14" units-per-em="1000" underline-position="-144.04297" underline-thickness="91.796875" slope="0" x-height="462.40234" cap-height="594.72656" ascent="753.90625" descent="-246.09375" font-weight="bold"><font-face-src><font-face-name name="Courier-Bold"/></font-face-src></font-face><font-face font-family="Courier" font-size="14" units-per-em="1000" underline-position="-178.22266" underline-thickness="57.617188" slope="0" x-height="462.40234" cap-height="594.72656" ascent="753.90625" descent="-246.09375" font-weight="500"><font-face-src><font-face-name name="Courier"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="StickArrow_Marker" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black"><g><path d="M 8 0 L 0 0 M 0 -3 L 8 0 L 0 3" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="StickArrow_Marker_2" viewBox="-1 -3 7 6" markerWidth="7" markerHeight="6" color="red"><g><path d="M 4.8 0 L 0 0 M 0 -1.8 L 4.8 0 L 0 1.8" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Zapf Dingbats" font-size="14" panose-1="5 2 1 2 1 7 4 2 6 9" units-per-em="1000" underline-position="-100.097656" underline-thickness="60.058594" slope="0" x-height="542.48047" cap-height="723.14453" ascent="813.96484" descent="-176.75781" font-weight="500"><font-face-src><font-face-name name="ZapfDingbatsITC"/></font-face-src></font-face><marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="Arrow_Marker" viewBox="-1 -3 7 6" markerWidth="7" markerHeight="6" color="purple"><g><path d="M 4.7999992 0 L 0 -1.7999997 L 0 1.7999997 Z" fill="none" stroke="currentColor" stroke-width="1"/></g></marker><font-face font-family="Helvetica" font-size="9" units-per-em="1000" underline-position="-75.683594" underline-thickness="49.316406" slope="0" x-height="522.94922" cap-height="717.28516" ascent="770.01953" descent="-229.98047" font-weight="500"><font-face-src><font-face-name name="Helvetica"/></font-face-src></font-face></defs><g stroke="none" stroke-opacity="1" stroke-dasharray="none" fill="none" fill-opacity="1"><title>Canvas 1</title><rect fill="white" width="768.0188" height="588.0188"/><g><title>Layer 1</title><text transform="translate(97.5 288)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="bold" fill="blue" x="0" y="14" textLength="25.204102">a=0</tspan></text><text transform="translate(51.5 335)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">b=0</tspan></text><text transform="translate(117 335)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">b=1</tspan></text><text transform="translate(182 335)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="bold" fill="blue" x="0" y="14" textLength="25.204102">b=2</tspan></text><line x1="102.18085" y1="305" x2="79.743833" y2="327.92478" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="114.026596" y1="305" x2="122.67953" y2="325.8558" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="125.781915" y1="305" x2="168.4446" y2="328.72954" marker-end="url(#StickArrow_Marker_2)" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/><text transform="translate(51.5 380)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">c=0</tspan></text><text transform="translate(117 380)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">c=0</tspan></text><text transform="translate(174.5 380)" fill="red"><tspan font-family="Courier" font-size="14" font-weight="bold" fill="red" x="0" y="14" textLength="42.006836">c=0/0</tspan></text><line x1="64.5" y1="352" x2="64.5" y2="370.1" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="130" y1="352" x2="130" y2="370.1" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="195.18889" y1="352" x2="195.52452" y2="367.10318" marker-end="url(#StickArrow_Marker_2)" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/><text transform="translate(200 245)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="bold" fill="blue" x="0" y="14" textLength="42.006836">start</tspan></text><line x1="199.55814" y1="262" x2="140.52895" y2="284.86716" marker-end="url(#StickArrow_Marker_2)" stroke="red" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/><text transform="translate(304.5 288)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">a=1</tspan></text><text transform="translate(258.5 335)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">b=0</tspan></text><text transform="translate(312.5 335)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">b=1</tspan></text><text transform="translate(366.5 335)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">b=2</tspan></text><line x1="309.18085" y1="305" x2="286.74383" y2="327.92478" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="318.9468" y1="305" x2="322.39198" y2="325.24037" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="328.71277" y1="305" x2="360.39788" y2="329.01936" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(254.5 380.5)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="33.605469">c=-1</tspan></text><text transform="translate(304 380.5)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="42.006836">c=1/0</tspan></text><text transform="translate(367.5 380)" fill="blue"><tspan font-family="Courier" font-size="14" font-weight="500" fill="blue" x="0" y="14" textLength="25.204102">c=1</tspan></text><line x1="271.5" y1="352" x2="271.5" y2="370.1" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="325.5" y1="352" x2="325.5" y2="370.1" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="379.68912" y1="352" x2="380.0919" y2="370.10245" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><line x1="240.47674" y1="262" x2="290.46495" y2="284.39055" marker-end="url(#StickArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/><text transform="translate(190 402)" fill="red"><tspan font-family="Zapf Dingbats" font-size="14" font-weight="500" fill="red" x="0" y="11" textLength="9.4746094">✘</tspan></text><path d="M 195 255.53846 C 184.3344 256.35889 171.9991 255.75663 163 258 C 154.0009 260.24337 148.17807 264.0005 141 269 C 135.49167 272.83653 130.1641 278.24436 124.8097 283.41438" marker-end="url(#Arrow_Marker)" stroke="purple" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><rect x="165.29035" y="251.01964" width="16" height="11" fill="white"/><text transform="translate(170.29035 251.01964)" fill="purple"><tspan font-family="Helvetica" font-size="9" font-weight="500" fill="purple" x="0" y="9" textLength="5.005371">1</tspan></text><path d="M 93.036364 305 C 80.025544 311.3327 61.83861 316.91738 54 324 C 46.16139 331.08262 44.88934 338.1676 46 347.5 C 46.909354 355.1409 52.88361 364.79484 57.70203 373.98866" marker-end="url(#Arrow_Marker)" stroke="purple" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><rect x="59.46112" y="310.53899" width="16" height="11" fill="white"/><text transform="translate(64.46112 310.53899)" fill="purple"><tspan font-family="Helvetica" font-size="9" font-weight="500" fill="purple" x="0" y="9" textLength="5.005371">2</tspan></text><path d="M 67.75532 380 C 72.66972 367.16795 76.257992 353.99875 82.5 341.5 C 87.77279 330.94197 94.94186 320.857 101.60377 310.64679" marker-end="url(#Arrow_Marker)" stroke="purple" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><rect x="66.688773" y="354.95894" width="16" height="11" fill="white"/><text transform="translate(71.688773 354.95894)" fill="purple"><tspan font-family="Helvetica" font-size="9" font-weight="500" fill="purple" x="0" y="9" textLength="5.005371">3</tspan></text><path d="M 110.03297 305 C 109.35538 317.3321 107.672194 331.58438 108 342 C 108.327806 352.41562 109.547864 361.1673 112 367.5 C 113.41764 371.1611 115.5836 373.37442 117.84884 375.39535" marker-end="url(#Arrow_Marker)" stroke="purple" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><rect x="100.541785" y="320.0904" width="16" height="11" fill="white"/><text transform="translate(105.541785 320.0904)" fill="purple"><tspan font-family="Helvetica" font-size="9" font-weight="500" fill="purple" x="0" y="9" textLength="5.005371">4</tspan></text><path d="M 133.36264 380 C 138.24127 367.6679 150.6677 355.49875 148 343 C 145.68608 332.1588 132.01485 321.06398 121.76401 310.04676" marker-end="url(#Arrow_Marker)" stroke="purple" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><rect x="136.39532" y="354.41076" width="16" height="11" fill="white"/><text transform="translate(141.39532 354.41076)" fill="purple"><tspan font-family="Helvetica" font-size="9" font-weight="500" fill="purple" x="0" y="9" textLength="5.005371">5</tspan></text><text transform="translate(59 402)" fill="#00c300"><tspan font-family="Zapf Dingbats" font-size="14" font-weight="500" fill="#00c300" x="0" y="11" textLength="11.84668">✔</tspan></text><text transform="translate(124 402)" fill="#00c300"><tspan font-family="Zapf Dingbats" font-size="14" font-weight="500" fill="#00c300" x="0" y="11" textLength="11.84668">✔</tspan></text><path d="M 128.5 303.40226 C 144.66505 309.60088 162.91808 315.15106 177 322 C 191.08192 328.84894 209.28636 334.8343 213 344.5 C 216.09567 352.55727 207.67603 363.62784 202.14012 373.94288" marker-end="url(#Arrow_Marker)" stroke="purple" stroke-linecap="round" stroke-linejoin="round" stroke-width="1" stroke-dasharray="2,2"/><rect x="152.59596" y="309.56811" width="16" height="11" fill="white"/><text transform="translate(157.59596 309.56811)" fill="purple"><tspan font-family="Helvetica" font-size="9" font-weight="500" fill="purple" x="0" y="9" textLength="5.005371">6</tspan></text></g></g></svg>