Task02 (1158525)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Задание 2.Размеченные системы переходов (LTS) (10 баллов).Формулировка заданияДано:Дан текст программы на языке С с функциями f и g. (см. задание 1)Предполагается, что функции f и g выполняются параллельно, в двух разных потоках управления(процессах) P_f и P_g соответственно.

Будем считать состоянием модели программы совокупностьзначений счѐтчиков команд c_f и c_g процессов P_f и P_g, значения глобальных и локальныхпеременных заданной программы.Требуется:1. (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 балла) Модифицировать программу из п.3 задания 1 так, чтобы при указании параметра «-ltsимя_файла» она строила и сохраняла в указанный файл систему переходов для асинхроннойпараллельной композиции функций f и g в формате dot (для значений входныхпараметров(f.a=1,f.b=2,g.a=3,g.b=4)). Состояния LTS должны быть размечены значениями счётчикауправления, глобальной переменной и локальных переменных x и y. Дуги должны быть размеченывыполняемыми операторами, для операторов ветвления дуги - истинным условием перехода (т.е.для оператора while(x<3) дуга, ведущая в тело цикла, размечается «(x<3)», ведущая на следующийза циклом оператор – «!(x<3)»).

Цвет дуг должен зависеть от того, какой процесс выполнилдействие.3. (2 балла) Считая состоянием программы значение переменной h, построить LTS такой моделипараллельной программы. Состояния LTS должны быть размечены значением глобальнойпеременной h (размечать состояния счетчиком операторов не нужно), дуги – выполняемымиоператорами, приводящими к изменению переменной h (если действие не приводит к изменению h,его отображать в виде дуги не нужно). Полученную LTS записать в формате dot и при помощипрограммного средства dot/GraphViz сгенерировать по ней картинку в формате png.4. (3 балла) Построить модель параллельной программы из первой задачи на языке временныхавтоматов и, запустив верификацию или симуляцию в среде UPPAAL, получить точное значениечисла достижимых состояний этой модели для значений входных параметров(f.a=1,f.b=2,f.c=3,f.d=4)5.

(1 балл) Обоснуйте, почему количество состояний, подсчитанное при помощи системы UPPAAL,отличается от полученного при построении LTS программой из п.2На выполнение задания отводится три недели. Последний срок сдачи задания – 28 октября.Требования к файлам решения:Решение задачи должно включать в себя 12 файлов: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 программы в файле group_surname_2.c,описание сгенерированной ей LTS в формате dot в файле lts_m12.dot и сгенерированную понему картинку в файле lts_m12.png.4.

Описание LTS с состоянием, включающим только значение h, в формате dot в файлеabstract_lts_m12.dot и сгенерированную по нему картинку в файле abstract_lts_m12.png5. Текстовой файл с расширением group_surname_2.xpml с моделью на UPPAAL, текстовойфайл log.txt с тем, что выдал верификатор или симулятор при запуске модели, текстовой файлstates.txt с 1) фразой «Согласно верификатору, у модели – N достижимых состояний», где N -число состояний, выданных верификатором, 2) фразой «В LTS для программы – Mдостижимых состояний», где М – число, выдаваемое программой из п.2 данной задачи и 3)текстом, описывающим разницу между Mи Nи объясняющим (с точностью до состояния) этуразницу.Дополнительная информация:1.

Пример описания LTS в виде графа в формате dot:digraph G {0 [label=”1,#,1”];1 [label=”2,1,1”];2 [label=”4,1,1”];0 -> 1 [label=”h = a;” color=”red”];1 -> 2 [label=”!(h < a)” color=”blue”];}Графический файл в формате png может быть сгенерирован следующей командой(имя_файла_1 – имя файла с картинкой, имя_файла_2 – имя файла в формате dot):>dot -Tpng -o имя_файла_1 имя_файла_2О том, как среди вывода верификатора распознать число состояний модели, можно прочитать вруководствексистемеUPPAAL(например,здесь:http://www.mbsd.cs.ru.nl/publications/papers/fvaan/uppaaltutorial.pdf).

Обратите внимание, что в ходепостроения пространства состояний UPPAAL выполняет редукцию частичных порядков, удалениенезначащих переменных, слияние состояний, накладывает ограничения на порядок завершенияпроцессов.2.3.Еслиразницаравна0,этотоженужнообосновать..

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лабораторной работы