ВПнМ, примеры задач/Задача 2

Материал из ESyr's Wiki.

Содержание 1 Задание 2 Вариант 1 2.1 Решение 2.1.1 Модель 2.1.2 Вывод spin 2.2 Как моделировать различные конструкции 2.2.1 if 2.2.2 Функции

[править] Задание

Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа состояний этой модели.

Результаты -- текстовой файл с исходной программой, текстовой файл с расширением .pml с моделью, текстовой файл log с тем, что выдал верификатор при запуске модели, а также фраза "согласно верификатору, у модели -- N достижимых состояний", где N -- число состояний, выданных верификатором.

[править] Вариант 1

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