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

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

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

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

== Задание ==
Будем считать состоянием модели значение счётчика команд (неявная переменная потока управления) и значения всех переменных заданной программы. Требуется:
# Оценить размер множества потенциальных состояний программы. Ответ обосновать. В обосновании описать множество потенциальных состояний.
# Оценить размер множества достижимых состояний программы. Ответ обосновать. В обосновании описать множество достижимых состояний.
# Построить LTS для значений параметра a = 1, b = 2, c =3. Описание LTS может быть как текстовым, так и графическим (например, выполненным при помощи средства GraphViz, http://www.graphviz.org).

== Вариант 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;
 }

=== Решение ===
==== Количество потенциальных состояний ====

void
     f (int a, int b, int c)
     {
  0: 	int x = 0, y = 0, z = 0;
  1: 	x = 4;
  2: 	y = 1;
  3: 	z = a;
  4: 	if (y > 6)
     	{
  5: 		x = 2;
  6: 		z = y + x;
  7: 		if (z > c)
     		{
  8: 			x = 10;
     		}
  9: 		if (y > 6)
     		{
 10: 			z = b;
     		}
     		else
     		{
 11: 			x = 5;
     		}
 12: 		y = 2;
 13: 		y = 2;
     	}
 14: 	y = 2;
     }

Количество потенциальных состояний (сумма состояний для каждого оператора, всего переменных 6 в каждой точке программы, для каждой 2^32 вариантов): 15 * 2^(32 * 6)

==== Количество достижимых состояний ====
                                      a       b       c       x       y       z
     void                           
     f (int a, int b, int c)
     {                              
  0:     int x = 0, y = 0, z = 0;   2^32    2^32    2^32      1       1       1
  1:     x = 4;                     2^32    2^32    2^32      1       1       1
  2:     y = 1;                     2^32    2^32    2^32      1       1       1
  3:     z = a;                     2^32    2^32    2^32      1       1     2^32
  4:     if (y > 6)                 2^32    2^32    2^32      1       1     2^32
         {                          
  5:         x = 2;                   0       0       0       0       0       0
  6:         z = y + x;               0       0       0       0       0       0
  7:         if (z > c)               0       0       0       0       0       0
             {                      
  8:             x = 10;              0       0       0       0       0       0
             }                      
  9:         if (y > 6)               0       0       0       0       0       0
             {                      
 10:             z = b;               0       0       0       0       0       0
             }                      
             else                   
             {                      
 11:             x = 5;               0       0       0       0       0       0
             }                      
 12:         y = 2;                   0       0       0       0       0       0
 13:         y = 2;                   0       0       0       0       0       0
         }                          
 14:     y = 2;                     2^32    2^32    2^32      1       1     2^32
     }

Количество достижимых состояний для программы — сумма количества достижимых состояний для каждой точки программы, что, в свою очередь — произведение количество состояний переменных в данной точке. Итого: (2^96 + 2^128) * 3.

==== LTS ====
[[Image:LTS1.png|thumb]]

digraph LTS1 {
 	0 [label="0 (1, 2, 3, 0, 0, 0)"];
 	1 [label="1 (1, 2, 3, 4, 0, 0)"];
 	2 [label="2 (1, 2, 3, 4, 1, 0)"];
 	3 [label="3 (1, 2, 3, 4, 1, 1)"];
 	4 [label="4 (1, 2, 3, 4, 1, 1)"];
 	14 [label="14 (1, 2, 3, 4, 2, 1)"];
  
 	0 -> 1 -> 2 -> 3 -> 4 -> 14;
 }

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. 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_1

@@ Строка 105: / Строка 105: @@
 ==== LTS ====
-[[Image:LTS1.png|thumb|PNG, полученный из сгенерированного SVG]]
+[[Image:LTS1.png|thumb]]
  digraph LTS1 {
@@ Строка 117: / Строка 117: @@
 -> 1 -> 2 -> 3 -> 4 -> 14;
  }
-Команда сборки диаграммы:
- dot -Tsvg -o"LTS1.svg" -Kdot LTS1.dot
 {{Курс ВПнМ}}

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

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

Просмотры

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

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты