Jon,
On Friday 12 Oct 2012 20:35, Jon Lockhart wrote:
> I got back to the specification today, and moved on to
> proving the elevator state schema, Elevator_State, and I
> moved the static component elevator to an axiom, similar
> to the static components of button. Unfortunately I get
> a weird
Roger,
Got that error corrected, thanks for the input. Encounterd a few more hang
ups on doing the proof but those were eliminated by grabbing the spec for
elevator on the rewrite tactic. Same for floor.
Now I am back to the Init operations. I have attached the specification
again for you veiwing
