//Probability of successfully querying for all stock prices given we never see web_0 failure
<<controller>> P>=0.9999 [ F "done" ]
<<controller>> P>=0.999 [ F "done" ]
//Querying for all stock prices below given time threshold
<<controller>> R<=10000 [ C ]