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
3. Not all uses of BOOLEAN values have been translated to
use True and False instead of 0 and 1, so the remainder give
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.
Proofpower mailing list