Groups
Conversations
All groups and messages
Send feedback to Google
Help
Sign in
Groups
ProB Users
Conversations
About
ProB Users
1–30 of 55
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 abusive group
0 selected
Pamudu Prabathiya
,
Michael Leuschel
4
Jan 5
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
Jan 5
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
marciano...@gmail.com
,
Ivaylo Dobrikov
2
5/26/18
Error TCLTK
Hi Lourenco, in order to start the Tcl/Tk version of ProB you have to install Tcl/Tk 8.5.18. You can
unread,
Error TCLTK
Hi Lourenco, in order to start the Tcl/Tk version of ProB you have to install Tcl/Tk 8.5.18. You can
5/26/18
fra...@gmail.com
3/1/18
trace refinements
Hello, I have a machine M1 that evolves by perfoming the two operations Op1, Op2 in sequence. And I
unread,
trace refinements
Hello, I have a machine M1 that evolves by perfoming the two operations Op1, Op2 in sequence. And I
3/1/18
r0ur...@gmail.com
2/16/18
Regarding the number of states when IGNORE HASH COLLISIONS is used
Hi, May I know why the number of Checked States and and Total Transition is similar when I used the
unread,
Regarding the number of states when IGNORE HASH COLLISIONS is used
Hi, May I know why the number of Checked States and and Total Transition is similar when I used the
2/16/18
zakiahzu...@gmail.com
10/3/17
Method to add new operation(s) in a refinement
Hi, I have read that b-method does not allowed to add a new operation in a refinement. Is there any
unread,
Method to add new operation(s) in a refinement
Hi, I have read that b-method does not allowed to add a new operation in a refinement. Is there any
10/3/17
maxime.g...@gmail.com
,
Michael Leuschel
3
9/27/17
Parsing error with tuple in set comprehension
Hello Michael, Thank you for the clarification. My professor is probably using an old version of ProB
unread,
Parsing error with tuple in set comprehension
Hello Michael, Thank you for the clarification. My professor is probably using an old version of ProB
9/27/17
zakiahzu...@gmail.com
,
Michael Leuschel
2
9/26/17
Question regarding B method refinement
Hi, I am not sure I understand the question. If you want to check that Y is a refinement of X you
unread,
Question regarding B method refinement
Hi, I am not sure I understand the question. If you want to check that Y is a refinement of X you
9/26/17
Michael Leuschel
,
lissy...@gmail.com
3
7/28/17
Re: Error occured when use ProB
You need to run probcli.cmd from a Windows command shell: http://www.digitalcitizen.life/7-ways-
unread,
Re: Error occured when use ProB
You need to run probcli.cmd from a Windows command shell: http://www.digitalcitizen.life/7-ways-
7/28/17
lissy...@gmail.com
7/27/17
Error occured when I use ProB
Hi, When I try to open an eample file in ProB, it shows that "Could not execute command "c:
unread,
Error occured when I use ProB
Hi, When I try to open an eample file in ProB, it shows that "Could not execute command "c:
7/27/17
r0ur...@gmail.com
,
Michael Leuschel
2
6/20/17
Check invariant preservation returns timeout
Hi, can you send us the model? Do you use ProB Tcl/Tk version and use the menu command in the Verify
unread,
Check invariant preservation returns timeout
Hi, can you send us the model? Do you use ProB Tcl/Tk version and use the menu command in the Verify
6/20/17