ProB Users

Hi, I guess you are using the default Tcl/Tk version provided by Apple, which is broken. Some hints

Hi Thanks Michael for the correction. I just want to learn basics B specification skills. I don't

Hi Michael, Thank you for supporting me in resole this problem. Active 8.6.9 solved the issue for me.

I work with models of networks in Alloy, and my research provides many opportunities for practical

Hello Mira, you can get traces ending in a deadlock state by applying Model Checking or LTL Model

======================================= ProB2-UI (JavaFX) ======================================= We

Hi Fabio, there are various ways to call a B machine from another one. The simplest is to INCLUDE the

Hello Denis, the invariant is evaluated as a single predicate in the internal implementation of ProB.

Hello Denis, the mechanism for Trace Replay has been moved to the ProB2 Java API. You can invoke the

I downloaded the sources from https://www3.hhu.de/stups/downloads/prob/source/ProB_src.tgz and

Hi Denis, what I typically do in Rodin is to have animation contexts. This is explained briefly here:

Hi, Let's suppose we've got Event-B model: context C0 sets NAMES constants NAMES_CARD axioms

Hi, have you looked at the manual page: https://www3.hhu.de/stups/prob/index.php/LTL_Model_Checking

Thanks for the very interesting suggestions. I need some time for digesting and experimenting them. I

Many thans!! I knew expected logical structure as hinted in the documentation on LTL_Model_Checking.

Is there a wayto pass set the -model_check or the -mc <nodes> options to the prob GUI? It seems

======================================= ProB 1.9.0 ======================================= We are

Thank you very much. So waiting for the fixed version. On Wednesday, July 17, 2019 at 7:35:56 PM UTC+

Dear Franco, you probably use SEES to include one machine into another. In that case you are not

Hi Lourenco, in order to start the Tcl/Tk version of ProB you have to install Tcl/Tk 8.5.18. You can

Hello, I have a machine M1 that evolves by perfoming the two operations Op1, Op2 in sequence. And I

Hi, May I know why the number of Checked States and and Total Transition is similar when I used the

Hi, I have read that b-method does not allowed to add a new operation in a refinement. Is there any

Hello Michael, Thank you for the clarification. My professor is probably using an old version of ProB

Hi, I am not sure I understand the question. If you want to check that Y is a refinement of X you

You need to run probcli.cmd from a Windows command shell: http://www.digitalcitizen.life/7-ways-

Hi, When I try to open an eample file in ProB, it shows that "Could not execute command "c:

Hi, can you send us the model? Do you use ProB Tcl/Tk version and use the menu command in the Verify

Hi Julien, you should be able to open the state view (State in the ProB menu of BMotionWeb), where at

Hi, On 23 May 2017, at 12:36, r0uruniz@gmail.com wrote: Hi, Thank you for your recommendation. I have