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!