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

EXPAND and IF-THEN?




I am running into some problems when I use EXPAND.  Basically each
time I expand a certain sequence of terms, PVS gets slower and slower,
and eventually never returns from a call to EXPAND.  If I use EXPAND
with the :ASSERT NONE option, the EXPAND command works just fine,
however, I eventually have to ASSERT/SIMPLIFY, and then PVS never
returns.  I still consider myself a new user to PVS, so I am looking
for some quick advice or guidance to help me figure out what is really
going on.

The term that I am expanding, expands into an IF-THEN statment.  If I
make the IF-THEN statement inert by making the THEN and ELSE clauses
the same, the prover runs through my proof at an acceptable rate.
However, if the THEN and ELSE clauses are different, the prover never
returns.  It may also be useful to know that all of these terms that I
am expanding manipulate a record which represents the state of my
system.  

Any help on the following questions would be great:
1. Why does EXPAND keep getting slower and slower?
2. How can I tell what PVS is doing when it is slow?
3. Is it common for people to use records to represent the state of a
system, or are there a number of problems that I will be running into
later?

Thanks.

Darryl Dieckman