model-checking Март 2010

model-checking@asvk.cs.msu.ru

1 участники
9 обсуждения

Замечания по третьему заданию
by model checking course mailing list 26 Мар '10

26 Мар '10

Дорогие студенты, Пожалуйста, используйте inline для более наглядного представления lock и unlock в модели. То же самое, в принципе, можно сделать и с malloc/free. С уважением, Константин Савенков.

1 0

Анонимные работы
by model checking course mailing list 25 Мар '10

25 Мар '10

Дорогие студенты, Контрольные проверены. Двое из вас, похоже, не успели подписать свои работы -- определитесь, кто это был. С уважением, Константин Савенков.

1 0

Сроки сдачи 2-го задания
by model checking course mailing list 17 Мар '10

17 Мар '10

Дорогие студенты, Поскольку третье задание для вас пока не готово, мы решили продлить сроки сдачи второго задания на семинаре, чтобы вы не скучали. Таким образом, НА ЗАНЯТИЯХ ПРАКТИКУМА вы можете сдавать второе задание по следующий понедельник (22 марта) включительно. Сдача "по почте" возможна, но со штрафом за просроченное задание. С уважением, Константин Савенков.

1 0

Разбирая почту
by model checking course mailing list 16 Мар '10

16 Мар '10

Дорогие студенты, В табличку внесена информация о присланных и сданных работах. Обратите внимание, что у многих присланы не все файлы -- то ли по ошибке, то ли намеренно. Если по ошибке -- пришлите их, но не в отдельном письме, а письмом, содержащим все 14 файлов. С уважением, Константин Савенков.

1 0

Ещё по поводу плагиата
by model checking course mailing list 03 Мар '10

03 Мар '10

По просьбам трудящихся, уточняю. Конкретно меня интересует вопрос авторства следующих работ: 1. Багрова-Сухаренко-Чеботарёв-Летунов-Шаповалов 2. Шахрай-Хайруллин 3. Староверов-Тарасенко 4. Колосов-Кравец С уважением, Константин Савенков.

1 0

Комментарий ко второму заданию
by model checking course mailing list 03 Мар '10

03 Мар '10

Дорогие студенты, Появились вопросы -- отчечаю. В п.3. нужно упростить программу, и в ходе построения LTS размечать состояния счётчиками и операторами _новых_ (упрощённых) функций. В ходе упрощения, естественно, нужно выкидывать переменные и операторы, не влияющие на h. С уважением, Константин Савекнов.

1 0

Результаты проверки на плагиат
by model checking course mailing list 02 Мар '10

02 Мар '10

Уважаемые студенты, Проверка на плагиат принесла интересные результаты. Я предлагаю следующий сценарий. Те, кто заимствовал у своих друзей и подруг часть программного решения, в течение следующих двух дней пишут объяснительные записки. В записке указывается, что автор знал о том, что списавший заимствовал у него код и разрешил это сделать без указания ссылки на себя. Объяснительная распечатывается, подписывается обоими и сдаётся мне в к.761. В противном случае я делаю вывод о том, что автор решения не знал о том, что у него списывали. Здесь мы имеем дело с присвоением результатов чужого труда и права авторства (не путать с копирайтом). Дальше вопрос будет решаться на уровне Б.И.Березина с формулировкой "за поведение, недостойное студента МГУ". С уважением, Константин Савенков.

1 0

Обработка присланных решений задания 1
by model checking course mailing list 02 Мар '10

02 Мар '10

Уважаемые студенты, В табличку (http://spreadsheets.google.com/pub?key=tW03VzK1KKvy0R_M2qe8FFg&output=html) выложена информация о том, кто прислал решения 1 задания практикума. Проверяйте, что всё отправленное вами дошло. Немного статистики: - получили задания 134 человека - прислали решение 107 человек - непреверенных решений 45. Задания будут проверены в обозримом будущем, а пока написанные вами программы отправляются в систему проверки плагиата. Теперь по поводу частичной сдачи заданий. Кто-то не написал программу, кто-то вообще пока ничего не прислал. Программа потребуется вам для 2-го задания (вы его уже получили). Поэтому -- если вы успешно сдадите 2-е задание, то неприсланная программа в 1-м выльется в штраф на оценку, не более того. Для того, кто её вообще не напишет, оба задания не будут зачтены, поскольку это -- одна из основных частей 1-2 заданий. С уважением, Константин Савенков.

1 0

Model Checking Task 2
by model checking course mailing list 01 Мар '10

01 Мар '10

Господа и дамы, Второе задание по практикуму состоит из четырёх частей. Описание ниже, если найдёте опечатки или непонятные моменты -- пишите! 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 марта. С уважением, Константин Савенков.

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Март 2010