Performance issue

[Laurent Payen]

hello,

We are experiencing a performance issue with the ProB engine. We use the latest version of ProbWin (1.12.1-final).

We have quite substantial sets. For the first operation (RVF354_MDYS_op1.mch), we check that each identifier present in the first constructed set (INFOS_MCMD) is present in the second set. Everything is going well and we get an answer in less than 4 minutes.

For the second operation (RVF354_MDYS_op2), with the same data, this time we check that each identifier in the second set exists as an identifier in the constructed set (INFOS_MCMD). This time, we don't get a response from ProB, which seems to be timed out.

We don't understand why, the complexity seems to be the same as for the operation 1.

If anyone could provide us some clarification, we would greatly appreciate it.

The main machines are RVF354_MDYS_op1.mch and RVF354_MDYS_op2.mch

[Michael Leuschel]

Dear Laurent,

with the latest version 1.12.2-nightly both examples run through very quickly (less than a second checking time, excluding parsing and loading).
The improvement appears in commit 6796bf80d653dbdfa2f88a30980158c82af0a5ec from 11th of June 2023
and deals with removing useless LET or existential quantifiers with just truth in the body.

Can you check if 1.12.2-nightly corrects the problem for you?
If not, can you send an example where the problem appears with the latest version of probcli?

Greetings,
Michael

> --
> 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.
> To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/77e12726-7bf8-4d14-8b42-ed683beb8a35n%40googlegroups.com.
>

[Laurent Payen]

Dear Michael,

Thank you very much for your answer.

Wow it's incredible the speed of execution with the latest version !!!!

A huge thank you !!!!

Laurent

[Laurent Payen]

Dear Michael,

We use the maven repository 4.12.1 of the ProB API, when does this nightly will be integrated to the repo ?

Best regards,

Laurent

[Michael Leuschel]

Dear Laurent,
probably next week (or maybe today) with the next ProB2-Java-API release.

Greetings,
Michael

[Laurent Payen]

Thanks a lot Michael !

Best regards,

Laurent