Text this: Modelovanie a verifikácia vlastností algoritmov vzájomného vylúčenia v prostredi SPIN