forked from glaserL/viasp
-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
ab22e5a
commit ad781c3
Showing
2 changed files
with
189 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,186 @@ | ||
{ | ||
"cells": [ | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": {}, | ||
"source": [ | ||
"# <center>Introduction to viASP</center>\n", | ||
"\n", | ||
"\n", | ||
"viASP is a visualization and interactive explanation tool for ASP programs and their stable models.\n", | ||
"\n", | ||
"viASP allows you to explore the visualization in a variety of ways:\n", | ||
"\n", | ||
"* Visualize the derivation of stable models step-by-step in a tree view\n", | ||
"* Inspect iterations of recursive rules individually\n", | ||
"* Show reasons for the derivation of individual symbols with arrows\n", | ||
"* Relax the constraints of unsatisfiable programs\n", | ||
"* Inspect single models\n", | ||
"* Add `#show` statements on the fly\n", | ||
"* Search models, signatures and rules.\n", | ||
"\n", | ||
"![Example visualization](../docs/img/sprinkler.png)\n", | ||
"\n", | ||
"To get started, the startup module starts the viASP server:" | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": null, | ||
"metadata": {}, | ||
"outputs": [], | ||
"source": [ | ||
"colors = {\n", | ||
" # node border colors\n", | ||
" \"ten\": {\"dark\": \"#3FA7D1\"}, \n", | ||
" # row background (arbitrary number and names)\n", | ||
" \"twenty\": { \"dark\": \"#a9a9a94a\", \"bright\": \"#ffffff\"},\n", | ||
" # text color of node, detail sidebar, row header (dark) and detail sidebar atoms (bright)\n", | ||
" \"thirty\": {\"dark\": \"#444\", \"bright\": \"#F6F4F3\"},\n", | ||
" # recursive node supernode background (dark) and border (bright)\n", | ||
" \"fourty\": { \"0\": \"#3FA7D1\", \"1\": \"#3FA7D1\"},\n", | ||
" # detail sidebar atom background (dark) and border (bright)\n", | ||
" \"fifty\": { \"dark\": \"#3FA7D1\"},\n", | ||
" # background color of node, detail sidebar, row header\n", | ||
" \"sixty\": {\"dark\": \"#F6F4F3\"},\n", | ||
" # edge color (dark) and edge to clingraph color (bright)\n", | ||
" \"seventy\": { \"dark\": \"#000000\", \"bright\": \"#000000\"},\n", | ||
" # arbitrary number of colors to highlight explanations\n", | ||
" \"highlight\": { \"0\": \"#d48521\", \"1\": \"#9a8298\", \"2\": \"#e0e4ac\", \"3\": \"#98f4e2\", \"4\": \"#21d485\"}, \n", | ||
" # currently not used\n", | ||
" \"error\": {\"ten\": \"#EB4A4E\", \"thirty\": \"#4C191A\", \"sixty\": \"#FCE8E8\"},\n", | ||
" \"warn\": {\"ten\": \"#FF9800\", \"thirty\": \"#653300\", \"sixty\": \"#FFF1DF\"}}" | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": null, | ||
"metadata": {}, | ||
"outputs": [], | ||
"source": [ | ||
"from viasp.server import startup\n", | ||
"app = startup.run(colors=colors)\n", | ||
"# if this cell encounters an error in binder, restart the kernel and run it again" | ||
] | ||
}, | ||
{ | ||
"cell_type": "markdown", | ||
"metadata": {}, | ||
"source": [ | ||
"Defining an encoding." | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": null, | ||
"metadata": {}, | ||
"outputs": [], | ||
"source": [ | ||
"%%file sprinkler.lp\n", | ||
"1{rain;sprinkler}1.\n", | ||
"wet :- rain.\n", | ||
"wet :- sprinkler." | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": null, | ||
"metadata": {}, | ||
"outputs": [], | ||
"source": [ | ||
"%%file hamiltonian.lp\n", | ||
"\n", | ||
"node(1..4). start(1).\n", | ||
"edge(1,2). edge(2,3). edge(2,4). edge(3,1).\n", | ||
"edge(3,4). edge(4,1). edge(4,3).\n", | ||
"\n", | ||
"{ hc(V,U) } :- edge(V,U).\n", | ||
"reached(V) :- hc(S,V), start(S).\n", | ||
"reached(V) :- reached(U), hc(U,V).\n", | ||
":- node(V), not reached(V).\n", | ||
":- hc(V,U), hc(V,W), U!=W.\n", | ||
":- hc(U,V), hc(W,V), U!=W.\n", | ||
"% :- hc(V,U), hc(W,V), U!=W. % uncomment to make the program unsatisfiable & comment the line above\n" | ||
] | ||
}, | ||
{ | ||
"cell_type": "code", | ||
"execution_count": null, | ||
"metadata": {}, | ||
"outputs": [], | ||
"source": [ | ||
"from viasp import Control\n", | ||
"\n", | ||
"options = ['0']\n", | ||
"programs = ['sprinkler.lp']\n", | ||
"ctl = Control(options)\n", | ||
"for path in programs:\n", | ||
" ctl.load(path)\n", | ||
"ctl.ground([(\"base\", [])])\n", | ||
"\n", | ||
"with ctl.solve(yield_=True) as handle:\n", | ||
" for m in handle:\n", | ||
" print(\"Answer:\\n{}\".format(m))\n", | ||
" ctl.viasp.mark(m) # mark the answer set for visualization\n", | ||
" print(handle.get())\n", | ||
"ctl.viasp.show() # start the graph generation\n", | ||
"app.run() # run the Dash app" | ||
] | ||
} | ||
], | ||
"metadata": { | ||
"kernelspec": { | ||
"display_name": "Python 3 (ipykernel)", | ||
"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", | ||
"version": "3.10.4" | ||
}, | ||
"varInspector": { | ||
"cols": { | ||
"lenName": 16, | ||
"lenType": 16, | ||
"lenVar": 40 | ||
}, | ||
"kernels_config": { | ||
"python": { | ||
"delete_cmd_postfix": "", | ||
"delete_cmd_prefix": "del ", | ||
"library": "var_list.py", | ||
"varRefreshCmd": "print(var_dic_list())" | ||
}, | ||
"r": { | ||
"delete_cmd_postfix": ") ", | ||
"delete_cmd_prefix": "rm(", | ||
"library": "var_list.r", | ||
"varRefreshCmd": "cat(var_dic_list()) " | ||
} | ||
}, | ||
"types_to_exclude": [ | ||
"module", | ||
"function", | ||
"builtin_function_or_method", | ||
"instance", | ||
"_Feature" | ||
], | ||
"window_display": false | ||
}, | ||
"vscode": { | ||
"interpreter": { | ||
"hash": "1785f8d9ecd06a5253af1fb2e0a107be454014433d34b629cfe3c91c9b2ab96a" | ||
} | ||
} | ||
}, | ||
"nbformat": 4, | ||
"nbformat_minor": 2 | ||
} |