Java API: how to reproduce “Execute with additional Guard constraint” in Event-B animation

[Paul Simon]

Dear Michael,

I am currently using ProB via the Java API (prob2-kernel / prob-java with the CLI socket server) to animate an Event-B model from a JavaFX application.

I would like to reproduce, from Java, the exact behavior of the Rodin UI command:

“Execute with additional Guard constraint”

Context

• The model loads correctly.

• From a given state (e.g., state id = 1), I retrieve the enabled transitions using trace.getNextTransitions().

• For an event like addSystemType, ProB generates multiple instantiated transitions.

• If I execute without additional constraint → I get an ambiguity (several candidates).

• If I try to enforce all parameter values via filtering in Java → I sometimes get noCandidateMatch.

In Rodin, when I use “Execute with additional Guard constraint” and provide a conjunction like:

t = TYPE1 &
IT = {...} &
ITP = {...} &
ITO = {...} &
...

the execution succeeds exactly as expected.

Question

From the Java API (prob-java / prob2-kernel), what is the correct way to reproduce this behavior?

More precisely:

• Does the Rodin UI:

  1. Filter the list of instantiated transitions and execute the unique remaining one?
     or

  2. Execute the operation symbolically while adding the given constraint directly to the solver during instantiation?

• Is there a specific Prolog/socket command corresponding to this feature (e.g., an equivalent to “execute operation with additional guard constraint”)?

• Is there an existing method in the Java API (Animator / StateSpace / Transition) that directly supports this mode of execution?

Technical details

• ProB CLI revision: e10c98eafba5a91367f8b51c96f659e2d3727226

• Prolog dialect: sicstus

  prob2-kernel version: 4.15.0

  RODIN version : 3.9.0-9b87fe13d (  ProB for Rodin 3.2.1.202508121324 de.prob2.feature.feature.group HHU Düsseldorf STUPS Group)

• I am using Trace and Transition objects to manage execution.

• I retrieve parameter values via get_op_from_id(...) when needed.

Any clarification on the intended API usage for this feature would be greatly appreciated.

Best regards,

Paul