Duelling Cowboys

To give a first intuition on probabilistic programs, consider the short example below which models two duelling cowboys. The program is specified basically in Dijkstra's guarded command language with the extension that ( x := 1 [0.6] x := 0 ) uses the new feature of a probabilistic choice, where x is set to 1 with probability 0.6 and set to 0 with probability 0.4.

( t := A [] t := B );
c := 1;
while ( c = 1 ) {
  if ( t = A ) {
    ( c := 0 [a]  t := B );
  } else {
    ( c := 0 [b] t := A );
  }
}

There are two cowboys, A and B, who are fighting a classical duel. They take turns, shooting at each other until one of them is hit. If A (resp. B) shoots then he hits B (resp. A) with probability a (resp. b). We assume that either cowboy A or B is allowed to start; the choice of who will start is resolved nondeterministically. Variable t keeps track of the turns, while c determines whether the duel continues or someone is hit. Note that it is a distinctive feature that we do not have to specify exact probabilities and instead allow arbitrary parameters such as a and b.