Выбрать соревнование | Задачи | Послать решение | Результаты проверки | Статистика по задачам | Вопросы и ответы | Результаты соревнования | Состояние сервера | Изменить данные | Управление командой | Помощь |

Поиск в глубину (DFS)

Олимпиадные задачи на английском языке

Олимпиадные задачи на английском языке

03/11/2009 | Тренировка (задачи Северного четвертьфинала 2009) (K) |

17/07/2020 | Летние сборы - 9 (командное) (K) |

*Ограничения: время – 3s/6s, память – 256MiB Ввод: input.txt или стандартный ввод Вывод: output.txt или стандартный вывод*

Послать решение Blockly Посылки Темы Где Обсудить (0)

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)`, where `P` is a
finite set of atomic propositions, `S` is a finite set of model's states,
`S_0\ sub\ S` is a set of initial states, `R\ &sub\ S\ times\ S`
is a transition relation, and `L\ sub\ S\ times\ P` 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\ "isin"\ S`.

A *path* `pi` beginning in state `s` in the Kripke model is an infinite
sequence of states `s_0\ s_1\ …` such that `s_0=s`, and for each `i\ ≥\ 0`
the `(s_i,\ s_{i+1})\ "isin"\ R`.

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\ "isin"\ P` then `p` is a state formula that holds in state `s` if
`(s,\ p)\ "isin"\ L`.

If `f` is a path formula, then `A\ f` and `E\ f` are state
formulae, where `A` and `E` are

- `A\ f` holds in a state `s`, if `f` holds for each path beginning in the state `s`;

- `E\ f` holds in state `s`, if there exists a path `pi`, beginning in the state `s`, such that `f` holds for `pi`.

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

- `G\ f` (Globally) holds for a path `pi\ =\ s_0\ s_1\ …` if for each `i\ ≥\ 0` the formula `f` holds in the state `s_i`;

- `f\ U\ g` (Until) holds for a path `pi\ =\ s_0\ s_1\ …` if there exists `i\ ≥\ 0` such that `f` holds for each state in the range `s_0,\ s_1,\ …,\ s_{i-1}`, and `g` holds in state `s_i`.

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 `c_i` – a number of atomic propositions
which are true for this state and a space-separated list of these atomic
propositions (`0\ ≤\ c_i\ ≤\ k`). Atomic propositions are denoted by first
`k` small English letters.

Next `m` lines describe transitions. Each of them contains two integer
numbers `s` and `t` (`1\ ≤\ s,\ t\ ≤\ n`; `s\ ≠\ t`) – the transition
from state `s` to state `t`. The verified Kripke model contains implicit
loop transitions `(s,\ s)` for each state `s` (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.

Sample Input

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))

Sample Output

5 1 2 3 4 5