debug of BMotionWeb Animation

[julie...@gmail.com]

Hello,
I'm currently debugging a large model written in Classical B. Unfortunately I'm experimenting a difference between the execution in ProB (TCL-TK) and the animation running in BMotionWeb : one of the events is perfectly triggerable in ProB while not in BMotionWeb. The states seem to be identical and trace is the same. There should be nothing that prevent the event from triggering and in ProB it does not lead to a bad state or broken invariant.

Is there a way to have more interaction in BMW ? for example know why the event is forbidden at some point ?

Thanks,
Julien

[Lukas Ladenberger]

Hi Julien,

the version of the underlying probcli (ProB core) may differ between the ProB TCL-TK and BMotionWeb application. This could be one reason. The second reason could be different ProB settings between both applications.

In case of BMotionWeb you can set ProB related options by means of the “modelOptions” property that can be set in the BMotionWeb manifest file (bmotion.json). Take the following mfile as an example: https://github.com/ladenberger/bmotion-prob-examples/blob/master/BMotionWeb/Event-B/HDMachine/bmotion.json

Best regards,

Lukas

--
You received this message because you are subscribed to the Google Groups "ProB Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+unsubscribe@googlegroups.com.
To post to this group, send email to prob-...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/55034b78-ca35-4b77-baf1-1d02cc67a048%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[julie...@gmail.com]

Hello Lukas and thank you for your answer.

I already put some ProB options via Constants :
    SET_PREF_MININT == -1;
    SET_PREF_MAXINT == 5000;

the bmotion.json you quote did not help, even if i'm way under the limit of 200 operations (around 50), btw, what is time_out about ? "modelOptions": {

"TIME_OUT": 10000,

"MAX_OPERATIONS": 200

},

My concern is that BMotionWeb does not explain why the operation is red at some point, is it possible to have more information via the consoles ?

Regards,
Julien

On Wednesday, May 24, 2017 at 8:30:07 PM UTC+2, Lukas Ladenberger wrote:

Hi Julien,

the version of the underlying probcli (ProB core) may differ between the ProB TCL-TK and BMotionWeb application. This could be one reason. The second reason could be different ProB settings between both applications.

In case of BMotionWeb you can set ProB related options by means of the “modelOptions” property that can be set in the BMotionWeb manifest file (bmotion.json). Take the following mfile as an example: https://github.com/ladenberger/bmotion-prob-examples/blob/master/BMotionWeb/Event-B/HDMachine/bmotion.json

Best regards,

Lukas

On 23. May 2017, at 17:23, julie...@clearsy.com <julie...@gmail.com> wrote:

Hello,
I'm currently debugging a large model written in Classical B. Unfortunately I'm experimenting a difference between the execution in ProB (TCL-TK) and the animation running in BMotionWeb : one of the events is perfectly triggerable in ProB while not in BMotionWeb. The states seem to be identical and trace is the same. There should be nothing that prevent the event from triggering and in ProB it does not lead to a bad state or broken invariant.

Is there a way to have more interaction in BMW ? for example know why the event is forbidden at some point ?

Thanks,
Julien

--
You received this message because you are subscribed to the Google Groups "ProB Users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.

[Michael Leuschel]

Hi Julien,

you should be able to open the state view (State in the ProB menu of BMotionWeb), where at the bottom you can type in your own expressions/predicates.

Alternatively, you should also be able to open a console/REPL from inside BMotionWeb. (However, with the version I am currently using, which is a bit older, I get a provisioning exception).

If you wish you can also send us the model for inspection.

Greetings,

Michael

On 29 May 2017, at 11:34, julie...@gmail.com wrote:

My concern is that BMotionWeb does not explain why the operation is red at some point, is it possible to have more information via the consoles ?