diff --git a/Apples_and_Oranges.ipynb b/Apples_and_Oranges.ipynb
index ec626b68a2dc350381ed0e35c6d7874c43fe7f5a..569681cfc701e7a1c9ed22016fc0dd8f45385613 100644
--- a/Apples_and_Oranges.ipynb
+++ b/Apples_and_Oranges.ipynb
@@ -9,7 +9,7 @@
"Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
"\n",
"This puzzle is [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from\n",
- "[1](https://bgr.com/2015/11/20/apple-interview-questions/) we have the\n",
+ "[here](https://bgr.com/2015/11/20/apple-interview-questions/) we have the\n",
"following information:\n",
"\n",
"* (1) There are three boxes, one contains only apples, one contains only oranges, and one contains both apples and oranges.\n",
@@ -264,27 +264,6 @@
"source": [
":table DecisionFunction"
]
- },
- {
- "cell_type": "markdown",
- "metadata": {},
- "source": [
- "## Argumentation Theory\n",
- "\n",
- "\n",
- "\n",
- "Below we try to model some concepts of argumentation theory in B. The examples try to show that classical (monotonic) logic with set theory can be used to model some aspects of argumentation theory quite naturally, and that ProB can solve and visualise some problems in argumentation theory. Alternative solutions are encoding arguments as normal logic programs (with non-monotonic negation) and using answer set solvers for problem solving.\n",
- "\n",
- "The following model was inspired by a talk given by Claudia Schulz.\n",
- "\n",
- "The model below represents the labelling of the arguments as a total function from arguments to its status, which can either be in (the argument is accepted), out (the argument is rejected), or undec (the argument is undecided). The relation between the arguments is given in the binary attacks relation.\n",
- "\n",
- "In case you are new to B, you probably need to know the following operators to understand the specification below (we als have a summary page about the B syntax in our handbook):\n",
- "\n",
- "* `x : S` specifies that x is an element of S\n",
- "* `a|→b` represents the pair (a,b); note that a relation and function in B is a set of pairs.\n",
- "* "
- ]
}
],
"metadata": {
diff --git a/Die_Hard_Jugs.ipynb b/Die_Hard_Jugs.ipynb
index a6a4c704a746895e8961488bf55880fa0acc986d..a36f7b74f92eb4532f7fe56f694199335f7073d7 100644
--- a/Die_Hard_Jugs.ipynb
+++ b/Die_Hard_Jugs.ipynb
@@ -6,6 +6,8 @@
"source": [
"# Die Hard Jugs Puzzle\n",
"\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
+ "\n",
"This is the B model of a puzzle from the movie \"Die Hard with a Vengeance\". [This clip](https://www.youtube.com/watch?v=BVtQNK_ZUJg) shows Bruce Willis and Samuel Jackson having a go at the puzzle. A more detailed explanation can be found [here](https://www.math.tamu.edu/~dallen/hollywood/diehard/diehard.htm). \n",
"At start we have one 3 gallon and one 5 gallon jug, and we need to measure precisely 4 gallons by filling, emptying or transferring water from the jugs."
]
diff --git a/Euler_Problem.ipynb b/Euler_Problem.ipynb
index 60433c7cc65c5b6fcef247c497bf3c255d06b4e7..5363dd5e63ddcbe6fa5210ae9b32817df20c7bcf 100644
--- a/Euler_Problem.ipynb
+++ b/Euler_Problem.ipynb
@@ -6,6 +6,8 @@
"source": [
"# Euler Problem 67 - Maximum Path Sum II\n",
"\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
+ "\n",
"In the following we will give a solution for the Euler Problem 67. For convenience, the description of the problem can be found on the official site for the [Euler Problem 67](https://projecteuler.net/problem=67).\n",
"\n",
"By starting at the top of the triangle below and moving to adjacent numbers on the row below, the maximum total from top to bottom is 23.\n",
diff --git a/Fibonacci_Numbers.ipynb b/Fibonacci_Numbers.ipynb
index a20c1c7bf573c436990d703164a5e4eac3e8f1c8..80985758ac2f086d5e539c82103ebf1b9e0f1ce2 100644
--- a/Fibonacci_Numbers.ipynb
+++ b/Fibonacci_Numbers.ipynb
@@ -6,11 +6,11 @@
"source": [
"# Fibonacci Numbers with Automatic Dynamic Programming\n",
"\n",
- "In this jupyter notebook, we show you how to encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding.\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
"\n",
- "First of all we have to load the machine, if you are struggeling with any operation of our jupyter kernel, try out `:help` or take a look at our `ProB Jupyter Noteboook Overview`.\n",
+ "In this jupyter notebook, we show you how to encode the Fibonacci problem in such a way that you get dynamic programming automatically when using ProB to solve the encoding.\n",
"\n",
- "After loading the machine, we are setting up the constants with `:constants` and initialising it with `:init`.\n",
+ "After loading the machine as seen below, we are setting up the constants with `:constants` and initialising it with `:init`.\n",
"\n",
"Now you can ask the machine for the solution of the `n`th fibonacci number by typing in `sol`."
]
diff --git a/Game_of_Life.ipynb b/Game_of_Life.ipynb
index 0fa9ee89dec082d642c0d5e2d23e41103d2e201f..bc2e776c58e2253f0e891dcd51f3643d0a158612 100644
--- a/Game_of_Life.ipynb
+++ b/Game_of_Life.ipynb
@@ -6,6 +6,8 @@
"source": [
"# Game of Life\n",
"\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
+ "\n",
"This is an improved model of Conway’s Game of Life. It was written for animation with ProB. One interesting aspect is that the simulation is unbounded, i.e., not restricted to some pre-determined area of the grid. In this notebook we will examine the following machine and animate it.\n",
"\n",
"To see all the specifications for Conway's Game of Life, click [here](https://en.wikipedia.org/wiki/Conway's_Game_of_Life)."
diff --git a/Gilbreath_Card_Trick.ipynb b/Gilbreath_Card_Trick.ipynb
index 88f29eb99c09416e2a5be7091e2b487a4aefb1e1..d9752f5b787a3e822b9dffd8357def71623022a6 100644
--- a/Gilbreath_Card_Trick.ipynb
+++ b/Gilbreath_Card_Trick.ipynb
@@ -6,6 +6,8 @@
"source": [
"# Gilbreath Card Trick\n",
"\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
+ "\n",
"A while ago a member of the research group that created ProB and ProB2 stumbled across a short article [Unraveling a Card Trick](https://link.springer.com/chapter/10.1007%2F978-3-642-13754-9_10) by Tony Hoare and Natarajan Shankar in the Dagstuhl library. In memory of Amir Pnueli they decided to model the problem as described in the article.\n",
"\n",
"The article unravels a card trick by Gilbreath that has several phases:\n",
diff --git a/N-Bishops.ipynb b/N-Bishops.ipynb
index fd2c351875fdb87761c954ef0cf2bb2f662075af..91639d1de53772442dccbb1fdfec9fe681e38a9c 100644
--- a/N-Bishops.ipynb
+++ b/N-Bishops.ipynb
@@ -6,6 +6,7 @@
"source": [
"# N-Bishops Puzzle\n",
"\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
"\n",
"This puzzle is a variation of the N-Queens puzzle. You can find the N-Queens puzzle in our modeling examples as well. In this puzzle we try to place as many bishops as possible on a n by n chess board. In contrast to the N-Queens puzzle, one can place more than one bishop per row. As such, we can now longer represent the positions of the bishops as an total function `1..n >-> 1..n`. \n",
"\n",
diff --git a/Peaceable_Armies_of_Queens.ipynb b/Peaceable_Armies_of_Queens.ipynb
index cb5709d33cbee483b97b8494802110b33bf58800..ea71b7f0af91dfa0e0f8a633d459175a1280afde 100644
--- a/Peaceable_Armies_of_Queens.ipynb
+++ b/Peaceable_Armies_of_Queens.ipynb
@@ -6,6 +6,8 @@
"source": [
"# Peaceable Armies of Queens\n",
"\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
+ "\n",
"The paper [Models and symmetry breaking for 'peaceable armies of queens'](https://link.springer.com/chapter/10.1007/978-3-540-24664-0_19) by Smith, Petrie and Gent describes a challenging constraint programming problem. \n",
"A variation of the problem can be found on page 329 of the [Handbook on Constraint Programming](https://www.elsevier.com/books/handbook-of-constraint-programming/rossi/978-0-444-52726-4).\n",
"\n",
@@ -664,115 +666,6 @@
":show"
]
},
- {
- "cell_type": "code",
- "execution_count": 22,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use `:load` to load an external machine file.\n",
- "\n",
- "You can also use any of the following commands. For more help on a particular command, run `:help commandname`.\n",
- "\n",
- "## Evaluation\n",
- "\n",
- "* `:eval` - Evaluate a formula and display the result.\n",
- "* `:solve` - Solve a predicate with the specified solver.\n",
- "* `:table` - Display an expression as a table.\n",
- "* `:type` - Display the static type of a formula.\n",
- "* `:prettyprint` - Pretty-print a predicate.\n",
- "* `:let` - Evaluate an expression and store it in a local variable.\n",
- "* `:unlet` - Remove a local variable.\n",
- "* `:assert` - Ensure that the predicate is true, and show an error otherwise.\n",
- "\n",
- "## Animation\n",
- "\n",
- "* `::load` - Load a B machine from the given source code.\n",
- "* `:load` - Load a machine from a file.\n",
- "* `:constants` - Set up the current machine's constants.\n",
- "* `:init` - Initialise the current machine with the specified predicate\n",
- "* `:exec` - Execute an operation.\n",
- "* `:browse` - Show information about the current state.\n",
- "* `:trace` - Display all states and executed operations in the current trace.\n",
- "* `:goto` - Go to the state with the specified index in the current trace.\n",
- "* `:find` - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
- "\n",
- "## Visualisation\n",
- "\n",
- "* `:show` - Show the machine's animation function visualisation for the current state.\n",
- "* `:dot` - Execute and show a dot visualisation.\n",
- "\n",
- "## Verification\n",
- "\n",
- "* `:check` - Check the machine's properties, invariant, or assertions in the current state.\n",
- "* `:modelcheck` - Run the ProB model checker on the current model.\n",
- "\n",
- "## Other\n",
- "\n",
- "* `::render` - Render some content with the specified MIME type.\n",
- "* `:bsymb` - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
- "* `:groovy` - Evaluate the given Groovy expression.\n",
- "* `:help` - Display help for a specific command, or general help about the REPL.\n",
- "* `:pref` - View or change the value of one or more preferences.\n",
- "* `:stats` - Show statistics about the state space.\n",
- "* `:time` - Execute the given command and measure how long it takes to execute.\n",
- "* `:version` - Display version info about the ProB CLI and ProB 2.\n"
- ],
- "text/plain": [
- "Enter a B expression or predicate to evaluate it. To load a B machine, enter its source code directly, or use :load to load an external machine file.\n",
- "You can also use any of the following commands. For more help on a particular command, run :help commandname.\n",
- "\n",
- "Evaluation:\n",
- ":eval - Evaluate a formula and display the result.\n",
- ":solve - Solve a predicate with the specified solver.\n",
- ":table - Display an expression as a table.\n",
- ":type - Display the static type of a formula.\n",
- ":prettyprint - Pretty-print a predicate.\n",
- ":let - Evaluate an expression and store it in a local variable.\n",
- ":unlet - Remove a local variable.\n",
- ":assert - Ensure that the predicate is true, and show an error otherwise.\n",
- "\n",
- "Animation:\n",
- "::load - Load a B machine from the given source code.\n",
- ":load - Load a machine from a file.\n",
- ":constants - Set up the current machine's constants.\n",
- ":init - Initialise the current machine with the specified predicate\n",
- ":exec - Execute an operation.\n",
- ":browse - Show information about the current state.\n",
- ":trace - Display all states and executed operations in the current trace.\n",
- ":goto - Go to the state with the specified index in the current trace.\n",
- ":find - Try to find a state for which the given predicate is true (in addition to the machine's invariant).\n",
- "\n",
- "Visualisation:\n",
- ":show - Show the machine's animation function visualisation for the current state.\n",
- ":dot - Execute and show a dot visualisation.\n",
- "\n",
- "Verification:\n",
- ":check - Check the machine's properties, invariant, or assertions in the current state.\n",
- ":modelcheck - Run the ProB model checker on the current model.\n",
- "\n",
- "Other:\n",
- "::render - Render some content with the specified MIME type.\n",
- ":bsymb - Load all bsymb.sty command definitions, so that they can be used in $\\LaTeX$ formulas in Markdown cells.\n",
- ":groovy - Evaluate the given Groovy expression.\n",
- ":help - Display help for a specific command, or general help about the REPL.\n",
- ":pref - View or change the value of one or more preferences.\n",
- ":stats - Show statistics about the state space.\n",
- ":time - Execute the given command and measure how long it takes to execute.\n",
- ":version - Display version info about the ProB CLI and ProB 2.\n"
- ]
- },
- "execution_count": 22,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- ":help"
- ]
- },
{
"cell_type": "code",
"execution_count": null,
diff --git a/SEND-MORE-MONEY.ipynb b/SEND-MORE-MONEY.ipynb
index d1492127b8db3df81cbf1ca826a1ced84d33108a..5d59c0c36136e8567f6f92f104c7139eb1c0d19c 100644
--- a/SEND-MORE-MONEY.ipynb
+++ b/SEND-MORE-MONEY.ipynb
@@ -6,7 +6,9 @@
"source": [
"# SEND-MORE-MONEY\n",
"\n",
- "In this jupyter notebook, we will study how to solve the famous [verbal arithmetic SEND-MORE-MONEY](https://en.wikipedia.org/wiki/Verbal_arithmetic) puzzle. The task is to find the digits S,E,N,D,M,O,R,Y such that the addition of SEND to MORE leads the decimal number MONEY.\n",
+ "Use `:help` to get an overview for the jupyter notebook commands. If you need more insight on how to use this tool, consider reading *ProB Jupyter Notebook Overview*.\n",
+ "\n",
+ "In this jupyter notebook, we will take a look on how to solve the famous [verbal arithmetic SEND-MORE-MONEY](https://en.wikipedia.org/wiki/Verbal_arithmetic) puzzle. The task is to find the digits S,E,N,D,M,O,R,Y such that the addition of SEND to MORE leads the decimal number MONEY.\n",
"The quickest way is to use the ProB Logic Calculator, which is implemented in Jupyter notebook. To solve the puzzle, simply type in: \n",
"`{S,E,N,D, M,O,R, Y} <: 0..9 & S>0 & M>0 & card({S,E,N,D, M,O,R, Y})=8 & S*1000 + E*100 + N*10 + D + M*1000 + O*100 + R*10 + E = M*10000 + O*1000 + N*100 + E*10 + Y` and press enter:"
]
@@ -315,6 +317,13 @@
"source": [
"{K,P} <: 1..9 & {I,S,A,O,N} <: 0..9 & (1000*K+100*I+10*S+S) * (1000*K+100*I+10*S+S) = 1000000*P+100000*A+10000*S+1000*S+100*I+10*O+N & card({K, I, S, P, A, O, N}) = 7"
]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": null,
+ "metadata": {},
+ "outputs": [],
+ "source": []
}
],
"metadata": {
diff --git a/Untitled.ipynb b/waiting_for_features/Jobs_Puzzle.ipynb
similarity index 78%
rename from Untitled.ipynb
rename to waiting_for_features/Jobs_Puzzle.ipynb
index 5426bf1fdea2fb49e56c435dbe492eb82ad43abe..2253d065719b06581c6dfbc89e6843062629c6b2 100644
--- a/Untitled.ipynb
+++ b/waiting_for_features/Jobs_Puzzle.ipynb
@@ -59,7 +59,21 @@
"cell_type": "code",
"execution_count": 1,
"metadata": {},
- "outputs": [],
+ "outputs": [
+ {
+ "data": {
+ "text/markdown": [
+ "$\\{\\text{\"Pete\"},\\text{\"Roberta\"},\\text{\"Steve\"},\\text{\"Thelma\"}\\}$"
+ ],
+ "text/plain": [
+ "{\"Pete\",\"Roberta\",\"Steve\",\"Thelma\"}"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
"source": [
":let PEOPLE {\"Roberta\", \"Thelma\", \"Steve\", \"Pete\"}"
]
@@ -207,43 +221,6 @@
"This is possible, because in B functions and relations can be treated as sets of pairs, where each pair consists of an element of the domain and the corresponding element from the range of the relation."
]
},
- {
- "cell_type": "code",
- "execution_count": 6,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$\\mathit{TRUE}$\n",
- "\n",
- "**Solution:**\n",
- "* $\\mathit{HoldsJob} = \\{(\\text{\"actor\"}\\mapsto\\text{\"Steve\"}),(\\text{\"boxer\"}\\mapsto\\text{\"Thelma\"}),(\\text{\"chef\"}\\mapsto\\text{\"Pete\"}),(\\text{\"clerk\"}\\mapsto\\text{\"Pete\"}),(\\text{\"guard\"}\\mapsto\\text{\"Pete\"}),(\\text{\"nurse\"}\\mapsto\\text{\"Pete\"}),(\\text{\"police\"}\\mapsto\\text{\"Pete\"}),(\\text{\"teacher\"}\\mapsto\\text{\"Roberta\"})\\}$\n",
- "* $\\mathit{JOBS} = \\{\\text{\"actor\"},\\text{\"boxer\"},\\text{\"chef\"},\\text{\"clerk\"},\\text{\"guard\"},\\text{\"nurse\"},\\text{\"police\"},\\text{\"teacher\"}\\}$\n",
- "* $\\mathit{PEOPLE} = \\{\\text{\"Pete\"},\\text{\"Roberta\"},\\text{\"Steve\"},\\text{\"Thelma\"}\\}$\n",
- "* $\\mathit{MALE} = \\{\\text{\"Pete\"},\\text{\"Steve\"}\\}$\n",
- "* $\\mathit{FEMALE} = \\{\\text{\"Roberta\"},\\text{\"Thelma\"}\\}$"
- ],
- "text/plain": [
- "TRUE\n",
- "\n",
- "Solution:\n",
- "\tHoldsJob = {(\"actor\"↦\"Steve\"),(\"boxer\"↦\"Thelma\"),(\"chef\"↦\"Pete\"),(\"clerk\"↦\"Pete\"),(\"guard\"↦\"Pete\"),(\"nurse\"↦\"Pete\"),(\"police\"↦\"Pete\"),(\"teacher\"↦\"Roberta\")}\n",
- "\tJOBS = {\"actor\",\"boxer\",\"chef\",\"clerk\",\"guard\",\"nurse\",\"police\",\"teacher\"}\n",
- "\tPEOPLE = {\"Pete\",\"Roberta\",\"Steve\",\"Thelma\"}\n",
- "\tMALE = {\"Pete\",\"Steve\"}\n",
- "\tFEMALE = {\"Roberta\",\"Thelma\"}"
- ]
- },
- "execution_count": 6,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- "HoldsJob : JOBS -->> PEOPLE & card(HoldsJob) = 8"
- ]
- },
{
"cell_type": "markdown",
"metadata": {},
@@ -255,24 +232,6 @@
"First of all, we have to add HoldsJob to our globals, however."
]
},
- {
- "cell_type": "code",
- "execution_count": 25,
- "metadata": {},
- "outputs": [
- {
- "ename": "EvaluationException",
- "evalue": "de.be4.classicalb.core.parser.exceptions.BCompoundException: [2,26] expecting: identifier literal",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31mde.prob.animator.domainobjects.EvaluationException: de.be4.classicalb.core.parser.exceptions.BCompoundException: [2,26] expecting: identifier literal\u001b[0m"
- ]
- }
- ],
- "source": [
- ":let HoldsJob JOBS -->> PEOPLE"
- ]
- },
{
"cell_type": "markdown",
"metadata": {},
@@ -281,44 +240,10 @@
]
},
{
- "cell_type": "code",
- "execution_count": 21,
- "metadata": {},
- "outputs": [
- {
- "data": {
- "text/markdown": [
- "$8$"
- ],
- "text/plain": [
- "8"
- ]
- },
- "execution_count": 21,
- "metadata": {},
- "output_type": "execute_result"
- }
- ],
- "source": [
- ":let card(HoldsJob) 8"
- ]
- },
- {
- "cell_type": "code",
- "execution_count": 24,
+ "cell_type": "markdown",
"metadata": {},
- "outputs": [
- {
- "ename": "EvaluationException",
- "evalue": "de.be4.classicalb.core.parser.exceptions.BCompoundException: [2,26] expecting: identifier literal",
- "output_type": "error",
- "traceback": [
- "\u001b[1m\u001b[31mde.prob.animator.domainobjects.EvaluationException: de.be4.classicalb.core.parser.exceptions.BCompoundException: [2,26] expecting: identifier literal\u001b[0m"
- ]
- }
- ],
"source": [
- ":let JobsOf HoldsJob~"
+ "### Needs possibility to save executed expressions"
]
},
{
diff --git a/Nine_Prisoners.ipynb b/waiting_for_features/Nine_Prisoners.ipynb
similarity index 100%
rename from Nine_Prisoners.ipynb
rename to waiting_for_features/Nine_Prisoners.ipynb
diff --git a/Rush_Hour_Puzzle.ipynb b/waiting_for_features/Rush_Hour_Puzzle.ipynb
similarity index 100%
rename from Rush_Hour_Puzzle.ipynb
rename to waiting_for_features/Rush_Hour_Puzzle.ipynb
diff --git a/Sudoku_Solved.ipynb b/waiting_for_features/Sudoku_Solved.ipynb
similarity index 100%
rename from Sudoku_Solved.ipynb
rename to waiting_for_features/Sudoku_Solved.ipynb