Phil,

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.

Thanks,
Jon

On Thu, Sep 20, 2012 at 4:10 PM, Phil Clayton <phil.clay...@lineone.net>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
> http://www.usingz.com/
>
>
>
>  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@lemma-one.com
> http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com>
>
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to