Kripke Model

문제

Testing and quality assurance are very time-consuming stages of software development process. Different techniques are used to reduce cost and time consumed by these stages. One of such techniques is software verification. Model checking is an approach to the software verification based on Kripke models.

A Kripke model is a 5-tuple $(P,S,S_0,R,L)(P,\; S,\; S\_\{0\},\; R,\; L)$, where $PP$ is a finite set of atomic propositions, $SS$ is a finite set of model's states, $S_0\subset SS\_\{0\}\; \backslash subset\; S$ is a set of initial states, $R\subset S\times SR\; \backslash subset\; S\; \backslash times\; S$ is a transition relation, and $L\subset S\times PL\; \backslash subset\; S\; \backslash times\; P$ is a truth relation. In this problem we will not take initial states into account and relation $RR$ will be a reflexive relation, so $R(s,s)R(s,\; s)$ will be true for all states $s\in Ss\; \backslash in\; S$.

A path $\pi \backslash pi$ beginning in state $ss$ in the Kripke model is an infinite sequence of states $s_0{s}_1\dots s\_0\; s\_1\; \backslash ldots$ such that $s_0=ss\_0=s$, and for each $i\ge 0i\; \backslash ge\; 0$ the $(s_i,s_{i+1})\in R(s\_i,\; s\_\{i+1\})\; \backslash in\; R$. 

Temporal logic and its subset Computational tree logic (CTL) are used to describe propositions qualified in terms of time. Kripke models are often used to check properties, described in CTL. 

There are two types of formulae in CTL: state formulae and path formulae. The values of state and path formulae are evaluated for states and paths correspondingly.

If $p\in Pp\; \backslash in\; P$ then $pp$ is a state formula that holds in state $ss$ iff $(s,p)\in L(s,\; p)\; \backslash in\; L$. 

If $ff$ is a path formula, then $\mathbf{A}f\backslash mathrm\{\backslash mathbf\{A\}\}\; f$ and $\mathbf{E}f\backslash mathrm\{\backslash mathbf\{E\}\}\; f$ are state formulae, where $\mathbf{A}\backslash mathrm\{\backslash mathbf\{A\}\}$ and $\mathbf{E}\backslash mathrm\{\backslash mathbf\{E\}\}$ are path quantifiers:

• $\mathbf{A}f\backslash mathrm\{\backslash mathbf\{A\}\}\; f$ holds in a state $ss$, iff $ff$ holds for each path beginning in the state $ss$;
• $\mathbf{E}f\backslash mathrm\{\backslash mathbf\{E\}\}\; f$ holds in state $ss$, iff there exists a path $\pi \backslash pi$, beginning in the state $ss$, such that $ff$ holds for $\pi \backslash pi$.

If $ff$ and $gg$ are state formulae, then $\mathbf{G}f\backslash mathrm\{\backslash mathbf\{G\}\}\; f$ and $f\mathbf{U}gf\; \backslash mathrm\{\backslash mathbf\{U\}\}\; g$ are path formulae, where $\mathbf{G}\backslash mathrm\{\backslash mathbf\{G\}\}$ and $\mathbf{U}\backslash mathrm\{\backslash mathbf\{U\}\}$ are temporal operators:

• $\mathbf{G}f\backslash mathrm\{\backslash mathbf\{G\}\}\; f$ (Globally) holds for a path $\pi =s_0{s}_1\dots \backslash pi\; =\; s\_0\; s\_1\; \backslash ldots$ iff  for each $i\ge 0i\; \backslash ge\; 0$ the formula $ff$ holds in the state $s_{i}s\_i$;
• $f\mathbf{U}gf\; \backslash mathrm\{\backslash mathbf\{U\}\}\; g$ (Until) holds for a path $\pi =s_0{s}_1\dots \backslash pi\; =\; s\_0\; s\_1\; \backslash ldots$ if there exists $i\ge 0i\; \backslash ge\; 0$ such that $ff$ holds for each state in the range $s_0,s_1,\dots ,s_{i-1}s\_0,\; s\_1,\; \backslash ldots,\; s\_\{i-1\}$, and $gg$ holds in state $s_{i}s\_i$;

To verify a property described by a state formula $ff$ means to find all states, $ff$ holds for. Verification of an arbitrary property is a pretty complex problem. Your problem is much easier --- you are to write a program that verifies a property described by a temporal logic formula $\mathbf{E}(x\mathbf{U}(\mathbf{A}\mathbf{G}y))\backslash mathrm\{\backslash mathbf\{E\}\}\; (x\; \backslash mathrm\{\backslash mathbf\{U\}\}\; (\backslash mathrm\{\backslash mathbf\{A\}\}\; \backslash mathrm\{\backslash mathbf\{G\}\}\; y))$, where $xx$ and $yy$ are some atomic propositions.

입력

The first line of the input file contains three positive integer numbers $nn$, $mm$ and $kk$ --- number of states, transitions and atomic propositions ($1\le n\le 100001\; \backslash le\; n\; \backslash le\; 10\backslash ,000$; $0\le m\le 1000000\; \backslash le\; m\; \backslash le\; 100\backslash ,000$; $1\le k\le 261\; \backslash le\; k\; \backslash le\; 26$).

The following $nn$ lines describe one state each. The state $ii$ ($1\le i\le n1\; \backslash le\; i\; \backslash le\; n$) is described by $c_{i}c\_i$ --- a number of atomic propositions which are true for this state and a space-separated list of these atomic propositions ($0\le c_i\le k0\; \backslash le\; c\_i\; \backslash le\; k$). Atomic propositions are denoted by first $kk$ small English letters.

Next $mm$ lines describe transitions. Each of them contains two integer numbers $ss$ and $tt$ ($1\le s,t\le n1\; \backslash le\; s,\; t\; \backslash le\; n$; $s\mathrm{\ne }ts\; \backslash ne\; t$) --- the transition from state $ss$ to state $tt$. The verified Kripke model contains implicit loop transitions $(s,s)(s,\; s)$ for each state $ss$ (they are not listed in the input file). No transition is listed in the input file twice.

The last line of the input file contains the formula of the property to be verified. This formula always has the form E(xU(AGy)), where x and y are some atomic propositions.

출력

The first line of the output file must contain the number of states for which the verified property holds. The following lines must contain the numbers of these states listed in increasing order.

7 8 2
1 a
1 a
2 a b
1 b
1 b
1 a
1 a
1 2
2 3
3 4
4 5
5 3
2 6
6 7
7 6
E(aU(AGb))

5
1
2
3
4
5