add comment on how to lock

50fef812 · Michael Leuschel · 063b72e1 · 50fef812
Commit 50fef812 authored 6 years ago by Michael Leuschel
--- a/notebooks/experiments/DeliveryExercise.ipynb
+++ b/notebooks/experiments/DeliveryExercise.ipynb
@@ -4,7 +4,7 @@
   "cell_type": "markdown",
   "metadata": {},
   "source": [
-    "# Exercice Sheet\n",
+    "# Exercice Sheet: B Expressions\n",
    "\n",
    "You are given a B machine with three given sets:\n",
    "* a set ```S``` of online shops\n",
@@ -17,8 +17,11 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 13,
+   "execution_count": 25,
-   "metadata": {},
+   "metadata": {
+    "deletable": false,
+    "editable": false
+   },
   "outputs": [
    {
     "data": {
@@ -26,7 +29,7 @@
       "Loaded machine: exercise1"
      ]
     },
-     "execution_count": 13,
+     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -48,7 +51,7 @@
  },
  {
   "cell_type": "code",
-   "execution_count": 14,
+   "execution_count": 26,
   "metadata": {},
   "outputs": [
    {
@@ -57,7 +60,7 @@
       "Machine constants set up using operation 0: $setup_constants()"
      ]
     },
-     "execution_count": 14,
+     "execution_count": 26,
     "metadata": {},
     "output_type": "execute_result"
    }
@@ -178,15 +181,51 @@
  },
  {
   "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 24,
   "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "ename": "CommandExecutionException",
+     "evalue": ":assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol2",
+     "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 sol2\u001b[0m"
+     ]
+    }
+   ],
   "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",
+    "```"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "metadata": {},
+   "outputs": [],
+   "source": []
  }
 ],
 "metadata": {
+  "celltoolbar": "Edit Metadata",
  "kernelspec": {
   "display_name": "ProB 2",
   "language": "prob",

 %% Cell type:markdown id: tags:
-# Exercice Sheet
+# Exercice Sheet: B Expressions
 You are given a B machine with three given sets:
 * a set ```S``` of online shops
 * a set ```A``` of articles that can be ordered
 * a set ```C``` of clients
 You are also given two relations:
 * a relation ```delivers:S<->A``` describing which shops can deliver which articles
 * a relation ```orders:C<->POW(A)``` describing current outstanding orders, an order consisting of a set of articles.
 %% Cell type:code id: tags:
 ``` prob
 ::load
 MACHINE exercise1
 DEFINITIONS "LibraryHash.def"
 SETS
  S = {s1,s2,s3,s4,s5} /* Shops */ ;
  A = {a1,a2,a3,a4,a5} /* Articles that can be ordered */;
  C = {c1,c2,c3} /* Clients */
 CONSTANTS delivers, orders
 PROPERTIES
  delivers = {s1↦a1,s1↦a2, s2↦a4, s3↦a3, s3↦a2, s4↦a4, s4↦a5} &
  orders = {c1 ↦ {a1,a5}, c1 ↦ {a4}, c2 ↦ {a1,a3,a5}, c3 ↦ {a2,a3}, c3 ↦ {a1}}
 END
 ```
 %% Output
    Loaded machine: exercise1
 %% Cell type:code id: tags:
 ``` prob
 :constants
 ```
 %% Output
    Machine constants set up using operation 0: $setup_constants()
 %% Cell type:markdown id: tags:
 The above machine also contains particular instantiations of the above sets and relations, which will be used in the exercises below.
 %% Cell type:markdown id: tags:
 ## Exercise 1
 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 id: tags:
 ``` prob
 :let sol1 {c| a5 : union(orders[{c}])}
 ```
 %% Output
    $\{\mathit{c1},\mathit{c2}\}$
    {c1,c2}
 %% Cell type:code id: tags:
 ``` prob
 :assert SHA_HASH_HEX(sol1) = "26365f212fb4cbe0ef2adc9eb42d3c6fac15442b"
 ```
 %% Output
    :assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol1
 %% Cell type:markdown id: tags:
 ## Exercise 2
 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 id: tags:
 ``` prob
 :let sol2 union(ran(orders))
 ```
 %% Output
    $\{\mathit{a1},\mathit{a2},\mathit{a3},\mathit{a4},\mathit{a5}\}$
    {a1,a2,a3,a4,a5}
 %% Cell type:code id: tags:
 ``` prob
 SHA_HASH_HEX(sol2)
 ```
 %% Output
    $\text{"29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3"}$
    "29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3"
 %% Cell type:code id: tags:
 ``` prob
 :assert SHA_HASH_HEX(sol2) = "29bac35e283e6637fd22c2c8ee4a17a8d4ff52a3"
 ```
+%% Output
+    :assert: Error while evaluating assertion: Computation not completed: Could not infer type of T,Could not infer type of sol2
+%% Cell type:markdown id: tags:
+# Comments:
+To lock cells you can do this:
+* menu: view → cell toolbar → edit metadata.
+* make this like
+```
+{
+  "trusted": true,
+  "editable": false,
+  "deletable": false
+}
+```
+%% Cell type:code id: tags:
+``` prob
+```