1 of 596

АПСУ

Автоматное программирование систем управления

12 лекций · практикум на строгом C90 · верификация на SPIN

Хлебников Андрей · версия курса 1.8.0

github.com/BasePractice/statecraft

2 of 596

План курса

Введение. Дискретные системы, алфавиты, слова и языки

Конечный автомат. Модели Мили и Мура

Синтез автоматов и автоматные схемы

Автоматы-акцепторы. ДКА и НКА

Регулярные события и теорема Клини

Регулярные выражения и лексический анализ

Автоматное программирование

Иерархические автоматы и кодогенерация

Верификация и тестирование автоматных программ

Границы модели. Машина Тьюринга и вычислимость

Клеточные автоматы и самовоспроизведение

Язык Takt: описание автоматов и порождение кода

Автоматное программирование систем управления

3 of 596

Откуда взялась дисциплина

Две родословные, до середины XX века не пересекавшиеся

Автоматное программирование систем управления

4 of 596

Откуда взялась дисциплина

Две родословные, до середины XX века не пересекавшиеся

Со стороны техники — релейная автоматика: Шеннон, 1938 — контактная схема есть булева функция, значит схемы можно считать, а не подбирать

Автоматное программирование систем управления

5 of 596

Откуда взялась дисциплина

Две родословные, до середины XX века не пересекавшиеся

Комбинационная схема не помнит ничего; чтобы описать реакцию, зависящую от предыстории, понадобилось состояние

Автоматное программирование систем управления

6 of 596

Откуда взялась дисциплина

Две родословные, до середины XX века не пересекавшиеся

Хаффман (1954) — синтез последовательностной схемы по таблице переходов; Мили (1955) и Мур (1956) — две модели

Автоматное программирование систем управления

7 of 596

Откуда взялась дисциплина

Две родословные, до середины XX века не пересекавшиеся

Хаффман (1954) — синтез последовательностной схемы по таблице переходов; Мили (1955) и Мур (1956) — две модели

Со стороны математики — Мак-Каллок и Питтс (1943), Клини (1951): распознаваемые события в точности регулярны

Автоматное программирование систем управления

8 of 596

Откуда взялась дисциплина

Две родословные, до середины XX века не пересекавшиеся

Хаффман (1954) — синтез последовательностной схемы по таблице переходов; Мили (1955) и Мур (1956) — две модели

Со стороны математики — Мак-Каллок и Питтс (1943), Клини (1951): распознаваемые события в точности регулярны

Границу очертил Тьюринг (1936): есть задачи, которые не решает никакая машина

Автоматное программирование систем управления

9 of 596

Откуда взялась дисциплина

Две родословные, до середины XX века не пересекавшиеся

Хаффман (1954) — синтез последовательностной схемы по таблице переходов; Мили (1955) и Мур (1956) — две модели

Со стороны математики — Мак-Каллок и Питтс (1943), Клини (1951): распознаваемые события в точности регулярны

Границу очертил Тьюринг (1936): есть задачи, которые не решает никакая машина

Один и тот же объект — схема, распознаватель и программа одновременно

Автоматное программирование систем управления

10 of 596

Чем эта дисциплина не является

Автоматное программирование систем управления

11 of 596

Чем эта дисциплина не является

Дискретная математика даёт язык — множества, отношения, булеву алгебру, — но не занимается управляющими программами

Автоматное программирование систем управления

12 of 596

Чем эта дисциплина не является

Схемотехника доводит автомат до вентилей; здесь синтез разбирается до черты, где начинается физическая реализация

Автоматное программирование систем управления

13 of 596

Чем эта дисциплина не является

Теория автоматического управления работает с непрерывными величинами; предмет курса — дискретные события

Автоматное программирование систем управления

14 of 596

Чем эта дисциплина не является

Теория автоматического управления работает с непрерывными величинами; предмет курса — дискретные события

Теория формальных языков пользуется тем же аппаратом, но ради разбора текста, а не ради управления

Автоматное программирование систем управления

15 of 596

Чем эта дисциплина не является

Теория автоматического управления работает с непрерывными величинами; предмет курса — дискретные события

Теория формальных языков пользуется тем же аппаратом, но ради разбора текста, а не ради управления

Программная инженерия отвечает на вопрос «как это сдавать» — отсюда требования к коду и порядок сдачи

Автоматное программирование систем управления

16 of 596

Формы контроля

Вид работы	Что сдаётся	Чем проверяется
Лабораторные	код в репозитории курса	сборка без предупреждений, тесты, оформление
Курсовая работа	автоматная модель прикладной задачи	полнота описания автомата и его реализация
Экзамен	теория лекций	контрольные вопросы в конце каждой лекции

Сквозной пример курса — practices/20-welding-line, линия точечной сварки — устроен так же, как курсовая, и служит образцом ожидаемого объёма.

Автоматное программирование систем управления

17 of 596

Порядок сдачи лабораторной работы

Автоматное программирование систем управления

18 of 596

Порядок сдачи лабораторной работы

Работа ведётся в отдельной ветке; в master и develop напрямую не коммитят

Автоматное программирование систем управления

19 of 596

Порядок сдачи лабораторной работы

Работа ведётся в отдельной ветке; в master и develop напрямую не коммитят

Код собирается в общем режиме курса: ISO C90 без расширений, -Wall -Wextra -pedantic -Werror

Автоматное программирование систем управления

20 of 596

Порядок сдачи лабораторной работы

Работа ведётся в отдельной ветке; в master и develop напрямую не коммитят

Код собирается в общем режиме курса: ISO C90 без расширений, -Wall -Wextra -pedantic -Werror

Предупреждение компилятора — это ошибка сборки, а не замечание

Автоматное программирование систем управления

21 of 596

Порядок сдачи лабораторной работы

Работа ведётся в отдельной ветке; в master и develop напрямую не коммитят

Код собирается в общем режиме курса: ISO C90 без расширений, -Wall -Wextra -pedantic -Werror

Предупреждение компилятора — это ошибка сборки, а не замечание

Тесты проходят полностью: ctest --test-dir build. Работа с падающим тестом не принимается

Автоматное программирование систем управления

22 of 596

Порядок сдачи лабораторной работы

Работа ведётся в отдельной ветке; в master и develop напрямую не коммитят

Код собирается в общем режиме курса: ISO C90 без расширений, -Wall -Wextra -pedantic -Werror

Предупреждение компилятора — это ошибка сборки, а не замечание

Тесты проходят полностью: ctest --test-dir build. Работа с падающим тестом не принимается

Оформление проверено автоматически: ./scripts/check-style.sh (и --fix)

Автоматное программирование систем управления

23 of 596

Порядок сдачи лабораторной работы

Работа ведётся в отдельной ветке; в master и develop напрямую не коммитят

Код собирается в общем режиме курса: ISO C90 без расширений, -Wall -Wextra -pedantic -Werror

Предупреждение компилятора — это ошибка сборки, а не замечание

Тесты проходят полностью: ctest --test-dir build. Работа с падающим тестом не принимается

Оформление проверено автоматически: ./scripts/check-style.sh (и --fix)

Результат оформляется pull request'ом; в описании — что сделано и как проверялось

Автоматное программирование систем управления

24 of 596

ЛЕКЦИЯ

Введение. Дискретные системы, алфавиты, слова и языки

Над чем работает автомат и что такое алгоритм

25 of 596

Алфавит, слово, язык

Практикум: practices/01-words

26 of 596

Алфавит, слово, язык

Алфавит A — конечное непустое множество, его элементы называются буквами

Практикум: practices/01-words

27 of 596

Алфавит, слово, язык

Алфавит A — конечное непустое множество, его элементы называются буквами

Слово в алфавите A — конечная последовательность букв; длина обозначается |α|

Практикум: practices/01-words

28 of 596

Алфавит, слово, язык

Алфавит A — конечное непустое множество, его элементы называются буквами

Слово в алфавите A — конечная последовательность букв; длина обозначается |α|

Слово нулевой длины называется пустым и обозначается ε

Практикум: practices/01-words

29 of 596

Алфавит, слово, язык

Алфавит A — конечное непустое множество, его элементы называются буквами

Слово в алфавите A — конечная последовательность букв; длина обозначается |α|

Слово нулевой длины называется пустым и обозначается ε

Конкатенация αβ — приписывание слова β справа к слову α

Практикум: practices/01-words

30 of 596

Алфавит, слово, язык

Алфавит A — конечное непустое множество, его элементы называются буквами

Слово в алфавите A — конечная последовательность букв; длина обозначается |α|

Слово нулевой длины называется пустым и обозначается ε

Конкатенация αβ — приписывание слова β справа к слову α

A* — множество всех слов алфавита, включая пустое; A⁺ — без пустого

Практикум: practices/01-words

31 of 596

Алфавит, слово, язык

Алфавит A — конечное непустое множество, его элементы называются буквами

Слово в алфавите A — конечная последовательность букв; длина обозначается |α|

Слово нулевой длины называется пустым и обозначается ε

Конкатенация αβ — приписывание слова β справа к слову α

A* — множество всех слов алфавита, включая пустое; A⁺ — без пустого

Язык над A — произвольное подмножество A*

Практикум: practices/01-words

32 of 596

Алфавит, слово, язык

Алфавит A — конечное непустое множество, его элементы называются буквами

Слово в алфавите A — конечная последовательность букв; длина обозначается |α|

Слово нулевой длины называется пустым и обозначается ε

Конкатенация αβ — приписывание слова β справа к слову α

A* — множество всех слов алфавита, включая пустое; A⁺ — без пустого

Язык над A — произвольное подмножество A*

Пустое слово и пустой язык — разные объекты: |{ε}| = 1, а |∅| = 0

Практикум: practices/01-words

33 of 596

Свойства алгоритма

Неформальные требования, точная формализация которых — машина Тьюринга

Автоматное программирование систем управления

34 of 596

Свойства алгоритма

Неформальные требования, точная формализация которых — машина Тьюринга

Дискретность: процесс разбит на шаги, каждый выполняется за конечное время

Автоматное программирование систем управления

35 of 596

Свойства алгоритма

Неформальные требования, точная формализация которых — машина Тьюринга

Дискретность: процесс разбит на шаги, каждый выполняется за конечное время

Определённость: на каждом шаге однозначно определено, что делать дальше; результат не зависит от исполнителя

Автоматное программирование систем управления

36 of 596

Свойства алгоритма

Неформальные требования, точная формализация которых — машина Тьюринга

Дискретность: процесс разбит на шаги, каждый выполняется за конечное время

Результативность: процесс заканчивается за конечное число шагов и выдаёт результат

Автоматное программирование систем управления

37 of 596

Свойства алгоритма

Неформальные требования, точная формализация которых — машина Тьюринга

Дискретность: процесс разбит на шаги, каждый выполняется за конечное время

Результативность: процесс заканчивается за конечное число шагов и выдаёт результат

Массовость: алгоритм применим не к одному входу, а к целому классу входных данных

Автоматное программирование систем управления

38 of 596

Свойства алгоритма

Неформальные требования, точная формализация которых — машина Тьюринга

Дискретность: процесс разбит на шаги, каждый выполняется за конечное время

Результативность: процесс заканчивается за конечное число шагов и выдаёт результат

Массовость: алгоритм применим не к одному входу, а к целому классу входных данных

К формализации курс возвращается в лекции 10 — разобравшись сначала с более простой моделью

Автоматное программирование систем управления

39 of 596

Пример: турникет

Два состояния, четыре перехода. Пример сопровождает курс от формализации (лекция 1) через синтез (лекция 3) до реализации в коде (лекция 7) и проверки (лекция 9)

Автоматное программирование систем управления

40 of 596

Почему Си и почему C90

Приложение курса: «Стандарт языка Си: справочник курса»

41 of 596

Почему Си и почему C90

Практикум курса — ISO C90 без расширений: этот стандарт поддерживают практически все компиляторы

Приложение курса: «Стандарт языка Си: справочник курса»

42 of 596

Почему Си и почему C90

Практикум курса — ISO C90 без расширений: этот стандарт поддерживают практически все компиляторы

Простой синтаксис и жёсткая стандартизация

Приложение курса: «Стандарт языка Си: справочник курса»

43 of 596

Почему Си и почему C90

Практикум курса — ISO C90 без расширений: этот стандарт поддерживают практически все компиляторы

Простой синтаксис и жёсткая стандартизация

Прямое обращение к памяти — обязательное требование для управляющих программ

Приложение курса: «Стандарт языка Си: справочник курса»

44 of 596

Почему Си и почему C90

Практикум курса — ISO C90 без расширений: этот стандарт поддерживают практически все компиляторы

Простой синтаксис и жёсткая стандартизация

Прямое обращение к памяти — обязательное требование для управляющих программ

Простота написания компилятора: язык реалистично портировать на новую платформу

Приложение курса: «Стандарт языка Си: справочник курса»

45 of 596

Почему Си и почему C90

Практикум курса — ISO C90 без расширений: этот стандарт поддерживают практически все компиляторы

Простой синтаксис и жёсткая стандартизация

Прямое обращение к памяти — обязательное требование для управляющих программ

Простота написания компилятора: язык реалистично портировать на новую платформу

Новая волна популярности — основной язык высокого уровня для embedded-платформ

Приложение курса: «Стандарт языка Си: справочник курса»

46 of 596

Почему Си и почему C90

Практикум курса — ISO C90 без расширений: этот стандарт поддерживают практически все компиляторы

Простой синтаксис и жёсткая стандартизация

Прямое обращение к памяти — обязательное требование для управляющих программ

Простота написания компилятора: язык реалистично портировать на новую платформу

Новая волна популярности — основной язык высокого уровня для embedded-платформ

Два документированных исключения: тесты на C++11 (Catch2) и порождённый taktc код на C99

Приложение курса: «Стандарт языка Си: справочник курса»

47 of 596

ЛЕКЦИЯ

Конечный автомат. Модели Мили и Мура

Система канонических уравнений и диаграмма переходов

48 of 596

Что такое автомат

Автоматное программирование систем управления

49 of 596

Что такое автомат

На вход — последовательность символов входного алфавита, на выходе — символы выходного

Автоматное программирование систем управления

50 of 596

Что такое автомат

На вход — последовательность символов входного алфавита, на выходе — символы выходного

Автомат функционирует в дискретном времени: i-й входной символ поступает в i-й момент

Автоматное программирование систем управления

51 of 596

Что такое автомат

На вход — последовательность символов входного алфавита, на выходе — символы выходного

Автомат функционирует в дискретном времени: i-й входной символ поступает в i-й момент

Детерминированность: выход в момент i зависит только от входов до момента i включительно

Автоматное программирование систем управления

52 of 596

Что такое автомат

На вход — последовательность символов входного алфавита, на выходе — символы выходного

Автомат функционирует в дискретном времени: i-й входной символ поступает в i-й момент

Детерминированность: выход в момент i зависит только от входов до момента i включительно

Слово длины n переводится в слово той же длины n

Автоматное программирование систем управления

53 of 596

Что такое автомат

На вход — последовательность символов входного алфавита, на выходе — символы выходного

Автомат функционирует в дискретном времени: i-й входной символ поступает в i-й момент

Детерминированность: выход в момент i зависит только от входов до момента i включительно

Слово длины n переводится в слово той же длины n

Без памяти — выход определяется текущим входом; с памятью — нужно помнить прошлое

Автоматное программирование систем управления

54 of 596

Что такое автомат

На вход — последовательность символов входного алфавита, на выходе — символы выходного

Автомат функционирует в дискретном времени: i-й входной символ поступает в i-й момент

Детерминированность: выход в момент i зависит только от входов до момента i включительно

Слово длины n переводится в слово той же длины n

Без памяти — выход определяется текущим входом; с памятью — нужно помнить прошлое

Запоминание реализуется через понятие состояния; конечное их число — конечный автомат

Автоматное программирование систем управления

55 of 596

Турникет: два состояния, четыре перехода

Петли существенны: толчок в закрытый турникет и вторая карта у открытого — не «ошибка» и не «ничего не происходит», а полноценные переходы, обязанные быть в таблице

Автоматное программирование систем управления

56 of 596

Что становится состоянием, а что остаётся переменной

Главный вопрос проектирования автоматных программ

Автоматное программирование систем управления

57 of 596

Что становится состоянием, а что остаётся переменной

Главный вопрос проектирования автоматных программ

Турникет не считает деньги, не знает о тарифах и не работает со временем

Автоматное программирование систем управления

58 of 596

Что становится состоянием, а что остаётся переменной

Главный вопрос проектирования автоматных программ

Турникет не считает деньги, не знает о тарифах и не работает со временем

Всё это — не состояния, а данные

Автоматное программирование систем управления

59 of 596

Что становится состоянием, а что остаётся переменной

Главный вопрос проектирования автоматных программ

Турникет не считает деньги, не знает о тарифах и не работает со временем

Всё это — не состояния, а данные

Попытка внести их в автомат («открыт с балансом 45 рублей») мгновенно взрывает число состояний

Автоматное программирование систем управления

60 of 596

Что становится состоянием, а что остаётся переменной

Главный вопрос проектирования автоматных программ

Турникет не считает деньги, не знает о тарифах и не работает со временем

Всё это — не состояния, а данные

Попытка внести их в автомат («открыт с балансом 45 рублей») мгновенно взрывает число состояний

Автомат тем и отличается от набора if, что для каждой пары «состояние, событие» ответ задан ровно один и задан явно

Автоматное программирование систем управления

61 of 596

Что становится состоянием, а что остаётся переменной

Главный вопрос проектирования автоматных программ

Турникет не считает деньги, не знает о тарифах и не работает со временем

Всё это — не состояния, а данные

Попытка внести их в автомат («открыт с балансом 45 рублей») мгновенно взрывает число состояний

К этому вопросу курс возвращается в лекции 7 — при разборе расширенного состояния

Автоматное программирование систем управления

62 of 596

Светофор с кнопкой пешехода: пять состояний

Время как источник событий. Нажатия кнопки вне состояния G поглощаются петлями; минимальная выдержка зелёного — отдельное состояние G_REQ, а не таймер сбоку

Автоматное программирование систем управления

63 of 596

Четыре примера из лекции

От простейшего элемента с памятью до автомата с бесконечной памятью

Практикум: practices/02-fsm-delay

64 of 596

Четыре примера из лекции

От простейшего элемента с памятью до автомата с бесконечной памятью

Задержка: y(1) = 0, y(t) = x(t−1). Состояние помнит предыдущий вход, Q = {0, 1}

Практикум: practices/02-fsm-delay

65 of 596

Четыре примера из лекции

От простейшего элемента с памятью до автомата с бесконечной памятью

Задержка: y(1) = 0, y(t) = x(t−1). Состояние помнит предыдущий вход, Q = {0, 1}

Дизъюнкция пары входов: y(t) = x₁(t) ∨ x₂(t). Состояние одно — автомат без памяти, функциональный элемент

Практикум: practices/02-fsm-delay

66 of 596

Четыре примера из лекции

От простейшего элемента с памятью до автомата с бесконечной памятью

Задержка: y(1) = 0, y(t) = x(t−1). Состояние помнит предыдущий вход, Q = {0, 1}

Дизъюнкция пары входов: y(t) = x₁(t) ∨ x₂(t). Состояние одно — автомат без памяти, функциональный элемент

Сумматор: q(t+1) = q(t) + x(t). Множество состояний бесконечно

Практикум: practices/02-fsm-delay

67 of 596

Четыре примера из лекции

От простейшего элемента с памятью до автомата с бесконечной памятью

Задержка: y(1) = 0, y(t) = x(t−1). Состояние помнит предыдущий вход, Q = {0, 1}

Дизъюнкция пары входов: y(t) = x₁(t) ∨ x₂(t). Состояние одно — автомат без памяти, функциональный элемент

Сумматор: q(t+1) = q(t) + x(t). Множество состояний бесконечно

Сумматор по модулю 2: q(t+1) = q(t) ⊕ x(t), y(t) = q(t) ⊕ x(t). Снова Q = {0, 1}

Практикум: practices/02-fsm-delay

68 of 596

Четыре примера из лекции

От простейшего элемента с памятью до автомата с бесконечной памятью

Задержка: y(1) = 0, y(t) = x(t−1). Состояние помнит предыдущий вход, Q = {0, 1}

Дизъюнкция пары входов: y(t) = x₁(t) ∨ x₂(t). Состояние одно — автомат без памяти, функциональный элемент

Сумматор: q(t+1) = q(t) + x(t). Множество состояний бесконечно

Сумматор по модулю 2: q(t+1) = q(t) ⊕ x(t), y(t) = q(t) ⊕ x(t). Снова Q = {0, 1}

Первый и четвёртый различаются не размером, а моделью: Мур против Мили

Практикум: practices/02-fsm-delay

69 of 596

Автоматная схема сумматора по модулю 2

Элемент G₀ — задержка с нулевым начальным состоянием, вентиль — сложение по модулю 2. Обратная связь с выхода задержки замыкает автомат

Автоматное программирование систем управления

70 of 596

Формальное определение

Автоматное программирование систем управления

71 of 596

Формальное определение

Конечный автомат — пятёрка V = (A, Q, B, φ, ψ)

Автоматное программирование систем управления

72 of 596

Формальное определение

Конечный автомат — пятёрка V = (A, Q, B, φ, ψ)

A — входной алфавит, Q — конечное множество состояний, B — выходной алфавит

Автоматное программирование систем управления

73 of 596

Формальное определение

Конечный автомат — пятёрка V = (A, Q, B, φ, ψ)

A — входной алфавит, Q — конечное множество состояний, B — выходной алфавит

φ: Q × A → Q — функция переходов, ψ: Q × A → B — функция выходов

Автоматное программирование систем управления

74 of 596

Формальное определение

Конечный автомат — пятёрка V = (A, Q, B, φ, ψ)

A — входной алфавит, Q — конечное множество состояний, B — выходной алфавит

φ: Q × A → Q — функция переходов, ψ: Q × A → B — функция выходов

Инициальный автомат V(q₀) — автомат с выделенным начальным состоянием

Автоматное программирование систем управления

75 of 596

Формальное определение

Конечный автомат — пятёрка V = (A, Q, B, φ, ψ)

A — входной алфавит, Q — конечное множество состояний, B — выходной алфавит

φ: Q × A → Q — функция переходов, ψ: Q × A → B — функция выходов

Инициальный автомат V(q₀) — автомат с выделенным начальным состоянием

Система канонических уравнений: q(1) = q₀, q(t+1) = φ(q(t), x(t)), y(t) = ψ(q(t), x(t))

Автоматное программирование систем управления

76 of 596

Формальное определение

Конечный автомат — пятёрка V = (A, Q, B, φ, ψ)

A — входной алфавит, Q — конечное множество состояний, B — выходной алфавит

φ: Q × A → Q — функция переходов, ψ: Q × A → B — функция выходов

Инициальный автомат V(q₀) — автомат с выделенным начальным состоянием

Система канонических уравнений: q(1) = q₀, q(t+1) = φ(q(t), x(t)), y(t) = ψ(q(t), x(t))

Диаграмма Мура — та же информация в виде размеченного графа

Автоматное программирование систем управления

77 of 596

Мили и Мур

Автоматное программирование систем управления

78 of 596

Мили и Мур

Автомат Мура: функция выходов зависит от входного символа фиктивно, ψ = ψ(q)

Автоматное программирование систем управления

79 of 596

Мили и Мур

Автомат Мура: функция выходов зависит от входного символа фиктивно, ψ = ψ(q)

Автомат Мили: выход зависит и от состояния, и от входного символа

Автоматное программирование систем управления

80 of 596

Мили и Мур

Автомат Мура: функция выходов зависит от входного символа фиктивно, ψ = ψ(q)

Автомат Мили: выход зависит и от состояния, и от входного символа

У Мура вторые элементы пар у всех дуг из одного круга совпадают — выход выносят внутрь круга

Автоматное программирование систем управления

81 of 596

Мили и Мур

Автомат Мура: функция выходов зависит от входного символа фиктивно, ψ = ψ(q)

Автомат Мили: выход зависит и от состояния, и от входного символа

У Мура вторые элементы пар у всех дуг из одного круга совпадают — выход выносят внутрь круга

Мур в Мили — даром: выход состояния приписывается всем входящим дугам

Автоматное программирование систем управления

82 of 596

Мили и Мур

Автомат Мура: функция выходов зависит от входного символа фиктивно, ψ = ψ(q)

Автомат Мили: выход зависит и от состояния, и от входного символа

У Мура вторые элементы пар у всех дуг из одного круга совпадают — выход выносят внутрь круга

Мур в Мили — даром: выход состояния приписывается всем входящим дугам

Мили в Мур — за состояния: состояние расщепляется по числу разных выходов на входящих дугах

Автоматное программирование систем управления

83 of 596

Мили и Мур

Автомат Мура: функция выходов зависит от входного символа фиктивно, ψ = ψ(q)

Автомат Мили: выход зависит и от состояния, и от входного символа

У Мура вторые элементы пар у всех дуг из одного круга совпадают — выход выносят внутрь круга

Мур в Мили — даром: выход состояния приписывается всем входящим дугам

Мили в Мур — за состояния: состояние расщепляется по числу разных выходов на входящих дугах

Задержка — автомат Мура; сумматор по модулю 2 — автомат Мили

Автоматное программирование систем управления

84 of 596

Детектор 1101: Мили — четыре состояния

Выход снимается с перехода: единица выдаётся на дуге, замыкающей образец

Автоматное программирование систем управления

85 of 596

Тот же детектор как автомат Мура

Понадобилось пятое состояние: выход приписан состоянию, поэтому «увидел 1101» пришлось отделить от «увидел 1»

Автоматное программирование систем управления

86 of 596

ЛЕКЦИЯ

Синтез автоматов и автоматные схемы

От словесного описания к булевым формулам и схеме

87 of 596

