Call a machine from another one

[Fabio Randazzo]

Hi everybody,

there is a way to call a machine from another one?

I mean, from state "B" of a first machine call a whole machine with its own variables, invariant, etc in order to avoid a merging my models in a single machine?

thank you in advance

Fabio

[Michael Leuschel]

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.