Skip to content
GitLab
Commit 798ed3f1 authored by dgelessus's avatar dgelessus
Browse files

Re-execute all notebooks using current kernel

parent d2d85b8b
Pipeline #78025 passed with stage
in 1 minute and 36 seconds
Expand all Hide whitespace changes
Inline Side-by-side
notebooks/experiments/DeliveryExercise.ipynb
View file @ 798ed3f1
......@@ -83,7 +83,7 @@
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
"Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
......
%% Cell type:markdown id: tags:
# Exercice Sheet: B Expressions
You are given a B machine with three given sets:
* a set ```S``` of online shops
* a set ```A``` of articles that can be ordered
* a set ```C``` of clients
You are also given two relations:
* a relation ```delivers:S<->A``` describing which shops can deliver which articles
* a relation ```orders:C<->POW(A)``` describing current outstanding orders, an order consisting of a set of articles.
%% Cell type:code id: tags:
``` prob
::load
MACHINE exercise1
DEFINITIONS "LibraryHash.def"
SETS
S = {s1,s2,s3,s4,s5} /* Shops */ ;
A = {a1,a2,a3,a4,a5} /* Articles that can be ordered */;
C = {c1,c2,c3} /* Clients */
CONSTANTS delivers, orders
PROPERTIES
delivers = {s1↦a1,s1↦a2, s2↦a4, s3↦a3, s3↦a2, s4↦a4, s4↦a5} &
orders = {c1 ↦ {a1,a5}, c1 ↦ {a4}, c2 ↦ {a1,a3,a5}, c3 ↦ {a2,a3}, c3 ↦ {a1}}
END
```
%%%% Output: execute_result
Loaded machine: exercise1
%% Cell type:code id: tags:
``` prob
:constants
```
%%%% Output: execute_result
Machine constants set up using operation 0: $setup_constants()
Executed operation: SETUP_CONSTANTS()
%% Cell type:markdown id: tags:
The above machine also contains particular instantiations of the above sets and relations, which will be used in the exercises below.
%% Cell type:markdown id: tags:
## Exercise 1
Write a B expression to compute the set of clients that have ordered article a5. Use the ```:let sol1 EXPRESSION``` in the cell below.
%% Cell type:code id: tags:
``` prob
:let sol1 {c| a5 : union(orders[{c}])}
```
%%%% Output: execute_result
$\{\mathit{c1},\mathit{c2}\}$
{c1,c2}
%% Cell type:code id: tags:
``` prob
:assert SHA_HASH_HEX(sol1) = "26365f212fb4cbe0ef2adc9eb42d3c6fac15442b"
```
%%%% Output: execute_result
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
## Exercise 2
Write a B expression which computes the set of all articles ordered by at least one client. Use the ```:let sol2 EXPRESSION``` in the cell below.
%% Cell type:code id: tags:
``` prob
:let sol2 union(ran(orders))
```
%%%% Output: execute_result
$\{\mathit{a1},\mathit{a2},\mathit{a3},\mathit{a4},\mathit{a5}\}$
{a1,a2,a3,a4,a5}
%% Cell type:code id: tags:
``` prob
SHA_HASH_HEX(sol2)
```
%%%% Output: execute_result
$\text{"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3"}$
"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3"
%% Cell type:code id: tags:
``` prob
:assert SHA_HASH_HEX(sol2) = "29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3"
```
%%%% Output: execute_result
$\mathit{TRUE}$
TRUE
%% Cell type:markdown id: tags:
# Comments:
To lock cells you can do this:
* menu: view → cell toolbar → edit metadata.
* make this like
```
{
"trusted": true,
"editable": false,
"deletable": false
}
```
......
notebooks/experiments/SMT_Translation_Experiments.ipynb
View file @ 798ed3f1
This diff is collapsed.
This diff is collapsed.
notebooks/manual/ExternalFunctions.ipynb
View file @ 798ed3f1
......@@ -1879,7 +1879,7 @@
"text/markdown": [
"|stringify|tostring|\n",
"|---|---|\n",
"|$\\text{\"\\\"abc\\\"\"}$|$\\text{\"abc\"}$|\n"
"|\"\\\"abc\\\"\"|\"abc\"|\n"
],
"text/plain": [
"stringify\ttostring\n",
......@@ -2391,78 +2391,78 @@
"<?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.40.1 (20161225.0304)\n",
"<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: state Pages: 1 -->\n",
"<svg width=\"176pt\" height=\"131pt\"\n",
" viewBox=\"0.00 0.00 176.00 131.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 127)\">\n",
"<title>state</title>\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-127 172,-127 172,4 -4,4\"/>\n",
"<!-- 4 -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>4</title>\n",
"<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"54,-123 0,-123 0,-87 54,-87 54,-123\"/>\n",
"<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
"<text text-anchor=\"middle\" x=\"27\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- 3 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>3</title>\n",
"<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"73,-36 19,-36 19,0 73,0 73,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"46\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">3</text>\n",
"<text text-anchor=\"middle\" x=\"46\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">3</text>\n",
"</g>\n",
"<!-- 4&#45;&gt;3 -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>4&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#b22222\" d=\"M13.9658,-86.8601C8.5525,-77.0267 4.4709,-64.7259 9,-54 10.4817,-50.491 12.4912,-47.1549 14.8124,-44.0309\"/>\n",
"<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"17.6245,-46.1306 21.5364,-36.2844 12.3382,-41.542 17.6245,-46.1306\"/>\n",
"<text text-anchor=\"middle\" x=\"16.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M14.23,-86.67C8.69,-76.96 4.4,-64.68 9,-54 10.57,-50.36 12.72,-46.92 15.21,-43.72\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"17.81,-46.06 21.93,-36.3 12.62,-41.36 17.81,-46.06\"/>\n",
"<text text-anchor=\"middle\" x=\"16.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 3&#45;&gt;4 -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>3&#45;&gt;4</title>\n",
"<path fill=\"none\" stroke=\"#b22222\" d=\"M42.0682,-36.0034C39.4963,-47.7801 36.0828,-63.4102 33.1552,-76.8156\"/>\n",
"<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"29.6511,-76.457 30.9368,-86.9735 36.4899,-77.9506 29.6511,-76.457\"/>\n",
"<text text-anchor=\"middle\" x=\"45.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M42.16,-36.18C39.56,-47.81 36.07,-63.42 33.09,-76.73\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"29.61,-76.28 30.84,-86.8 36.44,-77.8 29.61,-76.28\"/>\n",
"<text text-anchor=\"middle\" x=\"45.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>2</title>\n",
"<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"149,-123 95,-123 95,-87 149,-87 149,-123\"/>\n",
"<text text-anchor=\"middle\" x=\"122\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">2</text>\n",
"<text text-anchor=\"middle\" x=\"122\" y=\"-101.3\" font-family=\"Times,serif\" font-size=\"14.00\">2</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;3 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>2&#45;&gt;3</title>\n",
"<path fill=\"none\" stroke=\"#b22222\" d=\"M106.2528,-86.9735C95.3492,-74.4919 80.6716,-57.6899 68.533,-43.7944\"/>\n",
"<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"70.9419,-41.2319 61.7271,-36.0034 65.6701,-45.8371 70.9419,-41.2319\"/>\n",
"<text text-anchor=\"middle\" x=\"95.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M106.62,-86.8C95.6,-74.47 80.58,-57.68 68.25,-43.89\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"70.63,-41.3 61.36,-36.18 65.41,-45.96 70.63,-41.3\"/>\n",
"<text text-anchor=\"middle\" x=\"95.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 1 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>1</title>\n",
"<polygon fill=\"#cdba96\" stroke=\"#cdba96\" points=\"168,-36 114,-36 114,0 168,0 168,-36\"/>\n",
"<text text-anchor=\"middle\" x=\"141\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">1</text>\n",
"<text text-anchor=\"middle\" x=\"141\" y=\"-14.3\" font-family=\"Times,serif\" font-size=\"14.00\">1</text>\n",
"</g>\n",
"<!-- 2&#45;&gt;1 -->\n",
"<g id=\"edge4\" class=\"edge\">\n",
"<title>2&#45;&gt;1</title>\n",
"<path fill=\"none\" stroke=\"#b22222\" d=\"M120.4276,-86.8094C120.0556,-76.961 120.3724,-64.6623 123,-54 123.7054,-51.1377 124.6671,-48.2411 125.7816,-45.3993\"/>\n",
"<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"129.0662,-46.6305 130.0081,-36.0776 122.6909,-43.7398 129.0662,-46.6305\"/>\n",
"<text text-anchor=\"middle\" x=\"130.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M120.44,-86.62C120.04,-76.88 120.32,-64.61 123,-54 123.72,-51.14 124.71,-48.26 125.86,-45.43\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"129.12,-46.72 130.2,-36.18 122.78,-43.75 129.12,-46.72\"/>\n",
"<text text-anchor=\"middle\" x=\"130.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"<!-- 1&#45;&gt;2 -->\n",
"<g id=\"edge5\" class=\"edge\">\n",
"<title>1&#45;&gt;2</title>\n",
"<path fill=\"none\" stroke=\"#b22222\" d=\"M141.502,-36.171C141.3832,-46.0136 140.5982,-58.3131 138,-69 137.3184,-71.8037 136.4269,-74.6611 135.4132,-77.4782\"/>\n",
"<polygon fill=\"#b22222\" stroke=\"#b22222\" points=\"132.1613,-76.1836 131.6235,-86.7648 138.6425,-78.8284 132.1613,-76.1836\"/>\n",
"<text text-anchor=\"middle\" x=\"147.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">rel</text>\n",
"<path fill=\"none\" stroke=\"firebrick\" d=\"M141.52,-36.36C141.42,-46.09 140.65,-58.37 138,-69 137.33,-71.7 136.45,-74.45 135.45,-77.16\"/>\n",
"<polygon fill=\"firebrick\" stroke=\"firebrick\" points=\"132.11,-76.08 131.46,-86.65 138.56,-78.8 132.11,-76.08\"/>\n",
"<text text-anchor=\"middle\" x=\"147.5\" y=\"-57.8\" font-family=\"Times,serif\" font-size=\"14.00\">rel</text>\n",
"</g>\n",
"</g>\n",
"</svg>"
"</svg>\n"
],
"text/plain": [
"<Dot visualization: expr_as_graph [(\"rel\",{(1,2),(2,1),(2,3),(3,4),(4,3)})]>"
"<Dot visualization: expr_as_graph [(\"rel\",{1|->2,2|->1,2|->3,3|->4,4|->3})]>"
]
},
"execution_count": 87,
......@@ -2550,10 +2550,10 @@
{
"data": {
"text/markdown": [
"$\\text{\"1.9.3-nightly\"}$"
"$\\text{\"1.11.1-final\"}$"
],
"text/plain": [
"\"1.9.3-nightly\""
"\"1.11.1-final\""
]
},
"execution_count": 90,
......@@ -2573,10 +2573,10 @@
{
"data": {
"text/markdown": [
"$\\text{\"50333f1779dcae2a9e6d1b2aa95a23678821f851\"}$"
"$\\text{\"1125ea39af78125a39093c65a0af783b7636b362\"}$"
],
"text/plain": [
"\"50333f1779dcae2a9e6d1b2aa95a23678821f851\""
"\"1125ea39af78125a39093c65a0af783b7636b362\""
]
},
"execution_count": 91,
......@@ -2596,10 +2596,10 @@
{
"data": {
"text/markdown": [
"$\\text{\"Mon Feb 17 13:18:47 2020 +0100\"}$"
"$\\text{\"Wed Dec 29 13:14:39 2021 +0100\"}$"
],
"text/plain": [
"\"Mon Feb 17 13:18:47 2020 +0100\""
"\"Wed Dec 29 13:14:39 2021 +0100\""
]
},
"execution_count": 92,
......@@ -2619,10 +2619,10 @@
{
"data": {
"text/markdown": [
"$\\text{\"1.8.0_202-b08\"}$"
"$\\text{\"1.17.35\\\"\\n\"}$"
],
"text/plain": [
"\"1.8.0_202-b08\""
"\"1.17.35\\\"\\n\""
]
},
"execution_count": 93,
......@@ -2642,10 +2642,10 @@
{
"data": {
"text/markdown": [
"$\\text{\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\"}$"
"$\\text{\"/Library/Java/JavaVirtualMachines/temurin-17.jdk/Contents/Home/bin/java\"}$"
],
"text/plain": [
"\"/Library/Java/JavaVirtualMachines/jdk1.8.0_202.jdk/Contents/Home/bin/java\""
"\"/Library/Java/JavaVirtualMachines/temurin-17.jdk/Contents/Home/bin/java\""
]
},
"execution_count": 94,
......@@ -2665,10 +2665,10 @@
{
"data": {
"text/markdown": [
"$\\text{\"18/2/2020 - 15h29 52s\"}$"
"$\\text{\"6/1/2022 - 13h37 50s\"}$"
],
"text/plain": [
"\"18/2/2020 - 15h29 52s\""
"\"6/1/2022 - 13h37 50s\""
]
},
"execution_count": 95,
......@@ -2704,10 +2704,10 @@
{
"data": {
"text/markdown": [
"$151477456$"
"$166651936$"
],
"text/plain": [
"151477456"
"166651936"
]
},
"execution_count": 96,
......@@ -2819,10 +2819,10 @@
{
"data": {
"text/markdown": [
"$1582036192$"
"$1641472670$"
],
"text/plain": [
"1582036192"
"1641472670"
]
},
"execution_count": 101,
......@@ -2842,10 +2842,10 @@
{
"data": {
"text/markdown": [
"$1658$"
"$2295$"
],
"text/plain": [
"1658"
"2295"
]
},
"execution_count": 102,
......@@ -2865,10 +2865,10 @@
{
"data": {
"text/markdown": [
"$2881$"
"$18724$"
],
"text/plain": [
"2881"
"18724"
]
},
"execution_count": 103,
......@@ -3268,10 +3268,10 @@
{
"data": {
"text/markdown": [
"$\\{\\text{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}\\}$"
"$\\{\\text{\"9541282a9b1c250d7244201817fbc6f332a22940\"}\\}$"
],
"text/plain": [
"{\"86ff5ffb3ecd6cc4b17b13a797508440fa2faa4c\"}"
"{\"9541282a9b1c250d7244201817fbc6f332a22940\"}"
]
},
"execution_count": 119,
......@@ -3405,7 +3405,7 @@
{
"data": {
"text/markdown": [
"$\\{(1\\mapsto \\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"version\"}\\mapsto\\text{\"0.1\"})\\},\\mathit{element}\\in\\text{\"Data\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"3\"})\\},\\mathit{pId}\\in 0,\\mathit{recId}\\in 1)),(2\\mapsto \\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"attr1\"}\\mapsto\\text{\"value1\"}),(\\text{\"elemID\"}\\mapsto\\text{\"ID1\"})\\},\\mathit{element}\\in\\text{\"Tag1\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"4\"})\\},\\mathit{pId}\\in 1,\\mathit{recId}\\in 2))\\}$"
"$\\{(1\\mapsto\\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"version\"}\\mapsto\\text{\"0.1\"})\\},\\mathit{element}\\in\\text{\"Data\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"3\"})\\},\\mathit{pId}\\in 0,\\mathit{recId}\\in 1)),(2\\mapsto\\mathit{rec}(\\mathit{attributes}\\in\\{(\\text{\"attr1\"}\\mapsto\\text{\"value1\"}),(\\text{\"elemID\"}\\mapsto\\text{\"ID1\"})\\},\\mathit{element}\\in\\text{\"Tag1\"},\\mathit{meta}\\in\\{(\\text{\"xmlLineNumber\"}\\mapsto\\text{\"4\"})\\},\\mathit{pId}\\in 1,\\mathit{recId}\\in 2))\\}$"
],
"text/plain": [
"{(1↦rec(attributes∈{(\"version\"↦\"0.1\")},element∈\"Data\",meta∈{(\"xmlLineNumber\"↦\"3\")},pId∈0,recId∈1)),(2↦rec(attributes∈{(\"attr1\"↦\"value1\"),(\"elemID\"↦\"ID1\")},element∈\"Tag1\",meta∈{(\"xmlLineNumber\"↦\"4\")},pId∈1,recId∈2))}"
......@@ -5044,13 +5044,13 @@
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":eval: NOT-WELL-DEFINED: \n### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\n ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\n ### Line: 28, Column: 1 until 88\n ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\n\n",
"evalue": ":eval: UNKNOWN: \n### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\n ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\n ### Line: 34, Column: 1 until 88\n ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\n\n",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
"\u001b[1m\u001b[31m:eval: UNKNOWN: \u001b[0m",
"\u001b[1m\u001b[31m### Exception occurred while calling external function: 'REGEX_SEARCH':regex_exception('One of *?+{ was not preceded by a valid regular expression.')\u001b[0m",
"\u001b[1m\u001b[31m ### File: /Users/Shared/Uni/SHK/ProB2/prob_prolog/stdlib/LibraryRegex.def\u001b[0m",
"\u001b[1m\u001b[31m ### Line: 28, Column: 1 until 88\u001b[0m",
"\u001b[1m\u001b[31m ### Line: 34, Column: 1 until 88\u001b[0m",
"\u001b[1m\u001b[31m ### within: DEFINITION call of REGEX_SEARCH at Line: 1 Column: 0 until Line: 1 Column: 54\u001b[0m"
]
}
......@@ -5507,10 +5507,13 @@
"outputs": [
{
"ename": "CommandExecutionException",
"evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
"evalue": ":eval: NOT-WELL-DEFINED: \narg not positive x > 0\n ### Line: 1, Column: 27 until 30\n ### within: DEFINITION call of ASSERT_EXPR at Line: 1 Column: 10 until Line: 1 Column: 56\n\n",
"output_type": "error",
"traceback": [
"\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
"\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
"\u001b[1m\u001b[31marg not positive x > 0\u001b[0m",
"\u001b[1m\u001b[31m ### Line: 1, Column: 27 until 30\u001b[0m",
"\u001b[1m\u001b[31m ### within: DEFINITION call of ASSERT_EXPR at Line: 1 Column: 10 until Line: 1 Column: 56\u001b[0m"
]
}
],
......@@ -5606,8 +5609,13 @@
{
"data": {
"text/plain": [
"ProB CLI: 1.9.3-nightly (50333f1779dcae2a9e6d1b2aa95a23678821f851)\n",
"ProB 2: 4.0.0-SNAPSHOT (1d61b6ea7ef1b2e38a6b6045dbb0e81bcb6d8423)"
"ProB 2 Jupyter kernel: 1.2.1-SNAPSHOT (2aaa99bab781d6eca5a2b3388cca76b412fd52f6)\n",
"ProB 2: 3.15.0 (6ee6df4eab62d20df40c36cd42108b62962ec41b)\n",
"ProB B parser: 2.9.32 (7306d13499ba281a6e336c006d9fb23204624daa)\n",
"ProB CLI:\n",
"\t1.11.1-final (1125ea39af78125a39093c65a0af783b7636b362)\n",
"\tLast changed: Wed Dec 29 13:14:39 2021 +0100\n",
"\tProlog: SICStus 4.7.0 (x86_64-darwin-18.7.0): Wed Jul 7 17:07:32 CEST 2021"
]
},
"execution_count": 194,
......
notebooks/models/Jars_DieHard_Puzzle.ipynb
View file @ 798ed3f1
......@@ -86,7 +86,7 @@
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
"Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
......@@ -106,7 +106,7 @@
{
"data": {
"text/plain": [
"Machine initialised using operation 1: $initialise_machine()"
"Executed operation: INITIALISATION()"
]
},
"execution_count": 3,
......@@ -654,63 +654,63 @@
"<?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.40.1 (20161225.0304)\n",
"<!-- Generated by graphviz version 2.50.0 (20211204.2007)\n",
" -->\n",
"<!-- Title: g Pages: 1 -->\n",
"<svg width=\"304pt\" height=\"110pt\"\n",
" viewBox=\"0.00 0.00 304.00 110.00\" xmlns=\"http://www.w3.org/2000/svg\" xmlns:xlink=\"http://www.w3.org/1999/xlink\">\n",
"<svg width=\"303pt\" height=\"110pt\"\n",
" viewBox=\"0.00 0.00 303.00 110.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 106)\">\n",
"<title>g</title>\n",
"<polygon fill=\"#ffffff\" stroke=\"transparent\" points=\"-4,4 -4,-106 300,-106 300,4 -4,4\"/>\n",
"<polygon fill=\"white\" stroke=\"transparent\" points=\"-4,4 -4,-106 299,-106 299,4 -4,4\"/>\n",
"<!-- Noderoot -->\n",
"<g id=\"node1\" class=\"node\">\n",
"<title>Noderoot</title>\n",
"<path fill=\"#b3ee3a\" stroke=\"#000000\" d=\"M42,-72.5C42,-72.5 12,-72.5 12,-72.5 6,-72.5 0,-66.5 0,-60.5 0,-60.5 0,-46.5 0,-46.5 0,-40.5 6,-34.5 12,-34.5 12,-34.5 42,-34.5 42,-34.5 48,-34.5 54,-40.5 54,-46.5 54,-46.5 54,-60.5 54,-60.5 54,-66.5 48,-72.5 42,-72.5\"/>\n",
"<text text-anchor=\"middle\" x=\"27\" y=\"-57.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">∈</text>\n",
"<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">true</text>\n",
"<path fill=\"#b3ee3a\" stroke=\"black\" d=\"M42,-72.5C42,-72.5 12,-72.5 12,-72.5 6,-72.5 0,-66.5 0,-60.5 0,-60.5 0,-46.5 0,-46.5 0,-40.5 6,-34.5 12,-34.5 12,-34.5 42,-34.5 42,-34.5 48,-34.5 54,-40.5 54,-46.5 54,-46.5 54,-60.5 54,-60.5 54,-66.5 48,-72.5 42,-72.5\"/>\n",
"<text text-anchor=\"middle\" x=\"27\" y=\"-57.3\" font-family=\"Times,serif\" font-size=\"14.00\">∈</text>\n",
"<text text-anchor=\"middle\" x=\"27\" y=\"-42.3\" font-family=\"Times,serif\" font-size=\"14.00\">true</text>\n",
"</g>\n",
"<!-- Node1 -->\n",
"<g id=\"node2\" class=\"node\">\n",
"<title>Node1</title>\n",
"<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-65.5 90,-101.5 144,-101.5 144,-65.5 90,-65.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-79.8\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">4</text>\n",
"<polygon fill=\"white\" stroke=\"black\" points=\"90,-65.5 90,-101.5 144,-101.5 144,-65.5 90,-65.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-79.8\" font-family=\"Times,serif\" font-size=\"14.00\">4</text>\n",
"</g>\n",
"<!-- Node1&#45;&gt;Noderoot -->\n",
"<g id=\"edge1\" class=\"edge\">\n",
"<title>Node1&#45;&gt;Noderoot</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-74.499C81.796,-71.7653 72.6401,-68.7134 63.905,-65.8017\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"64.8886,-62.4403 54.295,-62.5983 62.675,-69.0811 64.8886,-62.4403\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M89.6,-74.5C81.43,-71.72 72.3,-68.6 63.62,-65.64\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"64.68,-62.31 54.08,-62.39 62.42,-68.93 64.68,-62.31\"/>\n",
"</g>\n",
"<!-- Node2 -->\n",
"<g id=\"node3\" class=\"node\">\n",
"<title>Node2</title>\n",
"<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"90,-.5 90,-46.5 144,-46.5 144,-.5 90,-.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">ran</text>\n",
"<polyline fill=\"none\" stroke=\"#000000\" points=\"90,-23.5 144,-23.5 \"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{3,4}</text>\n",
"<polygon fill=\"white\" stroke=\"black\" points=\"90,-0.5 90,-46.5 144,-46.5 144,-0.5 90,-0.5\"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">ran</text>\n",
"<polyline fill=\"none\" stroke=\"black\" points=\"90,-23.5 144,-23.5 \"/>\n",
"<text text-anchor=\"middle\" x=\"117\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">{3,4}</text>\n",
"</g>\n",
"<!-- Node2&#45;&gt;Noderoot -->\n",
"<g id=\"edge2\" class=\"edge\">\n",
"<title>Node2&#45;&gt;Noderoot</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M89.997,-32.501C81.796,-35.2347 72.6401,-38.2866 63.905,-41.1983\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"62.675,-37.9189 54.295,-44.4017 64.8886,-44.5597 62.675,-37.9189\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M89.6,-32.5C81.43,-35.28 72.3,-38.4 63.62,-41.36\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"62.42,-38.07 54.08,-44.61 64.68,-44.69 62.42,-38.07\"/>\n",
"</g>\n",
"<!-- Node3 -->\n",
"<g id=\"node4\" class=\"node\">\n",
"<title>Node3</title>\n",
"<polygon fill=\"#ffffff\" stroke=\"#000000\" points=\"180,-.5 180,-46.5 296,-46.5 296,-.5 180,-.5\"/>\n",
"<text text-anchor=\"middle\" x=\"238\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">level</text>\n",
"<polyline fill=\"none\" stroke=\"#000000\" points=\"180,-23.5 296,-23.5 \"/>\n",
"<text text-anchor=\"middle\" x=\"238\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\" fill=\"#000000\">{(j3↦3),(j5↦4)}</text>\n",
"<polygon fill=\"white\" stroke=\"black\" points=\"180,-0.5 180,-46.5 295,-46.5 295,-0.5 180,-0.5\"/>\n",
"<text text-anchor=\"middle\" x=\"237.5\" y=\"-31.3\" font-family=\"Times,serif\" font-size=\"14.00\">level</text>\n",
"<polyline fill=\"none\" stroke=\"black\" points=\"180,-23.5 295,-23.5 \"/>\n",
"<text text-anchor=\"middle\" x=\"237.5\" y=\"-8.3\" font-family=\"Times,serif\" font-size=\"14.00\">{(j3↦3),(j5↦4)}</text>\n",
"</g>\n",
"<!-- Node3&#45;&gt;Node2 -->\n",
"<g id=\"edge3\" class=\"edge\">\n",
"<title>Node3&#45;&gt;Node2</title>\n",
"<path fill=\"none\" stroke=\"#000000\" d=\"M179.9808,-23.5C171.2934,-23.5 162.5376,-23.5 154.4316,-23.5\"/>\n",
"<polygon fill=\"#000000\" stroke=\"#000000\" points=\"154.2102,-20.0001 144.2101,-23.5 154.2101,-27.0001 154.2102,-20.0001\"/>\n",
"<path fill=\"none\" stroke=\"black\" d=\"M179.68,-23.5C171.01,-23.5 162.26,-23.5 154.2,-23.5\"/>\n",
"<polygon fill=\"black\" stroke=\"black\" points=\"154.04,-20 144.04,-23.5 154.04,-27 154.04,-20\"/>\n",
"</g>\n",
"</g>\n",
"</svg>"
"</svg>\n"
],
"text/plain": [
"<Dot visualization: goal []>"
......
%% Cell type:markdown id: tags:
## Jars
This is the B model of a puzzle from the movie "Die Hard with a Vengeance":
https://www.youtube.com/watch?v=BVtQNK_ZUJg
http://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm
Input:
* one 3 gallon and one 5 gallon jug
* and we need to measure precisely 4 gallons
We can
* empty a jug,
* completely fill any jug and
* transfer water from one jug to another until either the destination jug is full or the source jug is empty.
Here is a generic B model with three operations ```FillJar```, ```EmptyJar``` and ```Transfer```.
It hase one variable ```level``` for the current level of the jars.
The constant ```maxf``` defines for each jar the maximum fill level in gallons.
%% Cell type:code id: tags:
``` prob
::load
MACHINE Jars
DEFINITIONS
GOAL == (4:ran(level));
ANIMATION_IMG1 == "images/Filled.gif";
ANIMATION_IMG2 == "images/Empty.gif";
ANIMATION_IMG3 == "images/Void.gif";
gmax == max(ran(maxf));
ANIMATION_FUNCTION_DEFAULT == {r,c,i | c:Jars & r:1..gmax & i=3};
ri == (gmax+1-r);
ANIMATION_FUNCTION == {r,c,i | c:Jars & ri:1..maxf(c) &
(ri<=level(c) => i=1 ) & (ri>level(c) => i=2)};
SETS
Jars = {j3,j5}
CONSTANTS maxf
PROPERTIES maxf : Jars --> NATURAL &
maxf = {j3 |-> 3, j5 |-> 5} /* in this puzzle we have two jars, with capacities 3 and 5 */
VARIABLES level
INVARIANT
level: Jars --> NATURAL
INITIALISATION level := Jars * {0} /* all jars start out empty */
OPERATIONS
FillJar(j) = /* we can completely fill a jar j */
PRE j:Jars & level(j)<maxf(j) THEN
level(j) := maxf(j)
END;
EmptyJar(j) = /* we can completely empty a jar j */
PRE j:Jars & level(j)>0 THEN
level(j) := 0
END;
Transfer(j1,amount,j2) = /* we can transfer from jar j1 to j2 until either j2 is full or j1 is empty */
PRE j1:Jars & j2:Jars & j1 /= j2 & amount>0 &
amount = min({level(j1), maxf(j2)-level(j2)}) THEN
level := level <+ { j1|-> level(j1)-amount, j2 |-> level(j2)+amount }
END
END
```
%%%% Output: execute_result
Loaded machine: Jars
%% Cell type:code id: tags:
``` prob
:constants
```
%%%% Output: execute_result
Machine constants set up using operation 0: $setup_constants()
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags:
``` prob
:init
```
%%%% Output: execute_result
Machine initialised using operation 1: $initialise_machine()
Executed operation: INITIALISATION()
%% Cell type:markdown id: tags:
We start off with all jars being empty:
%% Cell type:code id: tags:
``` prob
level
```
%%%% Output: execute_result
$\{(\mathit{j3}\mapsto 0),(\mathit{j5}\mapsto 0)\}$
{(j3↦0),(j5↦0)}
%% Cell type:markdown id: tags:
We now fill the 5 gallon jar using the operation FillJar with parameter j:
%% Cell type:code id: tags:
``` prob
:exec FillJar j=j5
```
%%%% Output: execute_result
Executed operation: FillJar(j5)
%% Cell type:markdown id: tags:
This jar is now full:
%% Cell type:code id: tags:
``` prob
level
```
%%%% Output: execute_result
$\{(\mathit{j3}\mapsto 0),(\mathit{j5}\mapsto 5)\}$
{(j3↦0),(j5↦5)}
%% Cell type:markdown id: tags:
We can inspect the state graphically using the defined ANIMATION_FUNCTION:
%% Cell type:code id: tags:
``` prob
:show
```
%%%% Output: execute_result
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
We now transfer water to the empty jar until it is filled using the operation FillJar with parameters j1, amount and j2:
%% Cell type:code id: tags:
``` prob
:exec Transfer (j1=j5 & amount=3 & j2=j3)
```
%%%% Output: execute_result
Executed operation: Transfer(j5,3,j3)
%% Cell type:code id: tags:
``` prob
level
```
%%%% Output: execute_result
$\{(\mathit{j3}\mapsto 3),(\mathit{j5}\mapsto 2)\}$
{(j3↦3),(j5↦2)}
%% Cell type:code id: tags:
``` prob
:show
```
%%%% Output: execute_result
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
We now empty the three gallon jar using the operation EmptyJar with parameter j:
%% Cell type:code id: tags:
``` prob
:exec EmptyJar j=j3
```
%%%% Output: execute_result
Executed operation: EmptyJar(j3)
%% Cell type:code id: tags:
``` prob
:show
```
%%%% Output: execute_result
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Transfer (j1=j5 & amount=2 & j2=j3)
```
%%%% Output: execute_result
Executed operation: Transfer(j5,2,j3)
%% Cell type:code id: tags:
``` prob
:show
```
%%%% Output: execute_result
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec FillJar j=j5
```
%%%% Output: execute_result
Executed operation: FillJar(j5)
%% Cell type:code id: tags:
``` prob
:show
```
%%%% Output: execute_result
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:code id: tags:
``` prob
:exec Transfer j1=j5 & amount=1 & j2=j3
```
%%%% Output: execute_result
Executed operation: Transfer(j5,1,j3)
%% Cell type:code id: tags:
``` prob
:show
```
%%%% Output: execute_result
<table style="font-family:monospace"><tbody>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="2" src="images/Empty.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="3" src="images/Void.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
<tr>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
<td style="padding:0px"><img alt="1" src="images/Filled.gif"/></td>
</tr>
</tbody></table>
<Animation function visualisation>
%% Cell type:markdown id: tags:
The puzzle has now been solve, the goal predicate has become true:
%% Cell type:code id: tags:
``` prob
GOAL
```
%%%% Output: execute_result
$\mathit{TRUE}$
TRUE
%% Cell type:code id: tags:
``` prob
:dot goal
```
%%%% Output: execute_result
<Dot visualization: goal []>
......
notebooks/models/NFA_to_DFA.ipynb
View file @ 798ed3f1
This diff is collapsed.
This diff is collapsed.
notebooks/models/NQueens_Puzzle.ipynb
View file @ 798ed3f1
......@@ -65,7 +65,7 @@
{
"data": {
"text/plain": [
"Machine constants set up using operation 0: $setup_constants()"
"Executed operation: SETUP_CONSTANTS()"
]
},
"execution_count": 2,
......@@ -85,7 +85,7 @@
{
"data": {
"text/plain": [
"Machine initialised using operation 1: $initialise_machine()"
"Executed operation: INITIALISATION()"
]
},
"execution_count": 3,
......@@ -1067,13 +1067,6 @@
"source": [
":show"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
......
%% Cell type:markdown id: tags:
## N-Queens Puzzle
The N-Queens is a famous constraint solving benchmark puzzle.
It is a generalisation of the original eight queens puzzle, where the goal is to place eight queens on a 8*8 chessboard so that no two queens attach each other.
We now write a B machine with constants
* n: the size of the chess board
* queens: a partial function from 1..n to 1..n, stating in which row the queen on any given column is placed
%% Cell type:code id: tags:
``` prob
::load
MACHINE Queens
CONSTANTS n, queens
PROPERTIES
n>0 & n<120 &
queens : (1..n) +-> (1..n)
DEFINITIONS
ANIMATION_FUNCTION_DEFAULT == ( {r,c,i|r:1..n & c:1..n & i=(r+c) mod 2 } );
ANIMATION_FUNCTION == ( {r,c,i|c:1..n & c|->r:queens & i=2+((r+c) mod 2) } );
ANIMATION_IMG0 == "images/ChessPieces/Chess_emptyl45.gif";
ANIMATION_IMG1 == "images/ChessPieces/Chess_emptyd45.gif";
ANIMATION_IMG2 == "images/ChessPieces/Chess_qll45.gif";
ANIMATION_IMG3 == "images/ChessPieces/Chess_qld45.gif";
no_attack(q1,q2,board) == no_attack_pos(q1,board(q1),q2,board(q2));
no_attack_pos(q1,q1row,q2,q2row) == (q1row+q2-q1 /= q2row & q1row-q2+q1 /= q2row);
Solution(board) == (
board : perm(1..n) /* for each column the row in which the queen is in */
&
!(q1,q2).(q1:1..n & q2:2..n & q2>q1 => no_attack(q1,q2,board) )
)
END
```
%%%% Output: execute_result
Loaded machine: Queens
%% Cell type:code id: tags:
``` prob
:constants
```
%%%% Output: execute_result
Machine constants set up using operation 0: $setup_constants()
Executed operation: SETUP_CONSTANTS()
%% Cell type:code id: tags:
``` prob
:init
```
%%%% Output: execute_result
Machine initialised using operation 1: $initialise_machine()
Executed operation: INITIALISATION()
%% Cell type:markdown id: tags:
In the PROPERTIES we have not stated any constraint of our puzzle. Hence the default solution is n=1 and an empty board:
%% Cell type:code id: tags:
``` prob
(queens,n)
```
%%%% Output: execute_result
$\renewcommand{\emptyset}{\mathord\varnothing}(\emptyset\mapsto 1)$
(∅↦1)
%% Cell type:markdown id: tags:
Let us now slowly tighten the constraints. We can use the ```:find``` command to find
states which satisfy the PROPERTIES and some additional predicate.
Let us first require that every queen is really placed.
We also impose an 8 by 8 board.
%% Cell type:code id: tags:
``` prob
:find queens : 1..8 --> 1..8
```
%%%% Output: execute_result
Found a matching state and made it current state