Machines with parameters (SETS and scalar) and INCLUDES

MACHINE
trucM4(AA, maxe)
CONSTRAINTS
maxe : 5..10 &
card(AA) >maxe

VARIABLES
var
INVARIANT
var <: AA & card(var) < trucm1op =" ANY" style="font-weight: bold;">MACHINE
trucM5(AA,maxe)
CONSTRAINTS
maxe : 5..10 & card(AA)> maxe
INCLUDES
tien.trucM4(AA, maxe), mon.trucM4(AA, maxe)
OPERATIONS
optrucM2 =
BEGIN
tien.trucM1op ||
mon.trucM1op
END
END

Type check and proofs ok with Atelier B