{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "f987e37f-deef-448a-bab4-0b3247c9e36e",
   "metadata": {},
   "source": [
    "*   [Overview](overview.ipynb)\n",
    "*   [Depth First and Breath First Search](puzzle.ipynb)\n",
    "*   [SAT Solvers](einstein.ipynb)\n",
    "*   [Pattern Recognition and Reinforcement Learning](rock_paper.ipynb)\n",
    "*   [SMT and Model Checkers](#) <--- (You Are Here)\n",
    "    *   [Technical Lingo](#technical-lingo)\n",
    "    *   [Dining Philosophers](#dining-philosophers)\n",
    "    *   [What the Solver Does](#what-the-solver-does)\n",
    "    *   [TLA⁺ model checker](#tla-model-checker)\n",
    "    *   [Other Tools](#other-tools)\n",
    "*   [AlphaZero](alpha_zero.ipynb)\n",
    "*   [The Future](philosophy.ipynb)\n",
    "\n",
    "* * *"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f53941f1-c541-43a4-9ca7-1eff06c15f7a",
   "metadata": {},
   "source": [
    "SMT and Model Checkers[¶](#smt-and-model-checkers \"Permalink to this headline\")\n",
    "===============================================================================\n",
    "\n",
    "The next steps up for tree searchers and SAT solvers:\n",
    "\n",
    "*   State more complex than just truth tables\n",
    "*   Searching a graph instead of a tree\n",
    "*   Temporal logic"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "e35c7f95-a6ba-439c-bd65-66fd3e6f5a2c",
   "metadata": {},
   "source": [
    "Technical Lingo[¶](#technical-lingo \"Permalink to this headline\")\n",
    "-----------------------------------------------------------------\n",
    "\n",
    "Satisfiability Modulo Theories (SMT) Problem\n",
    "\n",
    "Decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cb279bf9-8b52-484b-be88-499499c8a1e0",
   "metadata": {},
   "source": [
    "Dining Philosophers[¶](#dining-philosophers \"Permalink to this headline\")\n",
    "-------------------------------------------------------------------------\n",
    "\n",
    "![_images/dining_philosopher_problem.png](_images/dining_philosopher_problem.png)\n",
    "\n",
    "Core model:\n",
    "\n",
    "```\n",
    "State of one chopstick ∈ { Unused, LeftPhilosopher, RightPhilsopher }\n",
    "\n",
    "State of all chopsticks ∈ {'UUUUU', 'UUUUL', 'UUURL', 'RUURL', ... }\n",
    "\n",
    "Number of possible states:  3⁵ = 243\n",
    "\n",
    "Implied states for a philosopher:\n",
    "    0 chopsticks held ⟶  Thinking\n",
    "    1 chopsticks held ⟶  Trying to eat\n",
    "    2 chopsticks held ⟶  Eating\n",
    "\n",
    "Unconstrained chopstick state transitions:\n",
    "    Unused ⟶  LeftPhilosopher\n",
    "    Unused ⟶  RightPhilsopher\n",
    "    LeftPhilosopher ⟶  Unused\n",
    "    RightPhilsopher ⟶  Unused\n",
    "```\n",
    "\n",
    "Constrain the model with philosopher strategies:\n",
    "\n",
    "```\n",
    "Strategy D:\n",
    "    0 chopsticks held ⟶  AcquireLeft\n",
    "    1 chopsticks held ⟶  AcquireRight\n",
    "    2 chopsticks held ⟶  ReleaseBoth\n",
    "\n",
    "Strategy S:\n",
    "   Philosopher zero always holds left chopstick\n",
    "\n",
    "Strategy H:\n",
    "    0 chopsticks held ∧ no request  ⟶  Enqueue an eat request\n",
    "    0 chopsticks held ∧ requested but not available ⟶  Wait\n",
    "    0 chopsticks held ∧ requested available ⟶  AcquireLeft\n",
    "    1 chopsticks held ⟶  AcquireRight\n",
    "    2 chopsticks held ⟶  ReleaseBoth\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "78bfb7af-2809-4183-ac26-039bb048daa7",
   "metadata": {},
   "source": [
    "\n",
    "What the Solver Does[¶](#what-the-solver-does \"Permalink to this headline\")\n",
    "---------------------------------------------------------------------------\n",
    "\n",
    "The transitions generate a graph.\n",
    "\n",
    "The solver traverses the graph to see if: 1) every state has an exit state – deadlocks 2) every path loop has every philosopher eating – no one starves\n",
    "\n",
    "Unlike the puzzle solvers, we need “temporal operators” that check the relationship between a succession of states:\n",
    "\n",
    "**Predicate P is always true.**\n",
    "\n",
    "> A chopstick is held by 0 or 1 philosophers\n",
    "\n",
    "**Predicate P is eventually true**\n",
    "\n",
    "> A philosopher with a left chopstick eventually gets a right one\n",
    "\n",
    "**Predicate P is always eventually true**\n",
    "\n",
    "> After eating, a philosopher is always able to eat again\n",
    "\n",
    "For example:\n",
    "```\n",
    "UUUUU -> ... -> UURLU ->  ULUUU -> ... -> UURLU -> ...\n",
    "                   ^                         ^\n",
    "                   |                         |\n",
    "                P₃ eats   P₃ thinks       P₃ eats\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "959ef0c3-a147-489d-a5e0-af2c7697c15f",
   "metadata": {
    "jp-MarkdownHeadingCollapsed": true,
    "tags": []
   },
   "source": [
    "TLA⁺ model checker[¶](#tla-model-checker \"Permalink to this headline\")\n",
    "----------------------------------------------------------------------\n",
    "\n",
    "The TLA⁺ model checker generate the contrained graph, follows all paths, and checks all of the temporal invariants.\n",
    "\n",
    "Here’s [PlusCal](https://lamport.azurewebsites.net/tla/p-manual.pdf) model for the dining philosophers problem.\n",
    "\n",
    "![_images/dining_round_tla.png](_images/dining_round_tla.png)\n",
    "\n",
    "For a nice write-up on using TLA⁺ for the dining philosophers problem see the blog post by Murat Demirbas at [http://muratbuffalo.blogspot.com/2016/10/modeling-dining-philosophers-algorithm.html](http://muratbuffalo.blogspot.com/2016/10/modeling-dining-philosophers-algorithm.html)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cc1bc12a-e1d4-4376-9da6-2e772182f385",
   "metadata": {},
   "source": [
    "Other Tools[¶](#other-tools \"Permalink to this headline\")\n",
    "---------------------------------------------------------\n",
    "\n",
    "The **Z3Py** package lets you drive Microsoft’s Z3 solver, a production ready powerful SMT solver.\n",
    "\n",
    "To get started, see this tutorial: [https://ericpony.github.io/z3py-tutorial/guide-examples.htm](https://ericpony.github.io/z3py-tutorial/guide-examples.htm)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "1fee6d98-9785-4345-911d-2f5de0d33561",
   "metadata": {},
   "source": [
    "| [<<< Previous](rock_paper.ipynb \"Pattern Recognition and Reinforcement Learning\") | [Next >>>](alpha_zero.ipynb \"AlphaZero\") |\n",
    "|                                  :-:                                              |              :-:                    |\n",
    "\n",
    "* * *\n",
    "\n",
    "© Copyright 2019, Raymond Hettinger"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3 (ipykernel)",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}