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

12 views
Skip to first unread message

Denis Efremov

unread,
Mar 4, 2020, 6:54:49 AM3/4/20
to ProB Users
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!
test.zip

Michael Leuschel

unread,
Mar 4, 2020, 11:46:18 AM3/4/20
to Denis Efremov, ProB Users
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
Reply all
Reply to author
Forward
0 new messages