形式化方法（Z-符號） - 添加新的倍數關係

Question

我們已經得到了接受以下

一條線，一個BUS_ID和BUSROAD

• 給定的總線操作Bus_Arrives線路到達車站，並分配一個空的 巴士路（如果有的話）。否則它進入一個隊列。

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

| ΔBus_Station

| busline？：LINE

| bus_ID：BUS_ID

| br ?: BUSROAD

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

|先決條件在這裏（添加到隊列的情況已經實現，但我沒有添加它，因爲它與問題無關）。下面是在完成此操作後系統如何更改。

|免費'=免費\ {br}}

|路由'=路由

|離開'=出發U {br？ | - > bus？}

| 訪問'=訪問U {br？ | - >路由（|線|？）}

---

我的問題是：如果訪問是正確表示是Z，例如，當路由（行？）關係稱爲返回一組站元素{station1，station2，station3}。然而，當我將它映射到訪問關係來更新它時，我正在這樣做：br？映射到{station1，station2，station3}。這是可能的或我必須說br？分別映射到集合中的每個單獨元素。如果是這種情況，它是如何表示在Z？

關於什麼是描述附加信息：

路由：對於每一個對應公交線路，有什麼公交車經過車站到達那裏（即 - 8周線的旅行LA，紐約和邁阿密）。

路由：LINE < - >站（關係）

---

免費：哪路車，道路可供選擇。

免費：ΠBUSROAD（電源設置）

---

出發：對於每一個從它出發，什麼公交線路公交車（例如從A出發總線AY123）。

出發：LINE - > BUS_ID（功能）

---

訪問：對於目前已分配總線每總線的道路，它還將訪問哪些站點。一條公共汽車道路可以只有一輛公共汽車或可用。

訪問：BUS_ROAD < - >站（關係）

Answer 1

我設法解決這個問題。

當前操作是不正確的，因爲讓我的規格在CZT後我驗證它，我得到以下信息：

預期類型：ℙ（PLATFORM×STATION）×ℙ（PLATFORM×STATION） 實際類型：ℙ（PLATFORM×STATION）×ℙ（PLATFORM×ℙSTATION）

這意味着每個元素應需單獨映射。

應該使用的實際符號是Cartesian product。

在ZET被表示爲visits′ = visits ⊕ {br?} X route(|line?|)

將返回所有映射爲（寬？，站），它等同於BR？ | - >站，因此可以使用。

注意：笛卡爾產品可以套在兩套之間，應該被視爲一個集合。