Для студентов МГУ им. Ломоносова по предмету Надёжность программного обеспеченияЗадание 3Задание 3 2019-09-18СтудИзба

Лабораторная работа: Задание 3

Описание

Описание файла отсутствует

Характеристики лабораторной работы

Учебное заведение
Семестр
Просмотров
41
Скачиваний
1
Размер
446,17 Kb

Список файлов

2014_421_Vasilenko_ucomparison

!!! Поправка к файлам в решении:

У меня uppaal не сохраняет queries в файл, т.к. падает, поэтому мои queries сохранены xml файл.

(так же они объяснены и продублированны ниже)

Однако я добавил 2 файла - трассы, которые имеют минимальную длинну расписания (их можно открыть в uppaal)

Ещё я поджал количество состояний в модели 3_3 - по сравнению с моделью 3_1, что сильно помогло в подсчёте через verifyta, я обозвал файлы 3_3u - приложил к ответу (хотя это и не помогло запустить 3 на 9, хоть и пытался)

Поведение verifyta (количество требуемых ресурсов) (время для одного ядра моего процессора - 2,4ГГц):

Для первых 6 процессов - работает нормально и достаточно быстро (меньше минуты)

Для первых 7 процессов - работает нормально, но достаточно долго (минут 5) (требует достаточно много памяти - где-то 3-4 гига оперативной памяти)

Для первых 8, 9 процессов - ему не хватает даже 5 гигов памяти, он их выедает и падает

В связи с проблемами с возможностями аппараруты моё задание было переформулированно и вместо 3-х процессоров, я работаю на 2-х.

Особенность моей модели:

Дело в том, что если verifyta попросить выдать мне самую короткую трассу (в моей модели), то автоматически это будет та трасса, которая выполняется быстрее всего, т.е. мне автоматически выдадут после прогона трассу, в которой самое быстрое выполнение.

(Если поставить Options->DiagnosticTrace->Shortest)

Поэтому для вычисления в верификации я испольховал выражение:

E<> (solvedJobs[1]==1 && solvedJobs[2]==1 && solvedJobs[3]==1 && solvedJobs[4]==1 && solvedJobs[5]==1 && solvedJobs[6]==1 && solvedJobs[7]==1 && solvedJobs[8]==1 && solvedJobs[9]==1)

Вместе с просьбой uppaal выдать самую короткую трассу - даст нужную трассу, если вы считаете минимальное время

Проверка свойств:

Для того, чтобы проверить, что все работы выполняются при всех возможных комбинациях:

E<> (solvedJobs[1]==1 && solvedJobs[2]==1 && solvedJobs[3]==1 && solvedJobs[4]==1 && solvedJobs[5]==1 && solvedJobs[6]==1 && solvedJobs[7]==1 && solvedJobs[8]==1 && solvedJobs[9]==1)

Т.е. всегда для любой трассы найдётся состояние, в котором все задачи будут выполнены (это правило совпадает с правилом выше)

(моя модель построена так, что после выполнения всех задач - она останавливается)

Для того, чтобы угадывать время, при котором всё ещё есть трасса, на которой выполняется свойство:

E<> (time > 40 && (solvedJobs[1]==1 && solvedJobs[2]==1 && solvedJobs[3]==1 && solvedJobs[4]==1 && solvedJobs[5]==1 && solvedJobs[6]==1 && solvedJobs[7]==1 && solvedJobs[8]==1 && solvedJobs[9]==1))

(т.е. на любом пути существует событие, когда все задачи уже выполнены, а время больше 40, тогда если пороговое значение 40 - минимальная трасса, то для неё это свойство не будет выполняться, и тогда verifyta выдаст нам not satisfied, в то время, как для 41 - выдаст satisfied, что и будет значить, что 40 - наш порог)

(но я буду использовать особенность моей модели, описанную выше для получения минимального времени и трассы сразу)

пункт 2 (потребовал около 2-х гигов памяти):

Видел что при случайном симулировании в симуляторе - можно выполнить за 33 шага процессора.

Проверка свойств описана выше - свойства выполнены

Самое быстрое - 24 тика.

Пример трассы:

012345678901234567890123

cpu0 - BCCCCCCCC FFFFFFFFFFFFFF

cpu1 - AAEI DGGGGGGGGGGHH

При различных способах обхода дерева - в глубину и в ширину:

Т.к. нужно проверить свойство для каждой трассы - то приходится всё равно перебирать все возможные варианты, и потому скорость не сильно меняется, но важно количество используемой памяти - в случае, когда используется обход в глубину используется меньшее количество памяти, что важно.

пункт 4:

Момент времени отказа - 15

Видел что при случайном симулировании в симуляторе - можно выполнить за 31 шага процессора.

Проверка свойств описана выше

Самое быстрое - 28 тиков.

Пример трассы:

0123456789012345678901234567

cpu0 - BCCCCCCCC FFFFF FFFFFFFFFFFF

cpu1 - AAEI DGGGGGGGGGGHH

Замечу, что тут нумерация следующая:

с нуля

ошибка на процессоре происходит после момента отказа (поэтому в качестве момента отказа я в модели указал 14)

При различных способах обхода дерева - в глубину и в ширину:

Т.к. нужно проверить свойство для каждой трассы - то приходится всё равно перебирать все возможные варианты, и потому скорость не сильно меняется, но важно количество используемой памяти - в случае, когда используется обход в глубину используется меньшее количество памяти, что важно.

Возможности UPPAAL:

1) автоматизации несколько не хватает, для сбора всякого рода статистики, ...

