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.


Proofpower mailing list

Reply via email to