atva16-fig2a.ipynb 11.7 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
{
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
18
   "version": "3.5.4"
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
  },
  "name": ""
 },
 "nbformat": 3,
 "nbformat_minor": 0,
 "worksheets": [
  {
   "cells": [
    {
     "cell_type": "markdown",
     "metadata": {},
     "source": [
      "This example is the left part of Fig.2 in our ATVA'16 paper titled \"*Spot 2.0 \u2014 a framework for LTL and \u03c9-automata manipulation*\"."
     ]
    },
    {
     "cell_type": "code",
     "collapsed": true,
     "input": [
      "import spot\n",
      "spot.setup(show_default='.abr')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 1
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f = spot.formula('GFa <-> GFb'); f"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "latex": [
        "$\\mathsf{G} \\mathsf{F} a \\leftrightarrow \\mathsf{G} \\mathsf{F} b$"
       ],
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 2,
       "text": [
        "GFa <-> GFb"
       ]
      }
     ],
     "prompt_number": 2
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "f.translate()"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 3,
       "svg": [
        "<?xml version=\"1.0\" encoding=\"UTF-8\" standalone=\"no\"?>\n",
        "<!DOCTYPE svg PUBLIC \"-//W3C//DTD SVG 1.1//EN\"\n",
        " \"http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd\">\n",
        "<!-- Generated by graphviz version 2.38.0 (20140413.2041)\n",
        " -->\n",
        "<!-- Title: G Pages: 1 -->\n",
89
90
91
        "<svg width=\"198pt\" height=\"355pt\"\n",
        " viewBox=\"0.00 0.00 197.50 355.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
        "<g id=\"graph0\" class=\"graph\" transform=\"scale(1 1) rotate(0) translate(4 351)\">\n",
92
        "<title>G</title>\n",
93
94
95
96
97
98
99
        "<polygon fill=\"white\" stroke=\"none\" points=\"-4,4 -4,-351 193.5,-351 193.5,4 -4,4\"/>\n",
        "<text text-anchor=\"start\" x=\"47.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\">Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"69.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"85.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\">)&amp;Inf(</text>\n",
        "<text text-anchor=\"start\" x=\"121.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
        "<text text-anchor=\"start\" x=\"137.75\" y=\"-332.8\" font-family=\"Lato\" font-size=\"14.00\">)</text>\n",
        "<text text-anchor=\"start\" x=\"50.75\" y=\"-318.8\" font-family=\"Lato\" font-size=\"14.00\">[gen. B\u00fcchi 2]</text>\n",
100
        "<!-- I -->\n",
101
102
103
104
        "<!-- 0 -->\n",
        "<g id=\"node2\" class=\"node\"><title>0</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"56\" cy=\"-75\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"56\" y=\"-71.3\" font-family=\"Lato\" font-size=\"14.00\">0</text>\n",
105
        "</g>\n",
106
107
108
109
        "<!-- I&#45;&gt;0 -->\n",
        "<g id=\"edge1\" class=\"edge\"><title>I&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M1.15491,-75C2.79388,-75 17.1543,-75 30.6317,-75\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"37.9419,-75 30.9419,-78.1501 34.4419,-75 30.9419,-75.0001 30.9419,-75.0001 30.9419,-75.0001 34.4419,-75 30.9418,-71.8501 37.9419,-75 37.9419,-75\"/>\n",
110
        "</g>\n",
111
112
113
114
115
        "<!-- 0&#45;&gt;0 -->\n",
        "<g id=\"edge2\" class=\"edge\"><title>0&#45;&gt;0</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M49.6208,-92.0373C48.3189,-101.858 50.4453,-111 56,-111 60.166,-111 62.4036,-105.858 62.7128,-99.1433\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"62.3792,-92.0373 65.8541,-98.8818 62.5434,-95.5335 62.7076,-99.0296 62.7076,-99.0296 62.7076,-99.0296 62.5434,-95.5335 59.561,-99.1774 62.3792,-92.0373 62.3792,-92.0373\"/>\n",
        "<text text-anchor=\"start\" x=\"51.5\" y=\"-114.8\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
116
        "</g>\n",
117
118
119
120
        "<!-- 1 -->\n",
        "<g id=\"node3\" class=\"node\"><title>1</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"169\" cy=\"-118\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"start\" x=\"164.5\" y=\"-114.3\" font-family=\"Lato\" font-size=\"14.00\">1</text>\n",
121
        "</g>\n",
122
123
124
125
126
        "<!-- 0&#45;&gt;1 -->\n",
        "<g id=\"edge3\" class=\"edge\"><title>0&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M73.3784,-81.3448C92.4242,-88.7229 123.976,-100.946 145.359,-109.229\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"151.915,-111.769 144.25,-112.178 148.652,-110.505 145.388,-109.24 145.388,-109.24 145.388,-109.24 148.652,-110.505 146.526,-106.303 151.915,-111.769 151.915,-111.769\"/>\n",
        "<text text-anchor=\"start\" x=\"99\" y=\"-107.8\" font-family=\"Lato\" font-size=\"14.00\">a | b</text>\n",
127
        "</g>\n",
128
129
130
131
132
        "<!-- 2 -->\n",
        "<g id=\"node4\" class=\"node\"><title>2</title>\n",
        "<ellipse fill=\"#ffffaa\" stroke=\"black\" cx=\"169\" cy=\"-18\" rx=\"18\" ry=\"18\"/>\n",
        "<text text-anchor=\"middle\" x=\"169\" y=\"-14.3\" font-family=\"Lato\" font-size=\"14.00\">2</text>\n",
        "</g>\n",
133
134
135
136
137
        "<!-- 0&#45;&gt;2 -->\n",
        "<g id=\"edge4\" class=\"edge\"><title>0&#45;&gt;2</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M72.4341,-67.0744C91.6528,-57.2053 124.596,-40.2883 146.337,-29.1242\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"152.697,-25.8583 147.909,-31.8581 149.584,-27.4571 146.47,-29.056 146.47,-29.056 146.47,-29.056 149.584,-27.4571 145.031,-26.2538 152.697,-25.8583 152.697,-25.8583\"/>\n",
        "<text text-anchor=\"start\" x=\"92\" y=\"-59.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
138
        "</g>\n",
139
140
141
142
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge5\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M166.467,-136.153C166.078,-145.539 166.922,-154 169,-154 170.526,-154 171.387,-149.437 171.582,-143.295\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"171.533,-136.153 174.731,-143.131 171.557,-139.653 171.581,-143.153 171.581,-143.153 171.581,-143.153 171.557,-139.653 168.431,-143.174 171.533,-136.153 171.533,-136.153\"/>\n",
143
        "<text text-anchor=\"start\" x=\"148.5\" y=\"-157.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
144
        "</g>\n",
145
146
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge6\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
147
148
149
150
        "<path fill=\"none\" stroke=\"black\" d=\"M164.828,-135.699C162.523,-152.996 163.914,-172 169,-172 173.371,-172 175.012,-157.965 173.925,-143.04\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"173.172,-135.699 177.02,-142.341 173.529,-139.181 173.886,-142.663 173.886,-142.663 173.886,-142.663 173.529,-139.181 170.753,-142.984 173.172,-135.699 173.172,-135.699\"/>\n",
        "<text text-anchor=\"start\" x=\"150.5\" y=\"-190.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; b</text>\n",
        "<text text-anchor=\"start\" x=\"161\" y=\"-175.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
151
        "</g>\n",
152
153
154
155
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge7\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
        "<path fill=\"none\" stroke=\"black\" d=\"M164.049,-135.467C158.901,-163.149 160.551,-202 169,-202 176.756,-202 178.783,-169.261 175.081,-142.477\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"173.951,-135.467 178.174,-141.877 174.508,-138.923 175.065,-142.378 175.065,-142.378 175.065,-142.378 174.508,-138.923 171.955,-142.879 173.951,-135.467 173.951,-135.467\"/>\n",
156
157
        "<text text-anchor=\"start\" x=\"150.5\" y=\"-220.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; !b</text>\n",
        "<text text-anchor=\"start\" x=\"161\" y=\"-205.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
158
        "</g>\n",
159
160
        "<!-- 1&#45;&gt;1 -->\n",
        "<g id=\"edge8\" class=\"edge\"><title>1&#45;&gt;1</title>\n",
161
162
163
164
165
        "<path fill=\"none\" stroke=\"black\" d=\"M163.519,-135.237C155.333,-171.922 157.16,-232 169,-232 180.1,-232 182.399,-179.197 175.898,-142.369\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"174.481,-135.237 178.935,-141.488 175.163,-138.669 175.845,-142.102 175.845,-142.102 175.845,-142.102 175.163,-138.669 172.756,-142.716 174.481,-135.237 174.481,-135.237\"/>\n",
        "<text text-anchor=\"start\" x=\"152\" y=\"-249.8\" font-family=\"Lato\" font-size=\"14.00\">a &amp; b</text>\n",
        "<text text-anchor=\"start\" x=\"153\" y=\"-235.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"169\" y=\"-235.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
166
167
168
        "</g>\n",
        "<!-- 2&#45;&gt;2 -->\n",
        "<g id=\"edge9\" class=\"edge\"><title>2&#45;&gt;2</title>\n",
169
170
171
        "<path fill=\"none\" stroke=\"black\" d=\"M159.425,-33.5414C156.73,-43.9087 159.922,-54 169,-54 175.95,-54 179.45,-48.0847 179.499,-40.6591\"/>\n",
        "<polygon fill=\"black\" stroke=\"black\" points=\"178.575,-33.5414 182.6,-40.0771 179.026,-37.0123 179.477,-40.4831 179.477,-40.4831 179.477,-40.4831 179.026,-37.0123 176.353,-40.889 178.575,-33.5414 178.575,-33.5414\"/>\n",
        "<text text-anchor=\"start\" x=\"148.5\" y=\"-71.8\" font-family=\"Lato\" font-size=\"14.00\">!a &amp; !b</text>\n",
172
173
        "<text text-anchor=\"start\" x=\"153\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#1f78b4\">\u24ff</text>\n",
        "<text text-anchor=\"start\" x=\"169\" y=\"-57.8\" font-family=\"Lato\" font-size=\"14.00\" fill=\"#ff4da0\">\u2776</text>\n",
174
175
176
177
178
        "</g>\n",
        "</g>\n",
        "</svg>\n"
       ],
       "text": [
179
        "<spot.impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7f0d2406cc00> >"
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
       ]
      }
     ],
     "prompt_number": 3
    },
    {
     "cell_type": "code",
     "collapsed": true,
     "input": [
      "def implies(f, g):\n",
      "    f = spot.formula(f)\n",
      "    g = spot.formula_Not(spot.formula(g))\n",
      "    return spot.product(f.translate(), g.translate()).is_empty()\n",
      "def equiv(f, g):\n",
      "    return implies(f, g) and implies(g, f)"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [],
     "prompt_number": 4
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "equiv('a U (b U a)', 'b U a')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 5,
       "text": [
        "True"
       ]
      }
     ],
     "prompt_number": 5
    },
    {
     "cell_type": "code",
     "collapsed": false,
     "input": [
      "equiv('!(a U b)', '!a U !b')"
     ],
     "language": "python",
     "metadata": {},
     "outputs": [
      {
       "metadata": {},
       "output_type": "pyout",
       "prompt_number": 6,
       "text": [
        "False"
       ]
      }
     ],
     "prompt_number": 6
    }
   ],
   "metadata": {}
  }
 ]
}