Две основные задачи теории автоматов

Автоматное программирование систем управления

88 of 596

Две основные задачи теории автоматов

Синтез: по описанию требуемого отображения построить автомат

Автоматное программирование систем управления

89 of 596

Две основные задачи теории автоматов

Синтез: по описанию требуемого отображения построить автомат

Анализ: по заданному автомату описать реализуемое им отображение

Автоматное программирование систем управления

90 of 596

Две основные задачи теории автоматов

Синтез: по описанию требуемого отображения построить автомат

Анализ: по заданному автомату описать реализуемое им отображение

Структурный синтез: свести автомат к схеме из функциональных элементов и задержек

Автоматное программирование систем управления

91 of 596

Две основные задачи теории автоматов

Синтез: по описанию требуемого отображения построить автомат

Анализ: по заданному автомату описать реализуемое им отображение

Структурный синтез: свести автомат к схеме из функциональных элементов и задержек

Анализ поведения — обратная задача: по схеме или диаграмме назвать распознаваемое множество слов

Автоматное программирование систем управления

92 of 596

Две основные задачи теории автоматов

Синтез: по описанию требуемого отображения построить автомат

Анализ: по заданному автомату описать реализуемое им отображение

Структурный синтез: свести автомат к схеме из функциональных элементов и задержек

Анализ поведения — обратная задача: по схеме или диаграмме назвать распознаваемое множество слов

Обе задачи возникают на практике: первая при проектировании, вторая при разборе чужого решения

Автоматное программирование систем управления

93 of 596

Задача: разменный аппарат

Бросаем монету 1, 3, 5 или 10 копеек — аппарат выдаёт трёхкопеечные монеты

Автоматное программирование систем управления

94 of 596

Задача: разменный аппарат

Бросаем монету 1, 3, 5 или 10 копеек — аппарат выдаёт трёхкопеечные монеты

Входной алфавит A = {1, 3, 5, 10} — достоинство брошенной монеты

Автоматное программирование систем управления

95 of 596

Задача: разменный аппарат

Бросаем монету 1, 3, 5 или 10 копеек — аппарат выдаёт трёхкопеечные монеты

Входной алфавит A = {1, 3, 5, 10} — достоинство брошенной монеты

Выходной алфавит B = {0, 1, 2, 3, 4} — сколько трёхкопеечных монет выдано

Автоматное программирование систем управления

96 of 596

Задача: разменный аппарат

Бросаем монету 1, 3, 5 или 10 копеек — аппарат выдаёт трёхкопеечные монеты

Входной алфавит A = {1, 3, 5, 10} — достоинство брошенной монеты

Выходной алфавит B = {0, 1, 2, 3, 4} — сколько трёхкопеечных монет выдано

Состояние — остаток долга: Q = {0, 1, 2}

Автоматное программирование систем управления

97 of 596

Задача: разменный аппарат

Бросаем монету 1, 3, 5 или 10 копеек — аппарат выдаёт трёхкопеечные монеты

Входной алфавит A = {1, 3, 5, 10} — достоинство брошенной монеты

Выходной алфавит B = {0, 1, 2, 3, 4} — сколько трёхкопеечных монет выдано

Состояние — остаток долга: Q = {0, 1, 2}

q(t+1) = (q(t) + x(t)) mod 3 — новый остаток

Автоматное программирование систем управления

98 of 596

Задача: разменный аппарат

Бросаем монету 1, 3, 5 или 10 копеек — аппарат выдаёт трёхкопеечные монеты

Входной алфавит A = {1, 3, 5, 10} — достоинство брошенной монеты

Выходной алфавит B = {0, 1, 2, 3, 4} — сколько трёхкопеечных монет выдано

Состояние — остаток долга: Q = {0, 1, 2}

q(t+1) = (q(t) + x(t)) mod 3 — новый остаток

y(t) = ⌊(q(t) + x(t)) / 3⌋ — число выданных монет

Автоматное программирование систем управления

99 of 596

Задача: разменный аппарат

Бросаем монету 1, 3, 5 или 10 копеек — аппарат выдаёт трёхкопеечные монеты

Входной алфавит A = {1, 3, 5, 10} — достоинство брошенной монеты

Выходной алфавит B = {0, 1, 2, 3, 4} — сколько трёхкопеечных монет выдано

Состояние — остаток долга: Q = {0, 1, 2}

q(t+1) = (q(t) + x(t)) mod 3 — новый остаток

y(t) = ⌊(q(t) + x(t)) / 3⌋ — число выданных монет

Проверка: при фиксированном x столбец φ обязан быть циклической перестановкой {0, 1, 2}

Автоматное программирование систем управления

100 of 596

100

Диаграмма Мура разменного аппарата

Дуги помечены парами (входной символ, выходной символ). Две пометки на одной дуге означают два перехода с совпадающими началом и концом

Автоматное программирование систем управления

101 of 596

101

От автомата к схеме

Практикум: practices/03-synthesis

102 of 596

102

От автомата к схеме

Закодировать входной алфавит и множество состояний двоичными наборами

Практикум: practices/03-synthesis

103 of 596

103

От автомата к схеме

Закодировать входной алфавит и множество состояний двоичными наборами

Выписать перекодированную таблицу переходов и выходов

Практикум: practices/03-synthesis

104 of 596

104

От автомата к схеме

Закодировать входной алфавит и множество состояний двоичными наборами

Выписать перекодированную таблицу переходов и выходов

Недостижимые наборы дают звёздочки — их доопределяют так, как удобно для минимизации

Практикум: practices/03-synthesis

105 of 596

105

От автомата к схеме

Закодировать входной алфавит и множество состояний двоичными наборами

Выписать перекодированную таблицу переходов и выходов

Недостижимые наборы дают звёздочки — их доопределяют так, как удобно для минимизации

Каждую функцию φᵢ и ψⱼ минимизировать по карте Карно

Практикум: practices/03-synthesis

106 of 596

106

От автомата к схеме

Закодировать входной алфавит и множество состояний двоичными наборами

Выписать перекодированную таблицу переходов и выходов

Недостижимые наборы дают звёздочки — их доопределяют так, как удобно для минимизации

Каждую функцию φᵢ и ψⱼ минимизировать по карте Карно

Схема распадается на комбинационную часть C и регистр из элементов задержки G₀

Практикум: practices/03-synthesis

107 of 596

107

От автомата к схеме

Закодировать входной алфавит и множество состояний двоичными наборами

Выписать перекодированную таблицу переходов и выходов

Недостижимые наборы дают звёздочки — их доопределяют так, как удобно для минимизации

Каждую функцию φᵢ и ψⱼ минимизировать по карте Карно

Схема распадается на комбинационную часть C и регистр из элементов задержки G₀

Обратная связь с выходов регистра на входы C замыкает автомат

Практикум: practices/03-synthesis

108 of 596

108

Карта Карно функции φ₁

Строки — код входного символа x₁x₂, столбцы — код состояния q₁q₂, оба в коде Грея: соседние клетки отличаются ровно одним разрядом. Звёздочка — недостижимый набор, то есть ресурс минимизации, а не проблема

Автоматное программирование систем управления

109 of 596

109

Автоматная схема разменного аппарата

Комбинационная часть C вычисляет функции выходов ψ₁…ψ₃ и функции переходов φ₁, φ₂; два элемента G₀ хранят код состояния

Автоматное программирование систем управления

110 of 596

110

Построение автомата наращиванием состояний

Приём, которым автомат строится по словесному описанию

Автоматное программирование систем управления

111 of 596

111

Построение автомата наращиванием состояний

Приём, которым автомат строится по словесному описанию

Завести начальное состояние — «ничего ещё не прочитано»

Автоматное программирование систем управления

112 of 596

112

Построение автомата наращиванием состояний

Приём, которым автомат строится по словесному описанию

Завести начальное состояние — «ничего ещё не прочитано»

Состояние отвечает на вопрос «какой префикс образца уже набран»

Автоматное программирование систем управления

113 of 596

113

Построение автомата наращиванием состояний

Приём, которым автомат строится по словесному описанию

Завести начальное состояние — «ничего ещё не прочитано»

Состояние отвечает на вопрос «какой префикс образца уже набран»

Для каждой буквы алфавита из каждого состояния указать, куда ведёт переход

Автоматное программирование систем управления

114 of 596

114

Построение автомата наращиванием состояний

Приём, которым автомат строится по словесному описанию

Завести начальное состояние — «ничего ещё не прочитано»

Состояние отвечает на вопрос «какой префикс образца уже набран»

Для каждой буквы алфавита из каждого состояния указать, куда ведёт переход

Новое состояние заводится только тогда, когда ни одно из имеющихся не описывает ситуацию

Автоматное программирование систем управления

115 of 596

115

Построение автомата наращиванием состояний

Приём, которым автомат строится по словесному описанию

Завести начальное состояние — «ничего ещё не прочитано»

Состояние отвечает на вопрос «какой префикс образца уже набран»

Для каждой буквы алфавита из каждого состояния указать, куда ведёт переход

Новое состояние заводится только тогда, когда ни одно из имеющихся не описывает ситуацию

Построение заканчивается, когда все переходы ведут в уже существующие состояния

Автоматное программирование систем управления

116 of 596

116

Построение автомата наращиванием состояний

Приём, которым автомат строится по словесному описанию

Завести начальное состояние — «ничего ещё не прочитано»

Состояние отвечает на вопрос «какой префикс образца уже набран»

Для каждой буквы алфавита из каждого состояния указать, куда ведёт переход

Новое состояние заводится только тогда, когда ни одно из имеющихся не описывает ситуацию

Построение заканчивается, когда все переходы ведут в уже существующие состояния

Тот же приём даёт детектор 1101 из лекции 2 и автоматы-акцепторы из лекции 4

Автоматное программирование систем управления

117 of 596

117

Автомат «соседние символы различны»

Три состояния, шесть переходов — результат наращивания: состояние помнит последний прочитанный символ

Автоматное программирование систем управления

118 of 596

118

Анализ поведения: счётчик по модулю четыре

Обратная задача: автомат дан, требуется описать, что он делает. В трёх состояниях входная буква копируется, в четвёртом инвертируется — значит, инвертируется каждая четвёртая буква

Автоматное программирование систем управления

119 of 596

ЛЕКЦИЯ

Автоматы-акцепторы. ДКА и НКА

Детерминизация, достижимость, минимизация

120 of 596

120

Автомат как акцептор

Автоматное программирование систем управления

121 of 596

121

Автомат как акцептор

В лекциях 2 и 3 автомат был преобразователем: читает слово — выдаёт слово

Автоматное программирование систем управления

122 of 596

122

Автомат как акцептор

В лекциях 2 и 3 автомат был преобразователем: читает слово — выдаёт слово

Для распознавания языков удобнее: автомат либо допускает слово, либо нет

Автоматное программирование систем управления

123 of 596

123

Автомат как акцептор

В лекциях 2 и 3 автомат был преобразователем: читает слово — выдаёт слово

Для распознавания языков удобнее: автомат либо допускает слово, либо нет

Возьмём двухбуквенный выходной алфавит B = {0, 1} и B′ = {1}

Автоматное программирование систем управления

124 of 596

124

Автомат как акцептор

В лекциях 2 и 3 автомат был преобразователем: читает слово — выдаёт слово

Для распознавания языков удобнее: автомат либо допускает слово, либо нет

Возьмём двухбуквенный выходной алфавит B = {0, 1} и B′ = {1}

Тогда выход лишь сообщает, «хорошее» ли состояние достигнуто

Автоматное программирование систем управления

125 of 596

125

Автомат как акцептор

В лекциях 2 и 3 автомат был преобразователем: читает слово — выдаёт слово

Для распознавания языков удобнее: автомат либо допускает слово, либо нет

Возьмём двухбуквенный выходной алфавит B = {0, 1} и B′ = {1}

Тогда выход лишь сообщает, «хорошее» ли состояние достигнуто

Вместо функции выходов достаточно указать множество заключительных состояний F

Автоматное программирование систем управления

126 of 596

126

Автомат как акцептор

В лекциях 2 и 3 автомат был преобразователем: читает слово — выдаёт слово

Для распознавания языков удобнее: автомат либо допускает слово, либо нет

Возьмём двухбуквенный выходной алфавит B = {0, 1} и B′ = {1}

Тогда выход лишь сообщает, «хорошее» ли состояние достигнуто

Вместо функции выходов достаточно указать множество заключительных состояний F

ДКА — пятёрка M = ⟨Q, Σ, δ, q₀, F⟩ со всюду определённой δ: Q × Σ → Q

Автоматное программирование систем управления

127 of 596

127

Автомат как акцептор

В лекциях 2 и 3 автомат был преобразователем: читает слово — выдаёт слово

Для распознавания языков удобнее: автомат либо допускает слово, либо нет

Возьмём двухбуквенный выходной алфавит B = {0, 1} и B′ = {1}

Тогда выход лишь сообщает, «хорошее» ли состояние достигнуто

Вместо функции выходов достаточно указать множество заключительных состояний F

ДКА — пятёрка M = ⟨Q, Σ, δ, q₀, F⟩ со всюду определённой δ: Q × Σ → Q

Язык автомата: L(M) = {α ∈ Σ* : δ̂(q₀, α) ∈ F}

Автоматное программирование систем управления

128 of 596

128

ДКА: слова, оканчивающиеся на abb

Автомат выписан по смыслу: состояние хранит длину уже прочитанного правильного префикса образца. Стрелка слева — начальное состояние, двойной контур — заключительное

Автоматное программирование систем управления

129 of 596

129

Недетерминированный автомат

Автоматное программирование систем управления

130 of 596

130

Недетерминированный автомат

НКА — пятёрка N = ⟨Q, Σ, Δ, q₀, F⟩, где Δ: Q × Σ → 2^Q

Автоматное программирование систем управления

131 of 596

131

Недетерминированный автомат

НКА — пятёрка N = ⟨Q, Σ, Δ, q₀, F⟩, где Δ: Q × Σ → 2^Q

Паре «состояние, символ» сопоставляется множество состояний, возможно пустое

Автоматное программирование систем управления

132 of 596

132

Недетерминированный автомат

НКА — пятёрка N = ⟨Q, Σ, Δ, q₀, F⟩, где Δ: Q × Σ → 2^Q

Паре «состояние, символ» сопоставляется множество состояний, возможно пустое

Слово допускается, если существует хотя бы один путь из q₀ в состояние из F

Автоматное программирование систем управления

133 of 596

133

Недетерминированный автомат

НКА — пятёрка N = ⟨Q, Σ, Δ, q₀, F⟩, где Δ: Q × Σ → 2^Q

Паре «состояние, символ» сопоставляется множество состояний, возможно пустое

Слово допускается, если существует хотя бы один путь из q₀ в состояние из F

ε-НКА дополнительно разрешает переходы по пустому слову

Автоматное программирование систем управления

134 of 596

134

Недетерминированный автомат

НКА — пятёрка N = ⟨Q, Σ, Δ, q₀, F⟩, где Δ: Q × Σ → 2^Q

Паре «состояние, символ» сопоставляется множество состояний, возможно пустое

Слово допускается, если существует хотя бы один путь из q₀ в состояние из F

ε-НКА дополнительно разрешает переходы по пустому слову

Недетерминизм не увеличивает выразительной силы модели

Автоматное программирование систем управления

135 of 596

135

Недетерминированный автомат

НКА — пятёрка N = ⟨Q, Σ, Δ, q₀, F⟩, где Δ: Q × Σ → 2^Q

Паре «состояние, символ» сопоставляется множество состояний, возможно пустое

Слово допускается, если существует хотя бы один путь из q₀ в состояние из F

ε-НКА дополнительно разрешает переходы по пустому слову

Недетерминизм не увеличивает выразительной силы модели

Но позволяет описывать языки короче: для «n-й символ с конца равен a» НКА нужно n+1 состояние, минимальному ДКА — 2ⁿ

Автоматное программирование систем управления

136 of 596

136

Детерминизация

Теорема: для всякого НКА существует эквивалентный ДКА

Практикум: practices/04-dfa-nfa

137 of 596

137

Детерминизация

Теорема: для всякого НКА существует эквивалентный ДКА

Состояния строимого ДКА — подмножества множества состояний НКА (subset construction)

Практикум: practices/04-dfa-nfa

138 of 596

138

Детерминизация

Теорема: для всякого НКА существует эквивалентный ДКА

Состояния строимого ДКА — подмножества множества состояний НКА (subset construction)

Начальное состояние — {q₀}, для ε-НКА — ε-замыкание этого множества

Практикум: practices/04-dfa-nfa

139 of 596

139

Детерминизация

Теорема: для всякого НКА существует эквивалентный ДКА

Состояния строимого ДКА — подмножества множества состояний НКА (subset construction)

Начальное состояние — {q₀}, для ε-НКА — ε-замыкание этого множества

Переход из множества S по символу a ведёт в объединение Δ(q, a) по всем q ∈ S

Практикум: practices/04-dfa-nfa

140 of 596

140

Детерминизация

Теорема: для всякого НКА существует эквивалентный ДКА

Состояния строимого ДКА — подмножества множества состояний НКА (subset construction)

Начальное состояние — {q₀}, для ε-НКА — ε-замыкание этого множества

Переход из множества S по символу a ведёт в объединение Δ(q, a) по всем q ∈ S

Заключительными объявляются те S, которые пересекаются с F

Практикум: practices/04-dfa-nfa

141 of 596

141

Детерминизация

Теорема: для всякого НКА существует эквивалентный ДКА

Состояния строимого ДКА — подмножества множества состояний НКА (subset construction)

Начальное состояние — {q₀}, для ε-НКА — ε-замыкание этого множества

Переход из множества S по символу a ведёт в объединение Δ(q, a) по всем q ∈ S

Заключительными объявляются те S, которые пересекаются с F

Достижимые подмножества строятся по мере надобности: для (a|b)*abb их пять из 2¹⁴

Практикум: practices/04-dfa-nfa

142 of 596

142

Детерминизация

Теорема: для всякого НКА существует эквивалентный ДКА

Состояния строимого ДКА — подмножества множества состояний НКА (subset construction)

Начальное состояние — {q₀}, для ε-НКА — ε-замыкание этого множества

Переход из множества S по символу a ведёт в объединение Δ(q, a) по всем q ∈ S

Заключительными объявляются те S, которые пересекаются с F

Достижимые подмножества строятся по мере надобности: для (a|b)*abb их пять из 2¹⁴

Ровно это построение выполнено в лекции 5 при доказательстве леммы № 8 — там оно не названо своим именем

Практикум: practices/04-dfa-nfa

143 of 596

143

ДКА для (a|b)*abb после детерминизации

Четырнадцать состояний ε-НКА, построенного конструкцией Томпсона, свелись к пяти достижимым подмножествам

Автоматное программирование систем управления

144 of 596

144

Достижимость, эквивалентность, минимизация

Автоматное программирование систем управления

145 of 596

145

Достижимость, эквивалентность, минимизация

Состояние достижимо, если в него ведёт хотя бы одно слово из q₀; недостижимые удаляются обходом в ширину

Автоматное программирование систем управления

146 of 596

146

Достижимость, эквивалентность, минимизация

Состояние достижимо, если в него ведёт хотя бы одно слово из q₀; недостижимые удаляются обходом в ширину

В спроектированном вручную автомате недостижимое состояние — почти всегда признак ошибки

Автоматное программирование систем управления

147 of 596

147

Достижимость, эквивалентность, минимизация

Состояние достижимо, если в него ведёт хотя бы одно слово из q₀; недостижимые удаляются обходом в ширину

В спроектированном вручную автомате недостижимое состояние — почти всегда признак ошибки

Состояния p и q эквивалентны, если ни одно слово их не различает по признаку попадания в F

Автоматное программирование систем управления

148 of 596

148

Достижимость, эквивалентность, минимизация

Состояние достижимо, если в него ведёт хотя бы одно слово из q₀; недостижимые удаляются обходом в ширину

В спроектированном вручную автомате недостижимое состояние — почти всегда признак ошибки

Состояния p и q эквивалентны, если ни одно слово их не различает по признаку попадания в F

Теорема Майхилла — Нероуда: число классов эквивалентности равно числу состояний минимального ДКА

Автоматное программирование систем управления

149 of 596

149

Достижимость, эквивалентность, минимизация

Состояние достижимо, если в него ведёт хотя бы одно слово из q₀; недостижимые удаляются обходом в ширину

В спроектированном вручную автомате недостижимое состояние — почти всегда признак ошибки

Состояния p и q эквивалентны, если ни одно слово их не различает по признаку попадания в F

Теорема Майхилла — Нероуда: число классов эквивалентности равно числу состояний минимального ДКА

Минимальный автомат единствен с точностью до переименования состояний

Автоматное программирование систем управления

150 of 596

150

Достижимость, эквивалентность, минимизация

Состояние достижимо, если в него ведёт хотя бы одно слово из q₀; недостижимые удаляются обходом в ширину

В спроектированном вручную автомате недостижимое состояние — почти всегда признак ошибки

Состояния p и q эквивалентны, если ни одно слово их не различает по признаку попадания в F

Теорема Майхилла — Нероуда: число классов эквивалентности равно числу состояний минимального ДКА

Минимальный автомат единствен с точностью до переименования состояний

Алгоритм разбиения: начать с двух классов F и Q \ F и дробить, пока разбиение меняется

Автоматное программирование систем управления

151 of 596

151

Достижимость, эквивалентность, минимизация

Состояние достижимо, если в него ведёт хотя бы одно слово из q₀; недостижимые удаляются обходом в ширину

В спроектированном вручную автомате недостижимое состояние — почти всегда признак ошибки

Состояния p и q эквивалентны, если ни одно слово их не различает по признаку попадания в F

Теорема Майхилла — Нероуда: число классов эквивалентности равно числу состояний минимального ДКА

Минимальный автомат единствен с точностью до переименования состояний

Алгоритм разбиения: начать с двух классов F и Q \ F и дробить, пока разбиение меняется

Алгоритм Хопкрофта уточняет шаг дробления и работает за O(|Q|·|Σ|·log|Q|)

Автоматное программирование систем управления

152 of 596

152

Минимальный ДКА: четыре состояния

S₀ и S₂ оказались эквивалентны и слились. Сравните с автоматом, выписанным по смыслу в начале лекции: это тот же автомат

Автоматное программирование систем управления

153 of 596

153

Зачем минимизировать автомат, который уже работает

Автоматное программирование систем управления

154 of 596

154

Зачем минимизировать автомат, который уже работает

Объём таблицы переходов в прошивке: состояния занимают память контроллера

Автоматное программирование систем управления

155 of 596

155

Зачем минимизировать автомат, который уже работает

Объём таблицы переходов в прошивке: состояния занимают память контроллера

Число тестов на покрытие переходов растёт как |Q| × |Σ| (лекция 7)

Автоматное программирование систем управления

156 of 596

156

Зачем минимизировать автомат, который уже работает

Объём таблицы переходов в прошивке: состояния занимают память контроллера

Число тестов на покрытие переходов растёт как |Q| × |Σ| (лекция 7)

Сравнение двух автоматов на эквивалентность сводится к минимизации обоих

Автоматное программирование систем управления

157 of 596

157

Зачем минимизировать автомат, который уже работает

Объём таблицы переходов в прошивке: состояния занимают память контроллера

Число тестов на покрытие переходов растёт как |Q| × |Σ| (лекция 7)

Сравнение двух автоматов на эквивалентность сводится к минимизации обоих

Теорема Мура: различающее слово для автомата с n состояниями, если оно есть, не длиннее n − 2

Автоматное программирование систем управления

158 of 596

158

Зачем минимизировать автомат, который уже работает

Объём таблицы переходов в прошивке: состояния занимают память контроллера

Число тестов на покрытие переходов растёт как |Q| × |Σ| (лекция 7)

Сравнение двух автоматов на эквивалентность сводится к минимизации обоих

Теорема Мура: различающее слово для автомата с n состояниями, если оно есть, не длиннее n − 2

Цена детерминизации в худшем случае честно экспоненциальна: бывают языки, у которых подмножеств действительно 2ⁿ

Автоматное программирование систем управления

159 of 596

ЛЕКЦИЯ

Регулярные события и теорема Клини

Что конечный автомат распознать может — и чего не может

160 of 596

160

События и операции над ними

Автоматное программирование систем управления

161 of 596

161

События и операции над ними

Событие — подмножество A* без пустого слова

Автоматное программирование систем управления

162 of 596

162

События и операции над ними

Событие — подмножество A* без пустого слова

Событие M представимо в автомате V(q) посредством B′, если M = {α : ψ(q, α) ∈ B′}

Автоматное программирование систем управления

163 of 596

163

События и операции над ними

Событие — подмножество A* без пустого слова

Событие M представимо в автомате V(q) посредством B′, если M = {α : ψ(q, α) ∈ B′}

Произведение M₁·M₂ — все слова вида α₁α₂, где α₁ ∈ M₁, α₂ ∈ M₂

Автоматное программирование систем управления

164 of 596

164

События и операции над ними

Событие — подмножество A* без пустого слова

Событие M представимо в автомате V(q) посредством B′, если M = {α : ψ(q, α) ∈ B′}

Произведение M₁·M₂ — все слова вида α₁α₂, где α₁ ∈ M₁, α₂ ∈ M₂

Итерация M⁺ — все слова α₁…α_k, где каждое αᵢ ∈ M, k ≥ 1

Автоматное программирование систем управления

165 of 596

165

События и операции над ними

Событие — подмножество A* без пустого слова

Событие M представимо в автомате V(q) посредством B′, если M = {α : ψ(q, α) ∈ B′}

Произведение M₁·M₂ — все слова вида α₁α₂, где α₁ ∈ M₁, α₂ ∈ M₂

Итерация M⁺ — все слова α₁…α_k, где каждое αᵢ ∈ M, k ≥ 1

