alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

python: improve formating of double-quoted AP in MathJax

Browse source 
* python/spot/impl.i: Move the rendering code...
* python/spot/__init__.py: ... here, and ajust it for MathJax.
* tests/python/formulas.ipynb, tests/python/ltsmin-dve.ipynb: Adjust
expected results.
This commit is contained in:
Alexandre Duret-Lutz 2018-05-15 17:27:21 +02:00
parent 965d0ed6b7
commit 36b5b76ca5
4 changed files with 127 additions and 127 deletions
Download patch file Download diff file Expand all files Collapse all files

148
tests/python/formulas.ipynb
View file

@ -163,7 +163,7 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"If you prefer to print the string in another syntax, you may use the `to_str()` method, with an argument that indicates the output format to use. The `latex` format assumes that you will the define macros such as `\\U`, `\\R` to render all operators as you wish. On the otherhand, the `sclatex` (with `sc` for self-contained) format hard-codes the rendering of each of those operators: this is typically the output that is used to render formulas using MathJax in a notebook. "
"If you prefer to print the string in another syntax, you may use the `to_str()` method, with an argument that indicates the output format to use. The `latex` format assumes that you will the define macros such as `\\U`, `\\R` to render all operators as you wish. On the otherhand, the `sclatex` (with `sc` for self-contained) format hard-codes the rendering of each of those operators: this is almost the same output that is used to render formulas using MathJax in a notebook. `sclatex` and `mathjax` only differ in the rendering of double-quoted atomic propositions."
]
},
{
@ -181,12 +181,13 @@
"wring (p1=1) U ((p2=1) R ((p3=1) * (p4=0)))\n",
"utf8 p1 U (p2 R (p3∧¬p4))\n",
"latex p_{1} \\U (p_{2} \\R (p_{3} \\land \\lnot p_{4}))\n",
"sclatex p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n"
"sclatex p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n",
"mathjax p_{1} \\mathbin{\\mathsf{U}} (p_{2} \\mathbin{\\mathsf{R}} (p_{3} \\land \\lnot p_{4}))\n"
]
}
],
"source": [
"for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex']:\n",
"for i in ['spot', 'spin', 'lbt', 'wring', 'utf8', 'latex', 'sclatex', 'mathjax']:\n",
" print(\"%-10s%s\" % (i, f.to_str(i)))"
]
},
@ -262,6 +263,7 @@
" - 'w': use Wring's syntax\n",
" - 'x': use LaTeX output\n",
" - 'X': use self-contained LaTeX output\n",
" - 'j': use self-contained LaTeX output, adjusted for MathJax\n",
" \n",
" Add some of those letters for additional options:\n",
" \n",
@ -417,7 +419,7 @@
{
"data": {
"text/latex": [
"$``\\mathit{a > b}\\textrm{''} \\land ``\\mathit{proc[2]@init}\\textrm{''} \\land \\mathsf{G} \\mathsf{F} \\mathit{\\_foo\\_}$"
"$\\unicode{x201C}\\mathit{a > b}\\unicode{x201D} \\land \\unicode{x201C}\\mathit{proc[2]@init}\\unicode{x201D} \\land \\mathsf{G} \\mathsf{F} \\mathit{\\_foo\\_}$"
],
"text/plain": [
"\"a > b\" & \"proc[2]@init\" & GF_foo_"
@ -503,101 +505,119 @@
"<svg height=\"260pt\" viewBox=\"0.00 0.00 269.00 260.00\" width=\"269pt\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<g class=\"graph\" id=\"graph0\" transform=\"scale(1 1) rotate(0) translate(4 256)\">\n",
"<title>G</title>\n",
"<polygon fill=\"white\" points=\"-4,4 -4,-256 265,-256 265,4 -4,4\" stroke=\"none\"/>\n",
"<polygon fill=\"#ffffff\" points=\"-4,4 -4,-256 265,-256 265,4 -4,4\" stroke=\"transparent\"/>\n",
"<!-- 0 -->\n",
"<g class=\"node\" id=\"node1\"><title>0</title>\n",
"<ellipse cx=\"106\" cy=\"-234\" fill=\"none\" rx=\"40.8928\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"106\" y=\"-230.3\">EConcat</text>\n",
"<g class=\"node\" id=\"node1\">\n",
"<title>0</title>\n",
"<ellipse cx=\"98\" cy=\"-234\" fill=\"none\" rx=\"40.8928\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"98\" y=\"-230.3\">EConcat</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g class=\"node\" id=\"node2\"><title>1</title>\n",
"<ellipse cx=\"155\" cy=\"-162\" fill=\"none\" rx=\"35.9954\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"155\" y=\"-158.3\">Concat</text>\n",
"<g class=\"node\" id=\"node2\">\n",
"<title>1</title>\n",
"<ellipse cx=\"155\" cy=\"-162\" fill=\"none\" rx=\"35.9954\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"155\" y=\"-158.3\">Concat</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;1 -->\n",
"<g class=\"edge\" id=\"edge6\"><title>0-&gt;1</title>\n",
"<path d=\"M117.612,-216.411C123.593,-207.868 131.005,-197.278 137.649,-187.787\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"140.604,-189.669 143.471,-179.47 134.869,-185.655 140.604,-189.669\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"113.112\" y=\"-205.211\">L</text>\n",
"<g class=\"edge\" id=\"edge6\">\n",
"<title>0-&gt;1</title>\n",
"<path d=\"M111.5082,-216.937C118.6068,-207.9703 127.4402,-196.8124 135.288,-186.8993\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"138.1259,-188.9535 141.5888,-178.9405 132.6375,-184.6085 138.1259,-188.9535\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"107.0082\" y=\"-205.737\">L</text>\n",
"</g>\n",
"<!-- 7 -->\n",
"<g class=\"node\" id=\"node8\"><title>7</title>\n",
"<ellipse cx=\"58\" cy=\"-162\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"58\" y=\"-158.3\">G</text>\n",
"<g class=\"node\" id=\"node8\">\n",
"<title>7</title>\n",
"<ellipse cx=\"58\" cy=\"-162\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"58\" y=\"-158.3\">G</text>\n",
"</g>\n",
"<!-- 0&#45;&gt;7 -->\n",
"<g class=\"edge\" id=\"edge9\"><title>0-&gt;7</title>\n",
"<path d=\"M94.6247,-216.411C88.6815,-207.744 81.2945,-196.971 74.7146,-187.375\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"77.5052,-185.256 68.9633,-178.988 71.732,-189.215 77.5052,-185.256\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"89.6247\" y=\"-205.211\">R</text>\n",
"<g class=\"edge\" id=\"edge9\">\n",
"<title>0-&gt;7</title>\n",
"<path d=\"M88.1124,-216.2022C83.3928,-207.7071 77.6537,-197.3767 72.4568,-188.0223\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"75.4145,-186.139 67.4985,-179.0972 69.2954,-189.5386 75.4145,-186.139\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"83.1124\" y=\"-205.0022\">R</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g class=\"node\" id=\"node3\"><title>2</title>\n",
"<polygon fill=\"none\" points=\"261,-36 207,-36 207,-0 261,-0 261,-36\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"234\" y=\"-14.3\">a</text>\n",
"<g class=\"node\" id=\"node3\">\n",
"<title>2</title>\n",
"<polygon fill=\"none\" points=\"261,-36 207,-36 207,0 261,0 261,-36\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"234\" y=\"-14.3\">a</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g class=\"edge\" id=\"edge1\"><title>1-&gt;2</title>\n",
"<path d=\"M173.171,-146.485C184.356,-136.683 198.19,-122.858 207,-108 218.359,-88.8432 225.316,-64.4933 229.316,-46.1073\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"232.797,-46.5497 231.341,-36.0554 225.935,-45.1672 232.797,-46.5497\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"169.671\" y=\"-135.285\">1</text>\n",
"<g class=\"edge\" id=\"edge1\">\n",
"<title>1-&gt;2</title>\n",
"<path d=\"M173.9318,-146.4771C184.9807,-136.5145 198.3956,-122.7193 207,-108 218.2008,-88.8391 225.1222,-64.624 229.1492,-46.139\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"232.5946,-46.7593 231.1469,-36.2639 225.7336,-45.3713 232.5946,-46.7593\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"170.4318\" y=\"-135.2771\">1</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g class=\"node\" id=\"node4\"><title>3</title>\n",
"<ellipse cx=\"99\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"99\" y=\"-86.3\">Star</text>\n",
"<g class=\"node\" id=\"node4\">\n",
"<title>3</title>\n",
"<ellipse cx=\"99\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"99\" y=\"-86.3\">Star</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;3 -->\n",
"<g class=\"edge\" id=\"edge3\"><title>1-&gt;3</title>\n",
"<path d=\"M142.293,-145.116C135.032,-136.04 125.792,-124.49 117.715,-114.393\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"120.252,-111.962 111.272,-106.34 114.786,-116.335 120.252,-111.962\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"138.793\" y=\"-133.916\">2</text>\n",
"<g class=\"edge\" id=\"edge3\">\n",
"<title>1-&gt;3</title>\n",
"<path d=\"M141.7288,-144.937C134.6536,-135.8403 125.8244,-124.4886 118.0315,-114.4691\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"120.6927,-112.1897 111.7905,-106.4449 115.1672,-116.4873 120.6927,-112.1897\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"138.2288\" y=\"-133.737\">2</text>\n",
"</g>\n",
"<!-- 5 -->\n",
"<g class=\"node\" id=\"node6\"><title>5</title>\n",
"<ellipse cx=\"171\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"171\" y=\"-86.3\">Star</text>\n",
"<g class=\"node\" id=\"node6\">\n",
"<title>5</title>\n",
"<ellipse cx=\"171\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"171\" y=\"-86.3\">Star</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;5 -->\n",
"<g class=\"edge\" id=\"edge5\"><title>1-&gt;5</title>\n",
"<path d=\"M158.873,-144.055C160.655,-136.261 162.812,-126.822 164.811,-118.079\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"168.235,-118.804 167.051,-108.275 161.411,-117.244 168.235,-118.804\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"155.373\" y=\"-132.855\">3</text>\n",
"<g class=\"edge\" id=\"edge5\">\n",
"<title>1-&gt;5</title>\n",
"<path d=\"M159.0375,-143.8314C160.7941,-135.9266 162.8917,-126.4872 164.8363,-117.7365\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"168.2665,-118.4346 167.0192,-107.9134 161.4332,-116.916 168.2665,-118.4346\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"155.5375\" y=\"-132.6314\">3</text>\n",
"</g>\n",
"<!-- 4 -->\n",
"<g class=\"node\" id=\"node5\"><title>4</title>\n",
"<polygon fill=\"none\" points=\"81,-36 27,-36 27,-0 81,-0 81,-36\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"54\" y=\"-14.3\">b</text>\n",
"<g class=\"node\" id=\"node5\">\n",
"<title>4</title>\n",
"<polygon fill=\"none\" points=\"90,-36 36,-36 36,0 90,0 90,-36\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"63\" y=\"-14.3\">b</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge2\"><title>3-&gt;4</title>\n",
"<path d=\"M88.7888,-73.1159C83.4437,-64.8013 76.7639,-54.4105 70.6903,-44.9627\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"73.4681,-42.8113 65.1164,-36.2921 67.5799,-46.5966 73.4681,-42.8113\" stroke=\"black\"/>\n",
"<g class=\"edge\" id=\"edge2\">\n",
"<title>3-&gt;4</title>\n",
"<path d=\"M90.2854,-72.5708C86.1772,-64.3544 81.1804,-54.3608 76.5911,-45.1821\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"79.613,-43.3996 72.0103,-36.0206 73.352,-46.5301 79.613,-43.3996\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 6 -->\n",
"<g class=\"node\" id=\"node7\"><title>6</title>\n",
"<polygon fill=\"none\" points=\"189,-36 135,-36 135,-0 189,-0 189,-36\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"162\" y=\"-14.3\">c</text>\n",
"<g class=\"node\" id=\"node7\">\n",
"<title>6</title>\n",
"<polygon fill=\"none\" points=\"189,-36 135,-36 135,0 189,0 189,-36\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"162\" y=\"-14.3\">c</text>\n",
"</g>\n",
"<!-- 5&#45;&gt;6 -->\n",
"<g class=\"edge\" id=\"edge4\"><title>5-&gt;6</title>\n",
"<path d=\"M168.821,-72.055C167.83,-64.3456 166.632,-55.0269 165.518,-46.3642\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"168.968,-45.7473 164.221,-36.2753 162.025,-46.64 168.968,-45.7473\" stroke=\"black\"/>\n",
"<g class=\"edge\" id=\"edge4\">\n",
"<title>5-&gt;6</title>\n",
"<path d=\"M168.7289,-71.8314C167.7664,-64.131 166.6218,-54.9743 165.5521,-46.4166\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"169.0151,-45.9019 164.3017,-36.4133 162.0691,-46.7702 169.0151,-45.9019\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 8 -->\n",
"<g class=\"node\" id=\"node9\"><title>8</title>\n",
"<ellipse cx=\"27\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"black\"/>\n",
"<text font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"27\" y=\"-86.3\">F</text>\n",
"<g class=\"node\" id=\"node9\">\n",
"<title>8</title>\n",
"<ellipse cx=\"27\" cy=\"-90\" fill=\"none\" rx=\"27\" ry=\"18\" stroke=\"#000000\"/>\n",
"<text fill=\"#000000\" font-family=\"Times,serif\" font-size=\"14.00\" text-anchor=\"middle\" x=\"27\" y=\"-86.3\">F</text>\n",
"</g>\n",
"<!-- 7&#45;&gt;8 -->\n",
"<g class=\"edge\" id=\"edge8\"><title>7-&gt;8</title>\n",
"<path d=\"M50.6534,-144.411C46.9858,-136.129 42.4667,-125.925 38.3646,-116.662\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"41.5434,-115.196 34.2938,-107.47 35.1429,-118.031 41.5434,-115.196\" stroke=\"black\"/>\n",
"<g class=\"edge\" id=\"edge8\">\n",
"<title>7-&gt;8</title>\n",
"<path d=\"M50.4958,-144.5708C46.905,-136.2309 42.5258,-126.0598 38.5254,-116.7686\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"41.7119,-115.319 34.5426,-107.5182 35.2825,-118.0872 41.7119,-115.319\" stroke=\"#000000\"/>\n",
"</g>\n",
"<!-- 8&#45;&gt;4 -->\n",
"<g class=\"edge\" id=\"edge7\"><title>8-&gt;4</title>\n",
"<path d=\"M33.3986,-72.411C36.4351,-64.5386 40.1417,-54.9289 43.5695,-46.0421\" fill=\"none\" stroke=\"black\"/>\n",
"<polygon fill=\"black\" points=\"46.9373,-47.0364 47.2705,-36.4468 40.4062,-44.5172 46.9373,-47.0364\" stroke=\"black\"/>\n",
"<g class=\"edge\" id=\"edge7\">\n",
"<title>8-&gt;4</title>\n",
"<path d=\"M35.7146,-72.5708C39.8228,-64.3544 44.8196,-54.3608 49.4089,-45.1821\" fill=\"none\" stroke=\"#000000\"/>\n",
"<polygon fill=\"#000000\" points=\"52.648,-46.5301 53.9897,-36.0206 46.387,-43.3996 52.648,-46.5301\" stroke=\"#000000\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"