{
 "nbformat": 4,
 "nbformat_minor": 5,
 "metadata": {
  "kernelspec": {
   "name": "provsql-studio",
   "display_name": "ProvSQL (SQL)",
   "language": "sql"
  },
  "language_info": {
   "name": "sql"
  },
  "provsql": {
   "scheme": "semiring",
   "database": "tutorial",
   "generated_from": "doc/source/user/tutorial.rst"
  }
 },
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Tutorial: Who Killed Daphine?\n",
    "\n",
    "This tutorial introduces the core ProvSQL features through a self-contained crime mystery.\n",
    "\n",
    "## The Scenario\n",
    "\n",
    "A group of 20 persons spent the night in a manor. In the morning, Daphine, a young lady, went missing. Her dead body was found the following day in the cellar. The autopsy revealed the following facts:\n",
    "\n",
    "- She died of a head injury caused by a blunt-force instrument.\n",
    "- Her death happened between midnight and 8 am.\n",
    "- She was not killed in the cellar, but her body was moved there afterwards.\n",
    "- Goose down found in her wound proves that she died in bed in one of the bedrooms; unfortunately all beds have the same down pillows, and pillowcases were changed in the morning, so it is impossible to identify which bedroom.\n",
    "\n",
    "The police interviewed all 19 suspects and collected their statements about who they saw in which room at which time. They also assessed each witness’s reliability through a psychological evaluation.\n",
    "\n",
    "**Your mission:** help the police discover who killed Daphine, using the power of provenance management and probabilistic databases.\n",
    "\n",
    "## Setup"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "*The following cells set up the database with all the content this notebook requires; run them first, ideally on a fresh database.*"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Example tables"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS public.person CASCADE;\n",
    "CREATE TABLE public.person (\n",
    "    id integer NOT NULL,\n",
    "    name text NOT NULL,\n",
    "    date_of_birth date,\n",
    "    height smallint\n",
    ");"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS public.reliability CASCADE;\n",
    "CREATE TABLE public.reliability (\n",
    "    person integer NOT NULL,\n",
    "    score double precision NOT NULL\n",
    ");"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS public.room CASCADE;\n",
    "CREATE TABLE public.room (\n",
    "    id integer NOT NULL,\n",
    "    name text NOT NULL,\n",
    "    area smallint\n",
    ");"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS public.sightings CASCADE;\n",
    "CREATE TABLE public.sightings (\n",
    "    \"time\" time without time zone NOT NULL,\n",
    "    person integer NOT NULL,\n",
    "    room integer NOT NULL,\n",
    "    witness integer\n",
    ");"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "TRUNCATE public.person;\n",
    "COPY public.person (id, name, date_of_birth, height) FROM stdin;\n",
    "0\tTitus\t1969-04-03\t163\n",
    "1\tNorah\t1983-10-15\t194\n",
    "2\tGinny\t1989-10-23\t169\n",
    "3\tDemetra\t1957-07-20\t167\n",
    "4\tSheri\t1950-10-19\t195\n",
    "5\tKarleen\t2004-09-01\t199\n",
    "6\tDaisey\t2002-08-19\t163\n",
    "7\tAudrey\t2009-12-20\t167\n",
    "8\tAlaine\t1956-09-07\t192\n",
    "9\tEdwin\t1987-02-21\t210\n",
    "10\tShelli\t1985-03-05\t195\n",
    "11\tSantina\t1991-09-04\t164\n",
    "12\tBart\t1989-08-12\t163\n",
    "13\tHarriette\t1959-06-24\t160\n",
    "14\tJody\t1962-12-18\t202\n",
    "15\tTheodora\t1995-11-08\t204\n",
    "16\tRoman\t1964-12-14\t171\n",
    "17\tJack\t1976-06-11\t167\n",
    "18\tDaphine\t1998-09-21\t191\n",
    "19\tKyra\t1966-05-04\t202\n",
    "\\."
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "TRUNCATE public.reliability;\n",
    "COPY public.reliability (person, score) FROM stdin;\n",
    "0\t0.23828493492944236\n",
    "1\t0.657319818187148019\n",
    "2\t0.745325911826738019\n",
    "3\t0.656730287512349964\n",
    "4\t0.942979116189337052\n",
    "5\t0.600921893448834954\n",
    "6\t0.874435606539356036\n",
    "7\t0.990416985535926053\n",
    "8\t0.59251775051353095\n",
    "9\t0.688247502287665958\n",
    "10\t0.939401152561129993\n",
    "11\t0.960847979674174013\n",
    "12\t0.818769283596453956\n",
    "13\t0.834442059579594053\n",
    "14\t0.788371825897704048\n",
    "15\t0.620618845450902956\n",
    "16\t0.977769943596806024\n",
    "17\t0.840542782838639035\n",
    "19\t0.681836780693319988\n",
    "\\."
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "TRUNCATE public.room;\n",
    "COPY public.room (id, name, area) FROM stdin;\n",
    "0\tDining room\t23\n",
    "1\tBlue bedroom\t20\n",
    "2\tRed bedroom\t31\n",
    "3\tYellow bedroom\t27\n",
    "4\tGreen bedroom\t37\n",
    "5\tLiving room\t14\n",
    "6\tKitchen\t18\n",
    "7\tFirst bathroom\t26\n",
    "8\tSecond bathroom\t34\n",
    "9\tLibrary\t27\n",
    "\\."
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "TRUNCATE public.sightings;\n",
    "COPY public.sightings (\"time\", person, room, witness) FROM stdin;\n",
    "02:30:00\t19\t8\t0\n",
    "05:00:00\t11\t9\t0\n",
    "03:00:00\t19\t2\t0\n",
    "13:00:00\t8\t8\t0\n",
    "22:30:00\t5\t1\t0\n",
    "05:30:00\t19\t5\t0\n",
    "16:00:00\t11\t8\t0\n",
    "18:30:00\t11\t9\t0\n",
    "13:30:00\t11\t4\t0\n",
    "13:30:00\t6\t7\t0\n",
    "05:30:00\t13\t3\t0\n",
    "10:00:00\t5\t0\t0\n",
    "04:00:00\t14\t6\t0\n",
    "01:30:00\t12\t1\t0\n",
    "15:00:00\t1\t5\t0\n",
    "21:00:00\t16\t6\t0\n",
    "06:30:00\t17\t6\t1\n",
    "01:30:00\t10\t5\t1\n",
    "09:30:00\t9\t7\t1\n",
    "07:00:00\t17\t1\t1\n",
    "10:30:00\t3\t3\t1\n",
    "01:00:00\t18\t2\t1\n",
    "09:00:00\t17\t2\t1\n",
    "05:30:00\t18\t6\t1\n",
    "04:30:00\t16\t2\t2\n",
    "15:30:00\t14\t8\t2\n",
    "19:00:00\t1\t8\t2\n",
    "22:00:00\t5\t9\t2\n",
    "22:30:00\t0\t0\t2\n",
    "18:00:00\t10\t3\t2\n",
    "06:00:00\t11\t5\t2\n",
    "05:00:00\t17\t8\t2\n",
    "17:00:00\t14\t3\t2\n",
    "17:30:00\t12\t9\t2\n",
    "22:30:00\t10\t3\t2\n",
    "21:00:00\t5\t7\t2\n",
    "09:00:00\t9\t4\t2\n",
    "08:30:00\t18\t2\t2\n",
    "10:00:00\t13\t3\t2\n",
    "23:00:00\t7\t9\t2\n",
    "13:30:00\t5\t6\t3\n",
    "19:00:00\t16\t3\t3\n",
    "03:00:00\t16\t4\t3\n",
    "12:30:00\t16\t0\t3\n",
    "20:30:00\t8\t0\t3\n",
    "14:00:00\t15\t1\t3\n",
    "22:00:00\t8\t3\t3\n",
    "10:00:00\t15\t7\t3\n",
    "11:00:00\t15\t3\t3\n",
    "00:00:00\t15\t4\t3\n",
    "22:00:00\t14\t9\t3\n",
    "02:30:00\t15\t7\t4\n",
    "08:00:00\t11\t6\t4\n",
    "15:00:00\t13\t3\t4\n",
    "20:00:00\t8\t7\t4\n",
    "21:00:00\t7\t3\t4\n",
    "19:00:00\t15\t7\t4\n",
    "22:30:00\t9\t6\t5\n",
    "06:00:00\t0\t1\t5\n",
    "02:30:00\t0\t5\t5\n",
    "17:30:00\t1\t1\t5\n",
    "18:00:00\t7\t4\t5\n",
    "04:30:00\t18\t3\t5\n",
    "14:30:00\t17\t9\t5\n",
    "21:30:00\t15\t4\t5\n",
    "10:00:00\t1\t9\t5\n",
    "03:00:00\t3\t0\t5\n",
    "05:30:00\t3\t8\t5\n",
    "19:30:00\t17\t4\t6\n",
    "16:30:00\t0\t5\t7\n",
    "11:00:00\t1\t9\t7\n",
    "13:30:00\t18\t8\t7\n",
    "13:00:00\t12\t9\t7\n",
    "19:30:00\t3\t9\t7\n",
    "20:30:00\t3\t0\t7\n",
    "15:00:00\t6\t3\t7\n",
    "19:30:00\t6\t7\t7\n",
    "19:30:00\t10\t5\t7\n",
    "13:00:00\t5\t3\t8\n",
    "15:00:00\t14\t2\t8\n",
    "01:00:00\t1\t6\t8\n",
    "08:00:00\t7\t4\t8\n",
    "09:30:00\t12\t1\t8\n",
    "20:30:00\t12\t9\t8\n",
    "10:30:00\t11\t9\t8\n",
    "06:30:00\t7\t0\t8\n",
    "11:30:00\t13\t1\t8\n",
    "15:30:00\t5\t0\t9\n",
    "04:00:00\t6\t1\t9\n",
    "22:30:00\t2\t5\t9\n",
    "01:00:00\t8\t6\t9\n",
    "13:30:00\t15\t1\t9\n",
    "07:00:00\t19\t9\t9\n",
    "21:00:00\t7\t2\t9\n",
    "18:00:00\t0\t3\t9\n",
    "08:30:00\t14\t0\t9\n",
    "03:30:00\t11\t9\t9\n",
    "05:30:00\t3\t6\t9\n",
    "20:00:00\t15\t3\t9\n",
    "06:00:00\t7\t6\t9\n",
    "16:00:00\t14\t1\t9\n",
    "19:00:00\t7\t1\t10\n",
    "12:00:00\t17\t8\t10\n",
    "09:00:00\t8\t7\t10\n",
    "21:00:00\t8\t1\t10\n",
    "01:00:00\t8\t0\t10\n",
    "09:30:00\t17\t5\t10\n",
    "08:00:00\t3\t4\t10\n",
    "21:00:00\t18\t1\t10\n",
    "22:00:00\t3\t4\t10\n",
    "11:00:00\t15\t2\t10\n",
    "01:30:00\t18\t1\t10\n",
    "08:00:00\t14\t0\t10\n",
    "06:00:00\t7\t2\t10\n",
    "04:00:00\t18\t2\t10\n",
    "21:00:00\t12\t4\t10\n",
    "01:00:00\t4\t0\t10\n",
    "18:30:00\t13\t4\t10\n",
    "22:00:00\t5\t1\t10\n",
    "23:30:00\t11\t6\t10\n",
    "04:30:00\t5\t3\t11\n",
    "04:30:00\t12\t2\t11\n",
    "13:30:00\t7\t1\t11\n",
    "08:30:00\t7\t9\t11\n",
    "00:00:00\t6\t7\t11\n",
    "11:30:00\t6\t1\t11\n",
    "20:00:00\t6\t2\t11\n",
    "07:00:00\t9\t6\t11\n",
    "10:00:00\t16\t2\t11\n",
    "04:00:00\t8\t0\t11\n",
    "07:30:00\t15\t1\t11\n",
    "20:30:00\t10\t9\t11\n",
    "19:30:00\t3\t0\t11\n",
    "04:30:00\t4\t7\t11\n",
    "12:00:00\t1\t0\t11\n",
    "23:30:00\t17\t9\t11\n",
    "18:00:00\t4\t4\t11\n",
    "21:00:00\t0\t6\t11\n",
    "14:30:00\t17\t8\t12\n",
    "07:30:00\t10\t8\t12\n",
    "05:30:00\t13\t7\t12\n",
    "19:30:00\t18\t5\t12\n",
    "21:30:00\t8\t4\t12\n",
    "21:30:00\t11\t5\t12\n",
    "13:30:00\t3\t9\t12\n",
    "08:00:00\t2\t2\t12\n",
    "08:00:00\t5\t1\t12\n",
    "01:00:00\t13\t7\t12\n",
    "15:00:00\t19\t3\t12\n",
    "21:30:00\t3\t3\t12\n",
    "11:00:00\t12\t2\t13\n",
    "04:30:00\t3\t0\t13\n",
    "02:30:00\t3\t9\t13\n",
    "05:30:00\t5\t5\t13\n",
    "01:00:00\t1\t5\t13\n",
    "09:00:00\t15\t2\t13\n",
    "22:00:00\t18\t7\t13\n",
    "18:30:00\t7\t7\t13\n",
    "08:30:00\t18\t7\t13\n",
    "09:30:00\t6\t1\t13\n",
    "21:00:00\t6\t5\t13\n",
    "16:30:00\t19\t5\t13\n",
    "15:30:00\t1\t6\t14\n",
    "07:30:00\t7\t9\t14\n",
    "04:30:00\t13\t2\t14\n",
    "10:00:00\t17\t9\t14\n",
    "07:30:00\t12\t5\t14\n",
    "15:30:00\t8\t6\t14\n",
    "10:00:00\t18\t9\t14\n",
    "18:00:00\t0\t6\t14\n",
    "17:30:00\t2\t7\t14\n",
    "18:30:00\t5\t5\t14\n",
    "04:00:00\t4\t8\t14\n",
    "12:30:00\t7\t4\t14\n",
    "00:30:00\t19\t5\t14\n",
    "14:30:00\t9\t1\t14\n",
    "09:00:00\t3\t9\t14\n",
    "14:00:00\t7\t2\t14\n",
    "00:30:00\t12\t6\t14\n",
    "16:00:00\t8\t4\t15\n",
    "23:00:00\t12\t1\t15\n",
    "13:30:00\t18\t2\t15\n",
    "11:30:00\t2\t4\t15\n",
    "00:00:00\t10\t9\t15\n",
    "00:30:00\t3\t7\t15\n",
    "03:30:00\t3\t1\t15\n",
    "00:30:00\t0\t2\t15\n",
    "16:30:00\t10\t2\t15\n",
    "08:00:00\t8\t6\t15\n",
    "06:00:00\t2\t2\t15\n",
    "03:00:00\t13\t1\t15\n",
    "06:00:00\t8\t5\t15\n",
    "15:00:00\t18\t3\t15\n",
    "01:30:00\t3\t0\t15\n",
    "02:30:00\t5\t8\t15\n",
    "22:30:00\t19\t7\t15\n",
    "22:00:00\t15\t4\t16\n",
    "10:30:00\t0\t5\t17\n",
    "17:00:00\t1\t5\t17\n",
    "12:30:00\t5\t3\t17\n",
    "00:00:00\t19\t7\t17\n",
    "12:00:00\t1\t7\t17\n",
    "16:00:00\t5\t7\t17\n",
    "14:00:00\t3\t8\t17\n",
    "14:30:00\t14\t0\t17\n",
    "04:00:00\t6\t3\t19\n",
    "11:00:00\t4\t5\t19\n",
    "15:30:00\t5\t5\t19\n",
    "\\."
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE ONLY public.person DROP CONSTRAINT IF EXISTS person_pkey;\n",
    "ALTER TABLE ONLY public.person\n",
    "    ADD CONSTRAINT person_pkey PRIMARY KEY (id);"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE ONLY public.reliability DROP CONSTRAINT IF EXISTS reliability_pkey;\n",
    "ALTER TABLE ONLY public.reliability\n",
    "    ADD CONSTRAINT reliability_pkey PRIMARY KEY (person);"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE ONLY public.room DROP CONSTRAINT IF EXISTS room_pkey;\n",
    "ALTER TABLE ONLY public.room\n",
    "    ADD CONSTRAINT room_pkey PRIMARY KEY (id);"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE ONLY public.reliability DROP CONSTRAINT IF EXISTS reliability_person_fkey;\n",
    "ALTER TABLE ONLY public.reliability\n",
    "    ADD CONSTRAINT reliability_person_fkey FOREIGN KEY (person) REFERENCES public.person(id);"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE ONLY public.sightings DROP CONSTRAINT IF EXISTS sightings_person_fkey;\n",
    "ALTER TABLE ONLY public.sightings\n",
    "    ADD CONSTRAINT sightings_person_fkey FOREIGN KEY (person) REFERENCES public.person(id);"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE ONLY public.sightings DROP CONSTRAINT IF EXISTS sightings_room_fkey;\n",
    "ALTER TABLE ONLY public.sightings\n",
    "    ADD CONSTRAINT sightings_room_fkey FOREIGN KEY (room) REFERENCES public.room(id);"
   ],
   "outputs": []
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE ONLY public.sightings DROP CONSTRAINT IF EXISTS sightings_witness_fkey;\n",
    "ALTER TABLE ONLY public.sightings\n",
    "    ADD CONSTRAINT sightings_witness_fkey FOREIGN KEY (witness) REFERENCES public.person(id);"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "This creates four tables:\n",
    "\n",
    "- `person` – the 20 persons present at the manor\n",
    "- `room` – the rooms of the manor\n",
    "- `sightings` – witness statements: who was seen where, and when\n",
    "- `reliability` – the reliability score (between 0 and 1) of each witness\n",
    "\n",
    "## Step 1: Explore the Database"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Get familiar with the tables, for example through Studio's Schema panel."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Step 2: Build a Sightings Table\n",
    "\n",
    "Design a query that retrieves, for every sighting: the time, the name of the person seen, the name of the witness, and the name of the room. Store the result in a new table `s`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS s CASCADE;\n",
    "CREATE TABLE s AS\n",
    "SELECT\n",
    "  time,\n",
    "  person.name  AS person,\n",
    "  p2.name      AS witness,\n",
    "  room.name    AS room\n",
    "FROM sightings\n",
    "  JOIN person       ON person  = person.id\n",
    "  JOIN person AS p2 ON witness = p2.id\n",
    "  JOIN room         ON room    = room.id;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Step 3: Enable Provenance\n",
    "\n",
    "Activate provenance tracking on the table `s` using [`add_provenance`](https://provsql.org/doxygen-sql/html/group__table__management.html#ga00f0d0b04b2b693c974e72aaf095cb3b):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "SELECT add_provenance('s');"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "A hidden `provsql` column is added that holds a UUID provenance token for each tuple. Run a simple query to see this extra column in the output:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "SELECT * FROM s;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "**Note:**\n",
    "\n",
    "> The `provsql` column behaves specially: you cannot filter or sort on it directly. Use the [`provenance()`](https://provsql.org/doxygen-sql/html/group__provenance__output.html#ga93c314c9412aff767f5f5f994da091c9) function to obtain the current row’s token in expressions.\n",
    "\n",
    "Create a *provenance mapping* that associates each provenance token with the name of the witness who made the sighting, using [`create_provenance_mapping`](https://provsql.org/doxygen-sql/html/group__table__management.html#ga3a351113a8b4687b0acc678f7715cf1b):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS witness_mapping;\n",
    "SELECT create_provenance_mapping('witness_mapping', 's', 'witness');"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "The mapping is stored as an ordinary table – inspect it with `SELECT * FROM witness_mapping;`.\n",
    "\n",
    "## Step 4: Find Contradictions\n",
    "\n",
    "Some witnesses are unreliable: the same person may be reported in two different rooms at the same time – an impossibility. Write a query that identifies all such contradictions."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "SELECT s1.time, s1.person, s1.room\n",
    "FROM s AS s1, s AS s2\n",
    "WHERE s1.person = s2.person\n",
    "  AND s1.time   = s2.time\n",
    "  AND s1.room  <> s2.room;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Step 5: Display Provenance Formulas\n",
    "\n",
    "Extend the previous query by adding `sr_formula(provenance(), 'witness_mapping')` to the `SELECT` clause to see *which witnesses* are responsible for each contradiction.\n",
    "\n",
    "[`sr_formula`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga76c32e829ab40658af1103ffc22717a6) displays the provenance token as a formula, substituting each leaf token with the mapped value from `witness_mapping`."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "SELECT s1.time, s1.person, s1.room,\n",
    "       sr_formula(provenance(), 'witness_mapping')\n",
    "FROM s AS s1, s AS s2\n",
    "WHERE s1.person = s2.person\n",
    "  AND s1.time   = s2.time\n",
    "  AND s1.room  <> s2.room;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Step 6: Build a Consistent Sightings Table\n",
    "\n",
    "Create a table `consistent_s` containing all sightings *except* those identified as contradictions. Display its content along with the provenance formula for each tuple."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS consistent_s CASCADE;\n",
    "CREATE TABLE consistent_s AS\n",
    "SELECT time, person, room FROM s\n",
    "EXCEPT\n",
    "SELECT s1.time, s1.person, s1.room\n",
    "FROM s AS s1, s AS s2\n",
    "WHERE s1.person = s2.person\n",
    "  AND s1.time   = s2.time\n",
    "  AND s1.room  <> s2.room;\n",
    "\n",
    "SELECT *, sr_formula(provenance(), 'witness_mapping')\n",
    "FROM consistent_s;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Look closely at the output: the contradicted sightings are *still there*, annotated with monus formulas of the form `x ⊖ (…)`. This is deliberate – across possible worlds such a row is a real answer whenever its contradicting sightings are absent, so ProvSQL keeps it rather than spend a provenance evaluation filtering it. When you want exactly the rows of the vanilla `EXCEPT` answer, say so explicitly with [`present`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga7f46e475d4a8a199db9a366ac1246a2f):"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "SELECT *, sr_formula(provenance(), 'witness_mapping')\n",
    "FROM consistent_s\n",
    "WHERE provsql.present(provenance());"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "([`nonzero`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga56e444f359bb6eb41c060bde058b7e95) is the general form, testing the annotation against a chosen semiring’s zero; see [the chapter on NULL values and zero-annotated rows](https://provsql.org/docs/user/nulls.html).)\n",
    "\n",
    "## Step 7: Identify Suspects\n",
    "\n",
    "The murder happened between midnight and 8 am in a bedroom. Create a `suspects` table containing every person who was seen (in a consistent sighting) in a bedroom during that window. Display the suspects along with their provenance formula."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "DROP TABLE IF EXISTS suspects CASCADE;\n",
    "CREATE TABLE suspects AS\n",
    "SELECT DISTINCT person\n",
    "FROM consistent_s\n",
    "WHERE room LIKE '% bedroom'\n",
    "  AND time BETWEEN '00:00:00' AND '08:00:00';\n",
    "\n",
    "SELECT *, sr_formula(provenance(), 'witness_mapping')\n",
    "FROM suspects;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Step 8: Count Confirming Sightings\n",
    "\n",
    "Use the counting m-semiring to find how many sightings confirm that each person is a suspect. Add an integer column `count` to `s`, set it to `1` for all rows, and create a `count_mapping`. Then use [`sr_counting`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#gad3e2b6c5dc5d0041fc29ee086add1de6) to display the count for each suspect."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE s ADD COLUMN IF NOT EXISTS count int;\n",
    "UPDATE s SET count = 1;\n",
    "\n",
    "DROP TABLE IF EXISTS count_mapping;\n",
    "SELECT create_provenance_mapping('count_mapping', 's', 'count');\n",
    "\n",
    "SELECT *, sr_counting(provenance(), 'count_mapping') AS c\n",
    "FROM suspects\n",
    "ORDER BY c;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Step 9: Assign Reliability Probabilities\n",
    "\n",
    "Add a `reliability` float column to `s` and populate it with the reliability score of each sighting’s witness. Then assign these scores as the probability of each provenance token using [`set_prob`](https://provsql.org/doxygen-sql/html/group__gate__manipulation.html#ga17334fe1d3969d969eaa18e32a93b4e0)."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "ALTER TABLE s ADD COLUMN IF NOT EXISTS reliability float;\n",
    "\n",
    "UPDATE s\n",
    "SET reliability = score\n",
    "FROM reliability, person\n",
    "WHERE reliability.person = person.id\n",
    "  AND person.name = s.witness;\n",
    "\n",
    "SELECT set_prob(provenance(), reliability) FROM s;"
   ],
   "outputs": []
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Step 10: Find the Murderer\n",
    "\n",
    "The police needs a confidence of at least 0.99 before making an arrest. Use [`probability_evaluate`](https://provsql.org/doxygen-sql/html/group__probability.html#gabffa40fef0e37a75d39d4c39c4a1ec0f) to compute the probability that each suspect was truly present, and identify those above the threshold.\n",
    "\n",
    "[`probability_evaluate`](https://provsql.org/doxygen-sql/html/group__probability.html#gabffa40fef0e37a75d39d4c39c4a1ec0f) accepts an optional second argument for the computation method:\n",
    "\n",
    "- `'possible-worlds'` – exact, by exhaustive enumeration\n",
    "- `'monte-carlo'` – approximate sampling (add a sample count as third argument)\n",
    "- `'tree-decomposition'` – exact, via tree decomposition of the Boolean circuit\n",
    "- `'compilation'` – d-DNNF compilation (add the tool name, e.g. `'d4'`, as third argument)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "provsql": {}
   },
   "source": [
    "SELECT *,\n",
    "       sr_formula(provenance(), 'witness_mapping'),\n",
    "       probability_evaluate(provenance(), 'possible-worlds')\n",
    "FROM suspects\n",
    "WHERE probability_evaluate(provenance(), 'possible-worlds') > 0.99\n",
    "  AND person <> 'Daphine';"
   ],
   "outputs": []
  }
 ]
}
