Groups
Conversations
All groups and messages
Send feedback to Google
Help
Training
Sign in
Groups
ProB Users
Conversations
About
Groups keyboard shortcuts have been updated
Dismiss
See shortcuts
ProB Users
Contact owners and managers
1–30 of 64
Welcome to the prob-users mailing list.
Here we discuss issues around the
ProB
validation tool for formal models.
A
user manual
and a
few tutorials
are available.
We also have a
bug tracker
.
Mark all as read
Report group
0 selected
Boris
5/4/24
Optimizing Event Parameter Generation in JeB: Leveraging ProB Constraint Solver
Hello everyone, I am a student, and as part of my final project, I am working on an extension for the
unread,
Optimizing Event Parameter Generation in JeB: Leveraging ProB Constraint Solver
Hello everyone, I am a student, and as part of my final project, I am working on an extension for the
5/4/24
Guzmán Llambías
, …
Guzmán Llambías - INCO
4
1/24/24
BMotionWeb hungs when open model
Hi Michael, thanks for the tip, I'll check it out Greetings Guzmán On Wed, Jan 24, 2024 at 2:56
unread,
BMotionWeb hungs when open model
Hi Michael, thanks for the tip, I'll check it out Greetings Guzmán On Wed, Jan 24, 2024 at 2:56
1/24/24
Laurent Payen
,
Michael Leuschel
4
11/16/23
ProB and MultiThread
Hi, I myself do not have an example. I guess you should need to use Java's concurrency features
unread,
ProB and MultiThread
Hi, I myself do not have an example. I guess you should need to use Java's concurrency features
11/16/23
Laurent Payen
,
Michael Leuschel
6
8/11/23
Performance issue
Thanks a lot Michael ! Best regards, Laurent Le vendredi 11 août 2023 à 10:32:39 UTC+2, Michael
unread,
Performance issue
Thanks a lot Michael ! Best regards, Laurent Le vendredi 11 août 2023 à 10:32:39 UTC+2, Michael
8/11/23
Jing Sun
8/3/23
back window issue
When I launch ProB after the installation on my Mac laptop, the black window issue happened. I
unread,
back window issue
When I launch ProB after the installation on my Mac laptop, the black window issue happened. I
8/3/23
chuanjun niu
,
Michael Leuschel
2
6/26/23
BmotionWeb
Hi, what is the B model you are using? I would recommend you try and switch to ProB's new
unread,
BmotionWeb
Hi, what is the B model you are using? I would recommend you try and switch to ProB's new
6/26/23
sanjay a
,
Michael Leuschel
2
6/12/23
Doubt in Prob output
Hi Sanjay, you can use the probcli comman switch -logxml FILE. probcli scheduler.mch -ltlformula
unread,
Doubt in Prob output
Hi Sanjay, you can use the probcli comman switch -logxml FILE. probcli scheduler.mch -ltlformula
6/12/23
Marcel Oliveira
2
5/1/23
Finding Loaded Machine Invariant
Sorry... My question is related with the use of the Java API. Em segunda-feira, 1 de maio de 2023 às
unread,
Finding Loaded Machine Invariant
Sorry... My question is related with the use of the Java API. Em segunda-feira, 1 de maio de 2023 às
5/1/23
Marcel Oliveira
4/24/23
Broken Link
Page: https://stups.hhu-hosting.de/handbook/prob2/prob_handbook.html At the very beginning, in the
unread,
Broken Link
Page: https://stups.hhu-hosting.de/handbook/prob2/prob_handbook.html At the very beginning, in the
4/24/23
Pamudu Prabathiya
,
Michael Leuschel
4
1/5/23
Prob2 UI graph visualization
Hi, in ProB2-UI you can save the visualisations in a variety of formats by clicking on the save icon
unread,
Prob2 UI graph visualization
Hi, in ProB2-UI you can save the visualisations in a variety of formats by clicking on the save icon
1/5/23
Pamudu Prabathiya
,
Michael Leuschel
2
12/28/22
Evaluation window on proB2-UI
Hi, the view is called console in ProB2-UI and should be visible in the lower middle section of your
unread,
Evaluation window on proB2-UI
Hi, the view is called console in ProB2-UI and should be visible in the lower middle section of your
12/28/22
Pamudu Prabathiya
,
Michael Leuschel
2
10/10/22
How to install ProB on mac os
Hi, I guess you are using the default Tcl/Tk version provided by Apple, which is broken. Some hints
unread,
How to install ProB on mac os
Hi, I guess you are using the default Tcl/Tk version provided by Apple, which is broken. Some hints
10/10/22
Shakirullah Shah
,
Michael Leuschel
4
12/7/21
add two numbers
Hi Thanks Michael for the correction. I just want to learn basics B specification skills. I don't
unread,
add two numbers
Hi Thanks Michael for the correction. I just want to learn basics B specification skills. I don't
12/7/21
Jayamal Hettiarachchi
,
Michael Leuschel
9
10/30/21
ProB 1.10.2-final not displaying properly on macos Monterey
Hi Michael, Thank you for supporting me in resole this problem. Active 8.6.9 solved the issue for me.
unread,
ProB 1.10.2-final not displaying properly on macos Monterey
Hi Michael, Thank you for supporting me in resole this problem. Active 8.6.9 solved the issue for me.
10/30/21
Pamela Zave
7/16/21
Alloy analysis in ProB
I work with models of networks in Alloy, and my research provides many opportunities for practical
unread,
Alloy analysis in ProB
I work with models of networks in Alloy, and my research provides many opportunities for practical
7/16/21
Mirainf
,
Fabian Vu
2
6/29/21
Get deadlock states
Hello Mira, you can get traces ending in a deadlock state by applying Model Checking or LTL Model
unread,
Get deadlock states
Hello Mira, you can get traces ending in a deadlock state by applying Model Checking or LTL Model
6/29/21
fra...@gmail.com
,
Michael Leuschel
3
1/28/21
CTL Model checking
======================================= ProB2-UI (JavaFX) ======================================= We
unread,
CTL Model checking
======================================= ProB2-UI (JavaFX) ======================================= We
1/28/21
Fabio Randazzo
,
Michael Leuschel
2
10/22/20
Call a machine from another one
Hi Fabio, there are various ways to call a B machine from another one. The simplest is to INCLUDE the
unread,
Call a machine from another one
Hi Fabio, there are various ways to call a B machine from another one. The simplest is to INCLUDE the
10/22/20
Denis Efremov
, …
Fabian Vu
5
7/17/20
ProB: are invariants checked for random animation?
Hello Denis, the invariant is evaluated as a single predicate in the internal implementation of ProB.
unread,
ProB: are invariants checked for random animation?
Hello Denis, the invariant is evaluated as a single predicate in the internal implementation of ProB.
7/17/20
Denis Efremov
, …
Fabian Vu
6
7/13/20
ProB Java API: Is it possible to dump model state after animation and load it to the model in the next run?
Hello Denis, the mechanism for Trace Replay has been moved to the ProB2 Java API. You can invoke the
unread,
ProB Java API: Is it possible to dump model state after animation and load it to the model in the next run?
Hello Denis, the mechanism for Trace Replay has been moved to the ProB2 Java API. You can invoke the
7/13/20
yefremo...@gmail.com
7/4/20
How to build ProB?
I downloaded the sources from https://www3.hhu.de/stups/downloads/prob/source/ProB_src.tgz and
unread,
How to build ProB?
I downloaded the sources from https://www3.hhu.de/stups/downloads/prob/source/ProB_src.tgz and
7/4/20
Denis Efremov
,
Michael Leuschel
2
3/4/20
ProB Java API: Is it possible to refine a set cardinality before setup_constants step?
Hi Denis, what I typically do in Rodin is to have animation contexts. This is explained briefly here:
unread,
ProB Java API: Is it possible to refine a set cardinality before setup_constants step?
Hi Denis, what I typically do in Rodin is to have animation contexts. This is explained briefly here:
3/4/20
Denis Efremov
3/4/20
ProB Java API: Is it possible to fill sets with own values at setup_constants step?
Hi, Let's suppose we've got Event-B model: context C0 sets NAMES constants NAMES_CARD axioms
unread,
ProB Java API: Is it possible to fill sets with own values at setup_constants step?
Hi, Let's suppose we've got Event-B model: context C0 sets NAMES constants NAMES_CARD axioms
3/4/20
germa...@gmail.com
,
Michael Leuschel
2
12/17/19
About LTL checking
Hi, have you looked at the manual page: https://www3.hhu.de/stups/prob/index.php/LTL_Model_Checking
unread,
About LTL checking
Hi, have you looked at the manual page: https://www3.hhu.de/stups/prob/index.php/LTL_Model_Checking
12/17/19
Franco Mazzanti
,
Michael Leuschel
3
8/14/19
checking variable updates
Thanks for the very interesting suggestions. I need some time for digesting and experimenting them. I
unread,
checking variable updates
Thanks for the very interesting suggestions. I need some time for digesting and experimenting them. I
8/14/19
Franco Mazzanti
,
Dobrikov
3
8/3/19
-ltlfile
Many thans!! I knew expected logical structure as hinted in the documentation on LTL_Model_Checking.
unread,
-ltlfile
Many thans!! I knew expected logical structure as hinted in the documentation on LTL_Model_Checking.
8/3/19
Franco Mazzanti
8/3/19
-model_check, -mc
Is there a wayto pass set the -model_check or the -mc <nodes> options to the prob GUI? It seems
unread,
-model_check, -mc
Is there a wayto pass set the -model_check or the -mc <nodes> options to the prob GUI? It seems
8/3/19
Michael Leuschel
7/18/19
ProB 1.9.0 released
======================================= ProB 1.9.0 ======================================= We are
unread,
ProB 1.9.0 released
======================================= ProB 1.9.0 ======================================= We are
7/18/19
amirh...@gmail.com
,
Michael Leuschel
3
7/17/19
Error while openin tex file
Thank you very much. So waiting for the fixed version. On Wednesday, July 17, 2019 at 7:35:56 PM UTC+
unread,
Error while openin tex file
Thank you very much. So waiting for the fixed version. On Wednesday, July 17, 2019 at 7:35:56 PM UTC+
7/17/19
Franco Mazzanti
,
Michael Leuschel
2
6/6/19
module composition
Dear Franco, you probably use SEES to include one machine into another. In that case you are not
unread,
module composition
Dear Franco, you probably use SEES to include one machine into another. In that case you are not
6/6/19