Skip to content
Permalink
master
Go to file
 
 
Cannot retrieve contributors at this time
31 lines (28 sloc) 671 Bytes
// Coupon Collector Description (by Christian Dehnert)
// cite: Jansen et al., Bounded Model Checking for Probabilistic Programs, ATVA 2016
// Automatically Generated by: storm-pgcl-BG
// Sebastian Junges; RWTH Aachen University
function coupon() {
var {
bool coup0 := false;
bool coup1 := false;
bool coup2 := false;
int draw0 := 0;
int draw1 := 0;
int numberDraws := 0;
}
while (!(coup0 & coup1 & coup2)) {
draw0 := unif(0, 2);
draw1 := unif(0, 2);
numberDraws := numberDraws + 1;
if (draw0 = 0 | draw1 = 0) {
coup0 := true;
}
if (draw0 = 1 | draw1 = 1) {
coup1 := true;
}
if (draw0 = 2 | draw1 = 2) {
coup2 := true;
}
}
}
You can’t perform that action at this time.