6.4 Miscellaneous Propagators

disjoint

{Schedule.disjoint *D1 +I1 *D2 +I2}

creates a propagator for D1+I1\leq D2 \;\vee\;
D2+I2\leq D1. Its operational semantics is defined by

or D1 + I1 =<: D2 
[] 
D2 + I2 =<: D1 
end


Denys Duchier, Leif Kornstaedt, Martin Homik, Tobias Müller, Christian Schulte and Peter Van Roy
Version 1.4.0 (20080702)