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 <[email protected]>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 > [email protected] > http://lemma-one.com/mailman/**listinfo/proofpower_lemma-one.**com<http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com> >
_______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
