Skip to content
Snippets Groups Projects
Commit acaabec6 authored by dgelessus's avatar dgelessus
Browse files

Update www3 URLs to stups.hhu-hosting.de

parent c9a3ea98
No related branches found
No related tags found
No related merge requests found
Pipeline #106803 passed
Stage: test
Show whitespace changes
Inline Side-by-side
CHANGELOG.md
+ 4
− 4
View file @ acaabec6
...@@ -8,7 +8,7 @@ ...@@ -8,7 +8,7 @@
* Rewrote the kernel installation code in Python. This is mostly an internal change and shouldn't affect most users. As a side effect, uninstalling the kernel is now simpler and requires no extra steps after `jupyter kernelspec remove`. * Rewrote the kernel installation code in Python. This is mostly an internal change and shouldn't affect most users. As a side effect, uninstalling the kernel is now simpler and requires no extra steps after `jupyter kernelspec remove`.
* Disabled LaTeX formatting inside `:check` tables as well, because of the layout issues mentioned below. * Disabled LaTeX formatting inside `:check` tables as well, because of the layout issues mentioned below.
## [1.3.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar) ## [1.3.0](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar)
* Added support for Java 17. * Added support for Java 17.
* Updated ProB 2 to version 3.15.0. * Updated ProB 2 to version 3.15.0.
...@@ -25,7 +25,7 @@ ...@@ -25,7 +25,7 @@
* Fixed the `:trace` command sometimes displaying transitions as `null`. * Fixed the `:trace` command sometimes displaying transitions as `null`.
* Disabled LaTeX formatting inside `:table` output, because it leads to various layout issues inside Jupyter Notebook. The table contents are now rendered as plain Unicode text instead. * Disabled LaTeX formatting inside `:table` output, because it leads to various layout issues inside Jupyter Notebook. The table contents are now rendered as plain Unicode text instead.
## [1.2.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.2.0-all.jar) ## [1.2.0](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.2.0-all.jar)
* Added support for Java 14. * Added support for Java 14.
* Added B parser version information to `:version` output. * Added B parser version information to `:version` output.
...@@ -34,7 +34,7 @@ ...@@ -34,7 +34,7 @@
* Fixed a parse error when a line comment is used on the last line of an expression while any `:let` variables are defined. * Fixed a parse error when a line comment is used on the last line of an expression while any `:let` variables are defined.
* Fixed detection of B machines in cells without `::load`. Previously only single-line machines were recognized. * Fixed detection of B machines in cells without `::load`. Previously only single-line machines were recognized.
## [1.1.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.1.0-all.jar) ## [1.1.0](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.1.0-all.jar)
* Added a `--user` flag to the installer to allow installing the kernel into the user home directory. This allows installing the kernel without `sudo` when not using a virtual environment. * Added a `--user` flag to the installer to allow installing the kernel into the user home directory. This allows installing the kernel without `sudo` when not using a virtual environment.
* Added `:let` and `:unlet` commands to (un)define local variables. * Added `:let` and `:unlet` commands to (un)define local variables.
...@@ -52,6 +52,6 @@ ...@@ -52,6 +52,6 @@
* Fixed `:trace` not showing the parameters and return values of executed transitions. * Fixed `:trace` not showing the parameters and return values of executed transitions.
* Changed error handling so exception stack traces are no longer shown in the notebook. (They are still logged to the console.) * Changed error handling so exception stack traces are no longer shown in the notebook. (They are still logged to the console.)
## [1.0.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.0.0-all.jar) ## [1.0.0](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.0.0-all.jar)
* Initial release. * Initial release.
README.md
+ 1
− 1
View file @ acaabec6
...@@ -8,7 +8,7 @@ This is a [Jupyter](https://jupyter.org/) kernel for the [ProB animator and mode ...@@ -8,7 +8,7 @@ This is a [Jupyter](https://jupyter.org/) kernel for the [ProB animator and mode
## Downloads ## Downloads
* **[Download the latest version of the ProB2 Jupyter kernel here](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar).** * **[Download the latest version of the ProB2 Jupyter kernel here](https://stups.hhu-hosting.de/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar).**
* Download links for previous versions can be found in the [changelog]. * Download links for previous versions can be found in the [changelog].
* A [snapshot build](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.3.1-SNAPSHOT-all.jar?job=test) of the latest development version is also available. **Warning:** this is an unstable version that can contain bugs or breaking changes. * A [snapshot build](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.3.1-SNAPSHOT-all.jar?job=test) of the latest development version is also available. **Warning:** this is an unstable version that can contain bugs or breaking changes.
......
notebooks/manual/FloatsReals.ipynb
+ 1
− 1
View file @ acaabec6
%% Cell type:markdown id:85001897 tags: %% Cell type:markdown id:85001897 tags:
# Reals and Floats in ProB # Reals and Floats in ProB
### Michael Leuschel ### Michael Leuschel
%% Cell type:markdown id:42473a5e tags: %% Cell type:markdown id:42473a5e tags:
## Classical B ## Classical B
In Atelier-B the following two types were added to the B language: In Atelier-B the following two types were added to the B language:
* REAL * REAL
* FLOAT * FLOAT
ProB treats these keywords as synonyms for a new base type. ProB treats these keywords as synonyms for a new base type.
The current representation in ProB are floating point numbers; but this The current representation in ProB are floating point numbers; but this
will probably change in the future, at least for the REAL type. will probably change in the future, at least for the REAL type.
One can now also use literals in decimal point notation for REAL and FLOAT. One can now also use literals in decimal point notation for REAL and FLOAT.
%% Cell type:code id:cf76baf3 tags: %% Cell type:code id:cf76baf3 tags:
``` prob ``` prob
1.0 1.0
``` ```
%% Output %% Output
$1.0$ $1.0$
1.0 1.0
%% Cell type:code id:941433ba tags: %% Cell type:code id:941433ba tags:
``` prob ``` prob
1.0 : REAL & 1.0 : FLOAT 1.0 : REAL & 1.0 : FLOAT
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
TRUE TRUE
%% Cell type:markdown id:6caf3504 tags: %% Cell type:markdown id:6caf3504 tags:
### Conversion Operators ### Conversion Operators
The following conversion operators are available in classical B: The following conversion operators are available in classical B:
* floor * floor
* ceiling * ceiling
* real * real
%% Cell type:code id:8925f6fe tags: %% Cell type:code id:8925f6fe tags:
``` prob ``` prob
real(2) real(2)
``` ```
%% Output %% Output
$2.0$ $2.0$
2.0 2.0
%% Cell type:code id:bbd73954 tags: %% Cell type:code id:bbd73954 tags:
``` prob ``` prob
floor(2.2) floor(2.2)
``` ```
%% Output %% Output
$2$ $2$
2 2
%% Cell type:code id:838ea786 tags: %% Cell type:code id:838ea786 tags:
``` prob ``` prob
ceiling(2.2) ceiling(2.2)
``` ```
%% Output %% Output
$3$ $3$
3 3
%% Cell type:code id:ee31f934 tags: %% Cell type:code id:ee31f934 tags:
``` prob ``` prob
ceiling(-2.2) ceiling(-2.2)
``` ```
%% Output %% Output
$-2$ $-2$
−2 −2
%% Cell type:markdown id:f7398e0e tags: %% Cell type:markdown id:f7398e0e tags:
### Arithmetic Operators ### Arithmetic Operators
The documentation of Atelier-B is not entirely consistent according to which The documentation of Atelier-B is not entirely consistent according to which
operators to use. operators to use.
In ProB you can use the standard arithmetic operators also for In ProB you can use the standard arithmetic operators also for
floats: floats:
%% Cell type:code id:65a66ec9 tags: %% Cell type:code id:65a66ec9 tags:
``` prob ``` prob
1.0 + 1.0 1.0 + 1.0
``` ```
%% Output %% Output
$2.0$ $2.0$
2.0 2.0
%% Cell type:code id:35ce95d5 tags: %% Cell type:code id:35ce95d5 tags:
``` prob ``` prob
2.0 * 2.0 < 2.1 2.0 * 2.0 < 2.1
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:code id:531aa72d tags: %% Cell type:code id:531aa72d tags:
``` prob ``` prob
2.0 * 2.0 < 2.0 + 2.0 2.0 * 2.0 < 2.0 + 2.0
``` ```
%% Output %% Output
$\mathit{FALSE}$ $\mathit{FALSE}$
FALSE FALSE
%% Cell type:markdown id:9066aa50 tags: %% Cell type:markdown id:9066aa50 tags:
You can control whether to allow arithmetic operators for reals You can control whether to allow arithmetic operators for reals
in ProB via the preference ```ALLOW_REALS```. in ProB via the preference ```ALLOW_REALS```.
By default reals are allowed for classical B and disallowed for Event-B. By default reals are allowed for classical B and disallowed for Event-B.
The only disadvantage of allowing reals is that the arithmetic operators The only disadvantage of allowing reals is that the arithmetic operators
are overloaded, which may require stronger typing. are overloaded, which may require stronger typing.
E.g., without ```x:INT``` you get an error that the type of x and y cannot be inferred, when reals are allowed: 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 id:528e647d tags: %% Cell type:code id:528e647d tags:
``` prob ``` prob
x:INT & x < y x:INT & x < y
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = -1$ * $\mathit{x} = -1$
* $\mathit{y} = 0$ * $\mathit{y} = 0$
TRUE TRUE
Solution: Solution:
x = −1 x = −1
y = 0 y = 0
%% Cell type:markdown id:02b86510 tags: %% Cell type:markdown id:02b86510 tags:
### Constraint solving ### Constraint solving
Constraint solving and enumeration is very limited in ProB. Constraint solving and enumeration is very limited in ProB.
This will change in future. This will change in future.
Currently ProB will enumerate a few random values for unspecified reals, Currently ProB will enumerate a few random values for unspecified reals,
and then stop with an enumeration warning. and then stop with an enumeration warning.
%% Cell type:code id:9356ea2c tags: %% Cell type:code id:9356ea2c tags:
``` prob ``` prob
x:REAL x:REAL
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 0.0$ * $\mathit{x} = 0.0$
TRUE TRUE
Solution: Solution:
x = 0.0 x = 0.0
%% Cell type:code id:b6d8671d tags: %% Cell type:code id:b6d8671d tags:
``` prob ``` prob
x + 1.0 = 2.0 x + 1.0 = 2.0
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{x} = 1.0$ * $\mathit{x} = 1.0$
TRUE TRUE
Solution: Solution:
x = 1.0 x = 1.0
%% Cell type:markdown id:13388af0 tags: %% Cell type:markdown id:13388af0 tags:
### Other Operators ### Other Operators
The standard library ```LibraryReals.def``` provides many functions The standard library ```LibraryReals.def``` provides many functions
over reals as external functions. over reals as external functions.
These functions typically start with a capital R. These functions typically start with a capital R.
The functions are available in the REPL (aka console) but The functions are available in the REPL (aka console) but
one needs to import ```LibraryReals.def``` to use them in a B machine. one needs to import ```LibraryReals.def``` to use them in a B machine.
%% Cell type:code id:df6d2cd0 tags: %% Cell type:code id:df6d2cd0 tags:
``` prob ``` prob
RSQRT(2.0) RSQRT(2.0)
``` ```
%% Output %% Output
$1.4142135623730951$ $1.4142135623730951$
1.4142135623730951 1.4142135623730951
%% Cell type:code id:d2daab50 tags: %% Cell type:code id:d2daab50 tags:
``` prob ``` prob
RSIN(RPI) RSIN(RPI)
``` ```
%% Output %% Output
$1.2246467991473532E-16$ $1.2246467991473532E-16$
1.2246467991473532E-16 1.2246467991473532E-16
%% Cell type:code id:481e4f68 tags: %% Cell type:code id:481e4f68 tags:
``` prob ``` prob
r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=0.5 r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=0.5
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{r} = 1.0$ * $\mathit{r} = 1.0$
* $\mathit{x} = 0.5$ * $\mathit{x} = 0.5$
TRUE TRUE
Solution: Solution:
r = 1.0 r = 1.0
x = 0.5 x = 0.5
%% Cell type:code id:bfd74a24 tags: %% Cell type:code id:bfd74a24 tags:
``` prob ``` prob
r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=10.5 r=RPOW(RSIN(x),2.0)+RPOW(RCOS(x),2.0) & x=10.5
``` ```
%% Output %% Output
$\mathit{TRUE}$ $\mathit{TRUE}$
**Solution:** **Solution:**
* $\mathit{r} = 1.0$ * $\mathit{r} = 1.0$
* $\mathit{x} = 10.5$ * $\mathit{x} = 10.5$
TRUE TRUE
Solution: Solution:
r = 1.0 r = 1.0
x = 10.5 x = 10.5
%% Cell type:code id:34ca2773 tags: %% Cell type:code id:34ca2773 tags:
``` prob ``` prob
REULER REULER
``` ```
%% Output %% Output
$2.718281828459045$ $2.718281828459045$
2.718281828459045 2.718281828459045
%% Cell type:code id:4b24407f tags: %% Cell type:code id:4b24407f tags:
``` prob ``` prob
RSIGN(-2.2) RSIGN(-2.2)
``` ```
%% Output %% Output
$-1.0$ $-1.0$
−1.0 −1.0
%% Cell type:code id:ec855071 tags: %% Cell type:code id:ec855071 tags:
``` prob ``` prob
RABS(-2.2) RABS(-2.2)
``` ```
%% Output %% Output
$2.2$ $2.2$
2.2 2.2
%% Cell type:code id:c0bf9060 tags: %% Cell type:code id:c0bf9060 tags:
``` prob ``` prob
RLOG(2.0,1024.0) RLOG(2.0,1024.0)
``` ```
%% Output %% Output
$10.0$ $10.0$
10.0 10.0
%% Cell type:code id:152d2052 tags: %% Cell type:code id:152d2052 tags:
``` prob ``` prob
RLOGe(REULER) RLOGe(REULER)
``` ```
%% Output %% Output
$1.0$ $1.0$
1.0 1.0
%% Cell type:code id:0a81f12f tags: %% Cell type:code id:0a81f12f tags:
``` prob ``` prob
RMAX(1.4,RSQRT(2.0)) RMAX(1.4,RSQRT(2.0))
``` ```
%% Output %% Output
$1.4142135623730951$ $1.4142135623730951$
1.4142135623730951 1.4142135623730951
%% Cell type:code id:4669fcd2 tags: %% Cell type:code id:4669fcd2 tags:
``` prob ``` prob
RONE+RZERO RONE+RZERO
``` ```
%% Output %% Output
$1.0$ $1.0$
1.0 1.0
%% Cell type:markdown id:8df6222b tags: %% Cell type:markdown id:8df6222b tags:
There are also external functions which are equivalent to the arithmetic operators: RLEQ, RGEQ, RLT, RGT, ROUND, RINTEGER, RADD, RSUB, RMUL, RDIV. There are also external functions which are equivalent to the arithmetic operators: RLEQ, RGEQ, RLT, RGT, ROUND, RINTEGER, RADD, RSUB, RMUL, RDIV.
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). 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 tags: %% Cell type:markdown id:cc7e1768 tags:
## Event-B Theories ## Event-B Theories
Event-B does not have support for reals or floats as basic type but one can use the theory plugin. Event-B does not have support for reals or floats as basic type but one can use the theory plugin.
[https://prob.hhu.de/w/index.php?title=Event-B_Theories] [https://prob.hhu.de/w/index.php?title=Event-B_Theories]
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] To be able to view reals in ProB within Rodin you need to install a recent nightly build: [https://stups.hhu-hosting.de/rodin/prob1/nightly]
You need to use one of the standard theories. You need to use one of the standard theories.
To write your own theory you should add an axiomatic type called REAL, FLOAT or the unicode R for reals. To write your own theory you should add an axiomatic type called REAL, FLOAT or the unicode R for reals.
Then you have to define axiomatic operators and link them to ProB's real operators. Then you have to define axiomatic operators and link them to ProB's real operators.
You can do this either You can do this either
* 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] * 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]
* or use the same name as the external functions above (e.g., RSQRT); in this way ProB will do the mapping automatically. * or use the same name as the external functions above (e.g., RSQRT); in this way ProB will do the mapping automatically.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment