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

5 views
Skip to first unread message

Denis Efremov

unread,
Mar 4, 2020, 7:17:06 AM3/4/20
to ProB Users
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!
setfill.zip
Reply all
Reply to author
Forward
0 new messages