形式化方法（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？ | - >站，因此可以使用。

注意：笛卡尔产品可以套在两套之间，应该被视为一个集合。