{
 "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",
    "[1](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"
   ]
  },
  {
   "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": {
  "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
}