model-checking Март 2013

model-checking@asvk.cs.msu.ru

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

Проблемы с занятиями в понедельник
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

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Март 2013