"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 our team stumbled across this puzzle in a mailing list.\n",
"We took a look at it and found it was very suitable to be represented in a ProB Jupyter Notebook. \n",
"To solve this puzzle, we have to think about a way to represent this lock as a machine.\n",
"We chose to represent each digit of the code in a Digits function. This function enables us to place some assertions about the correct digits that we take from the hints on the picture. Additionally we make assertions about the correctly placed digits and ,eventually, we come to a solution that is stored in our Digits constant.\n",
"\n",
"To access the constant from the machine, we have to set it up with `:constants` and initialize the machine with `:init`."
"This means our solution for the crack the code puzzle is 0, 4, 2. If you are interested in the runtime of the operations, you can use `:time` before each operation to track it."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "ProB 2",
"language": "prob",
"name": "prob2"
},
"language_info": {
"codemirror_mode": "prob2_jupyter_repl",
"file_extension": ".prob",
"mimetype": "text/x-prob2-jupyter-repl",
"name": "prob"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
%% Cell type:markdown id: tags:
# Crack the Code Puzzle
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*.
A while ago a member of our team stumbled across this puzzle in a mailing list.
We took a look at it and found it was very suitable to be represented in a ProB Jupyter Notebook.
To solve this puzzle, we have to think about a way to represent this lock as a machine.
We chose to represent each digit of the code in a Digits function. This function enables us to place some assertions about the correct digits that we take from the hints on the picture. Additionally we make assertions about the correctly placed digits and ,eventually, we come to a solution that is stored in our Digits constant.
To access the constant from the machine, we have to set it up with `:constants` and initialize the machine with `:init`.
// [6,8,2] : one number is correct and well-placed
// [6,1,4]: one number is correct but wrongly placed
// [2,0,6]: two numbers are correct but wrongly placed
// [7,3,8]: nothing is correct
// [7,8,0]: one number is correct but wrongly placed
// Assertions about correct digits:
card(ran(Digits) /\ {6,8,2})=1 &
card(ran(Digits)/\{6,1,4})=1 &
card(ran(Digits)/\{2,0,6})=2 &
ran(Digits) /\ {7,3,8} = {} &
card(ran(Digits)/\{7,8,0})=1 &
// Assertions about correctly placed digits
card(Digits /\ [6,8,2])=1 &
(Digits /\ [6,1,4])={} &
(Digits /\ [2,0,6])={} &
(Digits /\ [7,8,0])={}
END
```
%% Output
Loaded machine: LockChallenge
%% Cell type:code id: tags:
``` prob
:constants
```
%% Output
Machine constants set up using operation 0: $setup_constants()
%% Cell type:code id: tags:
``` prob
:init
```
%% Output
Machine initialised using operation 1: $initialise_machine()
%% Cell type:markdown id: tags:
As we can see when we use the `:browse` functionality, our constant Digits can be called now, by simply typing it in.
%% Cell type:code id: tags:
``` prob
:browse
```
%% Output
Machine: LockChallenge
Sets: (none)
Constants: Digits
Variables: (none)
Operations:
%% Cell type:code id: tags:
``` prob
Digits
```
%% Output
$\{(1\mapsto 0),(2\mapsto 4),(3\mapsto 2)\}$
{(1↦0),(2↦4),(3↦2)}
%% Cell type:markdown id: tags:
This means our solution for the crack the code puzzle is 0, 4, 2. If you are interested in the runtime of the operations, you can use `:time` before each operation to track it.
