Мансуров Н. Н., Майлингова О. Л. - Методы формальной спецификации программ (1184226), страница 15
Текст из файла (страница 15)
Выполнение стартовых переходов системы1091. Введите команду show-next-symbol. Появится окно редактора SDLдиаграмм, в котором будет показан стартовый символ процесса Main. Вдальнейшем, это окно будет использоваться Монитором для показаграфической трассы.2. Выполните команду next-transition (введите n-t в поле ввода команды).Монитор отображает выполнение стартового перехода процесса Mainдвумя способами:- В окне сообщений Монитора текстовая трасса содержит следующуюинформацию о выполняемом переходе: идентификатор экземплярапроцесса, выполняющего переход, имя исходного состояния, текущеезначение модельного времени.
Трасса перехода завершается строкой,содержащей имя следующего состояния.*** TRANSITION START*Pid:Main:1*State :start_state*Now:0.0000*** NEXTSTATEGame_Off- В окне редактора SDL диаграмм графическая трасса показывает символ,который будет исполняться на следующем переходе. Следующий символ –это стартовый символ процесса Demon.3. Для выполнения стартового перехода процесса Demon воспользуемсявозможностью интерфейса Монитора повторять уже введенные команды:нажмите мышью на поле ввода команд и нажмите клавишу <Up>. В полеввода команды появится последняя введенная команда (n-t). Выполнитеее, нажав клавишу <Enter>.Выполняется стартовый переход процесса Demon.
Обратите внимание нато, что редактор SDL диаграмм выделяет текстовый символ, содержащийопределение таймера T. В системе SDT принято соглашение, что приотсутствии сигналов из окружения системы, следующим событием являетсясрабатывание таймера.Обратите внимание, что в текстовой трассе содержится сообщение обустановке таймера T.10.3.3. Посылка сигналов из окружения системы110Для взаимодействия с системой нужно уметь посылать сигналы изокружения системы (например, сигнал Newgame, предназначаемый процессуMain.) Для посылки сигнала системе воспользуемся командой Output-Via,аргументами которой являются имя сигнала, параметры сигнала(отсутствуют в случае сигнала Newgame) и имя канала, по которомуосуществляется посылка.Для ввода команды воспользуемся возможностями графическогоинтерфейса. Кнопки команд расположены на левой панели.
Кнопкисгруппированы в соответствии с их назначением.1. Выберите группу команд Send Signal и нажмите на кнопку Send Via (длянахождения этой кнопки может потребуется прокрутить окно с кнопками).Данная кнопка выполняет команду Output-Via (выполняемая командаотображается в окне сообщений Монитора). Выполнение командыприводит к появлению нескольких дополнительных диалогов для вводапараметров команды. Первый диалог предназначен для ввода именисигнала.
Диалог содержит список всех сигналов, которые могут бытьпосланы системе из окружения.Рис. 54. Посылка сигнала Newgame2. Выберите сигнал Newgame и нажмите кнопку OK.3. Следующий диалог предназначен для ввода имени канала:111Рис. 55. Выбор канала для посылки сигнала4. В списке имеется единственный элемент (канал C1). Выберите его, нажавна кнопку OK.В окне сообщений подтверждается посылка сигнала. Графическая трассапоказывает, что следующим символом является символ ввода сигналаNewgame.10.3.4.
Выполнение переходов1. Выполните следующий переход, используя кнопку Transition в группеExecute. Текстовая трасса показывает действия, выполняемые на переходев состояние Game_On. Заметим, что, в отличие от стартового перехода,начальное состояние перехода обозначается комбинацией именисостояния (Game_Off) и имени принимаемого сигнала (Newgame):*** TRANSITION START*Pid: Main:1*State: Game_Off*Input: Newgame*Sender: env:1*Now: 0.0000*CREATEGame:1*ASSIGNGameP := Game:1*** NEXTSTATEGame_On112На данном переходе создается экземпляр процесса Game, поэтомуграфическая трасса показывает, что следующим символом являетсястартовый символ процесса Game.Таким образом, текстовая трасса показывает события, произошедшие назавершившимся переходе, включая исходное и заключительное состоянияданного перехода.
Графическая трасса показывает некоторое будущеесобытие, которое произойдет при выполнении следующего перехода (причемпервый символ нового перехода может оказаться на диаграмме другогопроцесса).2.Выполните очередной переход процесса Game, нажав на кнопкуTransition. Процесс Game переходит в состояние Losing и графическаятрасса возвращается в процесс Demon.3.Выполните очередной переход (на котором должно произойтисрабатывание таймера). На данном переходе таймер посылает сигналпроцессу, который произвел установку данного таймера.
Срабатываниетаймера считается отдельным переходом. Обратите внимание на то, что наданном переходе произошло увеличение модельного времени.*** TIMER signal was sent*Timer:T*Receiver:Demon:1*** NOW: 1.00004. Выполните очередной переход. Исходное состояние данного переходахарактеризуестя состоянием Generate и получением сигнала таймера T.На данном переходе происходит посылка сигнала Bump процессу Game:*** TRANSITION START*Pid: Demon:1*State: Generate*Input: T*Sender : Demon:1*Now: 1.0000*OUTPUT ofBump to Game:1*SET on timer T at 2.0000*** NEXTSTATEGenerateГрафическая трасса показывает, что следующим символом будет приемсигнала Bump в процессе Game.
Как видно на диаграмме, после получения113сигнала Bump процесс Game попадет в состоянии Winning, в котором будетожидать приема сигнала Probe (либо нового сигнала Bump).5. Выполните очередной переход для перевода процесса Game в состояниеWinning. Графическая трасса возвращается в процесс Demon ипоказывает, что при отсутствии внешних сигналов следующим событиембудет срабатывание таймера T, Вместо этого, пошлем сигнал Probe изокружения системы:6. Пошлите сигнал Probe, используя кнопку Send Via. Графическая трассавозвращается в процесс Game.7.
Выполните следующий переход. На данном переходе происходит приемсигнала Probe и посылка сигнала Win в окружение системы. ПроцессGame возвращается в состояние Winning и ждет сигнала Probe илисигнала Bump.*************TRANSITION STARTPId: Game:1State: WinningInput: ProbeSender : env:1Now:1.0000OUTPUT of Win to env:1ASSIGN Count := 1NEXTSTATE Winning10.4. Исследование внешнего поведения системыПосле выполнения упражнений данного раздела вы должны научиться:- перезапускать исполняемую систему;- использовать возможность протоколирования внешних сигналов;- добавлять новые кнопки на панель управления Монитором;- выполнять все переходы в течение заданного интервала времени.10.4.1.
Протокол внешних сигналов1. Перезапустите исполняемую систему: выберите команду Restart из менюFile окна Монитора. Дополнительный диалог запросит подтверждениязавершения текущей трассы. Нажмите кнопку OK. Окно сообщений114Монитора очищается и исполняемая система приводится в начальноесостояние.2. Установите уровень детальности трассы равный 1. Это означает, чтотрасса будет показывать только взаимодействие системы с окружением,т.е.
сигналы из окружения и в окружение.3. Для включения протокола внешних сигналов введите команду signal-log вполе ввода команды и нажмите клавишу <Return>. Для данной командыне существует стандартной кнопки на панели управления Монитором.Команда имеет два параметра, значения которых запрашиваются вдополнительных диалогах. Первый параметр – это имя SDL объекта, длякоторого нужен протокол сигналов. В окне представлен список всехобъектов в системе.4. Введите название объекта env в текстовое поле ввода в нижней частиокна.
Этот объект означает окружение системы.Рис. 56. Включение протокола внешних сигналов5. Второй параметр команды signal-log является именем файла, вкоторый направляется протокол внешних сигналов. Появляетсястандартный диалог выбора файла. Введите имя файла signal.log вполе File.10.4.2. Добавление новых кнопок к интерфейсу МонитораГрафический интерфейс Монитора позволяет добавлять новые кнопки напанель управления Монитором и связывать с ними произвольные команды.1151.
Выберите группу кнопок Send Signal. Выберите команду Add из менюGroup для данной группы.Рис. 57. Добавление новой кнопки к группе2. В дополнительном диалоге введите Newgame как метку новой кнопки вполе Label. Не нажимайте клавишу <Return> !. Введите output-vianewgame – в поле Definition. Последний параметр “-“ в команде output-viaозначает значение по-умолчанию (эквивалент нажатию на кнопку OK) всоответствующем диалоге.Рис. 58. Добавление кнопки3.
Завершите выполнение команды, нажав на кнопку Apply. Новая кнопкапоявляется в группе, диалог может быть использован для определенияновой кнопки.4. Добавьте кнопку для посылки сигналов Probe, Result и Endgame.5. Завершите диалог, нажав кнопку OK.10.4.3. Взаимодействие с системой1. Пошлите сигнал Newgame, нажав на новую кнопку Newgame.1162. Выполните все переходы до достижения модельного времени равного 5.5.Для этого нажмите кнопку Until Time в группе Execute. Введите значение5.5.3.
Пошлите сигнал Probe.4. Выполните все переходы до достижения модельного времени 10.3.Обратите внимание на то, какой сигнал был послан системой в окружение(Win или Lose?).5. Пошлите два сигнала Probe подряд.6. Пошлите сигнал Result.7. Выполните все переходы до достижения модельного времени 13.5.Обратите внимание на то, какие сигналы были посланы системой вокружение.10.4.4. Просмотр протокола внешних сигналов1. Завершите выполнение исполняемой программы, нажав кнопку Stop Sim вгруппе Execute. По этой команде выключится протокол внешних событий.Окно Монитора при этом остается активным.2.
Файл signal.log должен содержать протокол внешних сигналовисполняемой системы:Signal log for system Demongame with unit Process envon file …0.0000 Newgame from env:1 to Main:15.5000Probe from env:1 to Game:15.5000Win from Game:1 to env:110.3000 Probe from env:1 to Game:110.3000 Probe from env:1 to Game:110.3000 Result from env:1 to Game:110:3000 Lose from Game:1 to env:110:3000 Lose from Game:1 to env:110:3000 Score from Game:1 to env:1Parameter(s) : 110.5. Генерация диаграмм взаимодействияВ данном упражении мы рассмотрим способы автоматической генерациидиаграмм взаимодействия по исполняемой системы.