{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {
    "nbgrader": {
     "grade": false,
     "grade_id": "cell-ca0e2d4a356e7ddd",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "# Exercice Sheet: B Expressions\n",
    "\n",
    "You are given a B machine with three given sets:\n",
    "* a set ```S``` of online shops\n",
    "* a set ```A``` of articles that can be ordered\n",
    "* a set ```C``` of clients\n",
    "You are also given two relations:\n",
    "* a relation ```delivers:S<->A``` describing which shops can deliver which articles\n",
    "* a relation ```orders:C<->POW(A)``` describing current outstanding orders, an order consisting of a set of articles."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {
    "deletable": false,
    "editable": false,
    "nbgrader": {
     "grade": false,
     "grade_id": "cell-9e087aee8a95121b",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Loaded machine: exercise1"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "::load\n",
    "MACHINE exercise1\n",
    "DEFINITIONS \"LibraryHash.def\"\n",
    "SETS\n",
    "  S = {s1,s2,s3,s4,s5} /* Shops */ ;\n",
    "  A = {a1,a2,a3,a4,a5} /* Articles that can be ordered */;\n",
    "  C = {c1,c2,c3} /* Clients */\n",
    "CONSTANTS delivers, orders\n",
    "PROPERTIES\n",
    "  delivers = {s1↦a1,s1↦a2, s2↦a4, s3↦a3, s3↦a2, s4↦a4, s4↦a5} &\n",
    "  orders = {c1 ↦ {a1,a5}, c1 ↦ {a4}, c2 ↦ {a1,a3,a5}, c3 ↦ {a2,a3}, c3 ↦ {a1}}\n",
    "END"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {
    "nbgrader": {
     "grade": false,
     "grade_id": "cell-bfffcdda64188e4c",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/plain": [
       "Executed operation: SETUP_CONSTANTS()"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":constants"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "nbgrader": {
     "grade": false,
     "grade_id": "cell-46338618f1b7edff",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "The above machine also contains particular instantiations of the above sets and relations, which will be used in the exercises below."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "nbgrader": {
     "grade": false,
     "grade_id": "cell-44701490d6a9260e",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "## Exercise 1\n",
    "Write a B expression to compute the set of clients that have ordered article a5. Use the ```:let sol1 EXPRESSION``` in the cell below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {
    "nbgrader": {
     "grade": false,
     "grade_id": "cell-bab176fbf0a75b6f",
     "locked": false,
     "schema_version": 3,
     "solution": true,
     "task": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\mathit{c1},\\mathit{c2}\\}$"
      ],
      "text/plain": [
       "{c1,c2}"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let sol1 {c| a5 : union(orders[{c}])}"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {
    "nbgrader": {
     "grade": true,
     "grade_id": "cell-2b74a8ed88e60492",
     "locked": true,
     "points": 0,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":assert SHA_HASH_HEX(sol1) = \"26365f212fb4cbe0ef2adc9eb42d3c6fac15442b\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {
    "nbgrader": {
     "grade": false,
     "grade_id": "exercise_2",
     "locked": true,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "source": [
    "## Exercise 2\n",
    "Write a B expression which computes the set of all articles ordered by at least one client. Use the ```:let sol2 EXPRESSION``` in the cell below."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {
    "nbgrader": {
     "grade": false,
     "grade_id": "cell-5fb80f74fa97df15",
     "locked": false,
     "schema_version": 3,
     "solution": true,
     "task": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\{\\mathit{a1},\\mathit{a2},\\mathit{a3},\\mathit{a4},\\mathit{a5}\\}$"
      ],
      "text/plain": [
       "{a1,a2,a3,a4,a5}"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":let sol2 union(ran(orders))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {
    "nbgrader": {
     "grade": true,
     "grade_id": "cell-b1cc285b1a32f2bd",
     "locked": true,
     "points": 0,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\text{\"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3\"}$"
      ],
      "text/plain": [
       "\"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3\""
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "SHA_HASH_HEX(sol2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {
    "nbgrader": {
     "grade": true,
     "grade_id": "cell-94e08eff5d6d66bf",
     "locked": true,
     "points": 0,
     "schema_version": 3,
     "solution": false,
     "task": false
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    ":assert SHA_HASH_HEX(sol2) = \"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Comments:\n",
    "To lock cells you can do this:\n",
    "\n",
    "\n",
    "* menu: view → cell toolbar → edit metadata.\n",
    "* make this like\n",
    "```\n",
    "{\n",
    "  \"trusted\": true,\n",
    "  \"editable\": false,\n",
    "  \"deletable\": false\n",
    "}\n",
    "```"
   ]
  }
 ],
 "metadata": {
  "celltoolbar": "Create Assignment",
  "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
}