model-checking Май 2013

model-checking@asvk.cs.msu.ru

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

Зачет и экзамены
by model checking course mailing list 24 Май '13

24 Май '13

Дорогие студенты, ПРАКТИКУМ Вчера был "зачет" по курсу, все кто хотел досдали практикум. Зачетные ведомости для АСВК ушли в учебную часть. Зачет был с оценкой, при выставлении оценки я достаточно сильно округлял вверх - но учтите, что на базовый балл это округление не влияет. Несколько человек не получили зачет в силу того, что даже с округлением не набрали на 3 балла (см. в таблице). Скорее всего, для вас на следующей неделе будет комиссия. Как только мне сообщат из учебной части, мы это организуем. Несколько человек не получили зачет в зачетку - вы сможете сделать это на комиссии. На комиссии нужно будет полностью сдать все несданные задания практикума. За это будет выставлено 3 балла (=> на экзамене базовый балл 1) Далее. Есть люди не с АСВК, получившие 2 балла за практикум. Я предлагаю вам также придти на комиссию и повысить свой базовый балл до 1, сдав все задания практикума. АВТОМАТЫ В таблице указано, кто можнет получить оценку "отлично" автоматом (= базовый балл 4). Те, у кого базовый балл = 3, также могут автоматом проставить "3" за экзамен, но я рекомендую попробовать сдать экзамен. Проставить оценки в зачетные книжки можено будет во время комиссии по практикуму на следующей неделе или во время основного экзамена. ДОСРОЧНЫЙ ЭКЗАМЕН К сожалению, достаточно небольшой группы студентов для досрочного экзамена я не вижу. Если кому-то нужен досрочный экзамен в силу того, что у вас сборы итп - напишите мне, мы сделаем так, что вы напишете экзаменационную работу во время комиссии по практикуму на следующей неделе. С уважением, Константин Савенков.

1 0

Прием практикума
by model checking course mailing list 23 Май '13

23 Май '13

Дорогие студенты, Сейчас (14:60) осталось сдавать пятое задание примерно 8 человек. Как только сдаст последний, прием будет прекращен. Поэтому, если вы все же планируете сегодня сдавать практикум, бегите быстрее в МЗ-4. Я буду на ф-те до 17:00 в к 761. С уважением, Константин Савенков.

1 0

Прием 5-го задания практикума в зачетную сессию
by model checking course mailing list 15 Май '13

15 Май '13

Дорогие студенты, День в зачетную сессию - 23 мая, четверг, МЗ-4 забронирован на все пять пар. С уважением, Константин Савенков.

1 0

Семинары 15.05
by model checking course mailing list 14 Май '13

14 Май '13

Дорогие студенты, Семинаров 15.05 не состоится, поскольку у всех ведущих семинары - экзамен по философии. Все, кто не успеет из-за этого что-то сдать, смогут сделать это в выделенный день в зачетную сессию. Что это за день - напишу чуть позже. С уважением, Константин Савенков.

1 0

Model Checking Task 5
by model checking course mailing list 06 Май '13

06 Май '13

