가했습니다 새로운 여러 관계를 추가는 다음정형 기법 (Z-표기) - 우리는 '
선하는 BUS_ID과 BUSROAD 특정의
- 버스를 받아들이는 작업 Bus_Arrives있어 선은 역에 도착하며 버스 도로가있는 경우 빈 버스 도로가 지정됩니다. 그렇지 않으면 대기열에 들어갑니다.
-------- New_Bus_Arrives ----------------------------------- -------------------------------------------------- ----------
| Δ 버스 _ 스테이션
| 버스 라인? LINE
| 버스? BUS_ID
| BR? BUSROAD
========================================== ====| 전제 조건은 여기에 있습니다 (큐에 추가하는 경우 구현되지만, 질문과 관련이 없기 때문에 추가하지 않습니다.) 아래는이 작업이 완료된 후 시스템이 변경되는 방법입니다.
| 무료 '= 무료 \ {BR?}
| 라우팅 '= 라우팅
| 출발 '= 출발 U {br? | -> 버스}
|? 방문수 = 방문수 U {br? | -> 라우팅 (| 라인 |?)}
내 질문은 : 방문이 올바르게 표시되는 경우 Z는, 예를 들어, 라우팅 (선?) 관계가 호출 될 때 그것은 반환 스테이션 요소 집합 {station1, station2, station3}. 그러나 이것을 업데이트 관계를 매핑 할 때 나는이 일을하고있다 : br? {station1, station2, station3}에 매핑됩니다. 이게 가능 할까? 아니면 그걸 말할 필요가 있니? 집합의 모든 단일 요소에 개별적으로 매핑됩니다. 또한이 경우 Z에서 어떻게 표현됩니까?
설명 된 사항에 대한추가 정보 :
라우팅 : 모든 대응 버스 라인의 경우, 버스가 통과하는 역이 도착 무엇인가 (예 - LA 8 여행 선, 뉴욕과 마이애미).
라우팅 : LINE < -> STATION (관계)
무료 : 버스 도로 사용할 수 있습니다.
무료 : Π BUSROAD (전원 설정)
출발 : 그것에서 출발 무엇을 버스 라인의 모든 버스의 (A에서 예 버스 AY123 출발).
출발 : LINE -> BUS_ID (기능)
방문 : 현재 할당 된 버스가있는 모든 버스 도로를 들어, 어떤 역을 방문합니다. 버스 도로에는 버스가 하나만 있거나 사용할 수 있습니다.
방문 : BUS_ROAD < -> STATION (관계)