Редактирование: ВПнМ, примеры задач/Задача 3
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 220: | Строка 220: | ||
2 processes created</pre> | 2 processes created</pre> | ||
- | == Пояснения == | + | === Пояснения === |
- | === Абстрагирование === | + | ==== Абстрагирование ==== |
В модели необходимо абстрагироваться ото всего, что не влияет на спецификацию. При этом надо учитывать, что, на первый взгляд посторонние переменные могут значимо влиять на поток управления и при их абстрагировании корректность и адекватность модели могут нарушаться. | В модели необходимо абстрагироваться ото всего, что не влияет на спецификацию. При этом надо учитывать, что, на первый взгляд посторонние переменные могут значимо влиять на поток управления и при их абстрагировании корректность и адекватность модели могут нарушаться. | ||
- | === Недетерминизм === | + | ==== Недетерминизм ==== |
Если необходимо проверить все возможные варианты, индуцированные различными значениями переменных, надо выделить различимые множества значений этих переменных, выбрать по одному значению из каждого множества (допустим в результате выбрали числа i1, i2, i3) и записать нечто следующее: | Если необходимо проверить все возможные варианты, индуцированные различными значениями переменных, надо выделить различимые множества значений этих переменных, выбрать по одному значению из каждого множества (допустим в результате выбрали числа i1, i2, i3) и записать нечто следующее: | ||
if | if | ||
Строка 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 --> | ||
{{Курс ВПнМ}} | {{Курс ВПнМ}} |