Jon, I had a brief look at the last spec that you posted. I also had a problem unzipping it, but despite a failure message got a decompression by opening the file in emacs.
The file decompressed in this way had two issues in it. The first was that it terminated mid paragraph. The second was that there were lower case beta signs systematically appearing throughout. I used a repetitive edit to remove the betas and partially processed the result. Some issues arising were: 1. Semicolons are needed between declarations but not after tha last one in the declaration part. 2. You used the same name (Elevator_State) twice for schemas (perhaps there was a significant beta there or some other problem with the decompression. The second occurence is for an operation over the first so presumably it was decorated in some way). 3. Not all uses of BOOLEAN values have been translated to use True and False instead of 0 and 1, so the remainder give type errors. You may will find it hard work proving the consistency of your specification, even where it looks pretty obvious, and so there might be better value for you in using axiomatic mode (which amounts to assuming consistency) and working on more interesting proofs. You can always go back later and prove the consistency results. On the other hand, consistency proofs will be simpler than proving significant properties of the spec as a whole so it is a place to start learning proof. Its not clear what consistency goal you were attempting, but I'm guessing it was masterStop, in which case using masterStop as a witness won't work. You could use True. And then you will have to rewrite with the definition of True and that of BOOLEAN. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
