module composition

Skip to first unread message

Franco Mazzanti

Jun 6, 2019, 6:50:42 AM6/6/19
to ProB Users
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?


Michael Leuschel

Jun 6, 2019, 7:13:47 AM6/6/19
to Franco Mazzanti, ProB Users
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,

On 6 Jun 2019, at 12:50, Franco Mazzanti <> wrote:

"query-operation expected
Reply all
Reply to author
0 new messages