Re: [CZT-Users] AIRPORT'

[<pet...@ec...>]

There is no definition of AIRPORT'. You want to refer to AIRPORT and then prime its components. In Standard Z you need a space between the name AIRPORT and the ' operator.

Hope this helps,
Petra


----- Reply message -----
From: "Philippe de Rochambeau" <ph...@fr...>
Date: Mon, Sep 20, 2010 18:32
Subject: [CZT-Users] AIRPORT'
To: <czt...@li...>

Hello,

after typing the following code (copied from "Formal Specification in Z" by D Lightfoot) in Eclipse, I got an error message stating that AIRPORT' is undeclared (in Init).  Why is that? 

Many thanks.

Philippe




─ section Airline parents standard_toolkit └

─ [ PLANE ] └
─ [ GATE ] └

┌ AIRPORT
  waiting: ℙ PLANE
  assignment: GATE ↣ PLANE
|
  waiting ∩ ran assignment = ∅
└
┌ Init
  AIRPORT′
|
  waiting′ = ∅
  empty′ = ∅
└