Hi Denis,
what I typically do in Rodin is to have animation contexts.
This is explained briefly here:
https://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_Parameters#Size_of_unspecified_sets_.28carrier_sets.29
Basically, you extend your context C0 into C0_prob with additional properties and constants.
context C0_prob extends C0
constants a,b,c
axioms
@prob_axm partition(NAMES,{a},{b},{c})
end
Then you also need to refine the machine you wish to animate/validate and see C0_prob.
The advantage is that the context C0 and the other machines are kept unchanged for proof.
We use Rodin refinement as a way to describe animation configurations using the B language.
However, I am not sure this is feasible for you here.
Otherwise, there are various ways to influence the size of the deferred sets in ProB (see
https://www3.hhu.de/stups/prob/index.php/Deferred_Sets):
- you can set the DEFAULT_SETSIZE preference, this can be done in the ProB-Java-API but affects all deferred sets,
- you can set a size per deferred set in probcli by providing a command-line argument: -card <GS> <VAL>
I am not sure this is available in the ProB-Java-API; but I guess it should be possible to add such a feature to ProB2.
Within the ProB-Java-API one can construct new Event-B models, so maybe the technique described above
(
https://www3.hhu.de/stups/prob/index.php/Tutorial_Rodin_Parameters#Size_of_unspecified_sets_.28carrier_sets.29)
could be done automatically at runtime, but it is of course a bit cumbersome.
> On 4 Mar 2020, at 12:54, Denis Efremov <
yefremo...@gmail.com> wrote:
>
>
> I want to alter the model to something like this with API without really changing the model:
Greetings,
Michael