Quelle  synch_parameter_constraints.pvs

%
% Purpose      : Definition of the constraint that is required for the
%                theory parameters of synchronization.
%
synch_parameter_constraints: THEORY

  BEGIN

  P: VAR posnat
  rho, alpha_l, alpha_u, pi: VAR nonneg_real

  P_bound?(P, rho, alpha_l, alpha_u, pi): bool =
    (1 + rho) * (pi + max(alpha_l, alpha_u) + P * ((1 + rho) - 1 / (1 + rho)))  < P

  END synch_parameter_constraints