{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "85001897",
   "metadata": {},
   "source": [
    "# Reals and Floats in ProB\n",
    "\n",
    "### Michael Leuschel\n"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "42473a5e",
   "metadata": {},
   "source": [
    "## Classical B\n",
    "\n",
    "In Atelier-B the following two types were added to the B language:\n",
    "* REAL\n",
    "* FLOAT\n",
    "\n",
    "ProB treats these keywords as synonyms for a new base type.\n",
    "The current representation in ProB are floating point numbers; but this\n",
    "will probably change in the future, at least for the REAL type.\n",
    "\n",
    "One can now also use literals in decimal point notation for REAL and FLOAT."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "cf76baf3",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$1.0$"
      ],
      "text/plain": [
       "1.0"
      ]
     },
     "execution_count": 5,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "1.0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "941433ba",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$"
      ],
      "text/plain": [
       "TRUE"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "1.0 : REAL & 1.0 : FLOAT"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6caf3504",
   "metadata": {},
   "source": [
    "### Conversion Operators\n",
    "The following conversion operators are available in classical B:\n",
    "* floor\n",
    "* ceiling\n",
    "* real"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 22,
   "id": "8925f6fe",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$2.0$"
      ],
      "text/plain": [
       "2.0"
      ]
     },
     "execution_count": 22,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "real(2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 23,
   "id": "bbd73954",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$2$"
      ],
      "text/plain": [
       "2"
      ]
     },
     "execution_count": 23,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "floor(2.2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 24,
   "id": "838ea786",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$3$"
      ],
      "text/plain": [
       "3"
      ]
     },
     "execution_count": 24,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ceiling(2.2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 25,
   "id": "ee31f934",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$-2$"
      ],
      "text/plain": [
       "−2"
      ]
     },
     "execution_count": 25,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ceiling(-2.2)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "f7398e0e",
   "metadata": {},
   "source": [
    "### Arithmetic Operators\n",
    "\n",
    "The documentation of Atelier-B is not entirely consistent according to which\n",
    "operators to use.\n",
    "In ProB you can use the standard arithmetic operators also for\n",
    "floats:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "65a66ec9",
   "metadata": {
    "vscode": {
     "languageId": "plaintext"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$2.0$"
      ],
      "text/plain": [
       "2.0"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "1.0 + 1.0"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "35ce95d5",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{FALSE}$"
      ],
      "text/plain": [
       "FALSE"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "2.0 * 2.0 < 2.1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "531aa72d",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{FALSE}$"
      ],
      "text/plain": [
       "FALSE"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "2.0 * 2.0 < 2.0 + 2.0"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "9066aa50",
   "metadata": {},
   "source": [
    "You can control whether to allow arithmetic operators for reals\n",
    "in ProB via the preference ```ALLOW_REALS```.\n",
    "By default reals are allowed for classical B and disallowed for Event-B.\n",
    "The only disadvantage of allowing reals is that the arithmetic operators\n",
    "are overloaded, which may require stronger typing.\n",
    "E.g., without ```x:INT``` you get an error that the type of x and y cannot be inferred, when reals are allowed:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "528e647d",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{x} = -1$\n",
       "* $\\mathit{y} = 0$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tx = −1\n",
       "\ty = 0"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x:INT & x < y"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "02b86510",
   "metadata": {},
   "source": [
    "### Constraint solving\n",
    "\n",
    "Constraint solving and enumeration is very limited in ProB.\n",
    "This will change in future.\n",
    "Currently ProB will enumerate a few random values for unspecified reals,\n",
    "and then stop with an enumeration warning."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "id": "9356ea2c",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{x} = 0.0$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tx = 0.0"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x:REAL"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "b6d8671d",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{x} = 1.0$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tx = 1.0"
      ]
     },
     "execution_count": 8,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "x + 1.0 = 2.0"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "13388af0",
   "metadata": {},
   "source": [
    "### Other Operators\n",
    "\n",
    "The standard library ```LibraryReals.def``` provides many functions\n",
    "over reals as external functions.\n",
    "These functions typically start with a capital R.\n",
    "The functions are available in the REPL (aka console) but\n",
    "one needs to import ```LibraryReals.def``` to use them in a B machine.\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "id": "df6d2cd0",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$1.4142135623730951$"
      ],
      "text/plain": [
       "1.4142135623730951"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RSQRT(2.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "id": "d2daab50",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$1.2246467991473532E-16$"
      ],
      "text/plain": [
       "1.2246467991473532E-16"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RSIN(RPI)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "481e4f68",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{r} = 1.0$\n",
       "* $\\mathit{x} = 0.5$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tr = 1.0\n",
       "\tx = 0.5"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=0.5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "id": "bfd74a24",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$\\mathit{TRUE}$\n",
       "\n",
       "**Solution:**\n",
       "* $\\mathit{r} = 1.0$\n",
       "* $\\mathit{x} = 10.5$"
      ],
      "text/plain": [
       "TRUE\n",
       "\n",
       "Solution:\n",
       "\tr = 1.0\n",
       "\tx = 10.5"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=10.5"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "id": "34ca2773",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$2.718281828459045$"
      ],
      "text/plain": [
       "2.718281828459045"
      ]
     },
     "execution_count": 13,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "REULER"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "4b24407f",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$-1.0$"
      ],
      "text/plain": [
       "−1.0"
      ]
     },
     "execution_count": 14,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RSIGN(-2.2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 21,
   "id": "ec855071",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$2.2$"
      ],
      "text/plain": [
       "2.2"
      ]
     },
     "execution_count": 21,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RABS(-2.2)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "c0bf9060",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$10.0$"
      ],
      "text/plain": [
       "10.0"
      ]
     },
     "execution_count": 17,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RLOG(2.0,1024.0)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "152d2052",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$1.0$"
      ],
      "text/plain": [
       "1.0"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RLOGe(REULER)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "id": "0a81f12f",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$1.4142135623730951$"
      ],
      "text/plain": [
       "1.4142135623730951"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RMAX(1.4,RSQRT(2.0))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "id": "4669fcd2",
   "metadata": {
    "vscode": {
     "languageId": "classicalb"
    }
   },
   "outputs": [
    {
     "data": {
      "text/markdown": [
       "$1.0$"
      ],
      "text/plain": [
       "1.0"
      ]
     },
     "execution_count": 20,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "RONE+RZERO"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "8df6222b",
   "metadata": {},
   "source": [
    "There are also external functions which are equivalent to the arithmetic operators: RLEQ, RGEQ, RLT, RGT, ROUND, RINTEGER, RADD, RSUB, RMUL, RDIV.\n",
    "This can be useful in some cases (e.g., when ALLOW_REALS is false or when mapping Event-B operators to classical B, see below)."
   ]
  },
  {
   "cell_type": "markdown",
   "id": "cc7e1768",
   "metadata": {},
   "source": [
    "## Event-B Theories\n",
    "Event-B does not have support for reals or floats as basic type but one can use the theory plugin.\n",
    "\n",
    "[https://prob.hhu.de/w/index.php?title=Event-B_Theories]\n",
    "\n",
    "To be able to view reals in ProB within Rodin you need to install a recent nightly build: [https://www3.hhu.de/stups/rodin/prob1/nightly]\n",
    "\n",
    "You need to use one of the standard theories.\n",
    "\n",
    "To write your own theory you should add an axiomatic type called REAL, FLOAT or the unicode R for reals.\n",
    "Then you have to define axiomatic operators and link them to ProB's real operators.\n",
    "You can do this either\n",
    "* using a theory mapping file (.ptm extension) which needs to be put into the Rodin project, see [https://prob.hhu.de/w/index.php?title=Event-B_Theories]\n",
    "* or use the same name as the external functions above (e.g., RSQRT); in this way ProB will do the mapping automatically.\n",
    "\n",
    "\n"
   ]
  }
 ],
 "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": 5
}