From 063b72e1d12ee70f622ca54e4700da62f40de4c5 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Fri, 10 May 2019 10:29:08 +0200
Subject: [PATCH] add exercise experiment
---
notebooks/experiments/DeliveryExercise.ipynb | 204 +++++++++++++++++++
1 file changed, 204 insertions(+)
create mode 100644 notebooks/experiments/DeliveryExercise.ipynb
diff --git a/notebooks/experiments/DeliveryExercise.ipynb b/notebooks/experiments/DeliveryExercise.ipynb
new file mode 100644
index 0000000..3f41be6
--- /dev/null
+++ b/notebooks/experiments/DeliveryExercise.ipynb
@@ -0,0 +1,204 @@
+{
+ "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
+}
--
GitLab