ProB Users

Hi, in ProB2-UI you can save the visualisations in a variety of formats by clicking on the save icon

Hi, the view is called console in ProB2-UI and should be visible in the lower middle section of your

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