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.