add exercise experiment

notebooks/experiments/DeliveryExercise.ipynb

+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "# Exercice Sheet\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": 13,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: exercise1"
+      ]
+     },
+     "execution_count": 13,
+     "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": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Machine constants set up using operation 0: $setup_constants()"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":constants"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "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": {},
+   "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": 16,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{\\mathit{c1},\\mathit{c2}\\}$"
+      ],
+      "text/plain": [
+       "{c1,c2}"
+      ]
+     },
+     "execution_count": 16,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let sol1 {c| a5 : union(orders[{c}])}"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 20,
+   "metadata": {},
+   "outputs": [
+    {
+     "ename": "CommandExecutionException",
+     "evalue": ":assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol1",
+     "output_type": "error",
+     "traceback": [
+      "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol1\u001b[0m"
+     ]
+    }
+   ],
+   "source": [
+    ":assert SHA_HASH_HEX(sol1) = \"26365f212fb4cbe0ef2adc9eb42d3c6fac15442b\""
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "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": 22,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\{\\mathit{a1},\\mathit{a2},\\mathit{a3},\\mathit{a4},\\mathit{a5}\\}$"
+      ],
+      "text/plain": [
+       "{a1,a2,a3,a4,a5}"
+      ]
+     },
+     "execution_count": 22,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":let sol2 union(ran(orders))"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 23,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\text{\"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3\"}$"
+      ],
+      "text/plain": [
+       "\"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3\""
+      ]
+     },
+     "execution_count": 23,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "SHA_HASH_HEX(sol2)"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    ":assert SHA_HASH_HEX(sol2) = \"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3\""
+   ]
+  }
+ ],
+ "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
+}