[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

How to get err status in PVS batch mode



Hello fellow PVS users,

I am trying to prove some theories in PVS batch mode. However, some theories 
should be proved or not depends on other theories' proving status. Is that 
possible to get the error status of proving explicitly? 

Following example may be helpful to understand my question.

Batch File (pseudo code)

--------------------------------------
 proving Mytheorem
 if something is wrong (e.g. unproved)  <==== Is that possible to get error status?
   then proving (not Mytheorem)
 else
   pvs-message "successful"  
--------------------------------------   

Thanks,

Min