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.

1   ( t := A [] t := B );
2   c := 1;
3   while ( c = 1 ) {
4      if ( t = A ) {
5         ( c := 0 [a]  t := B );
6      } else {
7         ( c := 0 [b] t := A );
8      }
9   }

 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.