module process
{
    var s : boolean;  // shared variable
    var y : boolean;  // local variable

    init {
        s = true;
        y = false;
    }

    next {
        if (y && s) {
            y' = false;
        }
    }
}

module main
{
    instance p0 : process;
    instance p1 : process;

    init {
        // initial state
    }

    next {
        next(p0);
        next(p1);
    }

    property mutual_exclusion {
        forall i : boolean {
            !((p0.y == 1) && (p1.y == 1) && (p0.s == p1.s));
        }
    }

    property starvation_freedom {
        forall i : boolean {
            !((p0.y == 1) && (p1.y == 1) && (p0.s == p1.s));
        }
    }
}
