I was also curious why you said that my system does not have an initial
state. Would not the declaration of the Button_State, Elevator_State, etc.
be the initial State, or would initialization be considered the initial
state? If Button_Init, etc. are not the initial state, would I use Δ
Button_Init rather than Δ Button_State in my operations that are further
down the line.


On Thu, Sep 20, 2012 at 4:10 PM, Phil Clayton <>wrote:

> Jon,
> On 20/09/12 17:59, Jon Lockhart wrote:
>> So based on what you have
>> said does that mean then that pushed = {} should be changed to pushed' =
>> {} since it would be a consequence of the Init operation running at
>> start up?
> I had a quick read yesterday but no time to reply.  My initial reaction
> was you meant pushed' = {}.
> However, for initialization, you don't have an initial state, so your
> schema should just have
>   State'
> where you currently have
>   Δ State
> I strongly recommend reading chapter 12 of Using Z, available at
>  If this change is necessary, and of course I will apply it to the other
>> two init operations, would the pre operator then be more useful in being
>> applied to this operation?
> pre Init is certainly worth establishing: it is useful to know whether the
> Init operation can be achieved.  Note that with the above change to use
> State', pre Init is either true or false as there are no unprimed
> variables.  You want to know that it is not false.  As there is no initial
> state, pre Init may be written
>   ∃ State' ∙ Init
> However, I see you're calculating
>   pre Button_State
>   pre Elevator_State
>   pre Floor_State
> which is pointless.  These schemas are not operations: they have no
> concept of before state and after state.  You'll see that none have primed
> variables.  Not surprisingly, you're finding
>   pre X_State = X_State
> I also recommend chapter 14 of Using Z.  The whole book is worth a read,
> in fact!
> Phil
> ______________________________**_________________
> Proofpower mailing list
Proofpower mailing list

Reply via email to