tla_lightning.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "These are the two examples from the presentation, runnable online via the magnificent [TLA+ kernel for Jupyter by Stas Kelvich](https://github.com/kelvich/tlaplus_jupyter).\n",
    "\n",
    "For additional details and the full presentation, please check the accompanying repository."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## A very simple example, finite state machine\n",
    "\n",
    "This is a very simple, finite, state machine in TLA+ You may recognise the tune"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [],
   "source": [
    "------------------------------- MODULE ThemeSong -------------------------------\n",
    "\n",
    "EXTENDS Integers\n",
    "\n",
    "VARIABLES s, count\n",
    "\n",
    "vars == <<s, count>>\n",
    "\n",
    "Sinit == s = \"na\" /\\ count = 2\n",
    "\n",
    "Na == s' = \"na\" /\\ count' = count - 1\n",
    "ToB == s' = \"Batman\" /\\ count' = 0\n",
    "\n",
    "Snext == IF count > 0 THEN /\\ ( Na \\/ ToB)\n",
    "                      ELSE /\\ ToB\n",
    "\n",
    "Spec == Sinit /\\ [][Snext]_vars /\\ WF_vars(ToB)\n",
    "\n",
    "Batman == s = \"Batman\" /\\ count = 0\n",
    "\n",
    "Liveness == <>Batman\n",
    "\n",
    "=============================================================================\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)\n",
      "Running breadth-first search Model-Checking with fp 70 and seed 8061182049641924230 with 4 workers on 4 cores with 3641MB heap and 64MB offheap memory (Mac OS X 10.14.6 x86_64, Oracle Corporation 1.8.0_192 x86_64, MSBDiskFPSet, DiskStateQueue).\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/tmpi73fvaod/ThemeSong.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/Integers.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/Naturals.tla\n",
      "Semantic processing of module Naturals\n",
      "Semantic processing of module Integers\n",
      "Semantic processing of module ThemeSong\n",
      "Starting... (2020-01-06 20:58:38)\n",
      "Implied-temporal checking--satisfiability problem has 1 branches.\n",
      "Computing initial states...\n",
      "Finished computing initial states: 1 distinct state generated at 2020-01-06 20:58:38.\n",
      "Progress(3) at 2020-01-06 20:58:38: 7 states generated, 4 distinct states found, 0 states left on queue.\n",
      "Checking temporal properties for the complete state space with 4 total distinct states at (2020-01-06 20:58:38)\n",
      "Finished checking temporal properties in 00s at 2020-01-06 20:58:38\n",
      "Model checking completed. No error has been found.\n",
      "  Estimates of the probability that TLC did not check all reachable states\n",
      "  because two distinct states had the same fingerprint:\n",
      "  calculated (optimistic):  val = 6.5E-19\n",
      "7 states generated, 4 distinct states found, 0 states left on queue.\n",
      "The depth of the complete state graph search is 3.\n",
      "The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).\n",
      "Finished in 00s at (2020-01-06 20:58:38)\n"
     ]
    }
   ],
   "source": [
    "%tlc:ThemeSong\n",
    "SPECIFICATION Spec\n",
    "PROPERTIES Liveness"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Below, we rewrite it as Pluscal \"P\" variant, and get the auto-generated TLA code"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "---------------------------- MODULE ThemeSongPC ----------------------------\n",
    "\n",
    "EXTENDS Integers\n",
    "\n",
    "(*--fair algorithm ThemeSong\n",
    "    variables count = 5, s = \"na\"\n",
    "    begin ThemeSong:\n",
    "        while count > 0 do\n",
    "            either\n",
    "                s := \"Batman\";\n",
    "                count := 0;\n",
    "            or\n",
    "                s := \"na\";\n",
    "                count := count - 1;\n",
    "            end either;\n",
    "        end while;\n",
    "        if count = 0 then\n",
    "            s := \"Batman\";\n",
    "        end if;\n",
    "    end algorithm; -*)\n",
    "\n",
    "\\* BEGIN TRANSLATION\n",
    "VARIABLES count, s, pc\n",
    "\n",
    "vars == << count, s, pc >>\n",
    "\n",
    "Init == (* Global variables *)\n",
    "        /\\ count = 5\n",
    "        /\\ s = \"na\"\n",
    "        /\\ pc = \"ThemeSong\"\n",
    "\n",
    "ThemeSong == /\\ pc = \"ThemeSong\"\n",
    "             /\\ IF count > 0\n",
    "                   THEN /\\ \\/ /\\ s' = \"Batman\"\n",
    "                              /\\ count' = 0\n",
    "                           \\/ /\\ s' = \"na\"\n",
    "                              /\\ count' = count - 1\n",
    "                        /\\ pc' = \"ThemeSong\"\n",
    "                   ELSE /\\ IF count = 0\n",
    "                              THEN /\\ s' = \"Batman\"\n",
    "                              ELSE /\\ TRUE\n",
    "                                   /\\ s' = s\n",
    "                        /\\ pc' = \"Done\"\n",
    "                        /\\ count' = count\n",
    "\n",
    "(* Allow infinite stuttering to prevent deadlock on termination. *)\n",
    "Terminating == pc = \"Done\" /\\ UNCHANGED vars\n",
    "\n",
    "Next == ThemeSong\n",
    "           \\/ Terminating\n",
    "\n",
    "Spec == /\\ Init /\\ [][Next]_vars\n",
    "        /\\ WF_vars(Next)\n",
    "\n",
    "Termination == <>(pc = \"Done\")\n",
    "\n",
    "\\* END TRANSLATION\n",
    "\n",
    "Batman == s = \"Batman\" /\\ count = 0\n",
    "\n",
    "Liveness == <>Batman\n",
    "\n",
    "\n",
    "=============================================================================\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)\n",
      "Running breadth-first search Model-Checking with fp 122 and seed 7166269695903366348 with 4 workers on 4 cores with 3641MB heap and 64MB offheap memory (Mac OS X 10.14.6 x86_64, Oracle Corporation 1.8.0_192 x86_64, MSBDiskFPSet, DiskStateQueue).\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/tmpp6tpplur/ThemeSongPC.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/Integers.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/Naturals.tla\n",
      "Semantic processing of module Naturals\n",
      "Semantic processing of module Integers\n",
      "Semantic processing of module ThemeSongPC\n",
      "Starting... (2020-01-06 20:58:40)\n",
      "Implied-temporal checking--satisfiability problem has 1 branches.\n",
      "Computing initial states...\n",
      "Finished computing initial states: 1 distinct state generated at 2020-01-06 20:58:41.\n",
      "Progress(6) at 2020-01-06 20:58:41: 14 states generated, 8 distinct states found, 0 states left on queue.\n",
      "Checking temporal properties for the complete state space with 8 total distinct states at (2020-01-06 20:58:41)\n",
      "Finished checking temporal properties in 00s at 2020-01-06 20:58:41\n",
      "Model checking completed. No error has been found.\n",
      "  Estimates of the probability that TLC did not check all reachable states\n",
      "  because two distinct states had the same fingerprint:\n",
      "  calculated (optimistic):  val = 2.6E-18\n",
      "14 states generated, 8 distinct states found, 0 states left on queue.\n",
      "The depth of the complete state graph search is 6.\n",
      "The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 2 and the 95th percentile is 2).\n",
      "Finished in 01s at (2020-01-06 20:58:41)\n"
     ]
    }
   ],
   "source": [
    "%tlc:ThemeSongPC\n",
    "SPECIFICATION Spec\n",
    "PROPERTIES Liveness"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## A very simple actor model example\n",
    "\n",
    "A very simple (Akka based) actor that on a message triggers a third party would look like the following in Scala\n",
    "\n",
    "```scala\n",
    "case class Trigger(payload: Payload)\n",
    "\n",
    "class SimpleActor extends Actor {\n",
    "  def receive = {\n",
    "    case Trigger(payload) => ThirdParty().trigger(payload)\n",
    "    case _                => log.warn(\"Duh\")\n",
    "  }\n",
    "}\n",
    "```"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We need to simulate the inboxes that the actor system offers, and simulate the mailbox by the actor fetching messages itself. Below you can see the PlusCal \"C\" code, followed by the TLA+ automated translation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "------------------------------- MODULE Actor -------------------------------\n",
    "\n",
    "EXTENDS TLC, Integers, Sequences\n",
    "\n",
    "(*--fair algorithm ActorStuff {\n",
    "\n",
    "variables actorInboxes = [ actor |-> <<>> ];\n",
    "          triggered = FALSE;\n",
    "\n",
    "procedure trigger(trigger_content=\"?\") {\n",
    "    triggerLabel:\n",
    "      triggered := TRUE;\n",
    "      return;\n",
    "}\n",
    "\n",
    "fair process (actor = \"actor\")\n",
    "variables currentMessage = <<\"?\", \"no_content\">>;\n",
    "  kind = \"?\";\n",
    "  content = \"no_content\";\n",
    "{\n",
    "  Send:\n",
    "    actorInboxes[\"actor\"] := Append(actorInboxes[\"actor\"], <<\"trigger\", \"foo\">>);\n",
    "  WaitForMessages:+\n",
    "    while (TRUE) {\n",
    "      if (actorInboxes[\"actor\"] /= <<>>) {\n",
    "         currentMessage := Head(actorInboxes[\"actor\"]);               \n",
    "         content := Head(Tail(currentMessage));\n",
    "         kind := Head(currentMessage);\n",
    "         actorInboxes[\"actor\"] := Tail(actorInboxes[\"actor\"]);\n",
    "        };\n",
    "        ProcessMessage:\n",
    "         if (kind = \"trigger\") {\n",
    "           call trigger(content);\n",
    "         }\n",
    "    }\n",
    "}\n",
    "\n",
    "}\n",
    "*)\n",
    "\\* BEGIN TRANSLATION\n",
    "VARIABLES actorInboxes, triggered, pc, stack, trigger_content, currentMessage, \n",
    "          kind, content\n",
    "\n",
    "vars == << actorInboxes, triggered, pc, stack, trigger_content, \n",
    "           currentMessage, kind, content >>\n",
    "\n",
    "ProcSet == {\"actor\"}\n",
    "\n",
    "Init == (* Global variables *)\n",
    "        /\\ actorInboxes = [ actor |-> <<>> ]\n",
    "        /\\ triggered = FALSE\n",
    "        (* Procedure trigger *)\n",
    "        /\\ trigger_content = [ self \\in ProcSet |-> \"?\"]\n",
    "        (* Process actor *)\n",
    "        /\\ currentMessage = <<\"?\", \"no_content\">>\n",
    "        /\\ kind = \"?\"\n",
    "        /\\ content = \"no_content\"\n",
    "        /\\ stack = [self \\in ProcSet |-> << >>]\n",
    "        /\\ pc = [self \\in ProcSet |-> \"Send\"]\n",
    "\n",
    "triggerLabel(self) == /\\ pc[self] = \"triggerLabel\"\n",
    "                      /\\ triggered' = TRUE\n",
    "                      /\\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]\n",
    "                      /\\ trigger_content' = [trigger_content EXCEPT ![self] = Head(stack[self]).trigger_content]\n",
    "                      /\\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]\n",
    "                      /\\ UNCHANGED << actorInboxes, currentMessage, kind, \n",
    "                                      content >>\n",
    "\n",
    "trigger(self) == triggerLabel(self)\n",
    "\n",
    "Send == /\\ pc[\"actor\"] = \"Send\"\n",
    "        /\\ actorInboxes' = [actorInboxes EXCEPT ![\"actor\"] = Append(actorInboxes[\"actor\"], <<\"trigger\", \"foo\">>)]\n",
    "        /\\ pc' = [pc EXCEPT ![\"actor\"] = \"WaitForMessages\"]\n",
    "        /\\ UNCHANGED << triggered, stack, trigger_content, currentMessage, \n",
    "                        kind, content >>\n",
    "\n",
    "WaitForMessages == /\\ pc[\"actor\"] = \"WaitForMessages\"\n",
    "                   /\\ IF actorInboxes[\"actor\"] /= <<>>\n",
    "                         THEN /\\ currentMessage' = Head(actorInboxes[\"actor\"])\n",
    "                              /\\ content' = Head(Tail(currentMessage'))\n",
    "                              /\\ kind' = Head(currentMessage')\n",
    "                              /\\ actorInboxes' = [actorInboxes EXCEPT ![\"actor\"] = Tail(actorInboxes[\"actor\"])]\n",
    "                         ELSE /\\ TRUE\n",
    "                              /\\ UNCHANGED << actorInboxes, currentMessage, \n",
    "                                              kind, content >>\n",
    "                   /\\ pc' = [pc EXCEPT ![\"actor\"] = \"ProcessMessage\"]\n",
    "                   /\\ UNCHANGED << triggered, stack, trigger_content >>\n",
    "\n",
    "ProcessMessage == /\\ pc[\"actor\"] = \"ProcessMessage\"\n",
    "                  /\\ IF kind = \"trigger\"\n",
    "                        THEN /\\ /\\ stack' = [stack EXCEPT ![\"actor\"] = << [ procedure |->  \"trigger\",\n",
    "                                                                            pc        |->  \"WaitForMessages\",\n",
    "                                                                            trigger_content |->  trigger_content[\"actor\"] ] >>\n",
    "                                                                        \\o stack[\"actor\"]]\n",
    "                                /\\ trigger_content' = [trigger_content EXCEPT ![\"actor\"] = content]\n",
    "                             /\\ pc' = [pc EXCEPT ![\"actor\"] = \"triggerLabel\"]\n",
    "                        ELSE /\\ pc' = [pc EXCEPT ![\"actor\"] = \"WaitForMessages\"]\n",
    "                             /\\ UNCHANGED << stack, trigger_content >>\n",
    "                  /\\ UNCHANGED << actorInboxes, triggered, currentMessage, \n",
    "                                  kind, content >>\n",
    "\n",
    "actor == Send \\/ WaitForMessages \\/ ProcessMessage\n",
    "\n",
    "(* Allow infinite stuttering to prevent deadlock on termination. *)\n",
    "Terminating == /\\ \\A self \\in ProcSet: pc[self] = \"Done\"\n",
    "               /\\ UNCHANGED vars\n",
    "\n",
    "Next == actor\n",
    "           \\/ (\\E self \\in ProcSet: trigger(self))\n",
    "           \\/ Terminating\n",
    "\n",
    "Spec == /\\ Init /\\ [][Next]_vars\n",
    "        /\\ WF_vars(Next)\n",
    "        /\\ WF_vars(actor) /\\ SF_vars(WaitForMessages) /\\ WF_vars(trigger(\"actor\"))\n",
    "\n",
    "Termination == <>(\\A self \\in ProcSet: pc[self] = \"Done\")\n",
    "\n",
    "\\* END TRANSLATION\n",
    "\n",
    "Triggered == triggered = TRUE\n",
    "\n",
    "Liveness == <>Triggered\n",
    "\n",
    "=============================================================================\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "And we check that eventually the third party is triggered, in the following specification property check"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "TLC2 Version 2.14 of 10 July 2019 (rev: 0cae24f)\n",
      "Running breadth-first search Model-Checking with fp 121 and seed -2385201558344987953 with 4 workers on 4 cores with 3641MB heap and 64MB offheap memory (Mac OS X 10.14.6 x86_64, Oracle Corporation 1.8.0_192 x86_64, MSBDiskFPSet, DiskStateQueue).\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/tmp6u3mw1hj/Actor.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/TLC.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/Integers.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/Sequences.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/Naturals.tla\n",
      "Parsing file /private/var/folders/dh/0s4sld5s23x9mvcl87x1y6_w0000gn/T/FiniteSets.tla\n",
      "Semantic processing of module Naturals\n",
      "Semantic processing of module Sequences\n",
      "Semantic processing of module FiniteSets\n",
      "Semantic processing of module TLC\n",
      "Semantic processing of module Integers\n",
      "Semantic processing of module Actor\n",
      "Starting... (2020-01-06 20:58:42)\n",
      "Implied-temporal checking--satisfiability problem has 1 branches.\n",
      "Computing initial states...\n",
      "Finished computing initial states: 1 distinct state generated at 2020-01-06 20:58:43.\n",
      "Progress(7) at 2020-01-06 20:58:43: 8 states generated, 7 distinct states found, 0 states left on queue.\n",
      "Checking temporal properties for the complete state space with 7 total distinct states at (2020-01-06 20:58:43)\n",
      "Finished checking temporal properties in 00s at 2020-01-06 20:58:43\n",
      "Model checking completed. No error has been found.\n",
      "  Estimates of the probability that TLC did not check all reachable states\n",
      "  because two distinct states had the same fingerprint:\n",
      "  calculated (optimistic):  val = 3.8E-19\n",
      "8 states generated, 7 distinct states found, 0 states left on queue.\n",
      "The depth of the complete state graph search is 7.\n",
      "The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 1 and the 95th percentile is 1).\n",
      "Finished in 00s at (2020-01-06 20:58:43)\n"
     ]
    }
   ],
   "source": [
    "%tlc:Actor\n",
    "SPECIFICATION Spec\n",
    "PROPERTY Liveness"
   ]
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "TLA⁺",
   "language": "tla",
   "name": "tlaplus_jupyter"
  },
  "language_info": {
   "codemirror_mode": "tlaplus",
   "file_extension": ".tla",
   "mimetype": "text/x-tlaplus",
   "name": "tlaplus"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}