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

Re: EXPAND and IF-THEN?




Darryl:
  Can you do M-x dump-pvs-files and email us the dump file of
the specification that provokes this problem?

> 1. Why does EXPAND keep getting slower and slower?

It could be that the terms are getting extremely large and
slowing down the simplifier.

> 2. How can I tell what PVS is doing when it is slow?

If you don't see a rewrite commentary, then the slowness must
be in some simplification step.  There is no clean way to
observe what's happening short of interrupting the computation and
examining the Lisp stack.

> 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?

It is common to use records for representing state.  If the
slowness is because expressions get large, then there isn't much
we can do, but we can fix any obvious inefficiencies in the simplifier.

-Shankar