ProB Java API: Is it possible to refine a set cardinality before setup_constants step?

[Denis Efremov]

Hi,

for example, I've got an Event-B model with NAMES set and I can't change this model:

context C0

sets
    NAMES

end

Is it possible to alter the model (for model-checking) so that NAMES is finite and set its cardinality with ProB Java API? I think that ProB already do this internally, but I need to use my cardinality size and not the default one (4).

I want to alter the model to something like this with API without really changing the model:

context C0

sets
    NAMES

constants
    NAMES_CARD

axioms
    @FINATE_NAMES
        finite(NAMES)
    @CARD_NAMES
        card(NAMES) = NAMES_CARD
    @NAMES_CARD_VALUE
        NAMES_CARD = 10

end

Java load:

public void start() throws Exception {
        System.out.println("ProB version: " + api.getVersion());
        System.out.println();
        System.out.println("Load Event-B Machine");

        Field f = api.getClass().getDeclaredField("modelFactoryProvider");
        f.setAccessible(true);
        FactoryProvider factory_provider = (FactoryProvider) f.get(api);
        EventBFactory factory = factory_provider.getEventBFactory();

        Path path = Paths.get(getClass().getResource("/test.zip").toURI());
        EventBModel model = factory.extractModelFromZip(path.toAbsolutePath().toString());

        AbstractElement m = model.getComponent("M0");
        StateSpace stateSpace = model.load(m);

// SET finite(NAMES) for model checking
// SET card(NAMES) = 10

        Trace t = new Trace(stateSpace);
        t = t.execute("$setup_constants");
        System.out.println(t.getCurrent().getTransition().evaluate().getPrettyRep());
        t = t.execute("$initialise_machine");
        System.out.println(t.getCurrent().getTransition().evaluate().getPrettyRep());

...

}

                                                                               

Thanks!

[Michael Leuschel]

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