2) Мощное, но постоянно что-то там падает (мне приходилось стыковать verifyta на винтуальном линуксе с работой java под windows)

3) Для больших моделей - быстро растёт количество комбинаций и в итоге не хватает памяти для проверки свойств модели

license

По всей видимости файл пустой

Централизованное заблуждение

1) Самая короткая трасса действительно самая быстрая по времени выполнения, а потому достаточно в uppaal попросить verify в настройках выдать минимальную трассу.

Нет это не обязательно, но как правило при написании модели она будет такой, что будет выполнино то, что выше.

2) Самая короткая трасса НИ В КОЕМ СЛУЧАЕ НЕ ОБЯЗАНА являться лучшей с точки зрения простоев процессоров.

Пример:

номер работы / время выполнения на процессоре 1 / 2

1 100 30

2 70 100

Самое короткое (по времени работы) - это чтобы 1-й проц выполнил 2-ю работу, а 2-й - 1-ю

Самое минимальное по простоям - это чтобы 1-й проц делал 1-ю работу, а 2-й - 2-ю

Итак, - будьте бдительны

3) Так же пример выше показывает, почему нельзя сразу же при освобождении процесса загружать его - это сильно изменит скорость и количество комбинаций, и программа станет считаться горзадо быстрее и есть меньше памяти.

Но это не правильное решение - тут самая короткая трасса не даёт лучшего решения по простоям процессоров.

Такое решение так же не переберёт все возможные варианты исполнения.

мануал (avasite)

Всем привет,

сегодня я сдавал 3-е задание Волканову и я с ним долго резвился на разные темы, в итоге

1) Моё решение вы можете уже найти рядом

2) Он просил передать вам, что делать так, как сделал я - ещё дополнительно заведя таймер, для того, чтобы связать время с выполнением задач на процессорах, и чтобы не было лишнего увеличения времени - нельзя. Скажу вам, что это не беда, ибо можно легко заменить это дело глобальными переменными.

3) Для тех, кто не уловил сразу фишку с каналами (channels)

1) их уместнее было бы называть флагами, и у них есть 3 режима и 2 способа использования

2) flagName! - поднимает флаг, flagName? - ждёт, пока кто-нибудь поднимет его

3) обычный флаг достаточно поднять один раз, чтобы потом на нём никто не останавливался

4) urgent флаг - нужно поднимать каждый раз заново

5) broadcast флаг - сами догадайтесь

6) когда 2 процесса - один, который ждёт поднятия флага, другой - поднимает его, то при поднятии, второй процесс не медленно передвигается, делая шаг, причём update на соответствующих рёбрах графа срабатывают сначало для того, кто поднял флаг, а потом для того, кто его ждал (в случае с broadcast - смотрится среди тех, кто ждал, в каком порядке были запущенны процессы в system команде)

Каналы полностью заменяемы глобальными переменными, но с ними частенько удобнее

Из каналов можно построить 2 концепции: семафоры (двоичные) и mutex (хотя разница конечно не большая) )

У меня вы найдёте концепцию mutex, но что делать - ваше дело.

3) у меня так сделано, что есть broadcast флаг отвечающих за тик, для всех процессоров, логично, что чем больше процессоров сделает тик, тем быстрее можно выполнить все работы, так что полезно сделать так же, и тогда в verifyta можно будет просто указать - выдать в конце самую короткую трассу, и тогда вы сразу вычислите минимальное время для расписания.

(стоит подумать о разнице между самым быстрым выполнением задач и самым малым простоем процессоров, и как это отразится на модели )) (по мне - так никак, вопрос лишь в том, что вы будете писать в своём ответе - нужно будет указать на то или другое))

другой способ выяснить лучшее расписание - описан у него в кратце и чуть подробнее в моём файле отчёта - там достаточно, чтобы вы поняли, как это делать и могли сделать свой выбор

4) Он дал (по крайней мере мне) 3 процессора и 9 задач, проблема в том, что просчёт моей модели by verifyta занимал больше 5 гигов памяти, которые я мог выделить и после выедания этих гигов, спустя эдак 15 минут - verifyta падает.

Он вам вскоре должен разослать поправки к заданию, где уменьшит количество чего-нибудь (мне он сократил количество процессоров до 2-х)

Правда частично я - лопух, потому что можно было бы улучшить результат, например слив первые 3 шага в моей модели задачи в одну ветвь, но погоды это не делает, потому что 3x9 - это просто эпичное количество состояний.

(но более компактная модель сохранена мною как 3_3u)

Вот так, как-то.

Прочти меня!!!

Файл скачан с сайта StudIzba.com

При копировании или цитировании материалов на других сайтах обязательно используйте ссылку на источник

Картинка-подпись
Хочешь зарабатывать на СтудИзбе больше 10к рублей в месяц? Научу бесплатно!
Начать зарабатывать

Комментарии

Поделитесь ссылкой:
Рейтинг-
0
0
0
0
0
Поделитесь ссылкой:
Сопутствующие материалы
Свежие статьи
Популярно сейчас
Как Вы думаете, сколько людей до Вас делали точно такое же задание? 99% студентов выполняют точно такие же задания, как и их предшественники год назад. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Нашёл ошибку?
Или хочешь предложить что-то улучшить на этой странице? Напиши об этом и получи бонус!
Бонус рассчитывается индивидуально в каждом случае и может быть в виде баллов или бесплатной услуги от студизбы.
Предложить исправление
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
5076
Авторов
на СтудИзбе
455
Средний доход
с одного платного файла
Обучение Подробнее