model-checking

model-checking@asvk.cs.msu.ru

130 обсуждения

Проблемы с занятиями в понедельник
by model checking course mailing list 25 Мар '13

25 Мар '13

Дорогие студенты, Сегодня два разных ДТП стали причиной отмены и лекции, и семинара у 424 группы. Лекцию я вам расскажу в следующий раз, а те, кто не успел сдать 2-е задание сегодня, могут сделать это либо на семинарах других групп, либо в следующий понедельник. То же с теми, у кого задолженность по первому заданию. На дедлайн по сдаче заданий на почту это, естественно, не распространяется. Если вы что-то присылали по 1 заданию, а в таблице оно не отмечено - напишите, пожалуйста, об этом. С учетом того, что жесткий дедлайн по первому заданию сегодня - учтите, если вы не пришлете копию сданного на семинаре решения, ваш балл будет аннулирован. С уважением, Константин Савенков.

1 0

Model Checking Task 2
by model checking course mailing list 11 Мар '13

11 Мар '13

??????? ????????, ?????? ??????? ?? ?????????? ??????? ?? ??????? ??????. 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,g.a=3,g.b=4)). ????????? LTS ?????? ???? ????????? ?????????? ???????? ??????????, ?????????? ?????????? ? ????????? ?????????? x ? y. ???? ?????? ???? ????????? ???????????? ???????????, ??? ?????????? ????????? ???? - ???????? ???????? ???????? (?.?. ??? ????????? while(x<3) ????, ??????? ? ???? ?????, ??????????? «(x<3)», ??????? ?? ????????? ?? ?????? ???????? -- «!(x<3)»). ???? ??? ?????? ???????? ?? ????, ????? ??????? ???????? ????????. 3. ?????? ?????????? ????????? ???????? ?????????? h, ????????? LTS ????? ?????? ???????????? ?????????. ????????? LTS ?????? ???? ????????? ????????? ?????????? ?????????? h (????????? ????????? ????????? ?????????? ?? ?????), ???? -- ???????????? ???????????, ??????????? ? ????????? ?????????? h (???? ???????? ?? ???????? ? ????????? h, ??? ?????????? ? ???? ???? ?? ?????). ?????????? LTS ???????? ? ??????? dot ? ??? ?????? ???????????? ???????? dot/GraphViz ????????????? ?? ??? ???????? ? ??????? png. 4. ????????? ?????? ???????????? ????????? ?? ?????? ?????? ?? ????? Promela ?, ???????? ??????????? ? ????? SPIN, ???????? ?????? ???????? ????? ?????????? ????????? ???? ?????? ??? ???????? ??????? ?????????? (f.a=1,f.b=2,f.c=3,f.d=4). 5. ?????????, ?????? ?????????? ?????????, ???????????? ??? ?????? ??????? Spin, ?????????? ?? ??????????? ??? ?????????? LTS ?????????? ?? ?.2. ????? ?? ???????: * LTS ????????? ????????? - 10 * ?????????, ???????? LTS - 25 * ??????????? LTS (????????? - ???????? h) - 20 * ?????? ?? promela - 25 * ??????????? ??????? ? ?????????? ????????? - 20 ?????: 100 ?????? ?? ?????????? ??????? ????????? ??? ??????, ?? ???? ?????? ????? -- 25-29 ?????. ?????????? ? ??????? ??????? ?????? ?????? ???????? ? ???? ????????? ????? (????? 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.png. 5. ????????? ???? ? ??????????? group_surname_2.pml ? ??????? ?? Promela, ????????? ???? 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 2. ? ???, ??? ????? ?????? ???????????? ?????????? ????? ????????? ??????, ????? ????????? ? ??????????? ? ??????? Spin (????????, ?????: http://spinroot.com/spin/Man/Pan.html#L9). ???????? ????????, ??? ? ???? ?????????? ???????????? ????????? Spin ????????? ???????? ????????? ????????, ???????? ?????????? ??????????, ??????? ?????????, ??????????? ??????????? ?? ??????? ?????????? ?????????. ????? ???????? ?? ???? ????? ?????????? ?? ????? ?? ????????? ??????. 3. ???? ??????? ????? 0, ??? ???? ????? ?????????? :-)

1 0

Сроки сдачи первого задания и ещё
by model checking course mailing list 04 Мар '13

04 Мар '13

Дорогие студенты, 1. Проясняю вопрос со сроками сдачи работ. У каждой группы на это отводится три семинара, начиная с семинара на той неделе, когда было выслано задание. То есть дедлайны выглядят следующим образом: 424-425 - 11.03, 422 и 427 - 13.03 420 и 421 - 14.03, 428 - 15.03 При этом у 428 группы пропадает семинар в эту пятницу, 8 марта. Для того, чтобы это компенсировать, 428 группа может выполнять и сдавать задания также 11.03 и 13.03. Две недели после дедлайна считаются со дня выдачи, то есть жесткий дедлайн по первому заданию для всех групп - 25 марта. 2. Как и было объявлено на лекции, сданные на семинаре решения нужно присылать на адрес model-checking(a)lvk.cs.msu.su для учета, контроля и проверки на плагиат. 3. Результаты контрольных работ и приема практикума появляются в таблице https://docs.google.com/spreadsheet/ccc?key=0AjDKRN6Wzv9_dHZ2aExQSVNFYXN0aX… (статика - на https://docs.google.com/spreadsheet/pub?key=0AjDKRN6Wzv9_dHZ2aExQSVNFYXN0aX…). С уважением, Константин Савенков.

1 0

Проставление оценок
by model checking course mailing list 03 Июл '12

03 Июл '12

Дорогие студенты, Проставление оценок по итогам первой пересдачи будет проходить завтра, с 11:00 до 11:30 в к.761. С уважением, Константин Савенков.

1 0

Проставление оценок и пересдача
by model checking course mailing list 15 Июн '12

15 Июн '12

Дорогие студенты, Ведомости закрыты. Часть студентов не подошла с зачетными книжками. Я могу предложить вам устроить ещё одну сессию раздачи автографов -- в произвольный из дней следующей недели с 9 до 10 утра. Давайте по умолчанию это будет среда 20-го июня. Если у кого-то не получается, передайте зачетку с товарищами. Если у всех не получается -- напишите, обсудим. Пересдача будет проходить аналогично основному экзамену и случится ориентировочно 3-4 июля (раньше меня не будет в РФ). Уточните в учебной части. С уважением, Константин Савенеков.

1 0

Результаты экзамена 13.06
by model checking course mailing list 14 Июн '12

14 Июн '12

Все работы проверены, результаты в таблице, жду вас завтра с 9 до 11 в к.761. С уважением, Константин Савенков.

1 0

Проставление оценок и аппеляция для сдававших 11 и 13 июня
by model checking course mailing list 13 Июн '12

13 Июн '12

Дорогие студенты, К сожалению, я не смогу проставить оценки сегодня в 13:00. Также, возможно, сегодня будут проверены не все работы. Работы сдающих сегодня будут проверены ориентировочно к вечеру 14 июня. Проставление оценок и апелляция для сдававших 10, 11 и 13 июня пройдет 15 июня в ауд.761. С уважением, Константин Савенков.

1 1

Выложены результаты проверки 11.06
by model checking course mailing list 11 Июн '12

11 Июн '12

Там же. Апелляция и проставление -- 13-го июня в 13:00 в к.761. С уважением, Константин Савенков.

1 0

Результаты проверки 10.06
by model checking course mailing list 11 Июн '12

11 Июн '12

Дорогие студенты, Результаты проверки экзамена групп 421-422 выложены третьей вкладкой в таблице https://docs.google.com/spreadsheet/ccc?key=0AhbmHMR5VBIJdFgwcVFnNF9vd3pSdH… Я постарался максимально подробно описать причины, по которым за те или иные задания снижена оценка. В большинстве случаев вам нужно обратиться к лекционному материалу и посмотреть, как надо. Если, тем не менее, вы полагаете, что вы правы -- подходите завтра к 13:00 к комнате 761 на апелляцию. Подчеркиваю -- не узнать, что не так (это написано в таблице) - а если вы полагаете, что при проверке допущена ошибка и ваша оценка должна быть повышена. Собственно, давайте завтра и проставим эти оценки в ведомости и зачетные книжки. Подходите туда же, куда на апелляцию. С уважением, Константин Савенков.

1 0

Re: [model-checking] Порядок экзамена + про тех, кто на пересдачу
by model checking course mailing list 08 Июн '12

08 Июн '12

> > А можно уточнить один вопрос, который будет интересен многим: если не > отвечать на доп.вопрос, то это грозит 0 баллов или -0.5? Нижняя планка. > > P.S. если набрать баллов, скажем на 2 больше, чем максимальная оценка, > это может повлиять на финальное решение, т.е. получить на балл выше > "максимально возможной" (макс.оценка = 3, со всеми доп.вопросами > набираем 5,5)? Может, но скорее всего не повлияет. С уважением, Константин Савенков. > > 8 июня 2012 г., 11:50 пользователь model checking course mailing list > <model-checking(a)lvk.cs.msu.su <mailto:model-checking@lvk.cs.msu.su>> > написал: > > Дорогие студенты, > > Для тех из вас, кто не был на консультации, сообщаю, как будет > проходить экзамен. > > Экзамен письменный. > > На экзамене вы получите следующие вопросы (в скобках указан > диапазон баллов, которые можно получить за ответ на вопрос - > [fail,win]): > - вопрос из первой половины списка вопросов (0..1) > - вопрос из второй половины списка вопросов (0..1) > - дополнительный вопрос (0..0.5) > - задача на LTL (-0.5..0.5) > - по одному дополнительному вопросу (-0.5..+0.5) за каждую > контрольную, за которую в семестре вы получили -1 (вопрос по > тематике контрольной) > > Да, при очень плохом ответе можно получить оценку меньше базового > балла. > > Да, базовый балл можно проставить в зачетку, не сдавая экзамена > (хотя я не рекомендую). > > Время на написание ответов - 2 часа. Пользоваться можно только > ручкой и головой, бумагу вам выдадут. Телефоны, вещи и разные > полезные гаджеты остаются при входе в аудиторию. Во время > написания ответов консультироваться с другими студентами нельзя, > списывать также нельзя. Выход из аудитории сопровождается > сдаванием работы. Нарушение этих правил влечет удаление с экзамена > и выставление оценки неуд. > > Мы постараемся проверить работы в тот же день и выложить > комментарии. Проставление оценок будет проходить в дополнительный > день после экзаменов (или на последующих экзаменах других групп). > Аппеляции -- строго в отдельный день. > > Важное дополнение, про которое я не сказал на консультации. > Студенты, получившие базовый балл -1 и не допущенные к сдаче > экзамена -- приходите на него, вам будет выдана контрольная по > мотивам практикума, по результатам проверки которой вы будете > допущены к следующей пересдаче. Или, при неудаче, будете там > писать такую же контрольную. > > С уважением, > Константин Савенков. > _______________________________________________ > model-checking mailing list > model-checking(a)lvk.cs.msu.su <mailto:model-checking@lvk.cs.msu.su> > https://lists.lvk.cs.msu.su/cgi-bin/mailman/listinfo/model-checking > >

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking