src/test_demos/Demo4-Scripted Model Construction.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Demo4 - Scripted Model Construction\n",
    "\n",
    "This demo illustrates the usage of sripted model consturction of pyuppaal, constructing the [model](https://github.com/Jack0Chan/pyuppaal/blob/main/src/test_unit/constructed_model1.xml) shown below:\n",
    "\n",
    "<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/scripted_model_building.png width=800 />"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 1. Setup Pyuppaal"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "import os\n",
    "import pyuppaal\n",
    "from pyuppaal.nta import Template, Location, Edge\n",
    "\n",
    "# pyuppaal.set_verifyta_path(r\"C:\\Users\\10262\\Documents\\GitHub\\cav2024\\bin\\uppaal64-4.1.26\\bin-Windows\\verifyta.exe\")\n",
    "pyuppaal.set_verifyta_path(r\"/Users/chenguangyao/Documents/GitHub/uppaal64-5.0.0/bin-Darwin/verifyta\")"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 2. Create New Model File with declaration.\n",
    "\n",
    "<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/scripted_model_building_declarations.png width=400 />"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "model_path = 'constructed_model1.xml'\n",
    "os.remove(model_path)\n",
    "umodel = pyuppaal.UModel.new(model_path)\n",
    "\n",
    "umodel.declaration = \"\"\"// Place global declarations here.\n",
    "broadcast chan a, b, c;\n",
    "int count = 0;\n",
    "int sender_count = 0;\n",
    "const int rec_end = 10;\\n\"\"\""
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 3. Construct Receiver Template\n",
    "\n",
    "<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/scripted_model_building_receiver.png width=500 />"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [],
   "source": [
    "# region: 构建tempaltes，一共两个\n",
    "# region: 构建第1个template\n",
    "template0 = Template(name=\"Receiver\",\n",
    "                        locations=[],\n",
    "                        init_ref=0,\n",
    "                        edges=[],\n",
    "                        params=\"broadcast chan &param1, broadcast chan &param2, int inv_start, int guard_start\",\n",
    "                        declaration=\"\"\"// Place local declarations here.\\nclock t;\"\"\")\n",
    "# 构造locations\n",
    "# l0 是initial location\n",
    "l0 = Location(location_id=0, location_pos=(-391, -102),\n",
    "                name=\"Start\", name_pos=(-401, -136),\n",
    "                invariant=\"t<=inv_start\", invariant_pos=(-401, -85),\n",
    "                test_code_on_enter=\"count ++;\", test_code_on_exit=\"count = 10;\",\n",
    "                is_initial=True)\n",
    "l1 = Location(location_id=1, location_pos=(-170, -102),\n",
    "                invariant=\"t<=200\", invariant_pos=(-178, -76),\n",
    "                rate_of_exponential=0.8, rate_of_exp_pos=(-179, -93))\n",
    "l2 = Location(location_id=2, location_pos=(-42, -93), is_urgent=True)\n",
    "l3 = Location(location_id=3, location_pos=(-76, -212), is_committed=True)\n",
    "l4 = Location(location_id=4, location_pos=(25, -212),\n",
    "                name=\"End1\", name_pos=(15, -246))\n",
    "l5 = Location(location_id=5, location_pos=(51, -93),\n",
    "                name=\"End2\", name_pos=(41, -127),\n",
    "                comments=\"备注End2\", comments_pos=(42, -34))\n",
    "\n",
    "# 构造branch points\n",
    "bp0 = Location(location_id=6, location_pos=(-119, -144),\n",
    "                is_branchpoint=True)\n",
    "\n",
    "template0.locations = [l0, l1, l2, l3, l4, l5, bp0]\n",
    "\n",
    "# 构造edges\n",
    "e0 = Edge(source_location_id=2, source_location_pos=(-42, -93),\n",
    "            target_location_id=5, target_location_pos=(34, -93),\n",
    "            sync=\"param2?\", sync_pos=(-24, -110),\n",
    "            update=\"t=888\", update_pos=(-24, -93))\n",
    "e1 = Edge(source_location_id=3, source_location_pos=(-76, -212),\n",
    "            target_location_id=4, target_location_pos=(25, -212),\n",
    "            sync=\"param1?\", sync_pos=(-58, -229),\n",
    "            update=\"t=999\", update_pos=(-51, -212))\n",
    "e2 = Edge(source_location_id=6, source_location_pos=(-119, -144),\n",
    "            target_location_id=3, target_location_pos=(-76, -212),\n",
    "            probability_weight=0.2, prob_weight_pos=(-93, -178))\n",
    "e3 = Edge(source_location_id=6, source_location_pos=(-119, -144),\n",
    "            target_location_id=2, target_location_pos=(-42, -93),\n",
    "            probability_weight=0.8, prob_weight_pos=(-93, -119))\n",
    "e4 = Edge(source_location_id=1, source_location_pos=(-178, -102),\n",
    "            target_location_id=6, target_location_pos=(-119, -144))\n",
    "e5 = Edge(source_location_id=0, source_location_pos=(-391, -102),\n",
    "            target_location_id=1, target_location_pos=(-178, -102),\n",
    "            guard=\"t>= guard_start\", guard_pos=(-331, -102),\n",
    "            update=\"count ++\", update_pos=(-306, -85),\n",
    "            test_code=\"count == -1;\")\n",
    "template0.edges = [e0, e1, e2, e3, e4, e5]\n",
    "# template0.branch_points = [bp0]\n",
    "# endregion"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 4. Construct Sender Template\n",
    "\n",
    "<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/scripted_model_building_sender.png width=500 />"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "# region: 构建第2个template\n",
    "template1 = Template(name=\"Sender\",\n",
    "                        locations=[],\n",
    "                        init_ref=7,\n",
    "                        edges=[],\n",
    "                        params=\"broadcast chan &param1, broadcast chan &param2\",\n",
    "                        declaration=None)\n",
    "\n",
    "# 构造locations\n",
    "l7 = Location(location_id=7, location_pos=(-459, -34),\n",
    "                name=\"Start\", name_pos=(-493, -68),\n",
    "                test_code_on_enter=\"sender_count = 10;\",\n",
    "                test_code_on_exit=\"sender_count = -1;\",\n",
    "                comments=\"\"\"Start:\\nTestCode\"\"\", comments_pos=(-469, 25),\n",
    "                is_initial=True)\n",
    "l8 = Location(location_id=8, location_pos=(-187, -102))\n",
    "l9 = Location(location_id=9, location_pos=(-178, 17))\n",
    "# l10 = Location(location_id=10,location_pos=(-323,-34))\n",
    "\n",
    "# 构造branch points\n",
    "bp1 = Location(location_id=10, location_pos=(-323, -34),\n",
    "                is_branchpoint=True)\n",
    "\n",
    "template1.locations = [l7, l8, l9, bp1]\n",
    "\n",
    "# 构造edges\n",
    "e6 = Edge(source_location_id=10, source_location_pos=(-323, -34),\n",
    "            target_location_id=9, target_location_pos=(-178, 17),\n",
    "            sync=\"param2!\", sync_pos=(-305, -34))\n",
    "e7 = Edge(source_location_id=10, source_location_pos=(-323, -34),\n",
    "            target_location_id=8, target_location_pos=(-187, -102),\n",
    "            sync=\"param1!\", sync_pos=(-305, -80),\n",
    "            probability_weight=0.8, prob_weight_pos=(-305, -51))\n",
    "e8 = Edge(source_location_id=7, source_location_pos=(-459, -34),\n",
    "            target_location_id=10, target_location_pos=(-323, -34),\n",
    "            nails=[(-382, -136)])\n",
    "template1.edges = [e6, e7, e8]\n",
    "# print(template1.edges)\n",
    "\n",
    "# template1.branch_points = [bp1]\n",
    "# endregion\n",
    "# endregion 构造templates\n",
    "\n",
    "umodel.templates = [template0, template1]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 5. Set System and Queries\n",
    "\n",
    "<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/scripted_model_building_systems.png width=400 />\n",
    "<img src=https://raw.githubusercontent.com/Jack0Chan/pyuppaal/main/src/test_demos/figs/scripted_model_building_queries.png width=400 />"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "umodel.system = \"\"\"// Place template instantiations here.\n",
    "rec = Receiver(a, b, 10, rec_end);\n",
    "sender = Sender(a, b);\n",
    "// List one or more processes to be composed into a system.\n",
    "system rec, sender;\\n\"\"\"\n",
    "umodel.queries = [\"E<> sender_count == 10\",\n",
    "                    \"E<> count == 1\",\n",
    "                    \"E<> rec.End1\",\n",
    "                    \"E<> rec.t >= 10\",\n",
    "                    \"A[] not deadlock\"]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 6. Verify and Easy Verify"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "umodel.verify() results: \n",
      "Options for the verification:\n",
      "  Generating shortest trace\n",
      "  Search order is breadth first\n",
      "  Using conservative space optimisation\n",
      "  Seed is 1715652637\n",
      "  State space representation uses minimal constraint systems with future testing\n",
      "  Using HashMap + Compress integers for discrete state storage\n",
      "\u001b[2K\n",
      "Verifying formula 1 at /nta/queries/query[1]/formula\n",
      " -- Formula: E<> sender_count == 10\n",
      "\u001b[2K -- Formula is NOT satisfied.\n",
      "\u001b[2K\n",
      "Verifying formula 2 at /nta/queries/query[2]/formula\n",
      " -- Formula: E<> count == 1\n",
      "\u001b[2K -- Formula is satisfied.\n",
      " -- Writing witness trace to constructed_model1_xtr-2\n",
      "\u001b[2K\n",
      "Verifying formula 3 at /nta/queries/query[3]/formula\n",
      " -- Formula: E<> rec.End1\n",
      "\u001b[2K -- Formula is satisfied.\n",
      " -- Writing witness trace to constructed_model1_xtr-3\n",
      "\u001b[2K\n",
      "Verifying formula 4 at /nta/queries/query[4]/formula\n",
      " -- Formula: E<> rec.t >= 10\n",
      "\u001b[2K -- Formula is satisfied.\n",
      " -- Writing witness trace to constructed_model1_xtr-4\n",
      "\u001b[2K\n",
      "Verifying formula 5 at /nta/queries/query[5]/formula\n",
      " -- Formula: A[] not deadlock\n",
      "\u001b[2K -- Formula is NOT satisfied.\n",
      " -- Writing witness trace to constructed_model1_xtr-5\n",
      "\n",
      "umodel.easy_verify().untime_pattern: (easy_verify() will only return the trace of the FIRST query.)\n",
      "['E<> rec.End1']\n",
      "\n",
      "State: rec.Start sender.Start count=0 sender_count=0 rec.inv_start=10 rec.guard_start=10 #t(0)-#time<=0 #t(0)-rec.t<=0 #time-#t(0)<=10 #time-rec.t<=0 rec.t-#time<=0 \n",
      "\n",
      "Transition: rec._id2 -> rec.End2 {1; param2?; t = 888;} \n",
      "\n",
      "State: rec._id1 sender.Start count=1 sender_count=0 rec.inv_start=10 rec.guard_start=10 #t(0)-#time<=-10 #t(0)-rec.t<=0 #time-#t(0)<=200 #time-rec.t<=0 rec.t-#time<=0 \n",
      "\n",
      "Transition: rec._id1 -> rec._id3 {1; 0; 1, 1;} rec.Start -> rec._id1 {t >= guard_start; 0; count++;} \n",
      "\n",
      "State: rec._id3 sender.Start count=1 sender_count=0 rec.inv_start=10 rec.guard_start=10 #t(0)-#time<=-10 #t(0)-rec.t<=0 #time-#t(0)<=200 #time-rec.t<=0 rec.t-#time<=0 \n",
      "\n",
      "Transition: sender.Start -> sender._id8 {1; param1!; 1, 1;} sender._id2 -> sender.End2 {1; param2?; t = 888;} rec._id3 -> rec.End1 {1; param1?; t = 999;} \n",
      "\n",
      "State: rec.End1 sender._id8 count=1 sender_count=0 rec.inv_start=10 rec.guard_start=10 #t(0)-#time<=0 #t(0)-rec.t<=-999 #time-rec.t<=-799 rec.t-#time<=989 \n",
      "\n"
     ]
    }
   ],
   "source": [
    "print(\"umodel.verify() results: \")\n",
    "print(umodel.verify())\n",
    "\n",
    "print(\"umodel.easy_verify().untime_pattern: (easy_verify() will only return the trace of the FIRST query.)\")\n",
    "# easy_verify() only aceepts ONE query.\n",
    "tmp_new_model = umodel.copy_as('tmp_new.xml')\n",
    "tmp_new_model.queries = \"E<> rec.End1\"\n",
    "print(tmp_new_model.queries)\n",
    "st = tmp_new_model.easy_verify(keep_tmp_file=True).raw\n",
    "print(st)\n",
    "# assert last state of st is rec.End1\n",
    "# os.remove('tmp_new.xml')\n",
    "# print(tmp_new_model.easy_verify(keep_tmp_file=True).untime_pattern)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 7. Check Correctness"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "target_model = pyuppaal.UModel(\"test_umodel_build.xml\")\n",
    "\n",
    "assert \"E<> sender_count == 10\" == umodel.queries[0]\n",
    "assert umodel.queries == target_model.queries\n",
    "assert umodel.system == target_model.system\n",
    "assert umodel.declaration == target_model.declaration\n",
    "assert umodel.templates[0].xml == target_model.templates[0].xml\n",
    "assert umodel.templates[1].xml == target_model.templates[1].xml\n",
    "assert umodel.xml == target_model.xml\n",
    "assert \"Verifying formula\" in umodel.verify()"
   ]
  }
 ],
 "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.9.18"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 2
}