Редактирование: ВПнМ, примеры задач/Задача 2

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

== Задание ==

Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель на языке 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

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Шаблон:Курс ВПнМ

Получено с http://esyr.org/wiki/%D0%92%D0%9F%D0%BD%D0%9C%2C_%D0%BF%D1%80%D0%B8%D0%BC%D0%B5%D1%80%D1%8B_%D0%B7%D0%B0%D0%B4%D0%B0%D1%87/%D0%97%D0%B0%D0%B4%D0%B0%D1%87%D0%B0_2

Редактирование: ВПнМ, примеры задач/Задача 2

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 81: / Строка 81: @@
 ==== Вывод spin ====
- % spin -a task2.pml
+ spin -a task2.pml
- % gcc -DSAFETY pan.c -o pan
+ gcc -DSAFETY pan.c -o pan
- % ./pan > log
+ ./pan > log
  (Spin Version 5.1.4 -- 27 January 2008)
          + Partial Order Reduction