module composition

6 views
Skip to first unread message

Franco Mazzanti

unread,
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?

Franco

Michael Leuschel

unread,
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,
Michael

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

"query-operation expected
Locks.mch
Doors.mch
Reply all
Reply to author
Forward
0 new messages