Question regarding the 4096 transition limit in ProB

[Paul Simon]

Dear Michael,

I am currently using ProB through the ProB2 Java API to animate an Event-B model from a JavaFX application.

While exploring the set of enabled transitions from a given state (using trace.getNextTransitions(true)), I encountered what appears to be a limit of 4096 transitions returned by ProB. In some situations, my model generates more parameterized instances of an operation than this limit.

My goal is not necessarily to enumerate all possible transitions but simply to determine whether at least one transition with a given prefix (operation name) is enabled in the current state, in order to activate or deactivate buttons in the user interface.

Therefore I would like to ask:

1. Is the 4096 transition limit configurable in ProB?

2. If so, how can it be changed (e.g., via preferences, CLI parameters, or API options)?

3. If not, would you recommend another approach to efficiently check whether an operation is enabled, without enumerating all parameter combinations?

For context:

• I am using ProB2 (prob2-kernel) with the Java API.

• The model is Event-B.

• The application calls ProB from a JavaFX UI to determine which operations are currently enabled.

Any advice or recommended pattern for this type of usage would be greatly appreciated.

Best regards,

Paul Simon

[Michael Leuschel]

Hi Paul,
can you send us an example Event-B or B model that exhibits the problem?
I know of no limit to 4096 transitions in the Prolog kernel.
There is the MAX_OPERATIONS preference with which one can influence the number of transitions computed per operation.

Greetings,
Michael

[Paul Simon]

Hi Michael,

Thank you for your reply.

The behaviour I observe is the following: when I call the API to obtain the enabled transitions from the current state (via the ProB2 Java API), the number of transitions returned appears to be capped at around 4096 when the number of transitions to be explored is huge.

In my model, some operations are highly parameterised, which can lead to a very large number of concrete transitions. My JavaFX UI only needs to know whether at least one instance of a given operation is enabled, but the current mechanism enumerates all transitions.

Your comment about the MAX_OPERATIONS preference is very helpful. I will investigate this parameter to see whether it influences the behaviour I observe.

Before sending a full model, could you confirm:

• whether MAX_OPERATIONS limits the number of generated transitions per operation, and

• whether there is a recommended way (via the API or a predicate) to check if an operation is enabled, without enumerating all its parameter instances?

The behaviour seems to appear when using trace.getNextTransitions(), which returns a Java LinkedHashSet of size 4096 in the situations described.

If useful, I can also send a small Event-B model that reproduces the situation.

Best regards,

Paul

--------------------------------------------------------------------

Annexes  (test realized in mode debug => the duration may not be significant)

1/ the parameters chosen for the test

2/ the place where I check that the settings used are indeed the desired ones

3/ I intentionally display some metrics on the work form (execution time, number of transitions explored)

4/ observing the limit of 4096 by manipulating the instruction « this.trace/getNextTransitions();"

All the enabled events are not identified. Particularly the « addSystemType » event is not listed in the 4096 transitions.

5/ If i reduce the number of max deferred set 

The limit of 4096 can be exceeded and all the enabled events are identified !