Формальные методы (Z-обозначение) — добавление нового множественного отношения

У нас есть операция Bus_Arrives, которая принимает следующие

LINE, BUS_ID и BUSROAD

  • Автобус данной линии прибывает на станцию, и ему назначается свободная автобусная дорога, если таковая имеется. В противном случае он попадает в очередь.

--------Прибытие нового_автобуса-------------------------------------------------------- -------------------------------------------------- ----

| Δ Bus_Station

| линия автобуса?: ЛИНИЯ

| автобус?: BUS_ID

| бр?: АВТОБУСНАЯ ДОРОГА

==============================================

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

| бесплатно' = бесплатно \ {br?}

| маршрутизация = маршрутизация

| отъезд' = отъезд U {br? |--> автобус?}

| посещения' = посещения U {br? |--> маршрутизация(|линия?|)

Мой вопрос: если посещения представлены правильно, это Z, например, когда вызывается отношение маршрутизации (линия?), оно возвращает набор элементов станции {station1,station2,station3}. Однако, когда я сопоставляю это с отношением посещений, чтобы обновить его, я делаю это: br? сопоставляется с {station1,station2,station3}. Это возможно или я должен сказать, что бр? сопоставляется с каждым элементом набора отдельно. Кроме того, если это так, как это представлено в Z?

Дополнительная информация о том, что описано:

маршрутизация: для каждой соответствующей автобусной линии, через какие станции проходит автобус, чтобы прибыть туда (например, линия 8 едет в Лос-Анджелес, Нью-Йорк и Майами).

маршрутизация: LINE ‹--> STATION (отношение)

бесплатно: Какие автобусные маршруты доступны.

бесплатно: Π BUSROAD (power-set)

отправление: Для каждого автобуса, с какой автобусной линии он отправляется (например, из А отправляется автобус AY123).

отправление: LINE --> BUS_ID (функция)

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

посещения: BUS_ROAD ‹--> STATION (отношение)


formal-languages formal-methods z-notation
person nmargaritis    schedule 05.01.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Мне удается решить проблему.

Текущая операция некорректна, т.к. после составления спецификации в CZT я ее проверил и получаю следующее сообщение:

Ожидаемый тип: ℙ (ПЛАТФОРМА × СТАНЦИЯ) × ℙ (ПЛАТФОРМА × СТАНЦИЯ) Фактический тип: ℙ (ПЛАТФОРМА × СТАНЦИЯ) × ℙ (ПЛАТФОРМА × ℙ СТАНЦИЯ)

Это означает, что каждый элемент должен отображаться отдельно.

Должен использоваться символ декартово произведение.

В Zet представлен как visits′ = visits ⊕ {br?} X route(|line?|)

Что вернет все сопоставления как (br?, станция), что эквивалентно br? |--> станция, поэтому ее можно использовать.

Примечание: между наборами может применяться декартово произведение, таким образом, br? следует рассматривать как набор.

person nmargaritis    schedule 11.01.2014