Лабораторная работа: Задание 3
Описание
Характеристики лабораторной работы
Список файлов
- Задание 3
- Task03.pdf 491,16 Kb
- The Best_ Smallest and Fastest model.xml 5,21 Kb
- answer
- 2014_421_Vasilenko_3.csv 202 b
- 2014_421_Vasilenko_3_1.xml 6,46 Kb
- 2014_421_Vasilenko_3_1_trace.xtr 26 Kb
- 2014_421_Vasilenko_3_3.xml 7,82 Kb
- 2014_421_Vasilenko_3_3_trace.xtr 32,33 Kb
- 2014_421_Vasilenko_3_3u.xml 6,8 Kb
- 2014_421_Vasilenko_3_3u_trace.xtr 25,55 Kb
- 2014_421_Vasilenko_ucomparison.txt 4,95 Kb
- license.txt 0 b
- Централизованное заблуждение.txt 1,08 Kb
- мануал (avasite).txt 2,9 Kb
- Прочти меня!!!.txt 136 b
!!! Поправка к файлам в решении:
У меня 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) Для больших моделей - быстро растёт количество комбинаций и в итоге не хватает памяти для проверки свойств модели
По всей видимости файл пустой
1) Самая короткая трасса действительно самая быстрая по времени выполнения, а потому достаточно в uppaal попросить verify в настройках выдать минимальную трассу.
Нет это не обязательно, но как правило при написании модели она будет такой, что будет выполнино то, что выше.
2) Самая короткая трасса НИ В КОЕМ СЛУЧАЕ НЕ ОБЯЗАНА являться лучшей с точки зрения простоев процессоров.
Пример:
номер работы / время выполнения на процессоре 1 / 2
1 100 30
2 70 100
Самое короткое (по времени работы) - это чтобы 1-й проц выполнил 2-ю работу, а 2-й - 1-ю
Самое минимальное по простоям - это чтобы 1-й проц делал 1-ю работу, а 2-й - 2-ю
Итак, - будьте бдительны
3) Так же пример выше показывает, почему нельзя сразу же при освобождении процесса загружать его - это сильно изменит скорость и количество комбинаций, и программа станет считаться горзадо быстрее и есть меньше памяти.
Но это не правильное решение - тут самая короткая трасса не даёт лучшего решения по простоям процессоров.
Такое решение так же не переберёт все возможные варианты исполнения.
Всем привет,
сегодня я сдавал 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
При копировании или цитировании материалов на других сайтах обязательно используйте ссылку на источник
Начать зарабатывать