Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL, страница 14
Описание файла
PDF-файл из архива "Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ - языки MSC и SDL", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 14 страницы из PDF
37).Символ соединенияРис. 37. Символ соединенияДля редактирования соединения нажмите кнопку мыши внутри нужноготекстового поля и введите имя канала.9.3.2. Создание диаграммы блока по существующей копии93В результате упражнений данного урока вы должны научиться следующему:• Создавать диаграмму по существующей копии• Сохранять диаграмму в новом файлеДиаграмму блока GameBlock вы создали, сделав двойной щелчокмышью по символу блока в Организаторе. Заметим, что команда Edit можетбыть выполнена также при двойном щелчке на символ блока в редактореSDL диаграмм (т.е.
на диаграмме системы).ДлясозданияблокаDemonBlockвыполнитеследующуюпоследовательность операций:1. Выберите символ блока DemonBlock в Организаторе или в редакторе.Сделайте двойной щелчок мышью по этому символу. Появится диалогредактирования Edit:Рис. 38. Диалог создания блока DemonBlockСоздадим блок путем копирования уже существующего файла. Имядиректории $examples/demongame. Имя файла, содержащего блокDemonBlock demonblock.sbk2. Убедитесь в том, что установка Copy existing file включена.3. Укажите файл, содержащий блок DemonBlock одним из следующихспособов:94- введите полный путь к файлу (включая директорию); либо- Нажмите на кнопку folder справа от текстового поля ввода. Появитсястандартный диалог выбора файла с названием Select File to Copy BlockDemonBlock.- Для перемещения по директориям нужно сделать двойной щелчокмышью по директории.
Файл demonblock.sbk должен появиться на левойпанели. Выберите этот файл и завершите операцию, нажав кнопку OK.4. Завершите диалог Edit, нажав на кнопку OK. Редактор откроет диаграмму втекущем окне редактирования.Рис. 39. Диаграмма блока DemonBlock5. Теперь, сохраните диаграмму (нажмите «быструю клавишу» Save).Появится диалог выбора файла.
Система SDT предложит имя файлаDemonBlock.sbk.6. Завершите операцию, нажав кнопку OK.9.4. Работа с несколькими диаграммами95Вы создали две SDL диаграммы. Обе диаграммы открыты в редактореSDL диаграмм, хотя показывается только одна из них.В редакторе имеется меню Diagrams, в котором находится список всехоткрытых диаграмм и отдельных страниц.1. Выберите меню Diagrams. Меню должно содержать две строки:Рис.
40. Меню открытых диаграммКаждая строка в меню соответствует одной диаграмме и странице, открытойв редакторе. Справа показано имя файла, в котором сохранена диаграмма.9.5. Диаграммы процессов9.5.1. Создание диаграммы процессаВы создали все структурные элементы SDL системы. Теперь нужно описатьповедение системы, т.е. создать графы процессов.9.5.2. Редактирование диаграммы процесса DemonВ результате выполнения упражнений данного урока вы должны научиться:• Добавлять символы по двойному щелчку мыши;• Работать с буфером копирования;• Вставлять символы в участок;• Получать информацию о грамматике языка SDL;Диаграмма процесса Demon приведена на Рис.
41.96Рис. 41. Диаграмма процесса Demon1. Когда появится диалог добавления страницы, задайте тип новой страницыGraph Page.Рис. 42. Установка типа страницы для диаграммы процесса972. Редактор SDL диаграмм создает диаграмму процесса. Обратите внимание,что палитра символов выглядит иначе, чем при редактированиидиаграммы блока.Как показано на Рис.
41, диаграмма состоит из двух участков. Редакторможет автоматически соединять символы линиями при добавлении новыхсимволов к участку. Каждый символ на диаграмме содержит определенныйтекст. Текст можно вводить в любое время, например, сразу после созданиянового символа или после того, как созданы все символы.9.5.2.1.1 Создание левого участкаДля создания левого участка нужно выполнить следующие операции:1. Выбрать стартовый символ из палитры символов и поместить его вобласть редактирования.2. Сделайте двойной щелчок мышью по символу действия.
Пустой символдействия будет добавлен к стартовому символу.3. Для ввода теста в символ действия воспользуемся контекстнойинформацией по грамматике языка SDL.Выберите команду Grammar Help из меню Windows. Появится окноинформации по грамматике SDL.Рис. 43. Окно информации по грамматике SDL98Список на левой стороне окна описывает несколько «ситуаций»использования текущего символа. Верхний элемент списка – GRAMMAR– описывает полную грамматику для текущего символа.В верхней части на правой стороне окна содержатся ссылки на стандартязыка SDL. Далее на этой панели приводятся предложения БНФ для всехконструкций, допустимых для данного символа.4. Выберите «ситуацию» установки таймера (set).Теперь на правой стороне окна показана БНФ для установки таймера:SET(Now+Expr,TimeName).Рис.
44. Грамматика для установки таймера5. Для ввода конструкции в текущий символ выберите команду Insert изменю Edit. Более быстрый способ ввода текста в символ – двойной щелчокмышью по названию «ситуации» в списке на левой стороне окна.6. Замените имена нетерминалов Expr и TimerName на конкретныевыражения (1 и T, соответственно). Для редактирования участка текстаможно использовать окно редактирования текста. Выделите мышьюучасток, подлежащий изменению, и введите новый текст.99Рис. 45.
Окно редактирования текстаДля закрытия окна информации по грамматике выберите команду Close вменю File.7. Завершите создание участка, сделав двойной щелчок по символусостояния. Введите текст: Generate.Создание правого участкаДля создания правого участка нужно выполнить следующие операции:1. Скопируйте символ состояния в буфер.
Команды работы с буферомнаходятся в меню Edit или в отдельном меню, всплывающем при нажатииправой кнопки мыши.2. Вставьте копию символа из буфера, выполнив команду Paste. Поместитеновый символ и завершите операцию, нажав левую кнопку мыши.3. Добавьте символ ввода сигнала двойным щелчком мыши. Введите текст:T.4. Добавьте символ посылки сигнала двойным щелчком мыши. Введитетекст: Bump.5. Скопируйте символ действия с текстом SET(NOW + 1, T).6.
Сделайте текущим символ посылки сигнала Bump. Нажмите правуюкнопку мыши и выберите команду Insert Paste. Данная командаодновременно копирует символ из буфера и добавляет его к участку.7. Завершите создание участка, сделав двойной щелчок мышью по символусостояния. Введите текст: -.8. Добавьте текстовый символ и введите определение таймера T.9. Сохраните диаграмму.9.5.3. Редактирование процесса GameУпражнения данного урока помогут вам научиться:- Редактировать параллельные участки- Соединять символы100Создайте диаграмму процесса Game. Окончательный вид диаграммыпроцесса Game приведен на рисунке 34.Рис. 46. Диаграмма процесса GameРедактирование стартового перехода1. Создайте стартовый символ, символ действия и символ состояния Losing.2. Теперь будем добавлять два параллельных символа ввода сигналов.Убедитесь в том, что символ состояния является текущим.
Нажмите101клавишу <Shift> и, не отпуская ее, сделайте два двойных щелчка мышьюпо символу ввода сигнала в палитре символов.3. Отпустите клавишу <Shift> и сделайте текущим левый символ вводасигнала.4. Введите имя сигнала Probe и завершите левый участок.5. Выберите правый символ ввода сигнала. Введите имя сигнала Bump изавершите прямую ветвь правого участка (без дополнительной ветви,связанной с вводом сигнала Probe в состоянии Winning).6. Выберите символ ввода сигнала Probe на левом участке.
Выберитекоманду Select Tail из меню Edit. Данная команда отмечает все символыдо конца текущего участка.7. Сделайте копию отмеченного участка и добавьте ее в диаграмму.8. Измените имя сигнала в символе ввода с Lose на Win.9. Измените текст в символе действия на Count := Count+110.Соедините символ состояния Winning с символом ввода сигнала Probe.Для этого выберите символ состояния, «потяните» за «ушко» и, неотпуская кнопки мыши, подведите линию к символу ввода сигнала.Рис.
47. Символ состояния и его «ушко»Рис. 48. Состояние после присоединения новой ветви11.Завершите редактирование диаграммы в соответствии с Рис. 49.102Рис. 49. Оставшиеся части диаграммы9.5.4. Редактирование процесса MainОкончательный вид диаграммы процесса Main приведен на Рис. 50.Рис. 50. Диаграмма процесса Main1039.6.