// These valueas are computed for pp1=pp2=0.25, pp3=0.4
Pmax=? [ F (ES=6) {ES=2} ]
//Maximal and minimal expected number of clients that server //addresses during adaptation from various phases
//The complete migration is covered with ES=2 (initialization) to //ES=6 reaching ToBe behaviour
Rmax=? [ F (ES=6) {ES=2} ]
Rmin=? [ F (ES=6) {ES=2} ]
Rmax=? [ F (ES=3) {ES=2} ]
Rmin=? [ F (ES=3) {ES=2} ]
Rmax=? [ F (ES=4) {ES=3} ]
Rmin=? [ F (ES=4) {ES=3} ]
Rmax=? [ F (ES=5) {ES=4} ]
Rmin=? [ F (ES=5) {ES=4} ]
Rmax=? [ F (ES=6) {ES=5} ]
Rmin=? [ F (ES=6) {ES=5} ]
//There is always, in any phase, at most one client served
P>=1 [G ( ("critical1" => (!"critical2" & !"critical3" & !"critical4")) & ("critical2" => (!"critical1" & !"critical3" & !"critical4")) & ("critical4" => (!"critical2" & !"critical3" & !"critical1")) & ("critical3" => (!"critical1" & !"critical2" & !"critical4")))]
//There is always, in any phase, at most one client served
num_procs_in_crit <= 1
//Liveness property
"one_trying" => P>=1 [ F "one_in_critical" ]
//Once ToBe, always ToBe
"ToBeOfClient1" => P>=1 [G !"AsIsOfClient1"]
//if Client1 requests service, it gets it eventually with //probability 1
s1=3 => P>=1 [F (S1=3 | S1=5)]
//The system adapts to ToBe behaviour with probability 1
P>=1[F ES=6 & E1=2 & E2=2 &E3=2 &E4=2]
//Interesting to check - If Client1 requests service in AsIs
//it is served not latter than phase ES=2, that is, either //immediattely in phase AsIs, or in the next Choice2 phase, but not //latter than these two. The next quantitative property computes the //maximal expected number of server steps
Rmax=? [ F ((S1=3|S1=5) & (ES=1|ES=2)) {(s1=3 & ES=1)} ]