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, but if I remember correctly we were going with using
the "There Exists" proof still on these like we did for the States.
Any direction on how to finish these up so I may move on to the actual
operations would be greatly appreciated.
Regards,
Jon
On Sat, Oct 13, 2012 at 12:28 PM, Roger Bishop Jones <r...@rbjones.com>wrote:
> 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 sub goal pop up that says "{} = elevator" after
> > I work on the existence proof. Is this b/c I used the
> > empty set as the witness to the elevator axiom proof?
>
> No, its because you set both moving and stopped to the empty
> set, and this can only be the case if there are no
> elevators.
> Your spec doesn't say there are no elevators, so you can't
> prove it.
>
> You need to supply a witness for which the union of "moving"
> and "stopped" can be proven to be "elevators", even though
> you don't know what "elevators" is.
> One way to do that is to use the state in which everything
> is stopped, i.e. in which moving = {} and stopped =
> elevators.
>
> I haven't checked that that satisfies the rest of the
> predicate, but I guess that's probable.
>
> Roger
>
>
elevatorSpecV5_P1.doc.gz
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
