-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathexample_3.html
170 lines (170 loc) · 12.1 KB
/
example_3.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
<div><?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">
<!-- Generated by graphviz version 2.40.1 (20161225.0304)
-->
<!-- Pages: 1 -->
<svg width="564pt" height="320pt"
viewBox="0.00 0.00 564.00 320.00" xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink">
<g id="graph0" class="graph" transform="scale(1.0 1.0) rotate(0) translate(4 316)">
<polygon fill="#ffffff" stroke="transparent" points="-4,4 -4,-316 560,-316 560,4 -4,4"/>
<text text-anchor="start" x="257" y="-297.8" font-family="Lato" font-size="14.00" fill="#000000">Inf(</text>
<text text-anchor="start" x="279" y="-297.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text>
<text text-anchor="start" x="295" y="-297.8" font-family="Lato" font-size="14.00" fill="#000000">)</text>
<text text-anchor="start" x="255" y="-283.8" font-family="Lato" font-size="14.00" fill="#000000">[Büchi]</text>
<!-- I -->
<!-- 0 -->
<g id="node2" class="node">
<title>0</title>
<ellipse fill="#ffffaa" stroke="#000000" cx="56" cy="-153" rx="18" ry="18"/>
<text text-anchor="middle" x="56" y="-149.3" font-family="Lato" font-size="14.00" fill="#000000">0</text>
</g>
<!-- I->0 -->
<g id="edge1" class="edge">
<title>I->0</title>
<path fill="none" stroke="#000000" d="M1.1233,-153C4.178,-153 17.9448,-153 30.9241,-153"/>
<polygon fill="#000000" stroke="#000000" points="37.9807,-153 30.9808,-156.1501 34.4807,-153 30.9807,-153.0001 30.9807,-153.0001 30.9807,-153.0001 34.4807,-153 30.9807,-149.8501 37.9807,-153 37.9807,-153"/>
</g>
<!-- 0->0 -->
<g id="edge2" class="edge">
<title>0->0</title>
<path fill="none" stroke="#000000" d="M49.6208,-170.0373C48.3189,-179.8579 50.4453,-189 56,-189 60.166,-189 62.4036,-183.8576 62.7128,-177.1433"/>
<polygon fill="#000000" stroke="#000000" points="62.3792,-170.0373 65.8541,-176.8818 62.5434,-173.5335 62.7076,-177.0296 62.7076,-177.0296 62.7076,-177.0296 62.5434,-173.5335 59.561,-177.1774 62.3792,-170.0373 62.3792,-170.0373"/>
<text text-anchor="start" x="39" y="-192.8" font-family="Lato" font-size="14.00" fill="#000000">!a | !b</text>
</g>
<!-- 3 -->
<g id="node3" class="node">
<title>3</title>
<ellipse fill="#ffffaa" stroke="#000000" cx="162" cy="-153" rx="18" ry="18"/>
<text text-anchor="middle" x="162" y="-149.3" font-family="Lato" font-size="14.00" fill="#000000">3</text>
</g>
<!-- 0->3 -->
<g id="edge3" class="edge">
<title>0->3</title>
<path fill="none" stroke="#000000" d="M74.4638,-153C91.6394,-153 117.386,-153 136.5153,-153"/>
<polygon fill="#000000" stroke="#000000" points="143.7478,-153 136.7478,-156.1501 140.2478,-153 136.7478,-153.0001 136.7478,-153.0001 136.7478,-153.0001 140.2478,-153 136.7478,-149.8501 143.7478,-153 143.7478,-153"/>
<text text-anchor="start" x="92" y="-156.8" font-family="Lato" font-size="14.00" fill="#000000">a & b</text>
</g>
<!-- 1 -->
<g id="node4" class="node">
<title>1</title>
<ellipse fill="#ffffaa" stroke="#000000" cx="443" cy="-171" rx="18" ry="18"/>
<text text-anchor="middle" x="443" y="-167.3" font-family="Lato" font-size="14.00" fill="#000000">1</text>
</g>
<!-- 3->1 -->
<g id="edge7" class="edge">
<title>3->1</title>
<path fill="none" stroke="#000000" d="M179.9392,-154.5731C185.7043,-155.0577 192.12,-155.575 198,-156 278.1573,-161.793 373.1747,-167.1913 417.6569,-169.6326"/>
<polygon fill="#000000" stroke="#000000" points="424.8569,-170.0261 417.6954,-172.7893 421.3622,-169.835 417.8674,-169.644 417.8674,-169.644 417.8674,-169.644 421.3622,-169.835 418.0393,-166.4987 424.8569,-170.0261 424.8569,-170.0261"/>
<text text-anchor="start" x="274" y="-167.8" font-family="Lato" font-size="14.00" fill="#000000">g1 & !g2</text>
</g>
<!-- 2 -->
<g id="node5" class="node">
<title>2</title>
<ellipse fill="#ffffaa" stroke="#000000" cx="538" cy="-138" rx="18" ry="18"/>
<text text-anchor="middle" x="538" y="-134.3" font-family="Lato" font-size="14.00" fill="#000000">2</text>
</g>
<!-- 3->2 -->
<g id="edge8" class="edge">
<title>3->2</title>
<path fill="none" stroke="#000000" d="M176.7147,-163.5557C222.0885,-194.7113 363.0998,-281.045 468,-231 497.2167,-217.0615 517.2776,-184.1532 528.2013,-161.4727"/>
<polygon fill="#000000" stroke="#000000" points="531.1692,-155.0832 531.0772,-162.7588 529.6947,-158.2575 528.2203,-161.4318 528.2203,-161.4318 528.2203,-161.4318 529.6947,-158.2575 525.3634,-160.1048 531.1692,-155.0832 531.1692,-155.0832"/>
<text text-anchor="start" x="348" y="-264.8" font-family="Lato" font-size="14.00" fill="#000000">g1 & g2</text>
<text text-anchor="start" x="365" y="-249.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text>
</g>
<!-- 4 -->
<g id="node6" class="node">
<title>4</title>
<ellipse fill="#ffffaa" stroke="#000000" cx="301" cy="-96" rx="18" ry="18"/>
<text text-anchor="middle" x="301" y="-92.3" font-family="Lato" font-size="14.00" fill="#000000">4</text>
</g>
<!-- 3->4 -->
<g id="edge9" class="edge">
<title>3->4</title>
<path fill="none" stroke="#000000" d="M178.7666,-146.1245C203.3959,-136.0247 249.4589,-117.1356 277.4664,-105.6505"/>
<polygon fill="#000000" stroke="#000000" points="284.1739,-102.8999 278.8925,-108.4703 280.9356,-104.2279 277.6973,-105.5558 277.6973,-105.5558 277.6973,-105.5558 280.9356,-104.2279 276.5021,-102.6414 284.1739,-102.8999 284.1739,-102.8999"/>
<text text-anchor="start" x="198" y="-140.8" font-family="Lato" font-size="14.00" fill="#000000">!g1 & !g2</text>
</g>
<!-- 5 -->
<g id="node7" class="node">
<title>5</title>
<ellipse fill="#ffffaa" stroke="#000000" cx="443" cy="-18" rx="18" ry="18"/>
<text text-anchor="middle" x="443" y="-14.3" font-family="Lato" font-size="14.00" fill="#000000">5</text>
</g>
<!-- 3->5 -->
<g id="edge10" class="edge">
<title>3->5</title>
<path fill="none" stroke="#000000" d="M173.2988,-138.6446C191.7355,-116.3621 230.6131,-73.9441 274,-54 321.893,-31.9845 383.658,-23.2308 417.6897,-19.9055"/>
<polygon fill="#000000" stroke="#000000" points="424.9173,-19.2408 418.2353,-23.0187 421.432,-19.5614 417.9467,-19.882 417.9467,-19.882 417.9467,-19.882 421.432,-19.5614 417.6582,-16.7452 424.9173,-19.2408 424.9173,-19.2408"/>
<text text-anchor="start" x="274" y="-57.8" font-family="Lato" font-size="14.00" fill="#000000">!g1 & g2</text>
</g>
<!-- 1->1 -->
<g id="edge4" class="edge">
<title>1->1</title>
<path fill="none" stroke="#000000" d="M434.3666,-186.916C432.1144,-197.1504 434.9922,-207 443,-207 449.131,-207 452.2548,-201.2263 452.3716,-193.9268"/>
<polygon fill="#000000" stroke="#000000" points="451.6334,-186.916 455.4992,-193.5477 452,-190.3968 452.3665,-193.8775 452.3665,-193.8775 452.3665,-193.8775 452,-190.3968 449.2338,-194.2074 451.6334,-186.916 451.6334,-186.916"/>
<text text-anchor="start" x="433" y="-210.8" font-family="Lato" font-size="14.00" fill="#000000">!g2</text>
</g>
<!-- 1->2 -->
<g id="edge5" class="edge">
<title>1->2</title>
<path fill="none" stroke="#000000" d="M460.4245,-164.9473C475.4229,-159.7373 497.2175,-152.1666 513.8893,-146.3753"/>
<polygon fill="#000000" stroke="#000000" points="520.686,-144.0143 515.1072,-149.2869 517.3798,-145.1628 514.0736,-146.3113 514.0736,-146.3113 514.0736,-146.3113 517.3798,-145.1628 513.0399,-143.3358 520.686,-144.0143 520.686,-144.0143"/>
<text text-anchor="start" x="486" y="-173.8" font-family="Lato" font-size="14.00" fill="#000000">g2</text>
<text text-anchor="start" x="486" y="-158.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text>
</g>
<!-- 2->2 -->
<g id="edge6" class="edge">
<title>2->2</title>
<path fill="none" stroke="#000000" d="M530.3321,-154.2903C528.4831,-164.3892 531.0391,-174 538,-174 543.2207,-174 545.9636,-168.5939 546.2287,-161.6304"/>
<polygon fill="#000000" stroke="#000000" points="545.6679,-154.2903 549.3421,-161.0299 545.9346,-157.7801 546.2013,-161.2699 546.2013,-161.2699 546.2013,-161.2699 545.9346,-157.7801 543.0604,-161.5099 545.6679,-154.2903 545.6679,-154.2903"/>
<text text-anchor="start" x="533.5" y="-192.8" font-family="Lato" font-size="14.00" fill="#000000">1</text>
<text text-anchor="start" x="530" y="-177.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text>
</g>
<!-- 4->1 -->
<g id="edge11" class="edge">
<title>4->1</title>
<path fill="none" stroke="#000000" d="M317.0132,-104.4577C342.2613,-117.7929 391.4126,-143.7531 420.2947,-159.0078"/>
<polygon fill="#000000" stroke="#000000" points="426.8275,-162.4582 419.1666,-161.9743 423.7326,-160.8235 420.6378,-159.1889 420.6378,-159.1889 420.6378,-159.1889 423.7326,-160.8235 422.1089,-156.4036 426.8275,-162.4582 426.8275,-162.4582"/>
<text text-anchor="start" x="346" y="-149.8" font-family="Lato" font-size="14.00" fill="#000000">g1 & !g2</text>
</g>
<!-- 4->2 -->
<g id="edge12" class="edge">
<title>4->2</title>
<path fill="none" stroke="#000000" d="M319.2551,-96.638C350.1968,-98.0139 414.7695,-102.1618 468,-114 483.9122,-117.5388 501.2469,-123.4654 514.6851,-128.5435"/>
<polygon fill="#000000" stroke="#000000" points="521.3291,-131.1046 513.6646,-131.526 518.0634,-129.8457 514.7976,-128.5868 514.7976,-128.5868 514.7976,-128.5868 518.0634,-129.8457 515.9306,-125.6476 521.3291,-131.1046 521.3291,-131.1046"/>
<text text-anchor="start" x="418" y="-132.8" font-family="Lato" font-size="14.00" fill="#000000">g1 & g2</text>
<text text-anchor="start" x="435" y="-117.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text>
</g>
<!-- 4->4 -->
<g id="edge13" class="edge">
<title>4->4</title>
<path fill="none" stroke="#000000" d="M289.2435,-110.0417C284.8468,-120.9126 288.7656,-132 301,-132 310.5581,-132 315.0408,-125.2328 314.4481,-117.0885"/>
<polygon fill="#000000" stroke="#000000" points="312.7565,-110.0417 317.4535,-116.1131 313.5735,-113.4451 314.3905,-116.8484 314.3905,-116.8484 314.3905,-116.8484 313.5735,-113.4451 311.3275,-117.5837 312.7565,-110.0417 312.7565,-110.0417"/>
<text text-anchor="start" x="272" y="-135.8" font-family="Lato" font-size="14.00" fill="#000000">!g1 & !g2</text>
</g>
<!-- 4->5 -->
<g id="edge14" class="edge">
<title>4->5</title>
<path fill="none" stroke="#000000" d="M317.6963,-88.518C341.8259,-77.6296 385.1781,-57.763 400,-49 407.7983,-44.3895 415.9572,-38.7411 423.0463,-33.5347"/>
<polygon fill="#000000" stroke="#000000" points="428.7182,-29.2978 424.9954,-36.0107 425.9142,-31.3924 423.1102,-33.4871 423.1102,-33.4871 423.1102,-33.4871 425.9142,-31.3924 421.225,-30.9634 428.7182,-29.2978 428.7182,-29.2978"/>
<text text-anchor="start" x="346" y="-77.8" font-family="Lato" font-size="14.00" fill="#000000">!g1 & g2</text>
</g>
<!-- 5->2 -->
<g id="edge15" class="edge">
<title>5->2</title>
<path fill="none" stroke="#000000" d="M459.0115,-26.6176C471.9743,-34.2492 489.9909,-46.4246 502,-61 514.8573,-76.6048 524.2642,-97.5629 530.231,-113.6739"/>
<polygon fill="#000000" stroke="#000000" points="532.7305,-120.6985 527.4161,-115.1595 531.5572,-117.401 530.3838,-114.1035 530.3838,-114.1035 530.3838,-114.1035 531.5572,-117.401 533.3516,-113.0475 532.7305,-120.6985 532.7305,-120.6985"/>
<text text-anchor="start" x="486" y="-79.8" font-family="Lato" font-size="14.00" fill="#000000">g1</text>
<text text-anchor="start" x="486" y="-64.8" font-family="Lato" font-size="14.00" fill="#1f78b4">⓿</text>
</g>
<!-- 5->5 -->
<g id="edge16" class="edge">
<title>5->5</title>
<path fill="none" stroke="#000000" d="M434.3666,-33.916C432.1144,-44.1504 434.9922,-54 443,-54 449.131,-54 452.2548,-48.2263 452.3716,-40.9268"/>
<polygon fill="#000000" stroke="#000000" points="451.6334,-33.916 455.4992,-40.5477 452,-37.3968 452.3665,-40.8775 452.3665,-40.8775 452.3665,-40.8775 452,-37.3968 449.2338,-41.2074 451.6334,-33.916 451.6334,-33.916"/>
<text text-anchor="start" x="433" y="-57.8" font-family="Lato" font-size="14.00" fill="#000000">!g1</text>
</g>
</g>
</svg>
</div>