M* = M⁺ ∪ {ε} — итерация, допускающая пустое слово

Автоматное программирование систем управления

166 of 596

166

События и операции над ними

Событие — подмножество A* без пустого слова

Событие M представимо в автомате V(q) посредством B′, если M = {α : ψ(q, α) ∈ B′}

Произведение M₁·M₂ — все слова вида α₁α₂, где α₁ ∈ M₁, α₂ ∈ M₂

Итерация M⁺ — все слова α₁…α_k, где каждое αᵢ ∈ M, k ≥ 1

M* = M⁺ ∪ {ε} — итерация, допускающая пустое слово

Тождества: ∅·M = ∅, M⁺ = M·M⁺ ∪ M, M·M⁺ = M⁺·M

Автоматное программирование систем управления

167 of 596

167

Регулярное событие и регулярное выражение

Устроены одинаково, но говорят о разном

Автоматное программирование систем управления

168 of 596

168

Регулярное событие и регулярное выражение

Устроены одинаково, но говорят о разном

Событие регулярно, если получается из ∅ и одноэлементных {a} конечным числом операций ∪, · и ⁺

Автоматное программирование систем управления

169 of 596

169

Регулярное событие и регулярное выражение

Устроены одинаково, но говорят о разном

Событие регулярно, если получается из ∅ и одноэлементных {a} конечным числом операций ∪, · и ⁺

Регулярное выражение — слово в алфавите A ∪ {∅, ∪, ·, ⁺, (, )}

Автоматное программирование систем управления

170 of 596

170

Регулярное событие и регулярное выражение

Устроены одинаково, но говорят о разном

Событие регулярно, если получается из ∅ и одноэлементных {a} конечным числом операций ∪, · и ⁺

Регулярное выражение — слово в алфавите A ∪ {∅, ∪, ·, ⁺, (, )}

Выражение — синтаксический объект, строка символов

Автоматное программирование систем управления

171 of 596

171

Регулярное событие и регулярное выражение

Устроены одинаково, но говорят о разном

Событие регулярно, если получается из ∅ и одноэлементных {a} конечным числом операций ∪, · и ⁺

Регулярное выражение — слово в алфавите A ∪ {∅, ∪, ·, ⁺, (, )}

Выражение — синтаксический объект, строка символов

Событие — множество слов, то есть значение этой строки

Автоматное программирование систем управления

172 of 596

172

Регулярное событие и регулярное выражение

Устроены одинаково, но говорят о разном

Событие регулярно, если получается из ∅ и одноэлементных {a} конечным числом операций ∪, · и ⁺

Регулярное выражение — слово в алфавите A ∪ {∅, ∪, ·, ⁺, (, )}

Выражение — синтаксический объект, строка символов

Событие — множество слов, то есть значение этой строки

Обозначая через [r] событие выражения r: [r₁ ∪ r₂] = [r₁] ∪ [r₂], [r⁺] = [r]⁺

Автоматное программирование систем управления

173 of 596

173

Регулярное событие и регулярное выражение

Устроены одинаково, но говорят о разном

Событие регулярно, если получается из ∅ и одноэлементных {a} конечным числом операций ∪, · и ⁺

Регулярное выражение — слово в алфавите A ∪ {∅, ∪, ·, ⁺, (, )}

Выражение — синтаксический объект, строка символов

Событие — множество слов, то есть значение этой строки

Обозначая через [r] событие выражения r: [r₁ ∪ r₂] = [r₁] ∪ [r₂], [r⁺] = [r]⁺

Спутать их легко: в исходной редакции определение выражения дословно повторяло определение события

Автоматное программирование систем управления

174 of 596

Событие представимо в конечном автомате

тогда и только тогда, когда оно регулярно

Теорема Клини, 1951

175 of 596

175

Доказательство: три леммы

Автоматное программирование систем управления

176 of 596

176

Доказательство: три леммы

Лемма № 6 даёт направление «представимо ⇒ регулярно»

Автоматное программирование систем управления

177 of 596

177

Доказательство: три леммы

Лемма № 6 даёт направление «представимо ⇒ регулярно»

Лемма № 7: по регулярному событию строится обобщённый источник

Автоматное программирование систем управления

178 of 596

178

Доказательство: три леммы

Лемма № 6 даёт направление «представимо ⇒ регулярно»

Лемма № 7: по регулярному событию строится обобщённый источник

Лемма № 8: обобщённый источник превращается в конечный автомат

Автоматное программирование систем управления

179 of 596

179

Доказательство: три леммы

Лемма № 6 даёт направление «представимо ⇒ регулярно»

Лемма № 7: по регулярному событию строится обобщённый источник

Лемма № 8: обобщённый источник превращается в конечный автомат

Обобщённый источник — это в точности ε-НКА, а построение леммы 7 — конструкция Томпсона (1968)

Автоматное программирование систем управления

180 of 596

180

Доказательство: три леммы

Лемма № 6 даёт направление «представимо ⇒ регулярно»

Лемма № 7: по регулярному событию строится обобщённый источник

Лемма № 8: обобщённый источник превращается в конечный автомат

Обобщённый источник — это в точности ε-НКА, а построение леммы 7 — конструкция Томпсона (1968)

Доказательство леммы 8 — переход через множества вершин, то есть детерминизация

Автоматное программирование систем управления

181 of 596

181

Доказательство: три леммы

Лемма № 6 даёт направление «представимо ⇒ регулярно»

Лемма № 7: по регулярному событию строится обобщённый источник

Лемма № 8: обобщённый источник превращается в конечный автомат

Обобщённый источник — это в точности ε-НКА, а построение леммы 7 — конструкция Томпсона (1968)

Доказательство леммы 8 — переход через множества вершин, то есть детерминизация

Нумерация лемм начинается с шестой: материал перенесён из книги, где ему предшествуют леммы 1—5

Автоматное программирование систем управления

182 of 596

182

Конструкция Томпсона: пять шаблонов

Пустое событие, одна буква, объединение, произведение, итерация. Каждый шаблон добавляет ровно две вершины — отсюда и оценка числа состояний в лемме 7

Практикум: practices/05-kleene

183 of 596

183

Граница модели: лемма о накачке

Теорема Клини говорит, что автомат может. Лемма о накачке — чего он не может

Автоматное программирование систем управления

184 of 596

184

Граница модели: лемма о накачке

Теорема Клини говорит, что автомат может. Лемма о накачке — чего он не может

Существует p ≥ 1 такое, что всякое слово языка длины |w| ≥ p разбивается на w = xyz

Автоматное программирование систем управления

185 of 596

185

Граница модели: лемма о накачке

Теорема Клини говорит, что автомат может. Лемма о накачке — чего он не может

Существует p ≥ 1 такое, что всякое слово языка длины |w| ≥ p разбивается на w = xyz

При этом |xy| ≤ p, |y| ≥ 1 и xyᵏz принадлежит языку для всех k ≥ 0

Автоматное программирование систем управления

186 of 596

186

Граница модели: лемма о накачке

Теорема Клини говорит, что автомат может. Лемма о накачке — чего он не может

Существует p ≥ 1 такое, что всякое слово языка длины |w| ≥ p разбивается на w = xyz

При этом |xy| ≤ p, |y| ≥ 1 и xyᵏz принадлежит языку для всех k ≥ 0

Доказательство: на первых p символах автомат с p состояниями проходит p+1 состояние — какое-то повторяется

Автоматное программирование систем управления

187 of 596

187

Граница модели: лемма о накачке

Теорема Клини говорит, что автомат может. Лемма о накачке — чего он не может

Существует p ≥ 1 такое, что всякое слово языка длины |w| ≥ p разбивается на w = xyz

При этом |xy| ≤ p, |y| ≥ 1 и xyᵏz принадлежит языку для всех k ≥ 0

Доказательство: на первых p символах автомат с p состояниями проходит p+1 состояние — какое-то повторяется

Участок y между двумя вхождениями можно повторить или выбросить

Автоматное программирование систем управления

188 of 596

188

Граница модели: лемма о накачке

Теорема Клини говорит, что автомат может. Лемма о накачке — чего он не может

Существует p ≥ 1 такое, что всякое слово языка длины |w| ≥ p разбивается на w = xyz

При этом |xy| ≤ p, |y| ≥ 1 и xyᵏz принадлежит языку для всех k ≥ 0

Доказательство: на первых p символах автомат с p состояниями проходит p+1 состояние — какое-то повторяется

Участок y между двумя вхождениями можно повторить или выбросить

Язык aⁿbⁿ не регулярен: y состоит из одних букв a, и xy²z содержит их больше, чем b

Автоматное программирование систем управления

189 of 596

189

Граница модели: лемма о накачке

Теорема Клини говорит, что автомат может. Лемма о накачке — чего он не может

Существует p ≥ 1 такое, что всякое слово языка длины |w| ≥ p разбивается на w = xyz

При этом |xy| ≤ p, |y| ≥ 1 и xyᵏz принадлежит языку для всех k ≥ 0

Доказательство: на первых p символах автомат с p состояниями проходит p+1 состояние — какое-то повторяется

Участок y между двумя вхождениями можно повторить или выбросить

Язык aⁿbⁿ не регулярен: y состоит из одних букв a, и xy²z содержит их больше, чем b

Это строгий ответ на вопрос, чем машина Тьюринга отличается от конечного автомата

Автоматное программирование систем управления

190 of 596

190

Обратный путь: от автомата к выражению

Автоматное программирование систем управления

191 of 596

191

Обратный путь: от автомата к выражению

Лемма Ардена: уравнение X = A·X ∪ B при ε ∉ A имеет единственное решение X = A*·B

Автоматное программирование систем управления

192 of 596

192

Обратный путь: от автомата к выражению

Лемма Ардена: уравнение X = A·X ∪ B при ε ∉ A имеет единственное решение X = A*·B

По автомату выписывается система уравнений: по одному на состояние

Автоматное программирование систем управления

193 of 596

193

Обратный путь: от автомата к выражению

Лемма Ардена: уравнение X = A·X ∪ B при ε ∉ A имеет единственное решение X = A*·B

По автомату выписывается система уравнений: по одному на состояние

Уравнения решаются подстановкой, лемма Ардена развязывает петли

Автоматное программирование систем управления

194 of 596

194

Обратный путь: от автомата к выражению

Лемма Ардена: уравнение X = A·X ∪ B при ε ∉ A имеет единственное решение X = A*·B

По автомату выписывается система уравнений: по одному на состояние

Уравнения решаются подстановкой, лемма Ардена развязывает петли

Метод исключения состояний — та же идея графически: вершина удаляется, а её пути переносятся на дуги

Автоматное программирование систем управления

195 of 596

195

Обратный путь: от автомата к выражению

Лемма Ардена: уравнение X = A·X ∪ B при ε ∉ A имеет единственное решение X = A*·B

По автомату выписывается система уравнений: по одному на состояние

Уравнения решаются подстановкой, лемма Ардена развязывает петли

Метод исключения состояний — та же идея графически: вершина удаляется, а её пути переносятся на дуги

Оба метода дают регулярное выражение, эквивалентное автомату, — то есть обратное направление теоремы Клини

Автоматное программирование систем управления

196 of 596

ЛЕКЦИЯ

Регулярные выражения и лексический анализ

Теория Клини против практики PCRE

197 of 596

197

Синтаксис регулярных выражений

Автоматное программирование систем управления

198 of 596

198

Синтаксис регулярных выражений

Язык РВ состоит из литералов (обычный текст) и метасимволов

Автоматное программирование систем управления

199 of 596

199

Синтаксис регулярных выражений

Язык РВ состоит из литералов (обычный текст) и метасимволов

Точка — любой символ; символьные классы [A-Za-z] и их отрицания

Автоматное программирование систем управления

200 of 596

200

Синтаксис регулярных выражений

Язык РВ состоит из литералов (обычный текст) и метасимволов

Точка — любой символ; символьные классы [A-Za-z] и их отрицания

Якоря позиции: начало строки, конец строки, граница слова

Автоматное программирование систем управления

201 of 596

201

Синтаксис регулярных выражений

Язык РВ состоит из литералов (обычный текст) и метасимволов

Точка — любой символ; символьные классы [A-Za-z] и их отрицания

Якоря позиции: начало строки, конец строки, граница слова

Скобки задают группу и влияют на порядок обработки; вертикальная черта — объединение

Автоматное программирование систем управления

202 of 596

202

Синтаксис регулярных выражений

Язык РВ состоит из литералов (обычный текст) и метасимволов

Точка — любой символ; символьные классы [A-Za-z] и их отрицания

Якоря позиции: начало строки, конец строки, граница слова

Скобки задают группу и влияют на порядок обработки; вертикальная черта — объединение

Квантификаторы: * — нуль или более, + — один или более, ? — необязательное вхождение

Автоматное программирование систем управления

203 of 596

203

Синтаксис регулярных выражений

Язык РВ состоит из литералов (обычный текст) и метасимволов

Точка — любой символ; символьные классы [A-Za-z] и их отрицания

Якоря позиции: начало строки, конец строки, граница слова

Скобки задают группу и влияют на порядок обработки; вертикальная черта — объединение

Квантификаторы: * — нуль или более, + — один или более, ? — необязательное вхождение

Интервальный квантификатор {n,m} задаёт число повторений явно

Автоматное программирование систем управления

204 of 596

204

Синтаксис регулярных выражений

Язык РВ состоит из литералов (обычный текст) и метасимволов

Точка — любой символ; символьные классы [A-Za-z] и их отрицания

Якоря позиции: начало строки, конец строки, граница слова

Скобки задают группу и влияют на порядок обработки; вертикальная черта — объединение

Квантификаторы: * — нуль или более, + — один или более, ? — необязательное вхождение

Интервальный квантификатор {n,m} задаёт число повторений явно

Механизм в его нынешнем виде популяризовал Perl (Ларри Уолл, 1987)

Автоматное программирование систем управления

205 of 596

205

Жадность, лень и ревность

Автоматное программирование систем управления

206 of 596

206

Жадность, лень и ревность

Жадный квантификатор захватывает максимум и отдаёт назад при откате

Автоматное программирование систем управления

207 of 596

207

Жадность, лень и ревность

Жадный квантификатор захватывает максимум и отдаёт назад при откате

Ленивый захватывает минимум и добирает по необходимости

Автоматное программирование систем управления

208 of 596

208

Жадность, лень и ревность

Жадный квантификатор захватывает максимум и отдаёт назад при откате

Ленивый захватывает минимум и добирает по необходимости

Ревнивый (сверхжадный) захватывает максимум и назад не отдаёт никогда

Автоматное программирование систем управления

209 of 596

209

Жадность, лень и ревность

Жадный квантификатор захватывает максимум и отдаёт назад при откате

Ленивый захватывает минимум и добирает по необходимости

Ревнивый (сверхжадный) захватывает максимум и назад не отдаёт никогда

Пример: a*a на строке из букв a совпадает — жадная часть отдаёт последнюю букву

Автоматное программирование систем управления

210 of 596

210

Жадность, лень и ревность

Жадный квантификатор захватывает максимум и отдаёт назад при откате

Ленивый захватывает минимум и добирает по необходимости

Ревнивый (сверхжадный) захватывает максимум и назад не отдаёт никогда

Пример: a*a на строке из букв a совпадает — жадная часть отдаёт последнюю букву

a*+a не совпадёт никогда: ревнивая часть съела всё, а откат запрещён

Автоматное программирование систем управления

211 of 596

211

Жадность, лень и ревность

Жадный квантификатор захватывает максимум и отдаёт назад при откате

Ленивый захватывает минимум и добирает по необходимости

Ревнивый (сверхжадный) захватывает максимум и назад не отдаёт никогда

Пример: a*a на строке из букв a совпадает — жадная часть отдаёт последнюю букву

a*+a не совпадёт никогда: ревнивая часть съела всё, а откат запрещён

Ревнивые квантификаторы — главный практический способ ограничить откат

Автоматное программирование систем управления

212 of 596

212

Где практика расходится с теорией

Автоматное программирование систем управления

213 of 596

213

Где практика расходится с теорией

Обратные ссылки: (.)\1 задаёт язык пар одинаковых символов — не регулярный

Автоматное программирование систем управления

214 of 596

214

Где практика расходится с теорией

Обратные ссылки: (.)\1 задаёт язык пар одинаковых символов — не регулярный

Просмотры вперёд и назад сами по себе силы не добавляют, но в паре с обратными ссылками выводят за регулярность

Автоматное программирование систем управления

215 of 596

215

Где практика расходится с теорией

Обратные ссылки: (.)\1 задаёт язык пар одинаковых символов — не регулярный

Рекурсивные шаблоны PCRE описывают скобочные последовательности — заведомо не регулярный язык

Автоматное программирование систем управления

216 of 596

216

Где практика расходится с теорией

Обратные ссылки: (.)\1 задаёт язык пар одинаковых символов — не регулярный

Рекурсивные шаблоны PCRE описывают скобочные последовательности — заведомо не регулярный язык

Отсюда: словом «регулярное выражение» называют два разных объекта

Автоматное программирование систем управления

217 of 596

217

Где практика расходится с теорией

Обратные ссылки: (.)\1 задаёт язык пар одинаковых символов — не регулярный

Рекурсивные шаблоны PCRE описывают скобочные последовательности — заведомо не регулярный язык

Отсюда: словом «регулярное выражение» называют два разных объекта

Теоретическое — то, для которого верна теорема Клини и существует эквивалентный автомат

Автоматное программирование систем управления

218 of 596

218

Где практика расходится с теорией

Обратные ссылки: (.)\1 задаёт язык пар одинаковых символов — не регулярный

Рекурсивные шаблоны PCRE описывают скобочные последовательности — заведомо не регулярный язык

Отсюда: словом «регулярное выражение» называют два разных объекта

Теоретическое — то, для которого верна теорема Клини и существует эквивалентный автомат

Практическое (PCRE) — язык шаблонов, надстроенный над теоретическим и заведомо более мощный

Автоматное программирование систем управления

219 of 596

219

Два семейства движков и ReDoS

Автоматное программирование систем управления

220 of 596

220

Два семейства движков и ReDoS

С возвратами: PCRE, Perl, Python re, JavaScript, Java — полный синтаксис, экспоненциальный худший случай

Автоматное программирование систем управления

221 of 596

221

Два семейства движков и ReDoS

С возвратами: PCRE, Perl, Python re, JavaScript, Java — полный синтаксис, экспоненциальный худший случай

Автоматные: RE2, rust regex, grep -E, awk — Томпсон плюс детерминизация на лету, линейное время

Автоматное программирование систем управления

222 of 596

222

Два семейства движков и ReDoS

С возвратами: PCRE, Perl, Python re, JavaScript, Java — полный синтаксис, экспоненциальный худший случай

Автоматные: RE2, rust regex, grep -E, awk — Томпсон плюс детерминизация на лету, линейное время

Выражение ^(a+)+$ на n буквах a с хвостом X перебирает порядка 2ⁿ разбиений

Автоматное программирование систем управления

223 of 596

223

Два семейства движков и ReDoS

С возвратами: PCRE, Perl, Python re, JavaScript, Java — полный синтаксис, экспоненциальный худший случай

Автоматные: RE2, rust regex, grep -E, awk — Томпсон плюс детерминизация на лету, линейное время

Выражение ^(a+)+$ на n буквах a с хвостом X перебирает порядка 2ⁿ разбиений

При n = 30 проверка занимает минуты, при n = 40 — часы

Автоматное программирование систем управления

224 of 596

224

Два семейства движков и ReDoS

С возвратами: PCRE, Perl, Python re, JavaScript, Java — полный синтаксис, экспоненциальный худший случай

Автоматные: RE2, rust regex, grep -E, awk — Томпсон плюс детерминизация на лету, линейное время

Выражение ^(a+)+$ на n буквах a с хвостом X перебирает порядка 2ⁿ разбиений

При n = 30 проверка занимает минуты, при n = 40 — часы

Подобное выражение в правилах фильтрации привело к масштабному сбою Cloudflare в 2019 году

Автоматное программирование систем управления

225 of 596

225

Два семейства движков и ReDoS

С возвратами: PCRE, Perl, Python re, JavaScript, Java — полный синтаксис, экспоненциальный худший случай

Автоматные: RE2, rust regex, grep -E, awk — Томпсон плюс детерминизация на лету, линейное время

Выражение ^(a+)+$ на n буквах a с хвостом X перебирает порядка 2ⁿ разбиений

При n = 30 проверка занимает минуты, при n = 40 — часы

Подобное выражение в правилах фильтрации привело к масштабному сбою Cloudflare в 2019 году

Правило для систем управления: на границе доверия — автоматные движки либо синтаксис без обратных ссылок

Автоматное программирование систем управления

226 of 596

226

Лексический анализ

Практикум: practices/06-lexical-analyze

227 of 596

227

Лексический анализ

Лексический анализатор — это ДКА, склеенный из автоматов отдельных лексем

Практикум: practices/06-lexical-analyze

228 of 596

228

Лексический анализ

Лексический анализатор — это ДКА, склеенный из автоматов отдельных лексем

Для каждой лексемы пишется регулярное выражение; выражения объединяются в один НКА

Практикум: practices/06-lexical-analyze

229 of 596

229

Лексический анализ

Лексический анализатор — это ДКА, склеенный из автоматов отдельных лексем

Для каждой лексемы пишется регулярное выражение; выражения объединяются в один НКА

НКА детерминизируется — ровно построение из лекций 4 и 5

Практикум: practices/06-lexical-analyze

230 of 596

230

Лексический анализ

Лексический анализатор — это ДКА, склеенный из автоматов отдельных лексем

Для каждой лексемы пишется регулярное выражение; выражения объединяются в один НКА

НКА детерминизируется — ровно построение из лекций 4 и 5

При совпадении выбирается самая длинная лексема — правило максимального поглощения

Практикум: practices/06-lexical-analyze

231 of 596

231

Лексический анализ

Лексический анализатор — это ДКА, склеенный из автоматов отдельных лексем

Для каждой лексемы пишется регулярное выражение; выражения объединяются в один НКА

НКА детерминизируется — ровно построение из лекций 4 и 5

При совпадении выбирается самая длинная лексема — правило максимального поглощения

Дальше начинается синтаксический анализ: вложенные скобки — уже не регулярный язык

Практикум: practices/06-lexical-analyze

232 of 596

232

Лексический анализ

Лексический анализатор — это ДКА, склеенный из автоматов отдельных лексем

Для каждой лексемы пишется регулярное выражение; выражения объединяются в один НКА

НКА детерминизируется — ровно построение из лекций 4 и 5

При совпадении выбирается самая длинная лексема — правило максимального поглощения

Дальше начинается синтаксический анализ: вложенные скобки — уже не регулярный язык

Это ровно та граница, на которой конечного автомата перестаёт хватать

Практикум: practices/06-lexical-analyze

233 of 596

233

Грамматика разбираемого языка

stmt := term | term '&' stmt

term := factor | factor '|' stmt

factor := '(' stmt ')' | ROLE

ROLE := [A-Z_]+

ws -> skip

ROLE — лексема, задаваемая регулярным выражением. Всё остальное уже синтаксис: для разбора вложенных скобок конечного автомата недостаточно.

Практикум: practices/06-lexical-analyze

234 of 596

234

Прикладной распознаватель: таблица вместо лестницы

Автомат разбора HTML-подобной разметки: у автомата нет счётчика, поэтому каждая ветвь «иначе» выписана явно — именно эту полноту лестница из if теряет незаметно

Практикум: practices/06-regular-expression

235 of 596

235

Автомат по выражению: декодер UTF-8

Байты, а не символы: длина последовательности определяется старшими битами первого байта, и каждый продолжающий байт проверяется отдельным состоянием

Автоматное программирование систем управления

236 of 596

ЛЕКЦИЯ

Автоматное программирование

Метод, его критика, ответ на критику и три формы записи

237 of 596

237

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Автоматное программирование систем управления

238 of 596

238

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Реализация автомата обязательно обёрнута циклом: while (cycle) { тело автомата }

Автоматное программирование систем управления

239 of 596

239

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Реализация автомата обязательно обёрнута циклом: while (cycle) { тело автомата }

Состояние программы — фрагмент кода, в котором ожидается локальное событие

Автоматное программирование систем управления

240 of 596

240

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Реализация автомата обязательно обёрнута циклом: while (cycle) { тело автомата }

Состояние программы — фрагмент кода, в котором ожидается локальное событие

Иначе: состояние — зацикливание на одном фрагменте до наступления события

Автоматное программирование систем управления

241 of 596

241

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Реализация автомата обязательно обёрнута циклом: while (cycle) { тело автомата }

Состояние программы — фрагмент кода, в котором ожидается локальное событие

Иначе: состояние — зацикливание на одном фрагменте до наступления события

Локальное событие — положительный результат вычисления логического выражения

Автоматное программирование систем управления

242 of 596

242

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Реализация автомата обязательно обёрнута циклом: while (cycle) { тело автомата }

Состояние программы — фрагмент кода, в котором ожидается локальное событие

Иначе: состояние — зацикливание на одном фрагменте до наступления события

Локальное событие — положительный результат вычисления логического выражения

Действие на переходе — что выполняется помимо смены state

Автоматное программирование систем управления

243 of 596

243

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Реализация автомата обязательно обёрнута циклом: while (cycle) { тело автомата }

Состояние программы — фрагмент кода, в котором ожидается локальное событие

Иначе: состояние — зацикливание на одном фрагменте до наступления события

Локальное событие — положительный результат вычисления логического выражения

Действие на переходе — что выполняется помимо смены state

Модификация — однократное изменение аргументов перед вычислением условий состояния

Автоматное программирование систем управления

244 of 596

244

Метод: while — switch — case

Изложение по работе Б. П. Кузнецова «Психология автоматного программирования»

Реализация автомата обязательно обёрнута циклом: while (cycle) { тело автомата }

