ВПнМ, примеры задач/Задача 2
Материал из eSyr's wiki.
ESyr01 (Обсуждение | вклад)
(Новая: == Задание == Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель ...)
К следующему изменению →
Версия 23:58, 24 апреля 2008
Содержание |
Задание
Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа состояний этой модели.
Результаты -- текстовой файл с исходной программой, текстовой файл с расширением .pml с моделью, текстовой файл log с тем, что выдал верификатор при запуске модели, а также фраза "согласно верификатору, у модели -- N достижимых состояний", где N -- число состояний, выданных верификатором.
Варианты
void f (int a, int b, int c) { int x = 0, y = 0, z = 0; x = 4; y = 1; z = a; if (y > 6) { x = 2; z = y + x; if (z > c) { x = 10; } if (y > 6) { z = b; } else { x = 5; } y = 2; y = 2; } y = 2; }
Решение
Модель
proctype f (int a; int b; int c) { int x = 0, y = 0, z = 0; x = 4; y = 1; z = a; if :: (y > 6) -> { x = 2; z = y + x; if :: (z > c) -> { x = 10; } :: else -> { skip; } fi; if :: (y > 6) -> { z = b; } :: else { x = 5; } fi; y = 2; y = 2; } :: else -> skip; fi; y = 2; } active proctype main() { run f(1,2,3); }
Вывод spin
spin -a task2.pml gcc -DSAFETY pan.c -o pan ./pan > log (Spin Version 5.1.4 -- 27 January 2008) + Partial Order Reduction Full statespace search for: never claim - (none specified) assertion violations + cycle checks - (disabled by -DSAFETY) invalid end states + State-vector 40 byte, depth reached 6, errors: 0 7 states, stored 0 states, matched 7 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved) 2.501 memory usage (Mbyte) unreached in proctype f line 14, state 9, "x = 10" line 18, state 12, "(1)" line 11, state 13, "((z>c))" line 11, state 13, "else" line 20, state 21, "((y>6))" line 20, state 21, "else" line 31, state 25, "x = 2" (5 of 31 states) unreached in proctype main (0 of 2 states) pan: elapsed time 0 seconds
Cогласно верификатору, у модели --- 7 достижимых состояний.
Как моделировать различные конструкции
if
Если if имеет одну ветку, то конструкция на С
if (condition) { expression; }
Преобразуется в слудующую конструкцию на Promela:
if :: condition -> { expression; } :: else -> skip; fi;
Где:
- if ... fi --- конструкция, порождающая недетерминизм --- выполняется любая возможная ветвь
- :: .... --- ветвь недетерминированной конструкции
- condition --- условие-страж --- ветвь не выполнится при ложном условии
- else --- ветка, которая выполняется, если все стражи ложны
- skip --- пустой оператор
Как следствие, если условие истинно, всегда выполняется первая ветвь, если нет --- вторая.
Аналогично, if с обеими ветвями моделируется следующим образом:
if :: condition -> { expression; } :: else -> { else_expression; } fi;
Функции
- Процессы, работающие на протяжении всей работы программы, обычно моделируют как active proctype. Подобные функции не принимают параметров
- Если необходимо передать параметры процессу (и/или смоделировать недетерминизм в их значении), то можно использовать типы функций inline или proctype. Первый вызывается так: func(), второй --- так: run func(). При этом inline рассматривается как некий аналог макроса, а proctype --- ещё один процесс, который запускается командой run