Formal Methods (Z-notation) - adding a new multiple relation

Question

We 've got an operation Bus_Arrives that accepts the following

A LINE, a BUS_ID and a BUSROAD

• A bus of a given line arrives at the station and is assigned an empty bus-road, if one is available. Otherwise it enters a queue.

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

| Δ Bus_Station

| busline?: LINE

| bus?: BUS_ID

| br?: BUSROAD

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

| preconditions go here(the case of adding that to the queue is implemented, but I am not adding it since its not related with the question.) below is how the system changes after this operation get completed.

| free' = free \ {br?}

| routing' = routing

| departure' = departure U {br? |--> bus?}

| visits' = visits U {br? |--> routing(|line?|) }

---

My question is: if the visits is represented correctly is Z, for example, when the routing(line?) relation is called it returns a set of station elements {station1,station2,station3}. However, when I am mapping this to the visits relation to update it I am doing this: br? maps to {station1,station2,station3}. Is this possible or i have to say that br? maps to every single element of the set separately. Also if this is the case how is it represented in Z?

Extra information about what is described:

routing: For every correspondence bus-line, what are the stations the bus passes through to arrive there(i.e - Line 8 travels to L.A, N.Y and Miami).

routing: LINE <--> STATION (relation)

---

free: Which bus-roads are available.

free: Π BUSROAD (power-set)

---

departure: For every bus what bus-line it departs from (example from A departs bus AY123).

departure: LINE --> BUS_ID (function)

---

visits: For every bus-road that currently has a bus assigned, what stations it will visit. A bus-road can either have one and only one bus on it or be available.

visits: BUS_ROAD <--> STATION (relation)

Answer 1

I manage to solve the problem.

The current operation is not correct, since after making my specification in CZT I verified it and I get the following message:

Expected type: ℙ ( PLATFORM × STATION ) × ℙ ( PLATFORM × STATION ) Actual type: ℙ ( PLATFORM × STATION ) × ℙ ( PLATFORM × ℙ STATION )

Which means that each element should be mapped seperately.

The actual symbol that should be used is the Cartesian product.

In Zet is represented as visits′ = visits ⊕ {br?} X route(|line?|)

Which will return all the mappings as (br?,station) which is equivalent to br? |--> station, therefore it can be used.

Note: cartesian product can be applied between sets, thus br? should be treated as a set.