Состояние программы — фрагмент кода, в котором ожидается локальное событие

Иначе: состояние — зацикливание на одном фрагменте до наступления события

Локальное событие — положительный результат вычисления логического выражения

Действие на переходе — что выполняется помимо смены state

Модификация — однократное изменение аргументов перед вычислением условий состояния

Состояния реализуются оператором switch (state) — case

Автоматное программирование систем управления

245 of 596

245

Автоматный алгоритм в общем виде

Рамка имитирует цикловую природу реализации: вверху явно указан while (cycle). Переходы помечены дробью «локальное событие / действие на переходе», Z — модификация в состоянии

Автоматное программирование систем управления

246 of 596

246

Каркас автоматной программы

static char state = 'A';

int cycle = 1;

while (cycle) {

switch (state) {

case 'A': call YAB; state = 'B'; break;

case 'B':

call ZB; /* модификация */

if (XBA) { call YBA; cycle = 0; state = 'A'; }

else if (XBC) { call YBC; state = 'C'; }

else { call YBB; /* петля: state не меняется */ }

break;

}

Цикл объемлет автомат — без него граф переходов остаётся рисунком. Каждый проход обязан менять аргументы вычисляемых логических выражений, иначе автомат зависает.

Автоматное программирование систем управления

247 of 596

247

Ортогональность и полнота — это вычисление, а не осмотр

Пусть из состояния q ведут переходы по условиям X₁ … X_k над входами x₁ … x_m

Автоматное программирование систем управления

248 of 596

248

Ортогональность и полнота — это вычисление, а не осмотр

Пусть из состояния q ведут переходы по условиям X₁ … X_k над входами x₁ … x_m

Ортогональность: Xᵢ ∧ Xⱼ ≡ 0 при i ≠ j — никакой набор входов не включает два перехода сразу

Автоматное программирование систем управления

249 of 596

249

Ортогональность и полнота — это вычисление, а не осмотр

Пусть из состояния q ведут переходы по условиям X₁ … X_k над входами x₁ … x_m

Ортогональность: Xᵢ ∧ Xⱼ ≡ 0 при i ≠ j — никакой набор входов не включает два перехода сразу

Иначе поведение зависит от порядка проверок в коде, то есть от того, как написан if, а не от модели

Автоматное программирование систем управления

250 of 596

250

Ортогональность и полнота — это вычисление, а не осмотр

Пусть из состояния q ведут переходы по условиям X₁ … X_k над входами x₁ … x_m

Ортогональность: Xᵢ ∧ Xⱼ ≡ 0 при i ≠ j — никакой набор входов не включает два перехода сразу

Иначе поведение зависит от порядка проверок в коде, то есть от того, как написан if, а не от модели

Полнота: X₁ ∨ … ∨ X_k ∨ L ≡ 1, где L — условие петли

Автоматное программирование систем управления

251 of 596

251

Ортогональность и полнота — это вычисление, а не осмотр

Пусть из состояния q ведут переходы по условиям X₁ … X_k над входами x₁ … x_m

Ортогональность: Xᵢ ∧ Xⱼ ≡ 0 при i ≠ j — никакой набор входов не включает два перехода сразу

Иначе поведение зависит от порядка проверок в коде, то есть от того, как написан if, а не от модели

Полнота: X₁ ∨ … ∨ X_k ∨ L ≡ 1, где L — условие петли

Непокрытый набор — это состояние, из которого поведение не определено

Автоматное программирование систем управления

252 of 596

252

Ортогональность и полнота — это вычисление, а не осмотр

Пусть из состояния q ведут переходы по условиям X₁ … X_k над входами x₁ … x_m

Ортогональность: Xᵢ ∧ Xⱼ ≡ 0 при i ≠ j — никакой набор входов не включает два перехода сразу

Иначе поведение зависит от порядка проверок в коде, то есть от того, как написан if, а не от модели

Полнота: X₁ ∨ … ∨ X_k ∨ L ≡ 1, где L — условие петли

Непокрытый набор — это состояние, из которого поведение не определено

Проверка — перебор 2^m наборов: ровно одно истинное условие — строка верна

Автоматное программирование систем управления

253 of 596

253

Ортогональность и полнота — это вычисление, а не осмотр

Пусть из состояния q ведут переходы по условиям X₁ … X_k над входами x₁ … x_m

Ортогональность: Xᵢ ∧ Xⱼ ≡ 0 при i ≠ j — никакой набор входов не включает два перехода сразу

Иначе поведение зависит от порядка проверок в коде, то есть от того, как написан if, а не от модели

Полнота: X₁ ∨ … ∨ X_k ∨ L ≡ 1, где L — условие петли

Непокрытый набор — это состояние, из которого поведение не определено

Проверка — перебор 2^m наборов: ровно одно истинное условие — строка верна

Два и больше — нарушена ортогональность; ноль и нет петли — нарушена полнота

Автоматное программирование систем управления

254 of 596

254

Проверка ортогональности таблицей

x₁	x₂	X_qr = x₁	X_qs = x₁ ∧ ¬x₂	Истинных условий
0	0	0	0	0 — нужна петля
0	1	0	0	0 — нужна петля
1	0	1	1	2 — ошибка
1	1	1	0	1 — порядок

В коде дефект выглядит безобидно: два if подряд, первый срабатывает, второй не проверяется. Работать программа будет; вопрос лишь в том, совпадает ли этот порядок с намерением автора — а по модели этого уже не установить.

Автоматное программирование систем управления

255 of 596

255

Словарь: одно и то же тремя языками

У Кузнецова	В теории автоматов	В коде
состояние — фрагмент программы	состояние q ∈ Q	значение переменной state
локальное событие X_ij	буква входного алфавита a ∈ A	значение логического выражения
действие на переходе Y_ij	функция выходов ψ(q, a) модели Мили	вызов в ветви, меняющей state
модификация Z_q	действие, приписанное состоянию (Мур)	операторы в начале ветви case
while (cycle)	дискретное время: проход — такт	цикл опроса, прерывание, цикл ПЛК
ортогональность условий	детерминированность: δ — функция	не более одного истинного условия

Самая частая ошибка — отождествить входное воздействие с буквой алфавита: буква абстрактна, выражение — её реализация, и одна буква может задаваться разными выражениями.

Автоматное программирование систем управления

256 of 596

256

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Автоматное программирование систем управления

257 of 596

257

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Не учтённые и дублирующие состояния — следствие незнания предметной области

Автоматное программирование систем управления

258 of 596

258

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Не учтённые и дублирующие состояния — следствие незнания предметной области

Не учтённые, лишние и неверно ориентированные переходы

Автоматное программирование систем управления

259 of 596

259

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Не учтённые и дублирующие состояния — следствие незнания предметной области

Не учтённые, лишние и неверно ориентированные переходы

Неортогональность входного алфавита и неверные приоритеты переходов при ней

Автоматное программирование систем управления

260 of 596

260

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Не учтённые и дублирующие состояния — следствие незнания предметной области

Не учтённые, лишние и неверно ориентированные переходы

Неортогональность входного алфавита и неверные приоритеты переходов при ней

Неполный учёт букв входного алфавита

Автоматное программирование систем управления

261 of 596

261

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Не учтённые и дублирующие состояния — следствие незнания предметной области

Не учтённые, лишние и неверно ориентированные переходы

Неортогональность входного алфавита и неверные приоритеты переходов при ней

Неполный учёт букв входного алфавита

Отождествление входных воздействий с буквами алфавита — самая распространённая ошибка

Автоматное программирование систем управления

262 of 596

262

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Не учтённые и дублирующие состояния — следствие незнания предметной области

Не учтённые, лишние и неверно ориентированные переходы

Неортогональность входного алфавита и неверные приоритеты переходов при ней

Неполный учёт букв входного алфавита

Отождествление входных воздействий с буквами алфавита — самая распространённая ошибка

Забытое обнуление или продление выходного воздействия

Автоматное программирование систем управления

263 of 596

263

Критика: восемнадцать типичных ошибок

Перечень принадлежит тому же автору, что и изложенный метод

Не учтённые и дублирующие состояния — следствие незнания предметной области

Не учтённые, лишние и неверно ориентированные переходы

Неортогональность входного алфавита и неверные приоритеты переходов при ней

Неполный учёт букв входного алфавита

Отождествление входных воздействий с буквами алфавита — самая распространённая ошибка

Забытое обнуление или продление выходного воздействия

Не прослеживаются полные пути в диаграмме состояний

Автоматное программирование систем управления

264 of 596

264

Ответ на критику

Список — часть полемики Б. П. Кузнецова и А. А. Шалыто, и у него есть ответ

Автоматное программирование систем управления

265 of 596

265

Ответ на критику

Список — часть полемики Б. П. Кузнецова и А. А. Шалыто, и у него есть ответ

Длина перечня — свидетельство формализации, а не порочности: каждый пункт называет конкретное место в модели

Автоматное программирование систем управления

266 of 596

266

Ответ на критику

Список — часть полемики Б. П. Кузнецова и А. А. Шалыто, и у него есть ответ

Для программы, написанной обычным образом, такой перечень вырождается в строку «в логике могут быть ошибки»

Автоматное программирование систем управления

267 of 596

267

Ответ на критику

Список — часть полемики Б. П. Кузнецова и А. А. Шалыто, и у него есть ответ

Для программы, написанной обычным образом, такой перечень вырождается в строку «в логике могут быть ошибки»

И сделать с ней нечего: не названо ни одного места, где ошибку искать

Автоматное программирование систем управления

268 of 596

268

Ответ на критику

Список — часть полемики Б. П. Кузнецова и А. А. Шалыто, и у него есть ответ

Для программы, написанной обычным образом, такой перечень вырождается в строку «в логике могут быть ошибки»

И сделать с ней нечего: не названо ни одного места, где ошибку искать

Почти всё перечисленное проверяется — инструментом или вручную по описанию, а не по коду

Автоматное программирование систем управления

269 of 596

269

Ответ на критику

Список — часть полемики Б. П. Кузнецова и А. А. Шалыто, и у него есть ответ

Для программы, написанной обычным образом, такой перечень вырождается в строку «в логике могут быть ошибки»

И сделать с ней нечего: не названо ни одного места, где ошибку искать

Почти всё перечисленное проверяется — инструментом или вручную по описанию, а не по коду

Граф переходов можно верифицировать и обсуждать с заказчиком, текст программы — нет

Автоматное программирование систем управления

270 of 596

270

Ответ на критику

Список — часть полемики Б. П. Кузнецова и А. А. Шалыто, и у него есть ответ

Для программы, написанной обычным образом, такой перечень вырождается в строку «в логике могут быть ошибки»

И сделать с ней нечего: не названо ни одного места, где ошибку искать

Почти всё перечисленное проверяется — инструментом или вручную по описанию, а не по коду

Граф переходов можно верифицировать и обсуждать с заказчиком, текст программы — нет

Обе позиции об одном: явная модель имеет цену, и оплачивается она проверяемостью

Автоматное программирование систем управления

271 of 596

271

Чего перечень не покрывает

Автоматное программирование систем управления

272 of 596

272

Чего перечень не покрывает

Ни одна проверка не отвечает на вопрос, делает ли автомат то, что нужно

Автоматное программирование систем управления

273 of 596

273

Чего перечень не покрывает

Ни одна проверка не отвечает на вопрос, делает ли автомат то, что нужно

Все проверки — о внутренней согласованности описания: полное, непротиворечивое, достижимое

Автоматное программирование систем управления

274 of 596

274

Чего перечень не покрывает

Ни одна проверка не отвечает на вопрос, делает ли автомат то, что нужно

Все проверки — о внутренней согласованности описания: полное, непротиворечивое, достижимое

Требование «шлагбаум не должен опускаться на машину» ни из одной из них не следует

Автоматное программирование систем управления

275 of 596

275

Чего перечень не покрывает

Ни одна проверка не отвечает на вопрос, делает ли автомат то, что нужно

Все проверки — о внутренней согласованности описания: полное, непротиворечивое, достижимое

Требование «шлагбаум не должен опускаться на машину» ни из одной из них не следует

Его формулируют отдельно и проверяют тоже отдельно — лекция 9

Автоматное программирование систем управления

276 of 596

276

Чего перечень не покрывает

Ни одна проверка не отвечает на вопрос, делает ли автомат то, что нужно

Все проверки — о внутренней согласованности описания: полное, непротиворечивое, достижимое

Требование «шлагбаум не должен опускаться на машину» ни из одной из них не следует

Его формулируют отдельно и проверяют тоже отдельно — лекция 9

Сто процентов покрытия переходов прекрасно уживаются с дефектом

Автоматное программирование систем управления

277 of 596

277

Когда автоматный подход оправдан

Подход оправдан	Подход избыточен
Реактивные системы: реакция на события, а не вычисление функции	Расчётные задачи: обработка массива, численный метод
Протоколы и разбор форматов	Прямолинейный последовательный алгоритм без состояния
Встраиваемые системы и логическое управление	Код, где состояний два и они не растут
Требуется верификация или доказуемое покрытие тестами	Одноразовый скрипт

Контрпример из практикума — practices/07-simple-program: вложенные switch и if, где состояние размазано по значениям нескольких переменных и порядку ветвлений.

Автоматное программирование систем управления

278 of 596

278

Три реализации одного автомата: шлагбаум

4 состояния, 5 событий, 20 клеток таблицы. Содержательных переходов шесть — остальные четырнадцать клеток это игнорирование события, и они тоже переходы

Практикум: practices/07-three-ways

279 of 596

279

Три реализации: чем отличаются

Критерий	switch	Таблица	State
Строк кода	70	104 (из них 20 — таблица)	73
Где модель	в потоке управления	в данных	в объектах
Видно ли автомат целиком	нет	да	нет
Добавить состояние	ветка + правки соседних	строка таблицы	новый объект
Добавить событие	правка каждого состояния	столбец таблицы	правка каждого объекта
Действие при входе	вручную	вручную	штатно (on_enter)
Покрытие переходов	через покрытие строк	счётчик на клетку	через покрытие строк

Разница в скорости — единицы тактов на событие, на фоне миллисекунд движения створки это шум. Выбирать форму по скорости почти никогда не приходится; по стоимости изменения — приходится всегда.

Автоматное программирование систем управления

280 of 596

280

Автомат и его окружение

В приложении вход приходит с датчиков, а выход уходит на приводы

Практикум: practices/03-control-program

281 of 596

281

Автомат и его окружение

В приложении вход приходит с датчиков, а выход уходит на приводы

Если автомат читает всё это сам, проверить его нечем и перенести на другую установку нельзя

Практикум: practices/03-control-program

282 of 596

282

Автомат и его окружение

В приложении вход приходит с датчиков, а выход уходит на приводы

Если автомат читает всё это сам, проверить его нечем и перенести на другую установку нельзя

Приём: между автоматом и миром ставится интерфейс — таблица функций, которую автомат получает параметром

Практикум: practices/03-control-program

283 of 596

283

Автомат и его окружение

В приложении вход приходит с датчиков, а выход уходит на приводы

Если автомат читает всё это сам, проверить его нечем и перенести на другую установку нельзя

Приём: между автоматом и миром ставится интерфейс — таблица функций, которую автомат получает параметром

В сквозном проекте курса интерфейсов три: входы, выходы и настройки

Практикум: practices/03-control-program

284 of 596

284

Автомат и его окружение

В приложении вход приходит с датчиков, а выход уходит на приводы

Если автомат читает всё это сам, проверить его нечем и перенести на другую установку нельзя

Приём: между автоматом и миром ставится интерфейс — таблица функций, которую автомат получает параметром

В сквозном проекте курса интерфейсов три: входы, выходы и настройки

Автомат объявлен как engine_execute(pi, si, di) и не содержит ни одного обращения к файлу, порту или сокету

Практикум: practices/03-control-program

285 of 596

285

Автомат и его окружение

В приложении вход приходит с датчиков, а выход уходит на приводы

Если автомат читает всё это сам, проверить его нечем и перенести на другую установку нельзя

Приём: между автоматом и миром ставится интерфейс — таблица функций, которую автомат получает параметром

В сквозном проекте курса интерфейсов три: входы, выходы и настройки

Автомат объявлен как engine_execute(pi, si, di) и не содержит ни одного обращения к файлу, порту или сокету

Что стоит по ту сторону — решает тот, кто собирает программу: заглушки, запись из файла, модель установки или сетевой эмулятор

Практикум: practices/03-control-program

286 of 596

286

Автомат и его окружение

В приложении вход приходит с датчиков, а выход уходит на приводы

Если автомат читает всё это сам, проверить его нечем и перенести на другую установку нельзя

Приём: между автоматом и миром ставится интерфейс — таблица функций, которую автомат получает параметром

В сквозном проекте курса интерфейсов три: входы, выходы и настройки

Автомат объявлен как engine_execute(pi, si, di) и не содержит ни одного обращения к файлу, порту или сокету

Логика при этом не меняется ни на строку — меняется только содержимое трёх таблиц функций

Практикум: practices/03-control-program

287 of 596

287

Четыре источника входов автомата

Между автоматом и миром ставится интерфейс — таблица функций, которую автомат получает параметром

Автомат

engine_execute(pi, si, di)

ни файла, ни порта, ни сокета

граница интерфейса

три таблицы

функций

Заглушки

по умолчанию: автомат запускается вообще без установки

Запись показаний из файла

-DENABLE_FILE_EMULATE=ON · повторяет то, что уже было; после правки автомата её надо переснимать

Модель установки в том же процессе

отвечает на команды, поэтому проверяет управление, а не совпадение с записью

Внешний эмулятор, обмен по TCP

-DENABLE_NETWORK_EMULATE=ON · то же, что модель, плюс сам обмен и его задержки

В курсе собраны три из четырёх. Логика не меняется ни на строку — меняется только то, чем заполнены таблицы функций

Лекция 7 · § «Автомат и его окружение» · practices/03-control-program

288 of 596

288

Три критерия покрытия

Автоматное программирование систем управления

289 of 596

289

Три критерия покрытия

Покрытие состояний: каждое состояние хотя бы раз посещено — слабый критерий

Автоматное программирование систем управления

290 of 596

290

Три критерия покрытия

Покрытие состояний: каждое состояние хотя бы раз посещено — слабый критерий

У шлагбаума достаточно одного сценария, чтобы побывать во всех четырёх состояниях

Автоматное программирование систем управления

291 of 596

291

Три критерия покрытия

Покрытие состояний: каждое состояние хотя бы раз посещено — слабый критерий

У шлагбаума достаточно одного сценария, чтобы побывать во всех четырёх состояниях

Покрытие переходов: каждая клетка таблицы хотя бы раз сработала — 20 клеток, а не 6 содержательных переходов

Автоматное программирование систем управления

292 of 596

292

Три критерия покрытия

Покрытие состояний: каждое состояние хотя бы раз посещено — слабый критерий

У шлагбаума достаточно одного сценария, чтобы побывать во всех четырёх состояниях

Покрытие переходов: каждая клетка таблицы хотя бы раз сработала — 20 клеток, а не 6 содержательных переходов

Покрытие путей: каждый различный путь пройден хотя бы раз

Автоматное программирование систем управления

293 of 596

293

Три критерия покрытия

Покрытие состояний: каждое состояние хотя бы раз посещено — слабый критерий

У шлагбаума достаточно одного сценария, чтобы побывать во всех четырёх состояниях

Покрытие переходов: каждая клетка таблицы хотя бы раз сработала — 20 клеток, а не 6 содержательных переходов

Покрытие путей: каждый различный путь пройден хотя бы раз

Если в графе есть достижимый цикл, различных путей бесконечно много — покрытие путей недостижимо

Автоматное программирование систем управления

294 of 596

294

Три критерия покрытия

Покрытие состояний: каждое состояние хотя бы раз посещено — слабый критерий

У шлагбаума достаточно одного сценария, чтобы побывать во всех четырёх состояниях

Покрытие переходов: каждая клетка таблицы хотя бы раз сработала — 20 клеток, а не 6 содержательных переходов

Покрытие путей: каждый различный путь пройден хотя бы раз

Если в графе есть достижимый цикл, различных путей бесконечно много — покрытие путей недостижимо

А управляющий автомат циклический по построению, поэтому практическим критерием остаётся покрытие переходов

Автоматное программирование систем управления

295 of 596

295

Покрытие — не корректность

Числа из практикума: ни один сценарий не даёт больше 35 %

Автоматное программирование систем управления

296 of 596

296

Покрытие — не корректность

Числа из практикума: ни один сценарий не даёт больше 35 %

«Нормальный» сценарий — подъехал, проехал, закрылся — покрывает 20 %

Автоматное программирование систем управления

297 of 596

297

Покрытие — не корректность

Числа из практикума: ни один сценарий не даёт больше 35 %

«Нормальный» сценарий — подъехал, проехал, закрылся — покрывает 20 %

Остальные 80 % — поведение при событиях, приходящих не вовремя

Автоматное программирование систем управления

298 of 596

298

Покрытие — не корректность

Числа из практикума: ни один сценарий не даёт больше 35 %

«Нормальный» сценарий — подъехал, проехал, закрылся — покрывает 20 %

Остальные 80 % — поведение при событиях, приходящих не вовремя

Концевик сработал дважды, карта приложена во время закрытия, такт таймера пришёл в закрытом состоянии

Автоматное программирование систем управления

299 of 596

299

Покрытие — не корректность

Числа из практикума: ни один сценарий не даёт больше 35 %

«Нормальный» сценарий — подъехал, проехал, закрылся — покрывает 20 %

Остальные 80 % — поведение при событиях, приходящих не вовремя

Концевик сработал дважды, карта приложена во время закрытия, такт таймера пришёл в закрытом состоянии

Именно там живут дефекты управляющих программ

Автоматное программирование систем управления

300 of 596

300

Покрытие — не корректность

Числа из практикума: ни один сценарий не даёт больше 35 %

«Нормальный» сценарий — подъехал, проехал, закрылся — покрывает 20 %

Остальные 80 % — поведение при событиях, приходящих не вовремя

Концевик сработал дважды, карта приложена во время закрытия, такт таймера пришёл в закрытом состоянии

Именно там живут дефекты управляющих программ

Уберите обнуление счётчика выдержки при входе в OPEN — покрытие останется 100 %, а дефект появится

Автоматное программирование систем управления

301 of 596

301

Покрытие — не корректность

Числа из практикума: ни один сценарий не даёт больше 35 %

«Нормальный» сценарий — подъехал, проехал, закрылся — покрывает 20 %

Остальные 80 % — поведение при событиях, приходящих не вовремя

Концевик сработал дважды, карта приложена во время закрытия, такт таймера пришёл в закрытом состоянии

Именно там живут дефекты управляющих программ

Уберите обнуление счётчика выдержки при входе в OPEN — покрытие останется 100 %, а дефект появится

Покрытие переходов — нижняя граница приличия, а не признак проверенности: расширенное состояние в таблицу не входит

Автоматное программирование систем управления

302 of 596

302

W-метод: как проверить чёрный ящик

Автоматное программирование систем управления

303 of 596

303

W-метод: как проверить чёрный ящик

Различающая последовательность: слово, на котором два состояния дают разные выходы

Автоматное программирование систем управления

304 of 596

304

W-метод: как проверить чёрный ящик

Различающая последовательность: слово, на котором два состояния дают разные выходы

Установочная: слово, после которого известно, в каком состоянии оказался автомат

Автоматное программирование систем управления

305 of 596

305

W-метод: как проверить чёрный ящик

Различающая последовательность: слово, на котором два состояния дают разные выходы

Установочная: слово, после которого известно, в каком состоянии оказался автомат

Диагностическая: слово, по реакции на которое определяется, в каком состоянии автомат был

Автоматное программирование систем управления

306 of 596

306

W-метод: как проверить чёрный ящик

Различающая последовательность: слово, на котором два состояния дают разные выходы

Установочная: слово, после которого известно, в каком состоянии оказался автомат

Диагностическая: слово, по реакции на которое определяется, в каком состоянии автомат был

W-множество различающее, если для любых двух неэквивалентных состояний в нём есть различающее их слово

Автоматное программирование систем управления

307 of 596

307

W-метод: как проверить чёрный ящик

Различающая последовательность: слово, на котором два состояния дают разные выходы

Установочная: слово, после которого известно, в каком состоянии оказался автомат

Диагностическая: слово, по реакции на которое определяется, в каком состоянии автомат был

W-множество различающее, если для любых двух неэквивалентных состояний в нём есть различающее их слово

Набор тестов строится как произведение P · W: довести до состояния, выполнить переход, убедиться словом из W

Автоматное программирование систем управления

308 of 596

308

W-метод: как проверить чёрный ящик

Различающая последовательность: слово, на котором два состояния дают разные выходы

Установочная: слово, после которого известно, в каком состоянии оказался автомат

Диагностическая: слово, по реакции на которое определяется, в каком состоянии автомат был

W-множество различающее, если для любых двух неэквивалентных состояний в нём есть различающее их слово

Набор тестов строится как произведение P · W: довести до состояния, выполнить переход, убедиться словом из W

При известной верхней оценке числа состояний реализации метод обнаруживает любое расхождение с моделью

Автоматное программирование систем управления

309 of 596

309

W-метод: как проверить чёрный ящик

Различающая последовательность: слово, на котором два состояния дают разные выходы

Установочная: слово, после которого известно, в каком состоянии оказался автомат

Диагностическая: слово, по реакции на которое определяется, в каком состоянии автомат был

W-множество различающее, если для любых двух неэквивалентных состояний в нём есть различающее их слово

Набор тестов строится как произведение P · W: довести до состояния, выполнить переход, убедиться словом из W

При известной верхней оценке числа состояний реализации метод обнаруживает любое расхождение с моделью

Это редкий случай, когда тестирование даёт не эвристику, а теорему; цена — размер набора

Автоматное программирование систем управления

310 of 596

ЛЕКЦИЯ

Иерархические автоматы и кодогенерация

Statecharts Харела, ПЛК, SimInTech

311 of 596

311

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Автоматное программирование систем управления

312 of 596

312

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Плоский автомат хорошо описывает объект с десятком состояний

Автоматное программирование систем управления

313 of 596

313

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Плоский автомат хорошо описывает объект с десятком состояний

Цикл стирки — шесть состояний

Автоматное программирование систем управления

314 of 596

314

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Плоский автомат хорошо описывает объект с десятком состояний

Цикл стирки — шесть состояний

Добавим режим паузы: каждое состояние удваивается

Автоматное программирование систем управления

315 of 596

315

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Плоский автомат хорошо описывает объект с десятком состояний

Цикл стирки — шесть состояний

Добавим режим паузы: каждое состояние удваивается

Добавим состояния индикатора — умножается снова

Автоматное программирование систем управления

316 of 596

316

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Плоский автомат хорошо описывает объект с десятком состояний

Цикл стирки — шесть состояний

Добавим режим паузы: каждое состояние удваивается

Добавим состояния индикатора — умножается снова

Добавим обработку обрыва датчика в любой момент — 37 состояний и 185 клеток

Автоматное программирование систем управления

317 of 596

317

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Плоский автомат хорошо описывает объект с десятком состояний

Цикл стирки — шесть состояний

Добавим режим паузы: каждое состояние удваивается

Добавим состояния индикатора — умножается снова

Добавим обработку обрыва датчика в любой момент — 37 состояний и 185 клеток

Содержательно различны при этом единицы

Автоматное программирование систем управления

318 of 596

318

Зачем расширять модель

Стиральная машина: как шесть состояний превращаются в тридцать семь

Плоский автомат хорошо описывает объект с десятком состояний

Цикл стирки — шесть состояний

Добавим режим паузы: каждое состояние удваивается

Добавим состояния индикатора — умножается снова

Добавим обработку обрыва датчика в любой момент — 37 состояний и 185 клеток

Содержательно различны при этом единицы

Выход — не отказ от автоматов, а иерархия и ортогональные регионы

Автоматное программирование систем управления

319 of 596

319

Statecharts Харела, 1987

Автоматное программирование систем управления

320 of 596

320

Statecharts Харела, 1987

Иерархия: составное состояние содержит вложенный автомат

Автоматное программирование систем управления

321 of 596

321

Statecharts Харела, 1987

Иерархия: составное состояние содержит вложенный автомат

Переход из составного состояния срабатывает независимо от того, где система внутри, — это и снимает взрыв

Автоматное программирование систем управления

322 of 596

322

Statecharts Харела, 1987

Иерархия: составное состояние содержит вложенный автомат

Переход из составного состояния срабатывает независимо от того, где система внутри, — это и снимает взрыв

Ортогональные регионы: несколько автоматов работают параллельно внутри одного состояния

Автоматное программирование систем управления

323 of 596

323

Statecharts Харела, 1987

Иерархия: составное состояние содержит вложенный автомат

Переход из составного состояния срабатывает независимо от того, где система внутри, — это и снимает взрыв

Ортогональные регионы: несколько автоматов работают параллельно внутри одного состояния

История: псевдосостояние запоминает, где система была при выходе, чтобы вернуться туда же

Автоматное программирование систем управления

324 of 596

324

Statecharts Харела, 1987

Иерархия: составное состояние содержит вложенный автомат

Переход из составного состояния срабатывает независимо от того, где система внутри, — это и снимает взрыв

Ортогональные регионы: несколько автоматов работают параллельно внутри одного состояния

История: псевдосостояние запоминает, где система была при выходе, чтобы вернуться туда же

Действия entry и exit выполняются при входе и выходе независимо от того, каким переходом

Автоматное программирование систем управления

325 of 596

325

Statecharts Харела, 1987

Иерархия: составное состояние содержит вложенный автомат

Переход из составного состояния срабатывает независимо от того, где система внутри, — это и снимает взрыв

Ортогональные регионы: несколько автоматов работают параллельно внутри одного состояния

История: псевдосостояние запоминает, где система была при выходе, чтобы вернуться туда же

Действия entry и exit выполняются при входе и выходе независимо от того, каким переходом

Широковещательные события: событие одного региона видно остальным

Автоматное программирование систем управления

326 of 596

326

Statecharts Харела, 1987

Иерархия: составное состояние содержит вложенный автомат

Переход из составного состояния срабатывает независимо от того, где система внутри, — это и снимает взрыв

Ортогональные регионы: несколько автоматов работают параллельно внутри одного состояния

История: псевдосостояние запоминает, где система была при выходе, чтобы вернуться туда же

Действия entry и exit выполняются при входе и выходе независимо от того, каким переходом

Широковещательные события: событие одного региона видно остальным

Нотация легла в основу диаграмм состояний UML

Автоматное программирование систем управления

327 of 596

327

Statechart стиральной машины

Цикл стирки как составное состояние, псевдосостояние истории H для возврата после паузы, ортогональный регион индикации, авария — переходом из границы составного состояния

Автоматное программирование систем управления

328 of 596

328

Плоский автомат против statechart на одной задаче

Величина	Плоский автомат	Statechart
Состояний	37	6 + 2 + 3 = 11
Переходов нарисовано	185 клеток	13
Переходов по fail	36	1
Переходов по pause/resume	36	2
Добавить седьмой шаг	+6 состояний, +30 клеток	+1 состояние, +1 переход
Добавить режим индикации	все состояния ×4/3	+1 состояние в регионе

Сокращение примерно в четырнадцать раз по числу переходов — и это на маленькой задаче. Существенно, что разрыв растёт: каждое новое независимое измерение умножает плоский автомат и добавляет константу statechart'у.

Автоматное программирование систем управления

329 of 596

329

Чего иерархия не даёт

Автоматное программирование систем управления

330 of 596

330

Чего иерархия не даёт

Statechart — это запись автомата, а не другая вычислительная модель

Автоматное программирование систем управления

331 of 596

331

Чего иерархия не даёт

Statechart — это запись автомата, а не другая вычислительная модель

Любой statechart разворачивается в плоский автомат: те самые 37 состояний

Автоматное программирование систем управления

332 of 596

332

Чего иерархия не даёт

Statechart — это запись автомата, а не другая вычислительная модель

Любой statechart разворачивается в плоский автомат: те самые 37 состояний

Мощность модели не меняется — распознаваемые языки остаются регулярными

Автоматное программирование систем управления

333 of 596

333

Чего иерархия не даёт

Statechart — это запись автомата, а не другая вычислительная модель

Любой statechart разворачивается в плоский автомат: те самые 37 состояний

Мощность модели не меняется — распознаваемые языки остаются регулярными

Выигрыш целиком в человеке: сколько переходов приходится придумать, нарисовать и проверить

Автоматное программирование систем управления

334 of 596

334

Чего иерархия не даёт

Statechart — это запись автомата, а не другая вычислительная модель

Любой statechart разворачивается в плоский автомат: те самые 37 состояний

Мощность модели не меняется — распознаваемые языки остаются регулярными

Выигрыш целиком в человеке: сколько переходов приходится придумать, нарисовать и проверить

Обратная сторона — сложная семантика: порядок exit/entry, приоритет вложенных переходов, момент доставки события

Автоматное программирование систем управления

335 of 596

335

Чего иерархия не даёт

Statechart — это запись автомата, а не другая вычислительная модель

Любой statechart разворачивается в плоский автомат: те самые 37 состояний

Мощность модели не меняется — распознаваемые языки остаются регулярными

Выигрыш целиком в человеке: сколько переходов приходится придумать, нарисовать и проверить

В разных инструментах это решено по-разному, и модель может вести себя иначе при переносе

Автоматное программирование систем управления

336 of 596

336

Автоматы в промышленных стандартах

Автоматное программирование систем управления

337 of 596

337

Автоматы в промышленных стандартах

Цикл ПЛК: чтение входов → выполнение программы → запись выходов — в точности такт автомата

Автоматное программирование систем управления

338 of 596

338

Автоматы в промышленных стандартах

Цикл ПЛК: чтение входов → выполнение программы → запись выходов — в точности такт автомата

IEC 61131-3 определяет пять языков ПЛК; один из них SFC, прямой потомок Grafcet

Автоматное программирование систем управления

339 of 596

339

Автоматы в промышленных стандартах

Цикл ПЛК: чтение входов → выполнение программы → запись выходов — в точности такт автомата

IEC 61131-3 определяет пять языков ПЛК; один из них SFC, прямой потомок Grafcet

Шаги, переходы с условиями и действия SFC — это состояния, переходы и выходные воздействия

Автоматное программирование систем управления

340 of 596

340

Автоматы в промышленных стандартах

Цикл ПЛК: чтение входов → выполнение программы → запись выходов — в точности такт автомата

IEC 61131-3 определяет пять языков ПЛК; один из них SFC, прямой потомок Grafcet

Шаги, переходы с условиями и действия SFC — это состояния, переходы и выходные воздействия

Но в SFC активны сразу несколько шагов: текущее состояние — множество, а не один шаг

Автоматное программирование систем управления

341 of 596

341

Автоматы в промышленных стандартах

Цикл ПЛК: чтение входов → выполнение программы → запись выходов — в точности такт автомата

IEC 61131-3 определяет пять языков ПЛК; один из них SFC, прямой потомок Grafcet

Шаги, переходы с условиями и действия SFC — это состояния, переходы и выходные воздействия

Но в SFC активны сразу несколько шагов: текущее состояние — множество, а не один шаг

Произвольной вложенности нет: шаг атомарен, иерархию изображают вызовом другой SFC-программы

Автоматное программирование систем управления

342 of 596

342

Автоматы в промышленных стандартах

Цикл ПЛК: чтение входов → выполнение программы → запись выходов — в точности такт автомата

IEC 61131-3 определяет пять языков ПЛК; один из них SFC, прямой потомок Grafcet

Шаги, переходы с условиями и действия SFC — это состояния, переходы и выходные воздействия

Но в SFC активны сразу несколько шагов: текущее состояние — множество, а не один шаг

Произвольной вложенности нет: шаг атомарен, иерархию изображают вызовом другой SFC-программы

Событий нет: есть выражения от входов, вычисляемые заново каждый такт — фронт приходится строить руками

Автоматное программирование систем управления

343 of 596

343

Автомат TCP: установление соединения

Спецификация TCP описана автоматом состояний соединения (RFC 793): одиннадцать состояний. Хороший пример автомата, который студент уже видел, но не опознавал как автомат

Автоматное программирование систем управления

344 of 596

344

Практика: циклограмма пневмоцилиндров

Два цилиндра Y1 и Y2, у каждого два концевых выключателя и один управляющий выход

Практикум: practices/08-fsm-control-pneumo

345 of 596

345

Практика: циклограмма пневмоцилиндров

Два цилиндра Y1 и Y2, у каждого два концевых выключателя и один управляющий выход

Состояния пронумерованы по шагам циклограммы; отдельно выделены начальное состояние и авария

Практикум: practices/08-fsm-control-pneumo

346 of 596

346

Практика: циклограмма пневмоцилиндров

Два цилиндра Y1 и Y2, у каждого два концевых выключателя и один управляющий выход

Состояния пронумерованы по шагам циклограммы; отдельно выделены начальное состояние и авария

У каждого состояния два времени: выдержка delay и таймаут timeout

Практикум: practices/08-fsm-control-pneumo

347 of 596

347

Практика: циклограмма пневмоцилиндров

Два цилиндра Y1 и Y2, у каждого два концевых выключателя и один управляющий выход

Состояния пронумерованы по шагам циклограммы; отдельно выделены начальное состояние и авария

У каждого состояния два времени: выдержка delay и таймаут timeout

Выдержка — сколько состояние должно длиться; таймаут — за какое время событие обязано наступить

Практикум: practices/08-fsm-control-pneumo

348 of 596

348

Практика: циклограмма пневмоцилиндров

Два цилиндра Y1 и Y2, у каждого два концевых выключателя и один управляющий выход

Состояния пронумерованы по шагам циклограммы; отдельно выделены начальное состояние и авария

У каждого состояния два времени: выдержка delay и таймаут timeout

Выдержка — сколько состояние должно длиться; таймаут — за какое время событие обязано наступить

Превышение таймаута означает, что цилиндр не дошёл до концевика: переход в PneumoState_FatalException

Практикум: practices/08-fsm-control-pneumo

349 of 596

349

Практика: циклограмма пневмоцилиндров

Два цилиндра Y1 и Y2, у каждого два концевых выключателя и один управляющий выход

Состояния пронумерованы по шагам циклограммы; отдельно выделены начальное состояние и авария

У каждого состояния два времени: выдержка delay и таймаут timeout

Выдержка — сколько состояние должно длиться; таймаут — за какое время событие обязано наступить

Превышение таймаута означает, что цилиндр не дошёл до концевика: переход в PneumoState_FatalException

Без явного таймаута автомат зависал бы в ожидании сигнала, которого не будет

Практикум: practices/08-fsm-control-pneumo

350 of 596

350

Практика: циклограмма пневмоцилиндров

Два цилиндра Y1 и Y2, у каждого два концевых выключателя и один управляющий выход

Состояния пронумерованы по шагам циклограммы; отдельно выделены начальное состояние и авария

У каждого состояния два времени: выдержка delay и таймаут timeout

Выдержка — сколько состояние должно длиться; таймаут — за какое время событие обязано наступить

Превышение таймаута означает, что цилиндр не дошёл до концевика: переход в PneumoState_FatalException

Без явного таймаута автомат зависал бы в ожидании сигнала, которого не будет

Поведение проверяется прогоном трека simulate.process: четыре входа и два ожидаемых выхода в строке

Практикум: practices/08-fsm-control-pneumo

351 of 596

351

Циклограмма: два пневмоцилиндра

Заливка — сигнал есть, пустая клетка — сигнала нет. Тринадцать тактов одного цикла

Y1.up

Y1.down

Y2.up

Y2.down

Y1 → шток

Y2 → шток

входы — датчики

выходы — команды

такт

Рисунок. Прогон practices/08-fsm-control-pneumo/simulate.process: четыре концевых датчика и две команды на штоки

Практикум: practices/08-fsm-control-pneumo

352 of 596

352

Что порождает кодогенератор SimInTech

Файл	Что содержит
PneumoAutomate.h	типы генератора, значения контактов по умолчанию, хеши схемы, таблицы имён переменных
PneumoAutomate.inc	тело шага: switch (action) с ветвями f_Stop, f_GetDeri, f_GetAlgFun
PneumoAutomate_init.inc	инициализация значениями по умолчанию и вызов пользовательской pneumo_engine_init
PneumoAutomate_state.inc	объявление переменных состояния схемы
default.list	список генерируемых подсхем

Две ловушки: в PneumoAutomate.h вшит абсолютный windows-путь, а файлы .inc и .log сохраняются в CP1251, а не UTF-8.

Автоматное программирование систем управления

353 of 596

353

Пример промышленного размера: загрузка сыпучих материалов

Одиннадцать состояний, восемь входов, семь выходов, выдержки времени и рецепт. Аварийное состояние не показано: в него ведут переходы из всех рабочих состояний, и одиннадцать одинаковых дуг ничего не объясняют

Практикум: practices/08-bulk-loading

354 of 596

354

Что находится на модели установки

Дефекты, найденные при переносе примера, полезнее самого примера

Автоматное программирование систем управления

355 of 596

355

Что находится на модели установки

Дефекты, найденные при переносе примера, полезнее самого примера

Команда «закрыть заслонку» была объявлена и не использована ни разу — заслонка закрывалась случайно

Автоматное программирование систем управления

356 of 596

356

Что находится на модели установки

Дефекты, найденные при переносе примера, полезнее самого примера

Команда «закрыть заслонку» была объявлена и не использована ни разу — заслонка закрывалась случайно

Счётчик малых циклов рос без ограничения, а бит рецепта читался по нему — чтение за границей массива

Автоматное программирование систем управления

357 of 596

357

Что находится на модели установки

Дефекты, найденные при переносе примера, полезнее самого примера

Команда «закрыть заслонку» была объявлена и не использована ни разу — заслонка закрывалась случайно

Счётчик малых циклов рос без ограничения, а бит рецепта читался по нему — чтение за границей массива

Результат открытия файла не проверялся — при отсутствии файла автомат молча зависал

Автоматное программирование систем управления

358 of 596

358

Что находится на модели установки

Дефекты, найденные при переносе примера, полезнее самого примера

Команда «закрыть заслонку» была объявлена и не использована ни разу — заслонка закрывалась случайно

Счётчик малых циклов рос без ограничения, а бит рецепта читался по нему — чтение за границей массива

Результат открытия файла не проверялся — при отсутствии файла автомат молча зависал

Главный дефект не виден в коде: между циклами контейнер обязан возвращаться в исходное положение

Автоматное программирование систем управления

359 of 596

359

Что находится на модели установки

Дефекты, найденные при переносе примера, полезнее самого примера

Команда «закрыть заслонку» была объявлена и не использована ни разу — заслонка закрывалась случайно

Счётчик малых циклов рос без ограничения, а бит рецепта читался по нему — чтение за границей массива

Результат открытия файла не проверялся — при отсутствии файла автомат молча зависал

Главный дефект не виден в коде: между циклами контейнер обязан возвращаться в исходное положение

Без возврата автомат гонит контейнер влево из позиции, которая уже левее цели, и упирается в упор

Автоматное программирование систем управления

360 of 596

360

Что находится на модели установки

Дефекты, найденные при переносе примера, полезнее самого примера

Команда «закрыть заслонку» была объявлена и не использована ни разу — заслонка закрывалась случайно

Счётчик малых циклов рос без ограничения, а бит рецепта читался по нему — чтение за границей массива

Результат открытия файла не проверялся — при отсутствии файла автомат молча зависал

Главный дефект не виден в коде: между циклами контейнер обязан возвращаться в исходное положение

Без возврата автомат гонит контейнер влево из позиции, которая уже левее цели, и упирается в упор

Каждая ветвь при этом выглядит правильно — неверна последовательность состояний, и только на некоторых рецептах

Автоматное программирование систем управления

361 of 596

ЛЕКЦИЯ

Верификация и тестирование автоматных программ

LTL, автоматы Бюхи, Promela и SPIN

362 of 596

362

Тестирование и верификация: в чём разница

Автоматное программирование систем управления

363 of 596

363

Тестирование и верификация: в чём разница

Тестирование проверяет поведение на конечном наборе входов

Автоматное программирование систем управления

364 of 596

364

Тестирование и верификация: в чём разница

Тестирование проверяет поведение на конечном наборе входов

Верификация доказывает свойство для всех возможных выполнений

Автоматное программирование систем управления

365 of 596

365

Тестирование и верификация: в чём разница

Тестирование проверяет поведение на конечном наборе входов

Верификация доказывает свойство для всех возможных выполнений

Первое находит ошибки, второе доказывает их отсутствие — в пределах модели и сформулированного свойства

Автоматное программирование систем управления

366 of 596

366

Тестирование и верификация: в чём разница

Тестирование проверяет поведение на конечном наборе входов

Верификация доказывает свойство для всех возможных выполнений

Первое находит ошибки, второе доказывает их отсутствие — в пределах модели и сформулированного свойства

Автоматные программы верифицируются проще произвольных потому, что у них есть явная модель

Автоматное программирование систем управления

367 of 596

367

Тестирование и верификация: в чём разница

Тестирование проверяет поведение на конечном наборе входов

Верификация доказывает свойство для всех возможных выполнений

Первое находит ошибки, второе доказывает их отсутствие — в пределах модели и сформулированного свойства

Автоматные программы верифицируются проще произвольных потому, что у них есть явная модель

Конечное множество состояний, известные переходы, известный набор воздействий — пространство можно обойти целиком

Автоматное программирование систем управления

368 of 596

368

Базовые операторы LTL

Оператор	Читается	Смысл
□ p	always p	p верно во всех состояниях выполнения
◇ p	eventually p	p когда-нибудь станет верно
p U q	p until q	p верно, пока не наступит q
○ p	next p	p верно в следующем состоянии

Безопасность: □ ¬(зелёный₁ ∧ зелёный₂). Живость: □ (нажата кнопка ⇒ ◇ лифт приехал). Логика предложена А. Пнуэли в 1977 году для рассуждений о поведении программ во времени.

Автоматное программирование систем управления

369 of 596

369

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автоматное программирование систем управления

370 of 596

370

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автомат Бюхи устроен как НКА, но читает бесконечные слова

Автоматное программирование систем управления

371 of 596

371

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автомат Бюхи устроен как НКА, но читает бесконечные слова

Слово принимается, если заключительные состояния встречаются бесконечно часто

Автоматное программирование систем управления

372 of 596

372

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автомат Бюхи устроен как НКА, но читает бесконечные слова

Слово принимается, если заключительные состояния встречаются бесконечно часто

Шаг 1: пространство состояний программы читается как автомат Бюхи A_M

Автоматное программирование систем управления

373 of 596

373

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автомат Бюхи устроен как НКА, но читает бесконечные слова

Слово принимается, если заключительные состояния встречаются бесконечно часто

Шаг 1: пространство состояний программы читается как автомат Бюхи A_M

Шаг 2: формула ¬φ переводится в автомат A_¬φ, принимающий нарушающие выполнения (в SPIN это never claim)

Автоматное программирование систем управления

374 of 596

374

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автомат Бюхи устроен как НКА, но читает бесконечные слова

Слово принимается, если заключительные состояния встречаются бесконечно часто

Шаг 1: пространство состояний программы читается как автомат Бюхи A_M

Шаг 2: формула ¬φ переводится в автомат A_¬φ, принимающий нарушающие выполнения (в SPIN это never claim)

Шаг 3: строится произведение A_M × A_¬φ

Автоматное программирование систем управления

375 of 596

375

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автомат Бюхи устроен как НКА, но читает бесконечные слова

Слово принимается, если заключительные состояния встречаются бесконечно часто

Шаг 1: пространство состояний программы читается как автомат Бюхи A_M

Шаг 2: формула ¬φ переводится в автомат A_¬φ, принимающий нарушающие выполнения (в SPIN это never claim)

Шаг 3: строится произведение A_M × A_¬φ

Шаг 4: проверка пустоты — поиск достижимого цикла с заключительным состоянием

Автоматное программирование систем управления

376 of 596

376

Как проверяется живость: автоматы Бюхи

Приём, которым живость сводится к достижимости

Автомат Бюхи устроен как НКА, но читает бесконечные слова

Слово принимается, если заключительные состояния встречаются бесконечно часто

Шаг 1: пространство состояний программы читается как автомат Бюхи A_M

Шаг 2: формула ¬φ переводится в автомат A_¬φ, принимающий нарушающие выполнения (в SPIN это never claim)

Шаг 3: строится произведение A_M × A_¬φ

Шаг 4: проверка пустоты — поиск достижимого цикла с заключительным состоянием

Пусто — свойство доказано; непусто — найденное слово и есть контрпример

Автоматное программирование систем управления

377 of 596

377

Автоматный подход: четыре шага

Приём Варди — Волпера: живость сводится к достижимости, а проверка свойства — к пустоте языка

Модель — автомат

пространство состояний программы читается как автомат Бюхи A_M: все её бесконечные выполнения

Отрицание — автомат

¬φ переводится в автомат Бюхи A_¬φ: ровно те выполнения, что нарушают свойство. В SPIN — spin -f, never claim

Пересечение

произведение A_M × A_¬φ: выполнения, которые одновременно возможны в модели и нарушают свойство

Проверка пустоты

пуст ли язык произведения. Формально — поиск достижимого цикла с заключительным состоянием

язык пуст

нарушающих выполнений нет,

свойство доказано

язык непуст

найденное слово — контрпример,

SPIN печатает его трассой

Проверка пустоты для автомата Бюхи — поиск цикла, достижимого из начального состояния и содержащего заключительное: «плохое поведение повторяется бесконечно». Обход в глубину, линейное время.

Лекция 9 · § «Как это проверяется: автоматы Бюхи»

378 of 596

378

Взрыв пространства состояний

У k процессов по n состояний — nᵏ глобальных состояний, и это до учёта данных

Автоматное программирование систем управления

379 of 596

379

Взрыв пространства состояний

У k процессов по n состояний — nᵏ глобальных состояний, и это до учёта данных

Редукция частичных порядков: независимые переходы можно рассмотреть в одном порядке из двух

Автоматное программирование систем управления

380 of 596

380

Взрыв пространства состояний

У k процессов по n состояний — nᵏ глобальных состояний, и это до учёта данных

Редукция частичных порядков: независимые переходы можно рассмотреть в одном порядке из двух

Символьная проверка: множества состояний представляются формулой (BDD, SAT, SMT), а не списком

Автоматное программирование систем управления

381 of 596

381

Взрыв пространства состояний

У k процессов по n состояний — nᵏ глобальных состояний, и это до учёта данных

Редукция частичных порядков: независимые переходы можно рассмотреть в одном порядке из двух

Символьная проверка: множества состояний представляются формулой (BDD, SAT, SMT), а не списком

Абстракция: счётчик заменяется признаком «ноль / не ноль»; ложные контрпримеры отсеиваются уточнением

Автоматное программирование систем управления

382 of 596

382

Взрыв пространства состояний

У k процессов по n состояний — nᵏ глобальных состояний, и это до учёта данных

Редукция частичных порядков: независимые переходы можно рассмотреть в одном порядке из двух

Символьная проверка: множества состояний представляются формулой (BDD, SAT, SMT), а не списком

Абстракция: счётчик заменяется признаком «ноль / не ноль»; ложные контрпримеры отсеиваются уточнением

Ограничение глубины: проверка выполнений длины не больше k — не доказывает, но быстро находит короткие контрпримеры

Автоматное программирование систем управления

383 of 596

383

Взрыв пространства состояний

У k процессов по n состояний — nᵏ глобальных состояний, и это до учёта данных

Редукция частичных порядков: независимые переходы можно рассмотреть в одном порядке из двух

Символьная проверка: множества состояний представляются формулой (BDD, SAT, SMT), а не списком

Абстракция: счётчик заменяется признаком «ноль / не ноль»; ложные контрпримеры отсеиваются уточнением

Хеширование состояний: память экономится радикально, но проверка перестаёт быть полной

Автоматное программирование систем управления

384 of 596

384

Взрыв пространства состояний

У k процессов по n состояний — nᵏ глобальных состояний, и это до учёта данных

Редукция частичных порядков: независимые переходы можно рассмотреть в одном порядке из двух

Символьная проверка: множества состояний представляются формулой (BDD, SAT, SMT), а не списком

Абстракция: счётчик заменяется признаком «ноль / не ноль»; ложные контрпримеры отсеиваются уточнением

Хеширование состояний: память экономится радикально, но проверка перестаёт быть полной

Управляющий автомат сам по себе мал; взрыв начинается там, где к нему добавляются данные

Автоматное программирование систем управления

385 of 596

385

Promela и SPIN: порядок работы

spin -a model.pml # породить верификатор pan.c

gcc -DSAFETY -o pan pan.c # только безопасность: assert и дедлоки

./pan # прогнать проверку

spin -t -p model.pml # воспроизвести контрпример

spin -a model.pml && cc -o pan pan.c

./pan -a -f -N safety # -a: искать циклы, -f: слабая справедливость

Модель с LTL-свойствами собирается без -DSAFETY и проверяется по одному свойству за запуск. Граф пространства состояний: ./pan -D > pan.dot && dot -Tpng pan.dot > pan.png

Практикум: practices/09-promela

386 of 596

386

Порядок работы со SPIN

Четыре шага от модели до контрпримера; каждый — одна команда

model.pml

модель на Promela

spin -a

model.pml

pan.c

исходник верификатора

cc -o pan

pan.c

./pan

полный обход состояний

./pan -a -f

-N liveness

трасса

контрпример по шагам

errors: 0

свойство доказано

Ключ -DSAFETY отключает поиск циклов и годится только для свойств безопасности — assert и дедлоков. Модель с LTL-свойствами собирается без него и проверяется по одному свойству за запуск.

граф пространства состояний: ./pan -D > pan.dot → dot -Tpng pan.dot > pan.png

Лекция 9 · § «Порядок работы» · practices/09-promela

387 of 596

387

Светофор из лекции 2: роль предположения о справедливости

Запуск	Итог	Что означает
./pan -a -N safety	0 ошибок	зелёный машинам и переход пешеходов не совмещаются ни на одном выполнении
./pan -a -N liveness	1 ошибка	есть выполнение, где контроллер не получает управления никогда
./pan -a -f -N liveness	0 ошибок	при слабой справедливости заявка обслуживается всегда

Отрицательный ответ верификатора — утверждение о модели И о предположениях, при которых её рассматривают. Прежде чем чинить программу, стоит понять, не о постановке ли вопроса говорит контрпример.

Автоматное программирование систем управления

388 of 596

388

Откуда берётся модель

Три способа, дающие разные гарантии

Автоматное программирование систем управления

389 of 596

389

Откуда берётся модель

Три способа, дающие разные гарантии

Модель пишется руками: быстро, но связь с кодом держится только дисциплиной автора

Автоматное программирование систем управления

390 of 596

390

Откуда берётся модель

Три способа, дающие разные гарантии

Модель пишется руками: быстро, но связь с кодом держится только дисциплиной автора

Программу поправили — модель устарела молча

Автоматное программирование систем управления

391 of 596

391

Откуда берётся модель

Три способа, дающие разные гарантии

Модель пишется руками: быстро, но связь с кодом держится только дисциплиной автора

Программу поправили — модель устарела молча

Модель порождается из кода: транслятор читает автоматное описание и печатает Promela

Автоматное программирование систем управления

392 of 596

392

Откуда берётся модель

Три способа, дающие разные гарантии

Модель пишется руками: быстро, но связь с кодом держится только дисциплиной автора

Программу поправили — модель устарела молча

Модель порождается из кода: транслятор читает автоматное описание и печатает Promela

Так сделано в сквозном проекте курса: 20-welding-line --promela; связь автоматическая

Автоматное программирование систем управления

393 of 596

393

Откуда берётся модель

Три способа, дающие разные гарантии

Модель пишется руками: быстро, но связь с кодом держится только дисциплиной автора

Программу поправили — модель устарела молча

Модель порождается из кода: транслятор читает автоматное описание и печатает Promela

Так сделано в сквозном проекте курса: 20-welding-line --promela; связь автоматическая

Модель и код порождаются из общего описания — путь UniMod и Takt (лекция 12)

Автоматное программирование систем управления

394 of 596

394

Откуда берётся модель

Три способа, дающие разные гарантии

Модель пишется руками: быстро, но связь с кодом держится только дисциплиной автора

Программу поправили — модель устарела молча

Модель порождается из кода: транслятор читает автоматное описание и печатает Promela

Так сделано в сквозном проекте курса: 20-welding-line --promela; связь автоматическая

Модель и код порождаются из общего описания — путь UniMod и Takt (лекция 12)

В последнем случае расхождение исключено по построению: и то и другое — проекции одного источника

Автоматное программирование систем управления

395 of 596

395

Что теряется при переводе программы в Promela

В программе	В модели	Следствие
условия на данные (x > 128)	недетерминированный выбор ветви	проверяются все ветви, в том числе недостижимые
арифметика и счётчики	выбрасываются или огрубляются	свойства вида «счётчик не переполнится» не проверяются
время, выдержки, таймауты	обычное событие без длительности	«не короче T_min» на такой модели не выражается
работа с памятью, указатели	нет вовсе	утечки ловятся санитайзерами, а не здесь
взаимодействие с железом	входные события выбираются свободно	модель проверяет автомат, а не установку

«Верификатор ошибок не нашёл» означает: в модели, при принятых предположениях, записанное формулой свойство выполняется. Все три оговорки существенны.

Автоматное программирование систем управления

396 of 596

ЛЕКЦИЯ

Границы модели. Машина Тьюринга и вычислимость

Что за границей автомата и где кончается сама машина

397 of 596

397

Машина Тьюринга

Практикум: practices/10-turing-machine

398 of 596

398

Машина Тьюринга

Лента бесконечна влево и вправо и разбита на клетки; в каждой — символ конечного ленточного алфавита

Практикум: practices/10-turing-machine

399 of 596

399

Машина Тьюринга

Лента бесконечна влево и вправо и разбита на клетки; в каждой — символ конечного ленточного алфавита

Головка двигается влево и вправо, читает символ и записывает любой символ алфавита

Практикум: practices/10-turing-machine

400 of 596

400

Машина Тьюринга

Лента бесконечна влево и вправо и разбита на клетки; в каждой — символ конечного ленточного алфавита

Головка двигается влево и вправо, читает символ и записывает любой символ алфавита

Управляющее устройство находится в одном из конечного числа состояний

Практикум: practices/10-turing-machine

401 of 596

401

Машина Тьюринга

Лента бесконечна влево и вправо и разбита на клетки; в каждой — символ конечного ленточного алфавита

Головка двигается влево и вправо, читает символ и записывает любой символ алфавита

Управляющее устройство находится в одном из конечного числа состояний

Выделены начальное состояние и заключительное

Практикум: practices/10-turing-machine

402 of 596

402

Машина Тьюринга

Лента бесконечна влево и вправо и разбита на клетки; в каждой — символ конечного ленточного алфавита

Головка двигается влево и вправо, читает символ и записывает любой символ алфавита

Управляющее устройство находится в одном из конечного числа состояний

Выделены начальное состояние и заключительное

Программа — конечная таблица команд вида aᵢqⱼ → a_r M q_s

Практикум: practices/10-turing-machine

403 of 596

403

Машина Тьюринга

Лента бесконечна влево и вправо и разбита на клетки; в каждой — символ конечного ленточного алфавита

Головка двигается влево и вправо, читает символ и записывает любой символ алфавита

Управляющее устройство находится в одном из конечного числа состояний

Выделены начальное состояние и заключительное

Программа — конечная таблица команд вида aᵢqⱼ → a_r M q_s

Управляющее устройство машины Тьюринга действительно является конечным автоматом

Практикум: practices/10-turing-machine

404 of 596

404

Машина Тьюринга

Лента бесконечна влево и вправо и разбита на клетки; в каждой — символ конечного ленточного алфавита

Головка двигается влево и вправо, читает символ и записывает любой символ алфавита

Управляющее устройство находится в одном из конечного числа состояний

Выделены начальное состояние и заключительное

Программа — конечная таблица команд вида aᵢqⱼ → a_r M q_s

Управляющее устройство машины Тьюринга действительно является конечным автоматом

Но сама машина Тьюринга конечным автоматом не является

Практикум: practices/10-turing-machine

405 of 596

машина Тьюринга =

конечное управление + неограниченная лента с записью

Ровно лента отделяет одну модель от другой

406 of 596

406

Абстрактная вычислительная машина

Управляющее устройство — конечный автомат; универсальным вычислителем машину делает лента

…

a₁

a₀

a₁

a₀

a₁

a₀

…

лента бесконечна влево и вправо; в клетке — символ алфавита A = {a₀, a₁, …, a_k}, a₀ пустой

головка

читает символ и пишет любой символ из A

сдвиг на клетку: L, R или S

управляющее устройство

конечное число состояний q₀, q₁, …, q_m

это и есть конечный автомат

МТ = конечное управление + неограниченная лента с записью

Лекция 10 · § «Определение»

407 of 596

407

Машина Поста рядом с машиной Тьюринга

Пост опубликовал свою машину в 1936 году независимо от Тьюринга; модели алгоритмически эквивалентны

Машина Тьюринга

лента, головка, состояния

a₁

a₀

a₁

a₀

головка

— алфавит A из k+1 символов

— состояния q₀ … q_m

— команда a_i q_j → a_r M q_s

— любая команда применима всегда

Машина Поста

та же лента, каретка вместо головки

●

каретка

— клетка: пусто или метка

— номер строки вместо состояния

— шесть команд: V, X, ←, →, ?, !

— команда может быть невыполнимой

Убрано: алфавит и состояния. Осталось: бесконечная лента, каретка, конечная программа — и та же вычислительная сила

Лекция 10 · § «Машина Поста»

408 of 596

408

Иерархия Хомского

Тип	Модель вычислений	Класс языков	Пример языка
3	конечный автомат	регулярные	слова с чётным числом a
2	автомат с магазинной памятью	контекстно-свободные	aⁿbⁿ, скобочные последовательности
1	линейно ограниченный автомат	контекстно-зависимые	aⁿbⁿcⁿ
0	машина Тьюринга	перечислимые	проблема останова

Каждая следующая строка распознаёт строго больше языков, чем предыдущая.

Автоматное программирование систем управления

409 of 596

409

Иерархия Хомского

Вложение классов языков: что распознаёт модель, распознают и все внешние классы

тип 0 — перечислимые машина Тьюринга · проблема останова

тип 1 — контекстно-зависимые линейно ограниченный автомат · aⁿbⁿcⁿ

тип 2 — контекстно-свободные магазинный автомат · aⁿbⁿ, скобочные последовательности

тип 3 — регулярные конечный автомат · слова с чётным числом a

каждое множество строго шире вложенного: мощнее модель — больше класс языков

Рисунок. Модель вычислений, класс языков и пример языка в каждом кольце

Лекция 10 · таблица «Иерархия Хомского»

410 of 596

410

Между автоматом и машиной: магазинная память

Автоматное программирование систем управления

411 of 596

411

Между автоматом и машиной: магазинная память

Конечному автомату не хватает памяти сосчитать буквы a; машине Тьюринга её хватает с избытком

Автоматное программирование систем управления

412 of 596

412

Между автоматом и машиной: магазинная память

Конечному автомату не хватает памяти сосчитать буквы a; машине Тьюринга её хватает с избытком

Но задача не требует такой свободы: достаточно складывать прочитанное и снимать последнее положенное

Автоматное программирование систем управления

413 of 596

413

Между автоматом и машиной: магазинная память

Конечному автомату не хватает памяти сосчитать буквы a; машине Тьюринга её хватает с избытком

Но задача не требует такой свободы: достаточно складывать прочитанное и снимать последнее положенное

МП-автомат — семёрка P = (Q, Σ, Γ, δ, q₀, Z₀, F) с магазином

Автоматное программирование систем управления

414 of 596

414

Между автоматом и машиной: магазинная память

Конечному автомату не хватает памяти сосчитать буквы a; машине Тьюринга её хватает с избытком

Но задача не требует такой свободы: достаточно складывать прочитанное и снимать последнее положенное

МП-автомат — семёрка P = (Q, Σ, Γ, δ, q₀, Z₀, F) с магазином

За такт автомат обязан посмотреть на вершину магазина и заменить её: снять, оставить или положить

Автоматное программирование систем управления

415 of 596

415

Между автоматом и машиной: магазинная память

Конечному автомату не хватает памяти сосчитать буквы a; машине Тьюринга её хватает с избытком

Но задача не требует такой свободы: достаточно складывать прочитанное и снимать последнее положенное

МП-автомат — семёрка P = (Q, Σ, Γ, δ, q₀, Z₀, F) с магазином

За такт автомат обязан посмотреть на вершину магазина и заменить её: снять, оставить или положить

Для aⁿbⁿ: каждая буква a кладёт символ A, каждая b его снимает; слово принято, если магазин пуст

Автоматное программирование систем управления

416 of 596

416

Между автоматом и машиной: магазинная память

Конечному автомату не хватает памяти сосчитать буквы a; машине Тьюринга её хватает с избытком

Но задача не требует такой свободы: достаточно складывать прочитанное и снимать последнее положенное

МП-автомат — семёрка P = (Q, Σ, Γ, δ, q₀, Z₀, F) с магазином

За такт автомат обязан посмотреть на вершину магазина и заменить её: снять, оставить или положить

Для aⁿbⁿ: каждая буква a кладёт символ A, каждая b его снимает; слово принято, если магазин пуст

Автомат не хранит число n — он хранит его высотой стопки, и это вся разница с конечным

Автоматное программирование систем управления

417 of 596

417

Между автоматом и машиной: магазинная память

Конечному автомату не хватает памяти сосчитать буквы a; машине Тьюринга её хватает с избытком

Но задача не требует такой свободы: достаточно складывать прочитанное и снимать последнее положенное

МП-автомат — семёрка P = (Q, Σ, Γ, δ, q₀, Z₀, F) с магазином

За такт автомат обязан посмотреть на вершину магазина и заменить её: снять, оставить или положить

Для aⁿbⁿ: каждая буква a кладёт символ A, каждая b его снимает; слово принято, если магазин пуст

Автомат не хранит число n — он хранит его высотой стопки, и это вся разница с конечным

У МП-автоматов недетерминизм не бесплатен: недетерминированные распознают строго больше

Автоматное программирование систем управления

418 of 596

418

Что распознаёт каждая модель

Язык	КА	МП-автомат	МТ
слова с чётным числом a	да	да	да
aⁿbⁿ	нет	да	да
скобочные последовательности	нет	да	да
aⁿbⁿcⁿ	нет	нет	да
ww (слово, повторённое дважды)	нет	нет	да
проблема останова	нет	нет	перечислима, но не разрешима

Практический вывод: если в управляющей задаче появляется вложенность — вложенные режимы, скобочная структура протокола, стек возвратов, — плоского автомата не хватит по существу, а не по недосмотру.

Автоматное программирование систем управления

419 of 596

419

Нумерация машин и универсальная машина

Автоматное программирование систем управления

420 of 596

420

Нумерация машин и универсальная машина

Программа машины — конечная таблица команд, а значит её можно записать словом: код машины ⟨M⟩

Автоматное программирование систем управления

421 of 596

421

Нумерация машин и универсальная машина

Программа машины — конечная таблица команд, а значит её можно записать словом: код машины ⟨M⟩

Упорядочив все такие слова, получаем нумерацию M₀, M₁, M₂, … — гёделев номер машины

Автоматное программирование систем управления

422 of 596

422

Нумерация машин и универсальная машина

Программа машины — конечная таблица команд, а значит её можно записать словом: код машины ⟨M⟩

Упорядочив все такие слова, получаем нумерацию M₀, M₁, M₂, … — гёделев номер машины

Машин счётное число, а функций ℕ → ℕ несчётно много: почти все функции невычислимы

Автоматное программирование систем управления

423 of 596

423

Нумерация машин и универсальная машина

Программа машины — конечная таблица команд, а значит её можно записать словом: код машины ⟨M⟩

Упорядочив все такие слова, получаем нумерацию M₀, M₁, M₂, … — гёделев номер машины

Машин счётное число, а функций ℕ → ℕ несчётно много: почти все функции невычислимы

Код машины — это данные: машине можно подать на вход описание машины, в том числе её собственное

Автоматное программирование систем управления

424 of 596

424

Нумерация машин и универсальная машина

Программа машины — конечная таблица команд, а значит её можно записать словом: код машины ⟨M⟩

Упорядочив все такие слова, получаем нумерацию M₀, M₁, M₂, … — гёделев номер машины

Машин счётное число, а функций ℕ → ℕ несчётно много: почти все функции невычислимы

Код машины — это данные: машине можно подать на вход описание машины, в том числе её собственное

Существует машина U, которая по паре (⟨M⟩, w) работает ровно так же, как M на слове w

Автоматное программирование систем управления

425 of 596

425

Нумерация машин и универсальная машина

Программа машины — конечная таблица команд, а значит её можно записать словом: код машины ⟨M⟩

Упорядочив все такие слова, получаем нумерацию M₀, M₁, M₂, … — гёделев номер машины

Машин счётное число, а функций ℕ → ℕ несчётно много: почти все функции невычислимы

Код машины — это данные: машине можно подать на вход описание машины, в том числе её собственное

Существует машина U, которая по паре (⟨M⟩, w) работает ровно так же, как M на слове w

Универсальная машина — первое описание того, что сегодня называют процессором

Автоматное программирование систем управления

426 of 596

426

Неразрешимость: останов и теорема Райса

Автоматное программирование систем управления

427 of 596

427

Неразрешимость: останов и теорема Райса

Проблема останова: по описанию алгоритма и входу определить, завершится ли выполнение

Автоматное программирование систем управления

428 of 596

428

Неразрешимость: останов и теорема Райса

Проблема останова: по описанию алгоритма и входу определить, завершится ли выполнение

Тьюринг, 1936: такой функции не существует — доказательство диагональное, через самоприменение

Автоматное программирование систем управления

429 of 596

429

Неразрешимость: останов и теорема Райса

Проблема останова: по описанию алгоритма и входу определить, завершится ли выполнение

Тьюринг, 1936: такой функции не существует — доказательство диагональное, через самоприменение

Теорема Райса, 1953: всякое нетривиальное свойство вычислимых функций неразрешимо

Автоматное программирование систем управления

430 of 596

430

Неразрешимость: останов и теорема Райса

Проблема останова: по описанию алгоритма и входу определить, завершится ли выполнение

Тьюринг, 1936: такой функции не существует — доказательство диагональное, через самоприменение

Теорема Райса, 1953: всякое нетривиальное свойство вычислимых функций неразрешимо

Неразрешимы вопросы «печатает ли программа хоть что-нибудь», «эквивалентны ли две программы»

Автоматное программирование систем управления

431 of 596

431

Неразрешимость: останов и теорема Райса

Проблема останова: по описанию алгоритма и входу определить, завершится ли выполнение

Тьюринг, 1936: такой функции не существует — доказательство диагональное, через самоприменение

Теорема Райса, 1953: всякое нетривиальное свойство вычислимых функций неразрешимо

Неразрешимы вопросы «печатает ли программа хоть что-нибудь», «эквивалентны ли две программы»

Разрешимы вопросы о тексте: сколько строк, есть ли goto — это свойства записи, а не функции

Автоматное программирование систем управления

432 of 596

432

Неразрешимость: останов и теорема Райса

Проблема останова: по описанию алгоритма и входу определить, завершится ли выполнение

Тьюринг, 1936: такой функции не существует — доказательство диагональное, через самоприменение

Теорема Райса, 1953: всякое нетривиальное свойство вычислимых функций неразрешимо

Неразрешимы вопросы «печатает ли программа хоть что-нибудь», «эквивалентны ли две программы»

Разрешимы вопросы о тексте: сколько строк, есть ли goto — это свойства записи, а не функции

Отсюда три законных выхода анализатора: отвечать «не знаю», отвечать с одной стороны, сузить язык

Автоматное программирование систем управления

433 of 596

433

Невычислимые функции и колмогоровская сложность

Автоматное программирование систем управления

434 of 596

434

Невычислимые функции и колмогоровская сложность

Бесконечный процесс и невычислимая функция — не одно и то же

Автоматное программирование систем управления

435 of 596

435

Невычислимые функции и колмогоровская сложность

Бесконечный процесс и невычислимая функция — не одно и то же

Снежинка Коха строится бесконечно, но каждый её конечный шаг вычисляется тривиально

Автоматное программирование систем управления

436 of 596

436

Невычислимые функции и колмогоровская сложность

Бесконечный процесс и невычислимая функция — не одно и то же

Снежинка Коха строится бесконечно, но каждый её конечный шаг вычисляется тривиально

Busy beaver BB(n) — наибольшее число тактов машины с n состояниями на пустой ленте

Автоматное программирование систем управления

437 of 596

437

Невычислимые функции и колмогоровская сложность

Бесконечный процесс и невычислимая функция — не одно и то же

Снежинка Коха строится бесконечно, но каждый её конечный шаг вычисляется тривиально

Busy beaver BB(n) — наибольшее число тактов машины с n состояниями на пустой ленте

BB определена для каждого n, но растёт быстрее любой вычислимой функции: BB(5) = 4098, доказано в 2024 году

Автоматное программирование систем управления

438 of 596

438

Невычислимые функции и колмогоровская сложность

Бесконечный процесс и невычислимая функция — не одно и то же

Снежинка Коха строится бесконечно, но каждый её конечный шаг вычисляется тривиально

Busy beaver BB(n) — наибольшее число тактов машины с n состояниями на пустой ленте

BB определена для каждого n, но растёт быстрее любой вычислимой функции: BB(5) = 4098, доказано в 2024 году

Колмогоровская сложность K(x) — длина кратчайшей программы, печатающей x

Автоматное программирование систем управления

439 of 596

439

Невычислимые функции и колмогоровская сложность

Бесконечный процесс и невычислимая функция — не одно и то же

Снежинка Коха строится бесконечно, но каждый её конечный шаг вычисляется тривиально

Busy beaver BB(n) — наибольшее число тактов машины с n состояниями на пустой ленте

BB определена для каждого n, но растёт быстрее любой вычислимой функции: BB(5) = 4098, доказано в 2024 году

Колмогоровская сложность K(x) — длина кратчайшей программы, печатающей x

Строка из миллиона нулей описывается фразой «миллион нулей»; у случайной строки короткого описания нет

Автоматное программирование систем управления

440 of 596

440

Невычислимые функции и колмогоровская сложность

Бесконечный процесс и невычислимая функция — не одно и то же

Снежинка Коха строится бесконечно, но каждый её конечный шаг вычисляется тривиально

Busy beaver BB(n) — наибольшее число тактов машины с n состояниями на пустой ленте

BB определена для каждого n, но растёт быстрее любой вычислимой функции: BB(5) = 4098, доказано в 2024 году

Колмогоровская сложность K(x) — длина кратчайшей программы, печатающей x

Строка из миллиона нулей описывается фразой «миллион нулей»; у случайной строки короткого описания нет

K невычислима — доказательство через парадокс Берри: «наименьшее число, не описываемое короче»

Автоматное программирование систем управления

441 of 596

441

Бесконечный процесс — это ещё не невычислимость

Снежинка Коха не заканчивается никогда, но каждый её конечный шаг считается тривиально. Настоящие невычислимые функции определены на всех входах и принимают конечные значения — их просто не вычисляет никакой алгоритм

Автоматное программирование систем управления

442 of 596

442

Перебор, криптография и алгоритм Шора

Автоматное программирование систем управления

443 of 596

443

Перебор, криптография и алгоритм Шора

P против NP: совпадают ли задачи, решаемые быстро, и задачи, у которых быстро проверяется ответ

Автоматное программирование систем управления

444 of 596

444

Перебор, криптография и алгоритм Шора

P против NP: совпадают ли задачи, решаемые быстро, и задачи, у которых быстро проверяется ответ

Разложение на множители и дискретное логарифмирование — разные задачи, и их часто смешивают

Автоматное программирование систем управления

445 of 596

445

Перебор, криптография и алгоритм Шора

P против NP: совпадают ли задачи, решаемые быстро, и задачи, у которых быстро проверяется ответ

Разложение на множители и дискретное логарифмирование — разные задачи, и их часто смешивают

На первой основана RSA, на второй — протокол Диффи — Хеллмана

Автоматное программирование систем управления

446 of 596

446

Перебор, криптография и алгоритм Шора

P против NP: совпадают ли задачи, решаемые быстро, и задачи, у которых быстро проверяется ответ

Разложение на множители и дискретное логарифмирование — разные задачи, и их часто смешивают

На первой основана RSA, на второй — протокол Диффи — Хеллмана

Алгоритм Шора сводит разложение к поиску периода функции aˣ mod n; период находит квантовое преобразование Фурье

Автоматное программирование систем управления

447 of 596

447

Перебор, криптография и алгоритм Шора

P против NP: совпадают ли задачи, решаемые быстро, и задачи, у которых быстро проверяется ответ

Разложение на множители и дискретное логарифмирование — разные задачи, и их часто смешивают

На первой основана RSA, на второй — протокол Диффи — Хеллмана

Тезис Чёрча — Тьюринга не затронут: квантовый компьютер не вычисляет ничего невычислимого

Автоматное программирование систем управления

448 of 596

448

Перебор, криптография и алгоритм Шора

P против NP: совпадают ли задачи, решаемые быстро, и задачи, у которых быстро проверяется ответ

Разложение на множители и дискретное логарифмирование — разные задачи, и их часто смешивают

На первой основана RSA, на второй — протокол Диффи — Хеллмана

Тезис Чёрча — Тьюринга не затронут: квантовый компьютер не вычисляет ничего невычислимого

Под ударом расширенный тезис — «физическое устройство не даёт полиномиального выигрыша»

Автоматное программирование систем управления

449 of 596

449

Перебор, криптография и алгоритм Шора

P против NP: совпадают ли задачи, решаемые быстро, и задачи, у которых быстро проверяется ответ

Разложение на множители и дискретное логарифмирование — разные задачи, и их часто смешивают

На первой основана RSA, на второй — протокол Диффи — Хеллмана

Тезис Чёрча — Тьюринга не затронут: квантовый компьютер не вычисляет ничего невычислимого

Под ударом расширенный тезис — «физическое устройство не даёт полиномиального выигрыша»

Вывод инженеру: не «криптография сломана», а «сроки известны» — отсюда переход на постквантовые схемы

Автоматное программирование систем управления

450 of 596

450

Языки, у которых полноты нет намеренно

Если завершение нужно гарантировать, у языка следует отнять полноту

Автоматное программирование систем управления

451 of 596

451

Языки, у которых полноты нет намеренно

Если завершение нужно гарантировать, у языка следует отнять полноту

Цикл ПЛК: тело фиксированного цикла, а превышение времени — авария по watchdog, а не ожидание

Автоматное программирование систем управления

452 of 596

452

Языки, у которых полноты нет намеренно

Если завершение нужно гарантировать, у языка следует отнять полноту

Цикл ПЛК: тело фиксированного цикла, а превышение времени — авария по watchdog, а не ожидание

eBPF в ядре Linux: циклы либо запрещены, либо обязаны иметь доказуемую границу

Автоматное программирование систем управления

453 of 596

453

Языки, у которых полноты нет намеренно

Если завершение нужно гарантировать, у языка следует отнять полноту

Цикл ПЛК: тело фиксированного цикла, а превышение времени — авария по watchdog, а не ожидание

eBPF в ядре Linux: циклы либо запрещены, либо обязаны иметь доказуемую границу

Языки конфигурации — Dhall, Starlark — намеренно лишены неограниченной рекурсии

Автоматное программирование систем управления

454 of 596

454

Языки, у которых полноты нет намеренно

Если завершение нужно гарантировать, у языка следует отнять полноту

Цикл ПЛК: тело фиксированного цикла, а превышение времени — авария по watchdog, а не ожидание

eBPF в ядре Linux: циклы либо запрещены, либо обязаны иметь доказуемую границу

Языки конфигурации — Dhall, Starlark — намеренно лишены неограниченной рекурсии

Языки описания автоматов: Takt и генераторы лекции 8 описывают такт, который по построению конечен

Автоматное программирование систем управления

455 of 596

455

Языки, у которых полноты нет намеренно

Если завершение нужно гарантировать, у языка следует отнять полноту

Цикл ПЛК: тело фиксированного цикла, а превышение времени — авария по watchdog, а не ожидание

eBPF в ядре Linux: циклы либо запрещены, либо обязаны иметь доказуемую границу

Языки конфигурации — Dhall, Starlark — намеренно лишены неограниченной рекурсии

Языки описания автоматов: Takt и генераторы лекции 8 описывают такт, который по построению конечен

Конечный автомат — модель, у которой нет полноты по Тьюрингу, и в первых лекциях это выглядело ограничением

Автоматное программирование систем управления

456 of 596

456

Языки, у которых полноты нет намеренно

Если завершение нужно гарантировать, у языка следует отнять полноту

Цикл ПЛК: тело фиксированного цикла, а превышение времени — авария по watchdog, а не ожидание

eBPF в ядре Linux: циклы либо запрещены, либо обязаны иметь доказуемую границу

Языки конфигурации — Dhall, Starlark — намеренно лишены неограниченной рекурсии

Языки описания автоматов: Takt и генераторы лекции 8 описывают такт, который по построению конечен

Конечный автомат — модель, у которой нет полноты по Тьюрингу, и в первых лекциях это выглядело ограничением

В управляющих системах то же свойство оказывается требованием: ограниченность модели и есть то, за что её выбирают

Автоматное программирование систем управления

457 of 596

ЛЕКЦИЯ

Клеточные автоматы и самовоспроизведение

Вольфрам, «Жизнь», муравей Лэнгтона

458 of 596

458

Понятие клеточного автомата

Практикум: practices/11-cells

459 of 596

459

Понятие клеточного автомата

Клеточный автомат — четвёрка σ = (Zᵏ, Eₙ, V, φ)

Практикум: practices/11-cells

460 of 596

460

Понятие клеточного автомата

Клеточный автомат — четвёрка σ = (Zᵏ, Eₙ, V, φ)

Zᵏ — ячейки, Eₙ = {0, …, n−1} — состояния ячейки, V — шаблон соседства, φ — локальная функция переходов

Практикум: practices/11-cells

461 of 596

461

Понятие клеточного автомата

Клеточный автомат — четвёрка σ = (Zᵏ, Eₙ, V, φ)

Zᵏ — ячейки, Eₙ = {0, …, n−1} — состояния ячейки, V — шаблон соседства, φ — локальная функция переходов

Состояние автомата — функция, сопоставляющая каждой ячейке её состояние

Практикум: practices/11-cells

462 of 596

462

Понятие клеточного автомата

Клеточный автомат — четвёрка σ = (Zᵏ, Eₙ, V, φ)

Zᵏ — ячейки, Eₙ = {0, …, n−1} — состояния ячейки, V — шаблон соседства, φ — локальная функция переходов

Состояние автомата — функция, сопоставляющая каждой ячейке её состояние

Глобальная функция переходов Φ применяет φ ко всем ячейкам одновременно

Практикум: practices/11-cells

463 of 596

463

Понятие клеточного автомата

Клеточный автомат — четвёрка σ = (Zᵏ, Eₙ, V, φ)

Zᵏ — ячейки, Eₙ = {0, …, n−1} — состояния ячейки, V — шаблон соседства, φ — локальная функция переходов

Состояние автомата — функция, сопоставляющая каждой ячейке её состояние

Глобальная функция переходов Φ применяет φ ко всем ячейкам одновременно

Конфигурация — состояние, у которого лишь конечное число ячеек отлично от нуля

Практикум: practices/11-cells

464 of 596

464

Понятие клеточного автомата

Клеточный автомат — четвёрка σ = (Zᵏ, Eₙ, V, φ)

Zᵏ — ячейки, Eₙ = {0, …, n−1} — состояния ячейки, V — шаблон соседства, φ — локальная функция переходов

Состояние автомата — функция, сопоставляющая каждой ячейке её состояние

Глобальная функция переходов Φ применяет φ ко всем ячейкам одновременно

Конфигурация — состояние, у которого лишь конечное число ячеек отлично от нуля

Автомат однороден: правило одно и то же для всех ячеек, и оно локально

Практикум: practices/11-cells

465 of 596

465

Понятие клеточного автомата

Клеточный автомат — четвёрка σ = (Zᵏ, Eₙ, V, φ)

Zᵏ — ячейки, Eₙ = {0, …, n−1} — состояния ячейки, V — шаблон соседства, φ — локальная функция переходов

Состояние автомата — функция, сопоставляющая каждой ячейке её состояние

Глобальная функция переходов Φ применяет φ ко всем ячейкам одновременно

Конфигурация — состояние, у которого лишь конечное число ячеек отлично от нуля

Автомат однороден: правило одно и то же для всех ячеек, и оно локально

Окрестность фон Неймана — клетка и четыре соседа по стороне; окрестность Мура — восемь соседей

Практикум: practices/11-cells

466 of 596

466

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Автоматное программирование систем управления

467 of 596

467

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Локальная функция задаётся значением на восьми возможных окрестностях

Автоматное программирование систем управления

468 of 596

468

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Локальная функция задаётся значением на восьми возможных окрестностях

Восемь битов дают число от 0 до 255 — это и есть номер правила по Вольфраму

Автоматное программирование систем управления

469 of 596

469

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Локальная функция задаётся значением на восьми возможных окрестностях

Восемь битов дают число от 0 до 255 — это и есть номер правила по Вольфраму

Класс I: всё приходит к однородному состоянию (правила 0, 32, 255)

Автоматное программирование систем управления

470 of 596

470

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Локальная функция задаётся значением на восьми возможных окрестностях

Восемь битов дают число от 0 до 255 — это и есть номер правила по Вольфраму

Класс I: всё приходит к однородному состоянию (правила 0, 32, 255)

Класс II: устойчивые или периодические структуры (правила 4, 108)

Автоматное программирование систем управления

471 of 596

471

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Локальная функция задаётся значением на восьми возможных окрестностях

Восемь битов дают число от 0 до 255 — это и есть номер правила по Вольфраму

Класс I: всё приходит к однородному состоянию (правила 0, 32, 255)

Класс II: устойчивые или периодические структуры (правила 4, 108)

Класс III: хаотические, статистически случайные узоры (правило 30)

Автоматное программирование систем управления

472 of 596

472

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Локальная функция задаётся значением на восьми возможных окрестностях

Восемь битов дают число от 0 до 255 — это и есть номер правила по Вольфраму

Класс I: всё приходит к однородному состоянию (правила 0, 32, 255)

Класс II: устойчивые или периодические структуры (правила 4, 108)

Класс III: хаотические, статистически случайные узоры (правило 30)

Класс IV: локальные структуры, взаимодействующие сложным образом (правило 110)

Автоматное программирование систем управления

473 of 596

473

Элементарные клеточные автоматы

Одномерное поле, два состояния ячейки, окрестность из трёх клеток

Локальная функция задаётся значением на восьми возможных окрестностях

Восемь битов дают число от 0 до 255 — это и есть номер правила по Вольфраму

Класс I: всё приходит к однородному состоянию (правила 0, 32, 255)

Класс II: устойчивые или периодические структуры (правила 4, 108)

Класс III: хаотические, статистически случайные узоры (правило 30)

Класс IV: локальные структуры, взаимодействующие сложным образом (правило 110)

Правило 30 проходит статистические тесты на случайность и использовалось в Mathematica как генератор

Автоматное программирование систем управления

474 of 596

474

Правило 90: треугольник Серпинского

Одна живая клетка в начальной строке, восемь строчек правила — и регулярный фрактальный узор. Класс II

Автоматное программирование систем управления

475 of 596

475

Правило 30: тот же старт, хаотический узор

Класс III. Предсказать состояние клетки, не прогнав все шаги, нельзя — при том что правило умещается в восемь битов

Автоматное программирование систем управления

476 of 596

476

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

Автоматное программирование систем управления

477 of 596

477

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

В узоре правила 110 выделяются устойчивые фоновые области и движущиеся структуры — планеры

Автоматное программирование систем управления

478 of 596

478

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

В узоре правила 110 выделяются устойчивые фоновые области и движущиеся структуры — планеры

Их столкновения играют роль логических операций

Автоматное программирование систем управления

479 of 596

479

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

В узоре правила 110 выделяются устойчивые фоновые области и движущиеся структуры — планеры

Их столкновения играют роль логических операций

Из них собирается моделирование циклической системы тегов — модели, эквивалентной машине Тьюринга

Автоматное программирование систем управления

480 of 596

480

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

В узоре правила 110 выделяются устойчивые фоновые области и движущиеся структуры — планеры

Их столкновения играют роль логических операций

Из них собирается моделирование циклической системы тегов — модели, эквивалентной машине Тьюринга

Автомат с двумя состояниями клетки и восемью строчками правила не проще машины Тьюринга

Автоматное программирование систем управления

481 of 596

481

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

В узоре правила 110 выделяются устойчивые фоновые области и движущиеся структуры — планеры

Их столкновения играют роль логических операций

Из них собирается моделирование циклической системы тегов — модели, эквивалентной машине Тьюринга

Автомат с двумя состояниями клетки и восемью строчками правила не проще машины Тьюринга

Со всеми следствиями, включая неразрешимость проблемы останова для него

Автоматное программирование систем управления

482 of 596

482

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

В узоре правила 110 выделяются устойчивые фоновые области и движущиеся структуры — планеры

Их столкновения играют роль логических операций

Из них собирается моделирование циклической системы тегов — модели, эквивалентной машине Тьюринга

Автомат с двумя состояниями клетки и восемью строчками правила не проще машины Тьюринга

Со всеми следствиями, включая неразрешимость проблемы останова для него

Практической пригодности это не означает: кодирование чудовищно неэффективно

Автоматное программирование систем управления

483 of 596

483

Правило 110 полно по Тьюрингу

Теорема Кука, 2000

В узоре правила 110 выделяются устойчивые фоновые области и движущиеся структуры — планеры

Их столкновения играют роль логических операций

Из них собирается моделирование циклической системы тегов — модели, эквивалентной машине Тьюринга

Автомат с двумя состояниями клетки и восемью строчками правила не проще машины Тьюринга

Со всеми следствиями, включая неразрешимость проблемы останова для него

Практической пригодности это не означает: кодирование чудовищно неэффективно

Ценность в другом — граница между «простым» и «универсальным» проходит гораздо ниже, чем кажется

Автоматное программирование систем управления

484 of 596

484

Игра «Жизнь»: планер

Пять поколений: конфигурация повторяет себя со сдвигом на клетку по диагонали. Правила Конуэя: клетка выживает при двух-трёх соседях, рождается ровно при трёх

Автоматное программирование систем управления

485 of 596

485

Ружьё Госпера

Конфигурация, периодически порождающая планеры. Её существование опровергло гипотезу Конуэя о том, что население поля не может расти неограниченно

Автоматное программирование систем управления

486 of 596

486

Муравей Лэнгтона: порядок из хаоса

Два правила, два состояния клетки, память муравья — направление

Автоматное программирование систем управления

487 of 596

487

Муравей Лэнгтона: порядок из хаоса

Два правила, два состояния клетки, память муравья — направление

На белой клетке — поворот направо, на чёрной — налево

Автоматное программирование систем управления

488 of 596

488

Муравей Лэнгтона: порядок из хаоса

Два правила, два состояния клетки, память муравья — направление

На белой клетке — поворот направо, на чёрной — налево

Клетка перекрашивается в противоположный цвет, муравей делает шаг вперёд

Автоматное программирование систем управления

489 of 596

489

Муравей Лэнгтона: порядок из хаоса

Два правила, два состояния клетки, память муравья — направление

На белой клетке — поворот направо, на чёрной — налево

Клетка перекрашивается в противоположный цвет, муравей делает шаг вперёд

Хаос: примерно первые 500 шагов узор почти симметричен, потом симметрия рушится

Автоматное программирование систем управления

490 of 596

490

Муравей Лэнгтона: порядок из хаоса

Два правила, два состояния клетки, память муравья — направление

На белой клетке — поворот направо, на чёрной — налево

Клетка перекрашивается в противоположный цвет, муравей делает шаг вперёд

Хаос: примерно первые 500 шагов узор почти симметричен, потом симметрия рушится

Беспорядок: до примерно 10 000 шагов пятно растёт без видимой структуры

Автоматное программирование систем управления

491 of 596

491

Муравей Лэнгтона: порядок из хаоса

Два правила, два состояния клетки, память муравья — направление

На белой клетке — поворот направо, на чёрной — налево

Клетка перекрашивается в противоположный цвет, муравей делает шаг вперёд

Хаос: примерно первые 500 шагов узор почти симметричен, потом симметрия рушится

Беспорядок: до примерно 10 000 шагов пятно растёт без видимой структуры

Шоссе: муравей внезапно строит периодическую дорожку и уходит по ней, повторяя цикл из 104 шагов

Автоматное программирование систем управления

492 of 596

492

Муравей Лэнгтона: порядок из хаоса

Два правила, два состояния клетки, память муравья — направление

На белой клетке — поворот направо, на чёрной — налево

Клетка перекрашивается в противоположный цвет, муравей делает шаг вперёд

Хаос: примерно первые 500 шагов узор почти симметричен, потом симметрия рушится

Беспорядок: до примерно 10 000 шагов пятно растёт без видимой структуры

Шоссе: муравей внезапно строит периодическую дорожку и уходит по ней, повторяя цикл из 104 шагов

Доказано, что траектория неограниченна; не доказано, что шоссе строится всегда — это открытая задача

Автоматное программирование систем управления

493 of 596

493

Три эпохи муравья Лэнгтона

200 шагов — узор почти симметричен; 2000 — симметрия разрушена; 7000 — беспорядочное пятно; 11 000 — из пятна уходит шоссе. «Формулы состояния на шаге n» здесь нет и, возможно, быть не может

Автоматное программирование систем управления

494 of 596

494

Одна ошибка, которую делают все

Автоматное программирование систем управления

495 of 596

495

Одна ошибка, которую делают все

Новое состояние поля обязано считаться по старому состоянию целиком

Автоматное программирование систем управления

496 of 596

496

Одна ошибка, которую делают все

Новое состояние поля обязано считаться по старому состоянию целиком

Если обновлять клетки на месте, соседи справа и снизу увидят уже новые значения

Автоматное программирование систем управления

497 of 596

497

Одна ошибка, которую делают все

Новое состояние поля обязано считаться по старому состоянию целиком

Если обновлять клетки на месте, соседи справа и снизу увидят уже новые значения

Получится другой автомат — обычно с правдоподобной, но неверной картинкой

Автоматное программирование систем управления

498 of 596

498

Одна ошибка, которую делают все

Новое состояние поля обязано считаться по старому состоянию целиком

Если обновлять клетки на месте, соседи справа и снизу увидят уже новые значения

Получится другой автомат — обычно с правдоподобной, но неверной картинкой

Второй буфер обязателен: это прямое следствие определения глобальной функции переходов Φ

Автоматное программирование систем управления

499 of 596

499

Одна ошибка, которую делают все

Новое состояние поля обязано считаться по старому состоянию целиком

Если обновлять клетки на месте, соседи справа и снизу увидят уже новые значения

Получится другой автомат — обычно с правдоподобной, но неверной картинкой

Второй буфер обязателен: это прямое следствие определения глобальной функции переходов Φ

Отсюда же естественность клеточных автоматов для параллельных вычислений

Автоматное программирование систем управления

500 of 596

500

Одна ошибка, которую делают все

Новое состояние поля обязано считаться по старому состоянию целиком

Если обновлять клетки на месте, соседи справа и снизу увидят уже новые значения

Получится другой автомат — обычно с правдоподобной, но неверной картинкой

Второй буфер обязателен: это прямое следствие определения глобальной функции переходов Φ

Отсюда же естественность клеточных автоматов для параллельных вычислений

Клетки одного поколения не зависят друг от друга и считаются независимо

Автоматное программирование систем управления

501 of 596

501

Задача об умном муравье

Последний пример лекции отличается тем, что автомат в нём не задан — его требуется найти

Практикум: practices/11-ant-search

502 of 596

502

Задача об умном муравье

Последний пример лекции отличается тем, что автомат в нём не задан — его требуется найти

По полю проложена тропа с едой и разрывами; муравей видит один бит — есть ли еда впереди

Практикум: practices/11-ant-search

503 of 596

503

Задача об умном муравье

Последний пример лекции отличается тем, что автомат в нём не задан — его требуется найти

По полю проложена тропа с едой и разрывами; муравей видит один бит — есть ли еда впереди

Действия: шаг, поворот налево, поворот направо. Требуется автомат Мили

Практикум: practices/11-ant-search

504 of 596

504

Задача об умном муравье

Последний пример лекции отличается тем, что автомат в нём не задан — его требуется найти

По полю проложена тропа с едой и разрывами; муравей видит один бит — есть ли еда впереди

Действия: шаг, поворот налево, поворот направо. Требуется автомат Мили

Тропа Санта-Фе: 89 клеток с едой на торе 32 × 32, лимит 600 тактов

Практикум: practices/11-ant-search

505 of 596

505

Задача об умном муравье

Последний пример лекции отличается тем, что автомат в нём не задан — его требуется найти

По полю проложена тропа с едой и разрывами; муравей видит один бит — есть ли еда впереди

Действия: шаг, поворот налево, поворот направо. Требуется автомат Мили

Тропа Санта-Фе: 89 клеток с едой на торе 32 × 32, лимит 600 тактов

Правило без состояний крутится на месте у первого же разрыва: стратегия обязана помнить, что проверено

Практикум: practices/11-ant-search

506 of 596

506

Задача об умном муравье

Последний пример лекции отличается тем, что автомат в нём не задан — его требуется найти

По полю проложена тропа с едой и разрывами; муравей видит один бит — есть ли еда впереди

Действия: шаг, поворот налево, поворот направо. Требуется автомат Мили

Тропа Санта-Фе: 89 клеток с едой на торе 32 × 32, лимит 600 тактов

Правило без состояний крутится на месте у первого же разрыва: стратегия обязана помнить, что проверено

Перебор не проходит: у автомата с n состояниями (3n)^(2n) вариантов — при n = 5 порядка 10¹⁴

Практикум: practices/11-ant-search

507 of 596

507

Задача об умном муравье

Последний пример лекции отличается тем, что автомат в нём не задан — его требуется найти

По полю проложена тропа с едой и разрывами; муравей видит один бит — есть ли еда впереди

Действия: шаг, поворот налево, поворот направо. Требуется автомат Мили

Тропа Санта-Фе: 89 клеток с едой на торе 32 × 32, лимит 600 тактов

Правило без состояний крутится на месте у первого же разрыва: стратегия обязана помнить, что проверено

Перебор не проходит: у автомата с n состояниями (3n)^(2n) вариантов — при n = 5 порядка 10¹⁴

Практикум ищет автомат (1 + 1)-эволюционной стратегией: мутация одного поля таблицы, прогон, отбор

Практикум: practices/11-ant-search

508 of 596

508

Цена эволюционного поиска

Автомат из 17 состояний за 181 такт против рукотворного из 5 состояний за 315. Он работает и проверен прогоном, но объяснить, почему он работает, нельзя: у состояний нет смысла, который можно назвать словом

Автоматное программирование систем управления

509 of 596

ЛЕКЦИЯ

Язык Takt: описание автоматов и порождение кода

Четвёртый способ записать автомат

510 of 596

510

Зачем языку автоматов отдельный синтаксис

Автоматное программирование систем управления

511 of 596

511

Зачем языку автоматов отдельный синтаксис

В лекции 7 автомат писался вручную: переменная состояния, цикл, switch, действия на переходах

Автоматное программирование систем управления

512 of 596

512

Зачем языку автоматов отдельный синтаксис

В лекции 7 автомат писался вручную: переменная состояния, цикл, switch, действия на переходах

Автоматная природа программы в таком коде не выражена, а подразумевается

Автоматное программирование систем управления

513 of 596

513

Зачем языку автоматов отдельный синтаксис

В лекции 7 автомат писался вручную: переменная состояния, цикл, switch, действия на переходах

Автоматная природа программы в таком коде не выражена, а подразумевается

Компилятор Си не знает, что state — состояние: он не проверит ни ортогональность, ни достижимость

Автоматное программирование систем управления

514 of 596

514

Зачем языку автоматов отдельный синтаксис

В лекции 7 автомат писался вручную: переменная состояния, цикл, switch, действия на переходах

Автоматная природа программы в таком коде не выражена, а подразумевается

Компилятор Си не знает, что state — состояние: он не проверит ни ортогональность, ни достижимость

Список типовых ошибок из лекции 7 — перечень того, что не проверяется, потому что не записано

Автоматное программирование систем управления

515 of 596

515

Зачем языку автоматов отдельный синтаксис

В лекции 7 автомат писался вручную: переменная состояния, цикл, switch, действия на переходах

Автоматная природа программы в таком коде не выражена, а подразумевается

Компилятор Си не знает, что state — состояние: он не проверит ни ортогональность, ни достижимость

Список типовых ошибок из лекции 7 — перечень того, что не проверяется, потому что не записано

В лекции 8 модель рисовалась в редакторе, но жила вне репозитория и плохо сливалась системой контроля версий

Автоматное программирование систем управления

516 of 596

516

Зачем языку автоматов отдельный синтаксис

В лекции 7 автомат писался вручную: переменная состояния, цикл, switch, действия на переходах

Автоматная природа программы в таком коде не выражена, а подразумевается

Компилятор Си не знает, что state — состояние: он не проверит ни ортогональность, ни достижимость

Список типовых ошибок из лекции 7 — перечень того, что не проверяется, потому что не записано

В лекции 8 модель рисовалась в редакторе, но жила вне репозитория и плохо сливалась системой контроля версий

Язык описания автоматов — третий вариант: модель остаётся текстом, но текст понимает компилятор

Автоматное программирование систем управления

517 of 596

517

Цели генерации компилятора taktc

Цель	Ключ	Где применяется
Си	-t c	прошивка, встраиваемая логика
Си + HAL	-t c-hal	то же плюс таблица адресов портов
Structured Text	-t st	библиотека блоков для ПЛК, IEC 61131-3
ST с адресами	-t st-at	программа ПЛК целиком, порты по адресам
Rust	-t rust	прошивка без std
SystemVerilog	-t sv	синтез для FPGA/ASIC
PlantUML	-t plantuml	диаграмма состояний в документацию

Одно описание — и прошивка, и программа ПЛК, и диаграмма для отчёта. Цель st связывает лекцию с материалом лекции 8: модель становится FUNCTION_BLOCK, состояния — ветвями CASE state OF.

Автоматное программирование систем управления

518 of 596

518

Первая модель: светофор

model TrafficLight {

out lamp: u8 := 0;

var timer: u8 := 0;

const RED_TIME: u8 := 20;

start Red {

enter { timer := 0; lamp := 0; }

always { timer := timer + 1; }

ref Green: timer = RED_TIME;

}

/* ... Green, Yellow ... */

}

start Entry = TrafficLight;

Присваивание — :=, сравнение — =, как в Structured Text; оператора == в языке нет вовсе. Внутри состояния три блока: enter при входе, always каждый такт, exit при выходе; ref — ребро автомата.

Практикум: practices/12-takt

519 of 596

519

Тот же светофор диаграммой

Выдержки заданы числом тактов. Такт — шаг логики автомата, а не единица времени: частоту задаёт вызывающая сторона

Автоматное программирование систем управления

520 of 596

520

Такт

Автоматное программирование систем управления

521 of 596

521

Такт

Такт — один шаг логики: вычисление тел активных состояний и проверка условий исходящих рёбер

Автоматное программирование систем управления

522 of 596

522

Такт

Такт — один шаг логики: вычисление тел активных состояний и проверка условий исходящих рёбер

Такт не связан с единицей времени; модель, где «10 тактов» означает «10 мс», молча ломается при смене частоты опроса

Автоматное программирование систем управления

523 of 596

523

Такт

Такт — один шаг логики: вычисление тел активных состояний и проверка условий исходящих рёбер

Порядок внутри такта: сначала тело активного состояния, затем условия рёбер

Автоматное программирование систем управления

524 of 596

524

Такт

Такт — один шаг логики: вычисление тел активных состояний и проверка условий исходящих рёбер

Порядок внутри такта: сначала тело активного состояния, затем условия рёбер

Если ребро сработало — выполняется exit текущего состояния и enter целевого

Автоматное программирование систем управления

525 of 596

525

Такт

Такт — один шаг логики: вычисление тел активных состояний и проверка условий исходящих рёбер

Порядок внутри такта: сначала тело активного состояния, затем условия рёбер

Если ребро сработало — выполняется exit текущего состояния и enter целевого

Вход в стартовое состояние такта не расходует: тело start-состояния исполняется уже на первом такте

Автоматное программирование систем управления

526 of 596

526

Такт

Такт — один шаг логики: вычисление тел активных состояний и проверка условий исходящих рёбер

Порядок внутри такта: сначала тело активного состояния, затем условия рёбер

Если ребро сработало — выполняется exit текущего состояния и enter целевого

Вход в стартовое состояние такта не расходует: тело start-состояния исполняется уже на первом такте

Отсюда правило: выдержки меряются тактами, а физическое время приходит с датчиков

Автоматное программирование систем управления

527 of 596

527

Состояние обязано удерживать управление

Типичная ошибка — написать «шаг работы» там, где нужно «состояние работы»

Автоматное программирование систем управления

528 of 596

528

Состояние обязано удерживать управление

Типичная ошибка — написать «шаг работы» там, где нужно «состояние работы»

Условия рёбер проверяются каждый такт

Автоматное программирование систем управления

529 of 596

529

Состояние обязано удерживать управление

Типичная ошибка — написать «шаг работы» там, где нужно «состояние работы»

Условия рёбер проверяются каждый такт

Ребро, истинное сразу после входа, выпускает управление раньше, чем состояние сделало работу

Автоматное программирование систем управления

530 of 596

530

Состояние обязано удерживать управление

Типичная ошибка — написать «шаг работы» там, где нужно «состояние работы»

Условия рёбер проверяются каждый такт

Ребро, истинное сразу после входа, выпускает управление раньше, чем состояние сделало работу

Модель охлаждения входит в Cooling со 101 градусом, за такт снимает три — и уходит, потому что 98 > 0

Автоматное программирование систем управления

531 of 596

531

Состояние обязано удерживать управление

Типичная ошибка — написать «шаг работы» там, где нужно «состояние работы»

Условия рёбер проверяются каждый такт

Ребро, истинное сразу после входа, выпускает управление раньше, чем состояние сделало работу

Модель охлаждения входит в Cooling со 101 градусом, за такт снимает три — и уходит, потому что 98 > 0

Состояние Done недостижимо при любом нагреве, а симулятор показывает это за два шага

Автоматное программирование систем управления

532 of 596

532

Состояние обязано удерживать управление

Типичная ошибка — написать «шаг работы» там, где нужно «состояние работы»

Условия рёбер проверяются каждый такт

Ребро, истинное сразу после входа, выпускает управление раньше, чем состояние сделало работу

Модель охлаждения входит в Cooling со 101 градусом, за такт снимает три — и уходит, потому что 98 > 0

Состояние Done недостижимо при любом нагреве, а симулятор показывает это за два шага

Исправление: условия выхода делают непересекающимися и покрывающими

Автоматное программирование систем управления

533 of 596

533

Состояние обязано удерживать управление

Типичная ошибка — написать «шаг работы» там, где нужно «состояние работы»

Условия рёбер проверяются каждый такт

Ребро, истинное сразу после входа, выпускает управление раньше, чем состояние сделало работу

Модель охлаждения входит в Cooling со 101 градусом, за такт снимает три — и уходит, потому что 98 > 0

Состояние Done недостижимо при любом нагреве, а симулятор показывает это за два шага

Исправление: условия выхода делают непересекающимися и покрывающими

Именованное условие cond Cooled = temperature = 0 даёт имя предикату, и это же имя попадает в проверку свойств

Автоматное программирование систем управления

534 of 596

534

Что порождается: тот же while — switch — case

void WatchdogWatchdog_tick(WatchdogWatchdog *m, Watchdog *main) {

switch (m->state) {

case WATCHDOG_WATCHING: {

if ((*main->read_bit)(WATCHDOG_KICK, main->userdata)) {

m->idle = 0;

} else {

m->idle = m->idle + 1;

}

if (m->idle >= CONST_WATCHDOG_LIMIT) {

(*main->write_bit)(WATCHDOG_ALARM, 1, main->userdata);

m->state = WATCHDOG_TRIPPED;

}

break;

}

Ровно та конструкция, которую в лекции 7 писали руками, — с одной разницей: её написал компилятор из описания, которое он же проверил.

Автоматное программирование систем управления

535 of 596

535

Три решения порождённого кода

Автоматное программирование систем управления

536 of 596

536

Три решения порождённого кода

Порты — вызовы, а не переменные: автоматная логика не знает, откуда берётся значение

Автоматное программирование систем управления

537 of 596

537

Три решения порождённого кода

Порты — вызовы, а не переменные: автоматная логика не знает, откуда берётся значение

Драйвер платформы подставляет функции, и модель отвязана от железа

Автоматное программирование систем управления

538 of 596

538

Три решения порождённого кода

Порты — вызовы, а не переменные: автоматная логика не знает, откуда берётся значение

Драйвер платформы подставляет функции, и модель отвязана от железа

Состояние — поле структуры: экземпляров модели может быть несколько, глобальных переменных нет

Автоматное программирование систем управления

539 of 596

539

Три решения порождённого кода

Порты — вызовы, а не переменные: автоматная логика не знает, откуда берётся значение

Драйвер платформы подставляет функции, и модель отвязана от железа

Состояние — поле структуры: экземпляров модели может быть несколько, глобальных переменных нет

Генерация детерминирована: один исходный файл даёт байт-в-байт одинаковый вывод

Автоматное программирование систем управления

540 of 596

540

Три решения порождённого кода

Порты — вызовы, а не переменные: автоматная логика не знает, откуда берётся значение

Драйвер платформы подставляет функции, и модель отвязана от железа

Состояние — поле структуры: экземпляров модели может быть несколько, глобальных переменных нет

Генерация детерминирована: один исходный файл даёт байт-в-байт одинаковый вывод

Числовые значения состояний и портов не «съезжают» при пересборке — у прошивки стабильный ABI

Автоматное программирование систем управления

541 of 596

541

Три решения порождённого кода

Порты — вызовы, а не переменные: автоматная логика не знает, откуда берётся значение

Драйвер платформы подставляет функции, и модель отвязана от железа

Состояние — поле структуры: экземпляров модели может быть несколько, глобальных переменных нет

Генерация детерминирована: один исходный файл даёт байт-в-байт одинаковый вывод

Числовые значения состояний и портов не «съезжают» при пересборке — у прошивки стабильный ABI

Порождённый код — C99, и practices/12-takt единственная практика, где требование C90 ослаблено

Автоматное программирование систем управления

542 of 596

542

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Автоматное программирование систем управления

543 of 596

543

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Свойство пишется в самом файле строкой : [LTL] φ; операторы те же, что в лекции 9

Автоматное программирование систем управления

544 of 596

544

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Свойство пишется в самом файле строкой : [LTL] φ; операторы те же, что в лекции 9

Модель абстрагируется до графа переходов: вершины — состояния, рёбра — ref, условия игнорируются

Автоматное программирование систем управления

545 of 596

545

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Свойство пишется в самом файле строкой : [LTL] φ; операторы те же, что в лекции 9

Модель абстрагируется до графа переходов: вершины — состояния, рёбра — ref, условия игнорируются

«Держится» — надёжный ответ: истинное на всех прогонах абстракции истинно и на всех реальных

Автоматное программирование систем управления

546 of 596

546

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Свойство пишется в самом файле строкой : [LTL] φ; операторы те же, что в лекции 9

Модель абстрагируется до графа переходов: вершины — состояния, рёбра — ref, условия игнорируются

«Держится» — надёжный ответ: истинное на всех прогонах абстракции истинно и на всех реальных

«Нарушено» — контрпример в абстракции, он может оказаться недостижим по данным

Автоматное программирование систем управления

547 of 596

547

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Свойство пишется в самом файле строкой : [LTL] φ; операторы те же, что в лекции 9

Модель абстрагируется до графа переходов: вершины — состояния, рёбра — ref, условия игнорируются

«Держится» — надёжный ответ: истинное на всех прогонах абстракции истинно и на всех реальных

«Нарушено» — контрпример в абстракции, он может оказаться недостижим по данным

Отличие от лекции 9: SPIN проверяет модель, написанную отдельно от программы

Автоматное программирование систем управления

548 of 596

548

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Свойство пишется в самом файле строкой : [LTL] φ; операторы те же, что в лекции 9

Модель абстрагируется до графа переходов: вершины — состояния, рёбра — ref, условия игнорируются

«Держится» — надёжный ответ: истинное на всех прогонах абстракции истинно и на всех реальных

«Нарушено» — контрпример в абстракции, он может оказаться недостижим по данным

Отличие от лекции 9: SPIN проверяет модель, написанную отдельно от программы

Здесь проверяется то же описание, из которого порождается прошивка, — расхождению взяться неоткуда

Автоматное программирование систем управления

549 of 596

549

Проверка свойств

taktc умеет проверять LTL-свойства model checking'ом — исчерпывающим перебором, а не тестами

Свойство пишется в самом файле строкой : [LTL] φ; операторы те же, что в лекции 9

Модель абстрагируется до графа переходов: вершины — состояния, рёбра — ref, условия игнорируются

«Держится» — надёжный ответ: истинное на всех прогонах абстракции истинно и на всех реальных

«Нарушено» — контрпример в абстракции, он может оказаться недостижим по данным

Отличие от лекции 9: SPIN проверяет модель, написанную отдельно от программы

Здесь проверяется то же описание, из которого порождается прошивка, — расхождению взяться неоткуда

Плата — более узкий класс свойств: вложенные модели и арифметика в предикатах в охват не входят

Автоматное программирование систем управления

550 of 596

550

Свойство «после аварии система обязана вернуться в рабочий режим»

G (Fault → F Idle). Проверяется по графу переходов: три состояния, четыре ребра — и доказательство вместо набора тестов

Автоматное программирование систем управления

551 of 596

551

Границы применимости

Автоматное программирование систем управления

552 of 596

552

Границы применимости

Язык описания автоматов не заменяет язык общего назначения

Автоматное программирование систем управления

553 of 596

553

Границы применимости

Язык описания автоматов не заменяет язык общего назначения

Takt уместен там, где задача по сути автоматная: управляющая логика, протоколы, последовательности с выдержками

Автоматное программирование систем управления

554 of 596

554

Границы применимости

Язык описания автоматов не заменяет язык общего назначения

Неуместен там, где логика — это вычисления над структурами данных

Автоматное программирование систем управления

555 of 596

555

Границы применимости

Язык описания автоматов не заменяет язык общего назначения

Неуместен там, где логика — это вычисления над структурами данных

Разбор форматов со сложной грамматикой, обработка массивов, всё требующее динамической памяти — её в языке нет вовсе

Автоматное программирование систем управления

556 of 596

556

Границы применимости

Язык описания автоматов не заменяет язык общего назначения

Неуместен там, где логика — это вычисления над структурами данных

Правило то же, что в лекции 7: если вы не можете нарисовать диаграмму состояний задачи, автоматный язык не поможет

Автоматное программирование систем управления

557 of 596

557

Границы применимости

Язык описания автоматов не заменяет язык общего назначения

Неуместен там, где логика — это вычисления над структурами данных

Он не сделает задачу автоматной, а лишь запишет то, что уже является автоматом

Автоматное программирование систем управления

558 of 596

ЛЕКЦИЯ

Практикум, лабораторные работы и приложения

Что студент делает руками

559 of 596

559

Практикум: каталог на лекцию

Каталог	Лекция	Что показывает
01-words	1	слова и языки: конкатенация, степень, префиксы, произведение, итерация
02-fsm-delay	2	автомат «задержка» в модели Мили + модель SimInTech
03-synthesis	3	синтез схемы: таблица переходов → булевы функции → код
04-dfa-nfa	4	детерминизация и минимизация, вывод в Graphviz
05-kleene	5	конструкция Томпсона: регулярное выражение в ε-НКА
06-regular-expression	6	учебный движок регулярных выражений и распознаватели форматов
06-lexical-analyze	6	лексический анализатор арифметических выражений
07-simple-program	7	контрпример: вложенные switch/if вместо автомата
07-three-ways	7	один автомат тремя способами; покрытие переходов

Автоматное программирование систем управления

560 of 596

560

Практикум: продолжение

Каталог	Лекция	Что показывает
03-control-program	7	линия точечной сварки: автомат отделён от установки тремя интерфейсами
08-fsm-control-pneumo	8	циклограмма пневмоцилиндров, кодогенерация SimInTech
08-bulk-loading	8	загрузка сыпучих материалов: автомат промышленного размера и модель установки
09-promela	9	одиннадцать моделей Promela для SPIN, включая светофор с LTL-свойствами
10-turing-machine	10	интерпретатор машины Тьюринга: aⁿbⁿ, палиндромы, копирование
11-cells	11	правила Вольфрама, игра «Жизнь», муравей Лэнгтона, тропа Санта-Фе
11-ant-search	11	поиск автомата для умного муравья: (1 + 1)-эволюционная стратегия
12-takt	12	модели на языке Takt и порождение кода
20-welding-line	3, 7, 8, 9	сквозной проект: управление сварочной линией

Собирается одной командой из корня: cmake -S . -B build && cmake --build build -j, затем ctest --test-dir build --output-on-failure.

Автоматное программирование систем управления

561 of 596

561

Лабораторные работы

№	Лекция	Тема	Что проверяет
1	3	Синтез автомата и его схемы	путь от словесного описания до кода: автомат, кодировка, минимизация, схема
2	4	От регулярного выражения к минимальному автомату	конструкция Томпсона, детерминизация, минимизация на своём примере
3	6	Распознаватель формата как конечный автомат	переход от описания формата к таблице переходов и обратно к коду
4	10	Программа для машины Тьюринга	таблица переходов, прогон по тактам, оценка числа тактов от длины входа
5	7	Прикладной автомат в трёх реализациях	автомат отдельно, ввод-вывод отдельно; три формы записи ведут себя одинаково

Работа № 5 — уменьшенная копия курсовой: тема из того же списка, объём меньше, требования к проверке те же.

Автоматное программирование систем управления

562 of 596

562

Приложения курса

Автоматное программирование систем управления

563 of 596

563

Приложения курса

«Система управления версиями Git» — как Git хранит данные, три состояния и три области, ветки, конфликты, порядок сдачи работ

Автоматное программирование систем управления

564 of 596

564

Приложения курса

«Требования к коду курса» — режим сборки и ключи, .clang-format, что проверяет check-style.sh, комментарии Doxygen, тесты

Автоматное программирование систем управления

565 of 596

565

Приложения курса

«Требования к коду курса» — режим сборки и ключи, .clang-format, что проверяет check-style.sh, комментарии Doxygen, тесты

«Стандарт языка Си: справочник курса» — восемь фаз трансляции, типы и преобразования, классы поведения, чего в C90 нет

Автоматное программирование систем управления

566 of 596

566

Приложения курса

«Требования к коду курса» — режим сборки и ключи, .clang-format, что проверяет check-style.sh, комментарии Doxygen, тесты

Приложения не читаются на занятии и не имеют номера в расписании — это справка

Автоматное программирование систем управления

567 of 596

567

Приложения курса

«Требования к коду курса» — режим сборки и ключи, .clang-format, что проверяет check-style.sh, комментарии Doxygen, тесты

Приложения не читаются на занятии и не имеют номера в расписании — это справка

Собираются той же командой, что и лекции, и входят в комплект: 21 PDF, сводный том 356 страниц

Автоматное программирование систем управления

568 of 596

568

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Автоматное программирование систем управления

569 of 596

569

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Установка изделия на конвейер, установка деталей на изделие, сварка деталей

Автоматное программирование систем управления

570 of 596

570

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Установка изделия на конвейер, установка деталей на изделие, сварка деталей

Покраска изделия, сортировка и упаковка, маркировка упакованных изделий

Автоматное программирование систем управления

571 of 596

571

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Установка изделия на конвейер, установка деталей на изделие, сварка деталей

Покраска изделия, сортировка и упаковка, маркировка упакованных изделий

Грузовой лифт трёхэтажного здания, конвейер подачи изделий

Автоматное программирование систем управления

572 of 596

572

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Установка изделия на конвейер, установка деталей на изделие, сварка деталей

Покраска изделия, сортировка и упаковка, маркировка упакованных изделий

Грузовой лифт трёхэтажного здания, конвейер подачи изделий

Холодная штамповка шайб, линия отжига, цепевязальная холодногибочная линия

Автоматное программирование систем управления

573 of 596

573

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Установка изделия на конвейер, установка деталей на изделие, сварка деталей

Покраска изделия, сортировка и упаковка, маркировка упакованных изделий

Грузовой лифт трёхэтажного здания, конвейер подачи изделий

Холодная штамповка шайб, линия отжига, цепевязальная холодногибочная линия

Гибкие производственные системы: фланец, корпус, вал-шестерня, зубчатое колесо, штуцер, крышка

Автоматное программирование систем управления

574 of 596

574

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Установка изделия на конвейер, установка деталей на изделие, сварка деталей

Покраска изделия, сортировка и упаковка, маркировка упакованных изделий

Грузовой лифт трёхэтажного здания, конвейер подачи изделий

Холодная штамповка шайб, линия отжига, цепевязальная холодногибочная линия

Гибкие производственные системы: фланец, корпус, вал-шестерня, зубчатое колесо, штуцер, крышка

Управление роботом: поиск объектов на плоскости, движение по заданной траектории

Автоматное программирование систем управления

575 of 596

575

Курсовая работа

Автоматная модель прикладной задачи — 22 темы

Установка изделия на конвейер, установка деталей на изделие, сварка деталей

Покраска изделия, сортировка и упаковка, маркировка упакованных изделий

Грузовой лифт трёхэтажного здания, конвейер подачи изделий

Холодная штамповка шайб, линия отжига, цепевязальная холодногибочная линия

Гибкие производственные системы: фланец, корпус, вал-шестерня, зубчатое колесо, штуцер, крышка

Управление роботом: поиск объектов на плоскости, движение по заданной траектории

Образец ожидаемого объёма — сквозной пример practices/20-welding-line

Автоматное программирование систем управления

576 of 596

★

ЛЕКЦИЯ

Итоги

Что вынести из курса

577 of 596

577

Карта курса

Лекции	Что изучалось	Главный вывод
1—3	алфавиты, языки, автомат Мили и Мура, синтез схемы	автомат задаётся таблицей и превращается в схему механически
4—6	акцепторы, ДКА и НКА, теорема Клини, регулярные выражения	регулярные языки, автоматы и выражения — три записи одного класса
7—9	автоматное программирование, statecharts, верификация	явная модель даёт проверяемость: покрытие, статические проверки, model checking
10—12	границы модели, клеточные автоматы, язык Takt	за границей автомата — магазин и лента; ограниченность модели ценна сама по себе

Автоматное программирование систем управления

578 of 596

578

Итоги

Автоматное программирование систем управления

579 of 596

579

Итоги

Конечный автомат — один объект в трёх ролях: схема, распознаватель и программа

Автоматное программирование систем управления

580 of 596

580

Итоги

Конечный автомат — один объект в трёх ролях: схема, распознаватель и программа

Управляющая программа не пишется как последовательность действий, а задаётся автоматом

Автоматное программирование систем управления

581 of 596

581

Итоги

Конечный автомат — один объект в трёх ролях: схема, распознаватель и программа

Управляющая программа не пишется как последовательность действий, а задаётся автоматом

Явная модель имеет цену — восемнадцать пунктов критики, — и оплачивается она проверяемостью

Автоматное программирование систем управления

582 of 596

582

Итоги

Конечный автомат — один объект в трёх ролях: схема, распознаватель и программа

Управляющая программа не пишется как последовательность действий, а задаётся автоматом

Явная модель имеет цену — восемнадцать пунктов критики, — и оплачивается она проверяемостью

Покрытие переходов — нижняя граница приличия, а не признак проверенности

Автоматное программирование систем управления

583 of 596

583

Итоги

Конечный автомат — один объект в трёх ролях: схема, распознаватель и программа

Управляющая программа не пишется как последовательность действий, а задаётся автоматом

Явная модель имеет цену — восемнадцать пунктов критики, — и оплачивается она проверяемостью

Покрытие переходов — нижняя граница приличия, а не признак проверенности

Верификация доказывает свойство в модели, при принятых предположениях и ровно то, что записано формулой

Автоматное программирование систем управления

584 of 596

584

Итоги

Конечный автомат — один объект в трёх ролях: схема, распознаватель и программа

Управляющая программа не пишется как последовательность действий, а задаётся автоматом

Явная модель имеет цену — восемнадцать пунктов критики, — и оплачивается она проверяемостью

Покрытие переходов — нижняя граница приличия, а не признак проверенности

Верификация доказывает свойство в модели, при принятых предположениях и ровно то, что записано формулой

Ограниченность модели и есть то, за что её выбирают: про автомат можно доказывать, про произвольную программу — нет

Автоматное программирование систем управления

585 of 596

Конечный автомат — самая сильная из моделей,

про которые ещё можно доказывать

содержательные утверждения автоматически

Всё, что мощнее, покупает выразительность ценой неразрешимости

586 of 596

586

Что читать дальше

Автоматное программирование систем управления

587 of 596

587

Что читать дальше

Теория автоматов и языков: Хопкрофт, Мотвани, Ульман — основной учебник; Сипсер — сжатое изложение вычислимости

Автоматное программирование систем управления

588 of 596

588

Что читать дальше

Кудрявцев, Гасанов, Подколзин — источник регулярных событий и клеточных автоматов этого курса

Автоматное программирование систем управления

589 of 596

589

Что читать дальше

Кудрявцев, Гасанов, Подколзин — источник регулярных событий и клеточных автоматов этого курса

Автоматное программирование: Шалыто, Поликарпова — Шалыто (SWITCH-технология); Samek — иерархические автоматы на практике

Автоматное программирование систем управления

590 of 596

590

Что читать дальше

Кудрявцев, Гасанов, Подколзин — источник регулярных событий и клеточных автоматов этого курса

«Дракон» — построение лексических и синтаксических анализаторов: автоматы и МП-автоматы в работе

Автоматное программирование систем управления

591 of 596

591

Что читать дальше

Кудрявцев, Гасанов, Подколзин — источник регулярных событий и клеточных автоматов этого курса

«Дракон» — построение лексических и синтаксических анализаторов: автоматы и МП-автоматы в работе

Верификация: Хольцман (SPIN от автора инструмента); Кларк и др., Байер и Катоен — теория model checking

Автоматное программирование систем управления

592 of 596

592

Что читать дальше

Кудрявцев, Гасанов, Подколзин — источник регулярных событий и клеточных автоматов этого курса

«Дракон» — построение лексических и синтаксических анализаторов: автоматы и МП-автоматы в работе

Верификация: Хольцман (SPIN от автора инструмента); Кларк и др., Байер и Катоен — теория model checking

Вельдер и др. — верификация именно автоматных программ, с переводом контрпримера обратно в термины автомата

Автоматное программирование систем управления

593 of 596

593

Материалы курса

Автоматное программирование систем управления

594 of 596

594

Материалы курса

Репозиторий: github.com/BasePractice/statecraft — лекции, практикум, приложения, лабораторные

Автоматное программирование систем управления

595 of 596

595

Материалы курса

Репозиторий: github.com/BasePractice/statecraft — лекции, практикум, приложения, лабораторные

Сборка комплекта: cd lectures && ./scripts/check.sh --fix && ./scripts/build.sh

Автоматное программирование систем управления

596 of 596

596

Материалы курса

Репозиторий: github.com/BasePractice/statecraft — лекции, практикум, приложения, лабораторные

Сборка комплекта: cd lectures && ./scripts/check.sh --fix && ./scripts/build.sh

Сборка практикума: cmake -S . -B build && cmake --build build -j && ctest --test-dir build

Автоматное программирование систем управления