{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# The Jobs Puzzle\n",
    "\n",
    "Based on *Michael Leuschel, David Schneider. Towards B as a High-Level Constraint Modeling Language. In Yamine Ait Amer, Klaus-Dieter Schewe (ed.): Abstract State Machines, Alloy, B, TLA, VDM, and Z, Springer Berlin Heidelberg, 8477: 101-116, 2014.*\n",
    "\n",
    "This puzzle was originally published in 1984 by [Wos et al., 1984](https://www.mcs.anl.gov/research/projects/AR/book1.html) as part of a collection of puzzles for automatic reasoners. A reference implementation of the puzzle, by one of the authors of the book, using [OTTER, 2003](https://arxiv.org/abs/cs/0310056).\n",
    "\n",
    "The puzzle consists of eight statements that describe the problem domain and provide some constraints on the elements of the domain. The problem is about a set of people and a set of jobs; the question posed by the puzzle is: who holds which job? The text of the puzzle as presented in \"The jobs puzzle: A challenge for logical expressibility and automated reasoning.\"[S. C. Shapiro, 2011](https://cse.buffalo.edu/~shapiro/Papers/SS11-06-017.pdf) is as follows:\n",
    "\n",
    "* There are four people: Roberta, Thelma, Steve, and Pete.\n",
    "* Among them, they hold eight different jobs.\n",
    "* Each holds exactly two jobs.\n",
    "* The jobs are: chef, guard, nurse, clerk, police officer (gender not implied), teacher, actor, and boxer.\n",
    "* The job of nurse is held by a male.\n",
    "* The husband of the chef is the clerk.\n",
    "* Roberta is not a boxer.\n",
    "* Pete has no education past the ninth grade.\n",
    "* Roberta, the chef, and the police officer went golfing together.\n",
    "\n",
    "What makes this puzzle interesting for automatic reasoners, is that not all the information required to solve the puzzle is provided explicitly in the text.\n",
    "\n",
    "The puzzle can only be solved if certain implicit assumptions about the world are taken into account, such as: the names in the puzzle denote gender or that some of the job names imply the gender of the person that holds it.\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Shapiro's Challenge\n",
    "\n",
    "Shapiro, following the original authors' remarks, that formalizing the puzzle was at times hard and tendious, identified three challenges posed by the puat times hard and tedious, identified three challenges posed by the puzzle with regard to automatic reasoners. According to Shapiro, the challenges posed by the jobs puzzle are to:\n",
    "\n",
    "1. formalize it in a non-difficult, non-tedious way\n",
    "2. formalize it in a way that adheres closely to the English statement of the puzzle\n",
    "3. have an automated general-purpose commonsense reasoner that can accept that formalization and solve the puzzle quickly.\n",
    "\n",
    "Any formalization also needs to encode the implicit knowledge used to solve the puzzle for the automatic reasoners while still trying to satisfy the aspects mentioned above. Addressing this challenge makes this puzzle a good case-study for the expressiveness of B to formalize such a problem."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## A Solution to the Jobs Puzzle using B\n",
    "\n",
    "The B encoding of the puzzle uses plain predicate logic, \n",
    "combined with set theory and arithmetic. We will show how this \n",
    "enables a very concise encoding of the problem, staying very close to the natural language requirements. Moreover, the puzzle can be quickly solved using the constraint solving capabilities of ProB. Following the order of the sentences in the puzzle we will discuss one or more possibilities to formalize them using B.\n",
    "\n",
    "To express \"*There are four people: Roberta, Thelma, Steve, and Pete*\" we define a set of people, that holds the list of names:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    ":let PEOPLE {\"Roberta\", \"Thelma\", \"Steve\", \"Pete\"}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We are using strings here to describe the elements of the set. This has the advantage, that the elements of the set are implicitly different.\n",
    "\n",
    "Alternatively, we could use enumerated or deferred sets defined in the SETS section of a B machine. As stated above we need some additional information that is not included in the puzzle to solve it. \n",
    "\n",
    "The first bit of information is that the names used in the puzzle imply the gender. In order to express this information we create two sets, MALE and FEMALE which are subsets of PEOPLE and contain the corresponding names."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\text{\"Roberta\"},\\text{\"Thelma\"}\\}$"
      ],
      "text/plain": [
       "{\"Roberta\",\"Thelma\"}"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let FEMALE {\"Roberta\", \"Thelma\"}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\text{\"Pete\"},\\text{\"Steve\"}\\}$"
      ],
      "text/plain": [
       "{\"Pete\",\"Steve\"}"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let MALE {\"Steve\", \"Pete\"}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The next statement of the puzzle is: \"*among them, they hold eight different jobs*\". This can be formalized in B using a function that maps from a job to the corresponding person that holds this job using a total surjection from JOBS to PEOPLE. \n",
    "\n",
    "To use that statement, however we have to define JOBS, or the fourth statement."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\text{\"actor\"},\\text{\"boxer\"},\\text{\"chef\"},\\text{\"clerk\"},\\text{\"guard\"},\\text{\"nurse\"},\\text{\"police\"},\\text{\"teacher\"}\\}$"
      ],
      "text/plain": [
       "{\"actor\",\"boxer\",\"chef\",\"clerk\",\"guard\",\"nurse\",\"police\",\"teacher\"}"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let JOBS {\"chef\", \"guard\", \"nurse\", \"clerk\", \"police\", \"teacher\", \"actor\", \"boxer\"}"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Now we can see what Holds Job will do. "
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "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": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "HoldsJob : JOBS -->> PEOPLE"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Since we have not yet added any additional information, the Jobs are just randomly assigned to each Person. \n",
    "\n",
    "Although redundant, as we will see below, to express “*Among them, they hold eight different jobs*” we can add the assertion that the cardinality of HoldsJob is 8. \n",
    "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": {},
   "source": [
    "Constraining the jobs each person holds, the puzzle states: “*Each holds exactly two jobs*”. To express this we use the inverse relation of HoldsJob, it maps a PERSON to the JOBS associated to her. The inverse function or relation is expressed in B using the ~ operator. \n",
    "\n",
    "For readability we assign the inverse of HoldsJob to a variable called JobsOf. JobsOf is in this case is a relation, because, as stated above, each person holds two jobs.\n",
    "\n",
    "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": {},
   "source": [
    "Because JobsOf is a relation and not a function, in order to read the values, we need to use B’s relational image operator. This operator maps a subset of the domain to a subset of the range, instead of a single value. To read the jobs Steve holds, the relational image of JobsOf is used as shown below:"
   ]
  },
  {
   "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,
   "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~"
   ]
  },
  {
   "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
}