Problem K. Kripke Model

Author:ACM ICPC 2009-2010, NEERC, Northern Subregional Contest   Time limit:3 sec
Input file:kripke.in   Memory limit:256 Mb
Output file:kripke.out  

Statement

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 (AP, S, S0, R, L), where AP is a finite set of atomic propositions, S is a finite set of model's states, S0 ⊂ S is a set of initial states, R ⊂ S × S is a transition relation, and L ⊂ S × AP is a truth relation. In this problem we will not take initial states into account and relation R will be a reflexive relation, so R(s, s) will be true for all states s ∈ S.

A path π beginning in state s in the Kripke model is an infinite sequence of states s0 s1 such that s0 = s, and for each i ≥ 0 the (si, si + 1) ∈ 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 ∈ AP then p is a state formula that holds in state s iff (s, p) ∈ L.

If f is a path formula, then A f and E f are state formulae, where A and E are path quantifiers:

If f and g are state formulae, then G f and fU g are path formulae, where G and U are temporal operators:

To verify a property described by a state formula f means to find all states, f 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 E (x U(A G y)), where x and y are some atomic propositions.

Input file format

The first line of the input file contains three positive integer numbers n, m and k — number of states, transitions and atomic propositions (1 ≤ n ≤ 10 000; 0 ≤ m ≤ 100 000; 1 ≤ k ≤ 26).

The following n lines describe one state each. The state i (1 ≤ i ≤ n) is described by ci — a number of atomic propositions which are true for this state and a space-separated list of these atomic propositions (0 ≤ ci ≤ k). Atomic propositions are denoted by first k small English letters.

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.

Output file format

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.

Sample tests

No. Input file (kripke.in) Output file (kripke.out)
1
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

0.117s 0.010s 13