Редактирование: ВПнМ, примеры задач/Задача 3
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 234: | Строка 234: | ||
Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них. | Что означает случайный выбор одного из перечисленных значений. При верификации будут проверены все возможные варианты, при симуляции выбирается (случайно, интерактивно или в соответствии с трассой) один из них. | ||
- | === Имитирование системных вызовов === | + | ==== Имитирование системных вызовов ==== |
Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения. | Допустим, у нас есть два процесса, ядро и некое приложение. Приложение по ходу работы осуществляет вызовы к ядру, ядро возвращает результат. Фактически, это можно представит, как взаимодействие двух процессов путём использования двух каналов --- по которому передаются данные от приложения к ядру и обратно. Существует несколько вариантов реализации подобного поведения. | ||
- | |||
- | == Полезная строка на шелле для обрезания вывода spin == | ||
- | |||
- | При помощи следующей нехитрой строчки можно ограничить вывод spin десятью пересылками: | ||
- | MKTEMP=`mktemp`;\ | ||
- | sed -n 0,/^$(echo $(spin -p task3.pml | tee ${MKTEMP} | grep 'from?' | \ | ||
- | head -n '''10'''\ | ||
- | | tail -n 1 | cut -d: -f 1) + 1 | bc)\:/p ${MKTEMP} | head -n -1 > log.txt; rm ${MKTEMP} | ||
- | |||
- | У выделенного head ключом -n <количество> можно задать другое количество строк для обрезания. | ||
<!-- TBD --> | <!-- TBD --> | ||
{{Курс ВПнМ}} | {{Курс ВПнМ}} |