function f (int<1> c; int x) : int {
    chp {
        [ c=0 -> self:=x+1 [] c=1 -> self:=x-1 ]
    }
}

defproc p1 () {
    int x,y;
    int<1> c;
    chp {
        y:=f(c,x)
    }
}

defproc p2 () {
    int x,y;
    int<1> c;
    chp {
        [ c=0 -> y:=x+1 [] c=1 -> y:=x-1 ]    
    }
}