Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more