ProB Users

Hello everyone, I am a student, and as part of my final project, I am working on an extension for the

Hi Michael, thanks for the tip, I'll check it out Greetings Guzmán On Wed, Jan 24, 2024 at 2:56

Hi, I myself do not have an example. I guess you should need to use Java's concurrency features

Thanks a lot Michael ! Best regards, Laurent Le vendredi 11 août 2023 à 10:32:39 UTC+2, Michael

When I launch ProB after the installation on my Mac laptop, the black window issue happened. I

Hi, what is the B model you are using? I would recommend you try and switch to ProB's new

Hi Sanjay, you can use the probcli comman switch -logxml FILE. probcli scheduler.mch -ltlformula

Sorry... My question is related with the use of the Java API. Em segunda-feira, 1 de maio de 2023 às

Page: https://stups.hhu-hosting.de/handbook/prob2/prob_handbook.html At the very beginning, in the

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