Optimizing Event Parameter Generation in JeB: Leveraging ProB Constraint Solver

[Boris]

Hello everyone,

I am a student, and as part of my final project, I am working on an extension for the JeB framework aimed at improving the efficiency of parameter generation for events. JeB allows simulating programs specified in Event-B, but parameter generation can sometimes be inefficient because it requires finding a parameter that meets a guard associated with each event. To address this issue, one proposed approach is to leverage the constraint solver of ProB.

I was wondering if there is a way to produce a file that can be used to exploit this solver, for example, in the form of a list of values that satisfy the guards for event parameters, or perhaps a standard file format that would allow leveraging the solver data in JeB. Have any of you encountered this kind of situation before?

Thank you for your feedback and advice !

 Best regards,

Boris Merminod