{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Apples and Oranges\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 [apparently an Interview question at Apple](https://bgr.com/2015/11/20/apple-interview-questions/). Quoting from\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",
    "* (2) The boxes have been incorrectly labeled such that no label identifies the actual contents of the box it labels.\n",
    "* (3) Opening just one box, and without looking in the box, you take out one piece of fruit.\n",
    "* (4) By looking at the fruit, how can you immediately label all of the boxes correctly?\n",
    "\n",
    "Here is one encoding of this puzzle in B:\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: ApplesOranges"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE ApplesOranges\n",
    "SETS\n",
    " Fruit={apple,orange}; // possible content for the boxes\n",
    " Label={A,O,Both} // labels for the boxes\n",
    "CONSTANTS a,o,b,  // a,o,b are the three boxes\n",
    "          Take,  // which box should we open (the label of that box)\n",
    "          DecisionFunction // given the fruit we pick from Take: what are the contents of the boxes labeled A,O,Both\n",
    "PROPERTIES\n",
    "  a = {apple} & o={orange} & b={apple,orange} // (1)\n",
    "  &\n",
    "  Take : Label //3\n",
    "  &\n",
    "  DecisionFunction : Fruit --> (Label >->> {a,o,b}) & //4\n",
    "  !label. ( // the decision function has to work for all allowed labelings\n",
    "  ( label : {a,o,b} >->> Label &\n",
    "    label(a) /= A & label(o) /= O & label(b) /= Both // (2)\n",
    "  )\n",
    "   =>\n",
    "  !f.(f: label~(Take)\n",
    "      => DecisionFunction(f)=label~ // the function should tell us what is behind label A,O,Both\n",
    "     )\n",
    "  )\n",
    "END"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We have abstracted the box of apples `a` by the set containing `apple`.\n",
    "Ditto for `o` and `b`, which are abstracted by `{orange}` and\n",
    "`{apple,orange}` respectively.\n",
    "\n",
    "NOTE: You need a recent version of ProB 1.5.1-beta3 or newer to load the above model on your own computer with its one-line comments. If you have an older version of ProB, simply use the normal comments `/* ... */`.\n",
    "\n",
    "`:goto Number` jumps to the state with the given number. \n",
    "\n",
    "With the `:trace` command, you will get the information of your current trace.\n",
    "\n",
    "There is an autocompletion tool, which allows you to see the possible commands, simply use TAB after you type in your `:`. \n",
    "\n",
    "This model gives you just one solution, after setting up the constants with `:constants`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Changed to state with index -1"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":goto -1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "* -1: Root state **(current)**"
      ],
      "text/plain": [
       "-1: Root state (current)"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":trace"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{Both}$"
      ],
      "text/plain": [
       "Both"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Take"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "As we can see, the only solution is to open the box labelled with\n",
    "\"Both\". We can inspect the decision function by using the jupyter notebook code block, like follows:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{(\\mathit{A}\\mapsto\\{\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{apple}\\})\\}$"
      ],
      "text/plain": [
       "{(A↦{orange}),(O↦{apple,orange}),(Both↦{apple})}"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "DecisionFunction(apple)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{(\\mathit{A}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{orange}\\})\\}$"
      ],
      "text/plain": [
       "{(A↦{apple,orange}),(O↦{apple}),(Both↦{orange})}"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "DecisionFunction(orange)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "In other words, when we pick an apple out of the box labelled with\n",
    "\"Both\", then it contains only apples and the box labelled \"O\"ranges\n",
    "contains both apples and oranges. The box labelled \"A\"pples contains\n",
    "just oranges. Similarly, if we pick up an orange out of the box labelled\n",
    "with \"Both\", then it contains only oranges and the box labelled with\n",
    "\"A\"pples contains contains both apples and oranges. The box labelled\n",
    "\"O\"ranges contains just apples.\n",
    "\n",
    "NOTE: You can use `:table Expression` to get values or expressions in a tabular form."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "|prj1|prj2|\n",
       "|---|---|\n",
       "|$\\mathit{apple}$|$\\{(\\mathit{A}\\mapsto\\{\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{apple}\\})\\}$|\n",
       "|$\\mathit{orange}$|$\\{(\\mathit{A}\\mapsto\\{\\mathit{apple},\\mathit{orange}\\}),(\\mathit{O}\\mapsto\\{\\mathit{apple}\\}),(\\mathit{Both}\\mapsto\\{\\mathit{orange}\\})\\}$|\n"
      ],
      "text/plain": [
       "prj1\tprj2\n",
       "apple\t{(A|->{orange}),(O|->{apple,orange}),(Both|->{apple})}\n",
       "orange\t{(A|->{apple,orange}),(O|->{apple}),(Both|->{orange})}\n"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":table DecisionFunction"
   ]
  }
 ],
 "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": 2
}