ВПнМ, примеры задач/Задача 1
Материал из eSyr's wiki.
Содержание |
[править] Задание
Будем считать состоянием модели значение счётчика команд (неявная переменная потока управления) и значения всех переменных заданной программы. Требуется:
- Оценить размер множества потенциальных состояний программы. Ответ обосновать. В обосновании описать множество потенциальных состояний.
- Оценить размер множества достижимых состояний программы. Ответ обосновать. В обосновании описать множество достижимых состояний.
- Построить 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
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
