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

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

Текущая версия

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

Будем считать состоянием модели значение счётчика команд (неявная переменная потока управления) и значения всех переменных заданной программы. Требуется:

1. Оценить размер множества потенциальных состояний программы. Ответ обосновать. В обосновании описать множество потенциальных состояний.
2. Оценить размер множества достижимых состояний программы. Ответ обосновать. В обосновании описать множество достижимых состояний.
3. Построить 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

PNG, полученный из сгенерированного SVG

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;
}

Команда сборки диаграммы:

dot -Tsvg -o"LTS1.svg" -Kdot LTS1.dot