Hi Fabio,
there are various ways to call a B machine from another one.
The simplest is to INCLUDE the machine.
Here is a simple example. The operation incb increments both y and calls the operation inc of machine A to increment x.
Greetings,
Michael
MACHINE A
VARIABLES x INVARIANT x:NAT INITIALISATION x:=0
OPERATIONS inc = BEGIN x:=x+1 END
END
MACHINE B
INCLUDES A
VARIABLES y INVARIANT y:NAT INITIALISATION y:=0
OPERATIONS
incb = inc || y:=y+1
END
> --
> 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/665eae1f-0cec-4efd-95d8-562531353561n%40googlegroups.com.