定義

x と y が action ならば，(x -> P | y -> Q) は初めに x または y のどちらか一方の動作を表す process を表す．1つ目の action が起こった後に，もし1つ目の action が x ならば P (y ならば Q) によって表されるプロセスと同じ振る舞いをする．

サンプル

FAULTY = (red   -> FAULTY
         |blue  -> FAULTY
         |green -> FAULTY
         |yellow -> candy -> FAULTY
         ).

Choice は，"{}" によってくくることが可能です．よって上の FSP と下の FSP は同じモデルを表します．

FAULTY = ({red,blue,green}-> FAULTY 
         |yellow -> candy -> FAULTY
         ).

LTS はどちらも以下のとおり．