{"Rabin_index":1,"Streett_index":1,"acc_word":"a & !b; !a & !b; cycle{!a & b}","mp_class":"R","mp_class_text":"a recurrence property","mp_hierarchy_svg":"\n<svg height=\"210\" width=\"220\" xmlns=\"http://www.w3.org/2000/svg\" version=\"1.1\">\n<polygon points=\"20,0 200,120 200,210 20,210\" fill=\"cyan\" opacity=\".2\" />\n<polygon points=\"20,120 155,210 20,210\" fill=\"cyan\" opacity=\".2\" />\n<polygon points=\"200,0 20,120 20,210 200,210\" fill=\"magenta\" opacity=\".15\" />\n<polygon points=\"200,120 65,210 200,210\" fill=\"magenta\" opacity=\".15\" />\n<g transform=\"translate(40,80)\">\n    <line x1=\"-10\" y1=\"-10\" x2=\"10\" y2=\"10\" stroke=\"red\" stroke-width=\"5\" />\n    <line x1=\"-10\" y1=\"10\" x2=\"10\" y2=\"-10\" stroke=\"red\" stroke-width=\"5\" />\n    </g>\n<g text-anchor=\"middle\" font-size=\"14\">\n<text x=\"110\" y=\"20\">Reactivity</text>\n<text x=\"60\" y=\"65\">Recurrence</text>\n<text x=\"160\" y=\"65\">Persistence</text>\n<text x=\"110\" y=\"125\">Obligation</text>\n<text x=\"60\" y=\"185\">Safety</text>\n<text x=\"160\" y=\"185\">Guarantee</text>\n</g>\n<g font-size=\"14\">\n<text text-anchor=\"begin\" transform=\"rotate(-90,18,210)\" x=\"18\" y=\"210\" fill=\"gray\">Monitor</text>\n<text text-anchor=\"end\" transform=\"rotate(-90,18,0)\" x=\"18\" y=\"0\" fill=\"gray\">Deterministic B\u00fcchi</text>\n<text text-anchor=\"begin\" transform=\"rotate(-90,214,210)\" x=\"214\" y=\"210\" fill=\"gray\">Terminal B\u00fcchi</text>\n<text text-anchor=\"end\" transform=\"rotate(-90,214,0)\" x=\"214\" y=\"0\" fill=\"gray\">Weak B\u00fcchi</text>\n</g>\n</svg>","rej_word":"a & !b; a & !b; !a & !b; cycle{!a & b}","safety_liveness":"none","sfh_class":"\u03a0\u2082","sfh_class_text":"Ignoring X operators, in each branch of the syntax tree, weak temporal operators (G, W, R, ...) appear above strong operators (F, U, M, ...).","stutter_invariant":false}