const int T; // time bound // maximum path length at time T R{"max_path_len_sq"}min=?[I=T] // minimum under all schedulers R{"max_path_len_sq"}max=?[I=T] // maximum under all schedulers R{"max_path_len_sq"}=?[I=T] // for DTMC model // to get the variance plots for the maximum path length (dtmc model) R{"max_path_len"}=?[I=T]+pow(R{"max_path_len_sq"}=?[I=T]-pow(R{"max_path_len"}=?[I=T],2), 0.5) R{"max_path_len"}=?[I=T]-pow(R{"max_path_len_sq"}=?[I=T]-pow(R{"max_path_len"}=?[I=T],2), 0.5) // states where network is connected label "done" = max_path_len<4; // minimum and maximum probability nodes become connected Pmin=? [ F<=T "done" ] Pmax=? [ F<=T "done" ] // minimum and maximum expected number of rounds until connected R{"rounds"}min=? [ F "done" ] R{"rounds"}max=? [ F "done" ]