1

我们有一个接受以下内容的操作 Bus_Arrives

一个 LINE、一个 BUS_ID 和一个 BUSROAD

  • 给定线路的公共汽车到达车站并分配一条空的公共汽车路（如果有的话）。否则进入队列。

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

| Δ Bus_Station

| 公交线路？：LINE

| 总线？：BUS_ID

| br?: BUSROAD

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

| 先决条件在这里（实现了将其添加到队列的情况，但我没有添加它，因为它与问题无关。）以下是此操作完成后系统如何更改。

| 免费' = 免费 \ {br?}

| 路由' = 路由

| 出发' = 出发 U {br? |--> 公交车？}

| 访问' = 访问 U {br? |--> 路由(|line?|) }

我的问题是：如果访问被正确表示为 Z，例如，当调用路由（线路？）关系时，它返回一组站元素 {station1，station2，station3}。但是，当我将其映射到访问关系以更新它时，我正在这样做：br？映射到 {station1,station2,station3}。这是可能的还是我不得不说这个？分别映射到集合的每个元素。此外，如果是这种情况，它如何在 Z 中表示？

关于所描述内容的额外信息：

路线：对于每条对应的公交线路，公交车经过哪些站点才能到达那里（即 - 8 号线前往洛杉矶、纽约和迈阿密）。

路由：LINE <--> STATION（关系）

免费：有哪些公交线路可用。

免费：Π BUSROAD（动力装置）

出发：对于每辆公共汽车它从哪条公交线路出发（例如从 A 出发的公共汽车 AY123）。

出发：LINE --> BUS_ID（函数）

访问：对于当前分配了公共汽车的每条公共汽车道路，它将访问哪些站点。一条公共汽车路可以有一辆且只有一辆公共汽车，也可以是可用的。

访问：BUS_ROAD <--> STATION（关系）

4

1 回答 1

1

我设法解决了这个问题。

当前操作不正确，因为在 CZT 中制定规范后，我对其进行了验证，并收到以下消息：

预期类型：ℙ（PLATFORM × STATION）×ℙ（PLATFORM × STATION）实际类型：ℙ（PLATFORM × STATION）×ℙ（PLATFORM ×ℙ STATION）

这意味着每个元素应该单独映射。

应该使用的实际符号是笛卡尔积。

在 Zet 中表示为visits′ = visits ⊕ {br?} X route(|line?|)

哪个会将所有映射返回为 (br?,station)，相当于 br？|--> 站，所以可以使用。

注意：笛卡尔积可以在集合之间应用，因此 br? 应该被视为一个集合。

于 2014-01-11T23:22:26.277 回答