Господа и дамы,
Второе задание по практикуму состоит из четырёх частей. Описание ниже, если найдёте опечатки или непонятные моменты -- пишите!
1. Построить размеченные системы переходов (LTS) М_1, М_2 функций f и g из первого задания для следующих значений параметров функций f и g: f.a = 1, f.b = 2, g.a = 3, g.b = 4. При этом предполагается, что функции выполняются независимо и никакая другая функция не может влиять на значение глобальной переменной. Состояния LTS должны быть размечены значениями счётчика управления, глобальной переменной и локальных переменных x и y, дуги – выполняемыми операторами. Полученную LTS записать в формате dot и при помощи программного средства dot/GraphViz сгенерировать по ней картинку в формате png.
2. Модифицировать программу из п.3 задания 1 так, чтобы при указании параметра «-lts имя_файла» она строила и сохраняла в указанный файл систему переходов для асинхронной параллельной композиции функций f и g в формате dot (для значений входных параметров(f.a=1,f.b=2,f.c=3,f.d=4)). Состояния LTS должны быть размечены значениями счётчика управления, глобальной переменной и локальных переменных x и y. Дуги должны быть размечены выполняемыми операторами, для операторов ветвления дуги - истинным условием перехода (т.е. для оператора while(x<3) дуга, ведущая в тело цикла, размечается «(x<3)», ведущая на следующий за циклом оператор – «!(x<3)»)
3. Считая состоянием программы совокупность значений счётчиков f, g и переменной h, упростить описание функций и построить LTS полученной модели параллельной программы. Состояния LTS должны быть размечены значениями счётчиков управления и глобальной переменной, дуги – выполняемыми операторами. Полученную LTS записать в формате dot и при помощи программного средства dot/GraphViz сгенерировать по ней картинку в формате png.
4. Построить модель параллельной программы из первой задачи на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа достижимых состояний этой модели для значений входных параметров (f.a=1,f.b=2,f.c=3,f.d=4). Обоснуйте, почему количество состояний, подсчитанное при помощи системы Spin, отличается от полученного при построении LTS программой из п.2.
Требования к решению
Решение задачи должно включать в себя следующие файлы (всего 14 файлов):
1. Текстовый файл task.txt c описанием функций f и g.
2. Описание LTS M_1 и M_2 в формате dot в файлах с именами lts_m1.txt и lts_m2.txt, а также сгенерированные по ним картинки в файлах lts_m1.png и lts_m2.png.
3. Исходный код модифицированной согласно п.2 программы в файле task2.c, описание сгенерированной ей LTS в формате dot в файле lts_m12.dot и сгенерированную по нему картинку в файле lts_m12.png.
4. Текстовой файл abstraction.txt с упрощённым описанием функций (п.3 задания) и комментарием, описывающим проведённую абстракцию, описание LTS этой «модели» в формате dot в файле abstract_lts_m12.dot и сгенерированную по нему картинку в файле abstract_lts_m12.png.
5. Текстовой файл с расширением task2.pml с моделью на Promela, текстовой файл log.txt с тем, что выдал верификатор при запуске модели, текстовой файл states.txt с 1) фразой «Согласно верификатору, у модели – N достижимых состояний», где N -- число состояний, выданных верификатором, 2) фразой «В LTS для программы – M достижимых состояний», где М – число, выдаваемое программой из п.2 данной задачи и 3) обоснованием отличия N от M.
Дополнительная информация
1. Пример описания LTS в виде графа в формате dot:
digraph G { 0 [label=”1,#,1”]; 1 [label=”2,1,1”]; 2 [label=”4,1,1”]; 0 -> 1 [label=”h = a;”]; 1 -> 2 [label=”!(h < a)”]; }
Графический файл в формате png может быть сгенерирован следующей командой (имя_файла_1 – имя файла с картинкой, имя_файла_2 – имя файла в формате dot):
dot -Tpng -o имя_файла_1 имя_файла_2
2. О том, как среди вывода верификатора распознать число состояний модели, можно прочитать в руководстве к системе Spin (например, здесь: http://spinroot.com/spin/Man/Pan.html#L9). Обратите внимание, что в ходе построения пространства состояний Spin выполняет редукцию частичных порядков. Её нужно отключить при помощи параметра -DNOREDUCE.
Последний срок сдачи задания -- 15 марта.
С уважением, Константин Савенков.