; Section 2.2, lift specification (3a)-(3n) ; ; trp++uc -s BFS -f ltl -u -g ltl --no-nnf --no-ltl-simplification lift.trp ; (not u) & f0 & (not b0) & (not b1) & (not up) & (always ((u -> not next u) & ((not next u) -> u))) & (always (f0 -> not f1)) & (always ((f0 -> next (f0 | f1)) & (f1 -> next (f0 | f1)))) & (always (u -> ((f0 -> next f0) & ((next f0) -> f0) & (f1 -> next f1) & ((next f1) -> f1)))) & (always ((not u) -> ((b0 -> next b0) & ((next b0) -> b0) & (b1 -> next b1) & ((next b1) -> b1)))) & (always (((b0 & not f0) -> next b0) & ((b1 & not f1) -> next b1))) & (always ((f0 & next f0) -> ((up -> next up) & ((next up) -> up)))) & (always ((f1 & next f1) -> ((up -> next up) & ((next up) -> up)))) & (always (((f0 & next f1) -> up) & ((f1 & next f0) -> not up))) & (always ((sb -> (b0 | b1)) & ((b0 | b1) -> sb))) & (always ((f0 & not sb) -> (f0 until not ((not sb) until not ((sometime f0) & not up))))) & (always ((f1 & not sb) -> (f1 until not ((not sb) until not ((sometime f0) & not up))))) & (always ((b0 -> sometime f0) & (b1 -> sometime f1))) ; ; 1st scenario (4) & b1 ; ; 2nd scenario (6) ;& next b1 ; ; 3rd scenario (not shown in paper) ;& next next b1 ; ; 4th scenario (8) ;& sometime b1