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

Question

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

ЛИНИЯ, BUS_ID и BUSROAD

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

-------- New_Bus_Arrives ----------------------------------------- -------------------------------------------------- ----

| Δ Bus_Station

| шинопровод?: ЛИНИЯ

| автобус?: BUS_ID

| br?: BUSROAD

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

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

| free ' = free \ {br?}

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

| вылет ' = вылет U {br? |-> автобус?}

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

---

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

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

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

маршрутизация: ЛИНИЯ <-> СТАНЦИЯ (отношение)

---

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

бесплатно: Π BUSROAD (в комплекте)

---

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

вылет: LINE -> BUS_ID (функция)

---

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

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

Answer 1

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

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

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

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

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

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

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

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