以下を受け入れる操作 Bus_Arrives があります
LINE、BUS_ID、BUSROAD
- ある路線のバスが駅に到着し、空いているバス道路が割り当てられます。それ以外の場合はキューに入ります。
--------New_Bus_Arrives--------------------------------------------- -------------------------------------------------- ----
| | △バス停
| | バスライン?: LINE
| | バス?: BUS_ID
| | br?: バスロード
==============================================
| | 前提条件はこちら（それをキューに追加するケースは実装されていますが、質問とは関係ないので追加しません。） 以下は、この操作が完了した後のシステムの変化です。
| | free' = free \ {br?}
| | routing' = ルーティング
| | 出発' = 出発 U {br? |--> バス?}
| | 訪問数 = 訪問数 U {br? |--> ルーティング(|ライン?|) }
私の質問は次のとおりです。たとえば、訪問が正しく表現されている場合は Z です。たとえば、ルーティング (回線?) リレーションが呼び出されると、一連のステーション要素 {station1,station2,station3} が返されます。ただし、これを訪問関係にマッピングして更新するときは、次のようにしています: br? {station1,station2,station3} にマップされます。これは可能ですか、それとも br と言わなければなりませんか? セットのすべての要素に個別にマップされます。また、この場合、Z ではどのように表されますか?
説明内容に関する追加情報:
ルーティング: 対応するバス路線ごとに、バスがそこに到着するために通過する駅は何ですか (つまり、8 号線は LA、NY、マイアミに移動します)。
ルーティング: LINE <--> STATION (関係)
free: 利用可能なバス路線。
free: Π BUSROAD (パワーセット)
出発: すべてのバスがどのバス路線から出発するか (例: A がバス AY123 を出発)。
出発: LINE --> BUS_ID (機能)
訪問: 現在バスが割り当てられているすべてのバス道路について、どの駅を訪問するか。バス道路には、バスが 1 つだけある場合と、利用できる場合があります。
訪問: BUS_ROAD <--> STATION (関係)