module Prop() { process = { int proportion; } int MaxProp = 100; admission = { int totalProp = 0; admission_criteria(int prop) = { prop >= 0 && totalProp + prop <= MaxProp } admission_attach(process p) = { totalProp += p.proportion; } admission_detach(process p) = { totalProp -= p.proportion; } } interface = { void attach(requires process p, int prop) { p.proportion = prop; next(); } } }