checking variable updates

[Franco Mazzanti]

Is there a way to  assert /  verify /  model_check  that:

+ only the operation myop   can modify a variable  v

+ the operation myop always increments by one variable v

So far I have not been able to find a solution, but maybe there is a simple way to specify/verify that?

Best Regards

 Franco Mazzanti

[Michael Leuschel]

Dear Franco,

1) (only the operation myop can modify a variable v)
To check which variables are read and written you can inspect the read-write matrix.

with the command-line version of ProB (probcli) you can output the read/write matrix.
Here is an example:

$ probcli scheduler.mch -read_write_matrix
Operation,ReadsGuard,ReadsAction,MustWrite,MayWrite
nr_ready,{},{ready},{},{}
new,{},{active ready waiting},{waiting},{}
del,{},{waiting},{waiting},{}
ready,{},{active ready waiting},{waiting},{active ready}
swap,{active},{active ready waiting},{active waiting},{ready}

In ProB Tcl/Tk you can use the command “Read/Write Matrix” in the Analyse -> Enabling Analysis menu.
Here you can also save the result to a CSV file.

Similarly, in ProB2-UI there is a “Table Visualization” dialog, where you can select the read/write matrix.

=================

2) ( only the operation myop can modify a variable v + the operation myop always increments by one variable v )

You could use refinement to check your particular verification condition, e.g., try to write something like this:

MACHINE A
VARIABLES v
INVARIANT v:NATURAL
INITIALISATION v:=0
OPERATIONS myop = v := v+1
END

REFINEMENT R REFINES A
DEFINITIONS SET_PREF_ALLOW_NEW_OPERATIONS_IN_REFINEMENT == TRUE
…

If you code (the Event-B equivalent of) this in Rodin and use ProB then the multi-level animation will check that your refinement machine R respects the abstraction A.
If you wish to use classical B things are a bit more difficult.
Maybe if you send me your full specification, I can give you more precise instructions.

I don’t think your property can be expressed in propositional LTL, as supported by ProB.

Greetings,
Michael

> --
> You received this message because you are subscribed to the Google Groups "ProB Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prob-users+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/prob-users/80b1b000-fc39-40e6-aca8-1b7c845abb2d%40googlegroups.com.

[Franco Mazzanti]

Thanks for the very interesting suggestions.

I need some time for digesting and experimenting them.

I will surely send you the specification on which I am working,

hoping it might provide interesting feedbacks on your tool (and further useful suggestions for me :-) )

Best Regards

 Franco