mtype = { open, close } mtype out=open, in=close; byte water_level=25; byte user_water=0; /* user reservoir */ active proctype Sensors() { do :: atomic{ (water_level<=20) -> out=close; in=open } :: atomic{ (water_level>=30) -> out=open; in=close } od } active proctype User() { do :: (user_water>0) -> user_water-- :: true -> skip od } active proctype Inlet() { do :: (in==open) -> water_level++ od } active proctype Outlet() { do :: (out==open) -> atomic{ water_level--; user_water++ } od } active proctype Monitor() { do :: assert( water_level>=20 && water_level<=30 ) od }