diff --git a/notebooks/manual/FloatsReals.ipynb b/notebooks/manual/FloatsReals.ipynb index c4707b991b1faeb52da2854c3dd2da1a38e054f4..c781695306c3b4d5c50c30ee96133eed7f927770 100644 --- a/notebooks/manual/FloatsReals.ipynb +++ b/notebooks/manual/FloatsReals.ipynb @@ -30,7 +30,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 12, "id": "cf76baf3", "metadata": { "vscode": { @@ -41,19 +41,19 @@ { "data": { "text/markdown": [ - "$1.0$" + "$2.0$" ], "text/plain": [ - "1.0" + "2.0" ] }, - "execution_count": 5, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "1.0" + "1.0+real(1)" ] }, { @@ -403,7 +403,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 14, "id": "b6d8671d", "metadata": { "vscode": { @@ -426,7 +426,7 @@ "\tx = 1.0" ] }, - "execution_count": 8, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -479,7 +479,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 16, "id": "d2daab50", "metadata": { "vscode": { @@ -490,19 +490,19 @@ { "data": { "text/markdown": [ - "$1.2246467991473532E-16$" + "$-2.4492935982947064E-16$" ], "text/plain": [ - "1.2246467991473532E-16" + "−2.4492935982947064E-16" ] }, - "execution_count": 10, + "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "RSIN(RPI)" + "RSIN(2.0*RPI)" ] }, { @@ -782,6 +782,234 @@ "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": "dbb9c880", + "metadata": {}, + "source": [ + "### Generating Random Values\n", + "\n", + "ProB also provides the RNORMAL external function, which is not a real mathematical function. It provides a random value according to a Gaussian distribution" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "31e86284", + "metadata": { + "vscode": { + "languageId": "classicalb" + } + }, + "outputs": [ + { + "data": { + "text/markdown": [ + "$8.998407411179912$" + ], + "text/plain": [ + "8.998407411179912" + ] + }, + "execution_count": 1, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "RNORMAL(10.0,2.0)" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "8c360bee", + "metadata": { + "vscode": { + "languageId": "classicalb" + } + }, + "outputs": [ + { + "data": { + "text/markdown": [ + "$10.939727825559297$" + ], + "text/plain": [ + "10.939727825559297" + ] + }, + "execution_count": 2, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "RNORMAL(10.0,2.0)" + ] + }, + { + "cell_type": "markdown", + "id": "cc7d2262", + "metadata": {}, + "source": [ + "We can use this function to for example find counter-examples to the associativity law (which holds for reals but not for floats):" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "71b6b98c", + "metadata": { + "vscode": { + "languageId": "classicalb" + } + }, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{xyz1} = -21.476244724718985$\n", + "* $\\mathit{xyz2} = -21.47624472471899$\n", + "* $\\mathit{r} = \\{(-10\\mapsto-6.232527651509804),(-9\\mapsto-8.787575429804837),(-8\\mapsto-7.404530875937022),(-7\\mapsto-3.9010938651093108),(-6\\mapsto-6.971757103640787),(-5\\mapsto-4.067108000394238),(-4\\mapsto-5.677513300835528),(-3\\mapsto-2.9235589072847077),(-2\\mapsto-1.9803650954876497),(-1\\mapsto-2.9075176813814254),(0\\mapsto 0.3083048289690526),(1\\mapsto-1.3723215929523715),(2\\mapsto 5.0255955535739165),(3\\mapsto 3.6059142437344507),(4\\mapsto 1.4538189188785093),(5\\mapsto 6.024768884849674),(6\\mapsto 5.197220399935867),(7\\mapsto 8.144029305129449),(8\\mapsto 11.748894277644647),(9\\mapsto 10.505167136831435),(10\\mapsto 12.441743874437144)\\}$\n", + "* $\\mathit{x} = -8.787575429804837$\n", + "* $\\mathit{y} = -8.787575429804837$\n", + "* $\\mathit{z} = -3.9010938651093108$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\txyz1 = −21.476244724718985\n", + "\txyz2 = −21.47624472471899\n", + "\tr = {(−10↦−6.232527651509804),(−9↦−8.787575429804837),(−8↦−7.404530875937022),(−7↦−3.9010938651093108),(−6↦−6.971757103640787),(−5↦−4.067108000394238),(−4↦−5.677513300835528),(−3↦−2.9235589072847077),(−2↦−1.9803650954876497),(−1↦−2.9075176813814254),(0↦0.3083048289690526),(1↦−1.3723215929523715),(2↦5.0255955535739165),(3↦3.6059142437344507),(4↦1.4538189188785093),(5↦6.024768884849674),(6↦5.197220399935867),(7↦8.144029305129449),(8↦11.748894277644647),(9↦10.505167136831435),(10↦12.441743874437144)}\n", + "\tx = −8.787575429804837\n", + "\ty = −8.787575429804837\n", + "\tz = −3.9010938651093108" + ] + }, + "execution_count": 3, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "r = %i.(i:-10..10|RNORMAL(real(i),2.0)) & // generate some random numbers\n", + " x:ran(r) & y:ran(r) & z:ran(r) & // pick three random numbers from above\n", + " xyz1 = (x+y)+z &\n", + " xyz2 = x+(y+z) &\n", + " xyz1 > xyz2" + ] + }, + { + "cell_type": "markdown", + "id": "909a9b2d", + "metadata": {}, + "source": [ + "When using RNORMAL one has to be wary: ProB expects RNORMAL to be a mathematical function; hence in the expression below RNORMAL is evaluated only once an the same \"random\" value is generated for the 21 values:" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "1b8acb8f", + "metadata": { + "vscode": { + "languageId": "classicalb" + } + }, + "outputs": [ + { + "data": { + "text/markdown": [ + "$\\mathit{TRUE}$\n", + "\n", + "**Solution:**\n", + "* $\\mathit{r} = \\{(-10\\mapsto 0.8324329020860423),(-9\\mapsto 0.8324329020860423),(-8\\mapsto 0.8324329020860423),(-7\\mapsto 0.8324329020860423),(-6\\mapsto 0.8324329020860423),(-5\\mapsto 0.8324329020860423),(-4\\mapsto 0.8324329020860423),(-3\\mapsto 0.8324329020860423),(-2\\mapsto 0.8324329020860423),(-1\\mapsto 0.8324329020860423),(0\\mapsto 0.8324329020860423),(1\\mapsto 0.8324329020860423),(2\\mapsto 0.8324329020860423),(3\\mapsto 0.8324329020860423),(4\\mapsto 0.8324329020860423),(5\\mapsto 0.8324329020860423),(6\\mapsto 0.8324329020860423),(7\\mapsto 0.8324329020860423),(8\\mapsto 0.8324329020860423),(9\\mapsto 0.8324329020860423),(10\\mapsto 0.8324329020860423)\\}$" + ], + "text/plain": [ + "TRUE\n", + "\n", + "Solution:\n", + "\tr = {(−10↦0.8324329020860423),(−9↦0.8324329020860423),(−8↦0.8324329020860423),(−7↦0.8324329020860423),(−6↦0.8324329020860423),(−5↦0.8324329020860423),(−4↦0.8324329020860423),(−3↦0.8324329020860423),(−2↦0.8324329020860423),(−1↦0.8324329020860423),(0↦0.8324329020860423),(1↦0.8324329020860423),(2↦0.8324329020860423),(3↦0.8324329020860423),(4↦0.8324329020860423),(5↦0.8324329020860423),(6↦0.8324329020860423),(7↦0.8324329020860423),(8↦0.8324329020860423),(9↦0.8324329020860423),(10↦0.8324329020860423)}" + ] + }, + "execution_count": 7, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "r = %i.(i:-10..10|RNORMAL(0.0,2.0))" + ] + }, + { + "cell_type": "markdown", + "id": "efc04915", + "metadata": {}, + "source": [ + "Another external function for generating random values is RAND:" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "66b2fe21", + "metadata": { + "vscode": { + "languageId": "classicalb" + } + }, + "outputs": [ + { + "data": { + "text/markdown": [ + "$3.665076557575515$" + ], + "text/plain": [ + "3.665076557575515" + ] + }, + "execution_count": 5, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "RAND(0.0,10.0)" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "52798a87", + "metadata": { + "vscode": { + "languageId": "classicalb" + } + }, + "outputs": [ + { + "data": { + "text/markdown": [ + "$8.733457267613282$" + ], + "text/plain": [ + "8.733457267613282" + ] + }, + "execution_count": 6, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "RAND(0.0,10.0)" + ] + }, { "cell_type": "markdown", "id": "cc7e1768", @@ -800,10 +1028,16 @@ "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", + "* or use the same name as the external functions above (e.g., RSQRT) and set the preference AUTO_DETECT_THEORY_MAPPING to TRUE; in this way ProB will do the mapping automatically.\n", "\n", "\n" ] + }, + { + "cell_type": "markdown", + "id": "b659ae13", + "metadata": {}, + "source": [] } ], "metadata": {