From 4184bb5ae228ec53daf2f55a561e45987ca8e725 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Mon, 3 Oct 2022 08:39:21 +0200
Subject: [PATCH] add more operator descriptions

---
 notebooks/manual/FloatsReals.ipynb | 327 ++++++++++++++++++++++++++++-
 1 file changed, 325 insertions(+), 2 deletions(-)

diff --git a/notebooks/manual/FloatsReals.ipynb b/notebooks/manual/FloatsReals.ipynb
index c584d19..41dc6e1 100644
--- a/notebooks/manual/FloatsReals.ipynb
+++ b/notebooks/manual/FloatsReals.ipynb
@@ -84,6 +84,130 @@
     "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",
@@ -455,14 +579,213 @@
   },
   {
    "cell_type": "code",
-   "execution_count": null,
+   "execution_count": 13,
    "id": "34ca2773",
    "metadata": {
     "vscode": {
      "languageId": "classicalb"
     }
    },
-   "outputs": [],
+   "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": []
   }
  ],
-- 
GitLab