??? ?????? ? ??????? ??????? ????????? ? ??????????? ??? ??? ??????: 1. ????????? ???????? ?????????? ??????? (invalid end-states). ??????? ? ?????? ???? ?? ??????. ????? ???????????? ?? ???????? ???????? ????????? ? ????????? ???? ? ?????? task5_safety_out.txt. 2. ? ?????? ?? ?????? ???? ????????????? ???? (unreachable code), ?? ??????????? ???????? ????????? ????????? (-end-). ???? ????? ??? ? ?????? ??????, ????????? ??. 3. ? ?????? ?? ?????? ???? ?????? ??????????? (non-progress cycles), ?? ???????????: 3.1) ?????, ?????????? ? ??????????? ??????????? ???????????? ??????? 3.2) ??????, ??????????????? ?????? ???????????? ???????, ??????? ????? ?????????? ?????????? ????? ????????????. ????? ???????, ???????????, ??????????? ? ?????? (????????, ??????????????? ??? ????????????? ????????? ??????) ?? ?????? ??????? ? ?????? ??????????? ??????. ????? ???????????? ??? ???????? ?????????? ?????? ??????????? ????????? ? ????? ? ?????? task5_nonprogress_out.txt. ????? progress, ??????????????? ??? ????, ????? ??????????? ?? ??????? ???????? ?? ??????????? ?????, ????????????? ? ??????? 3.1 ? 3.2, ?????? ???? ??????????? ? ?????? model_assert.pml. 4. ????????????? ???? ???????? ??????? ? ??????? ?????? ????????? ??????? ? ??????? Spin, ????????? ? ??????? Spin. ??? ???? ?? ?????? ?????????????? ?????-???? ??????????????? ??????????. ???????????? ????????? ? ????? ? ??????? spec.ltl: 4.1. ? ???? ?????????? ???? ??????? ???? ??? ?????? ?????????? ??????? ??????? ??????? ??? ?????? ?????????? ??????*alloc*. 4.2. ? ???? ?????????? ???? ??????? ????? ????????? ??????? ??????? ???? ??? ?????? ?????? ????????????? ??? ?????? ??????*free*, 4.3. ?? ?????? ????? ????????? ??????? ????????? ? ???????????? ??????? ??????????? ???????? ?????? ?? ????????? ????????. 4.4. ? ??????????? ?????? (????? ???????? spin_lock* ? spin_unlock*) ????? ?????????? ?? ????? ?????? ????????. 4.5. ? ???? ?????????? ???? ???????, ??????? kfree ?????????? ?? ????? ?????? ????. ????????, ??? ???????? ???????? ??????? ?????? ???????? ????????: ????????? ??????, ???????? ??????? ???????????, ???????? ????????? ??????, ?? ???????? ? ??????, ??-??????? ??????? ???????? ??????? ? ??????????? ?????? ???. 5a. ? ??????, ???? ?????? ???????? ????????: - ???????, ?????? ???????????? ?? ??????????? ?? ???????? ??????; - ???????, ??? ?????????? ?????? ? ??????; - ???????, ?????? ????? ?????? ?????????; - ????????? ???????????, ???????? pan, ? ????? counterexample.txt; - ????????? ???????? ? ?????????? ?????? ? ?????? task5.pml ? task5_modified.pml; - ????????? ????? pan ? ????? task5_ver_out.txt. 5b. ? ??????, ???? ???????????? ?? ??????????? ?? ??????: - ????????? ???????????, ???????? pan, ? ????? counterexample.txt; - ????????? ?? ???????????? Spin ??????????? ?? ???????? ?????????; - ????????? ? ???, ??? ??????????? ?? ???????? ????????? ???????????; - ????????? ??????????? ?? ???????? ????????? ? ????? prog_counterexample.txt. ??????????? ?????? ???? ?????? ? ???? ?????????????????? ??????? ????? ???????? ????????? ? ???????? ??????????. - ????????? ?????? ? ????? task5.pml; - ????????? ????? pan ? ????? task4_ver_out.txt. - ??????? ??????????????? ???? ?? ????????????? (????????, «spec_1.ltl») ??? ???????? ?????????? ???????. 5c. ? ??????, ???? ????????? ? ?????? ?? ????????????? ? ???????????? ???????????: - ????????? ?????? ? ????? task4.pml; - ????????? ????? pan ? ????? ver_out.txt. ??????e ????? ????? -- "????????" ???? ? ???????? ?????? (?????????? ???? ?????? ?????). ??????? ?? ????????? ? ?????? ?????? ?? ?????, ?? ???? ?? ?? ??????? ???????/????? ??????? ? ????? ????????? ???, ????? ????? ?? ??????????? ??????? ???????. ? ?????????, ?????????? ????????.

1 0

Re: [model-checking] Лекция 6.05.13
by model checking course mailing list 06 Май '13

06 Май '13

Дорогие студенты, Простите, если кто-то пришел в пустую аудиторию, я полагал, что в конце прошлой мы обсудили - следующая будет после праздников. Соответственно, она будет 13-го мая. Будет контрольная по последней лекции, а затем я кратко пройдусь по всему курсу. С уважением, Константин Савенков. On 5/6/13 12:55 AM, Валерий Бицоев wrote: > Здравствуйте! > Я слегка запутался, слышал противоречивые мнения, подскажите > пожалуйста, будет ли завтра(06.05.13) лекция/консультация по > верификации на первой паре? > > -- > С уважением, > Бицоев Валерий

1 0

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

model-checking Май 2013