ProB Java API: Is it possible to fill sets with own values at setup_constants step?

[Denis Efremov]

Hi,

Let's suppose we've got Event-B 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


machine M0
    sees C0

variables
    Names

invariants
    @Names_type
        Names ⊆ NAMES

events
    event INITIALISATION
      then
        @act1 Names ≔ ∅
    end

    event add_name
      any
        name
      where
        @grd1 name ∈ NAMES ∖ Names
      then
        @act1 Names ≔ Names ∪ {name}
    end

end

NAMES is filled by ProB with default values {NAMES1, NAMES2, ... NAMES10}.

Is there an API to use custom values? For example I want to fill the set with {Bill, John, Mary, Ann, ...}.

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);
        System.out.println(f.get(api));
        FactoryProvider factory_provider = (FactoryProvider) f.get(api);
        EventBFactory factory = factory_provider.getEventBFactory();

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

        AbstractElement fsp = model.getComponent("M0");

        StateSpace stateSpace = model.load(fsp);

// Fill sets with own values

        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());

        t = t.execute("add_name", "name=NAMES1"); // Works with default value
        System.out.println(t.getCurrent().getTransition().evaluate().getPrettyRep());
}

Thanks!