module composition

[Franco Mazzanti]

I struggled to find a way to define two modules A and B, where an operation of A calls an operation of B.

According to the ProB syntax, a call operation seems to be accepted as a possible Statement 

  "x <-- OP(x)  call operation and assign return value"

but I cannot find a way to exploit this feature, as ai get the error message "query-operation expected"

Is it possible to see a minimal example on how to correctly use this feature?

Franco

[Michael Leuschel]

Dear Franco,

you probably use SEES to include one machine into another.

In that case you are not allowed to change the state of the seen machine; in B a machine’s state can only be changed by one other machine.

Try and use INCLUDES instead of SEES.

Below is an example from Steve Schneider’s book on B.

Kind regards,

Michael

On 6 Jun 2019, at 12:50, Franco Mazzanti <fra...@gmail.com> wrote:

"query-operation expected