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

Auto-rewrites and instantiations



Hi,

I am using the new PVS release 2.2 and am having problems with rewrites and
instantiations. 
These problems are both under SunOS 5.5.1 and Linux 4.1.

There are two basic problems which keep recurring and which are illustrated
by the following example:


[-1]    iex!1(FU2!1) > 0
[-2]    iex!1(FU!1) > 0
[-3]    p(RS!1(iex!1(FU!1))) = p(RS!1(iex!1(FU2!1)))
[-4]    (FORALL (FU: FU_ID[R, U, Z, B]):
         (iex!1(FU) > 0
              IMPLIES
            (can_execute(ROB!1)
                 AND
               ((NOT st(ss(RS!1(iex!1(FU)))(1)) = BUSY
                     AND NOT st(ss(RS!1(iex!1(FU)))(2)) = BUSY
                       AND oc(RS!1(iex!1(FU))))
                    AND NOT a(res!1(FU))
                      AND FU = fu_table(op(RS!1(iex!1(FU))))))))
[-5]    (FORALL (S: SLOT_ID[R, U, Z, B]), (S2: SLOT_ID[R, U, Z, B]):
         (oc(RS!1(S)) AND oc(RS!1(S2)) AND p(RS!1(S)) = p(RS!1(S2)))
             IMPLIES S = S2)
  |-------
[1]    FU!1 = FU2!1

________________________________________________________________________

PROBLEM 1 : auto-rewriting hangs.


After using (auto-rewrite -4 -5) and then assert I get infrequent '
responses of 

Warning: Rewriting depth = 50; Rewriting with activeRes_execute_5$1
Warning: Rewriting depth = 100; Rewriting with activeRes_execute_5$1
5116296 bytes have been tenured, next gc will be global.
See the documentation for variable EXCL:*GLOBAL-GC-BEHAVIOR* for more information.


Where 
activeRes_execute_5$1:  (FORALL (S: SLOT_ID[R, U, Z, B]),
                        (S2: SLOT_ID[R, U, Z, B]):
                          (oc(RS!1(S))
                               AND oc(RS!1(S2)) AND p(RS!1(S)) = p(RS!1(S2)))
                              IMPLIES S = S2)


This is the only response in 10 min.

In another example I let this continue and got lots of rewriting messages.
At a certain point PVS indicated "signal" and I found that the PVS process had 
died. 

My question is how can I get the rewriting to terminate?
I used a lot of auto-rewriting when at SRI and it worked fine then.
Now, I get continuous errors. 
(I am keen to use auto-rewrites of line numbers as I have a strategy which
does this as I want, but whether I use the strategy or the simply 
auto-rewrite command, I get the same problem.)
__________________________________________________________________________

PROBLEM 2 : Instantiation

After manually instantiating [4] with FU!1 and FU2!1 I get



[-1]    iex!1(FU2!1) > 0
[-2]    iex!1(FU!1) > 0
[-3]    p(RS!1(iex!1(FU!1))) = p(RS!1(iex!1(FU2!1)))
{-4}    can_execute(ROB!1)
{-5}    oc(RS!1(iex!1(FU2!1)))
{-6}    FU2!1 = fu_table(op(RS!1(iex!1(FU2!1))))
{-7}    can_execute(ROB!1)
{-8}    oc(RS!1(iex!1(FU!1)))
{-9}    FU!1 = fu_table(op(RS!1(iex!1(FU!1))))
[-10]    (FORALL (S: SLOT_ID[R, U, Z, B]), (S2: SLOT_ID[R, U, Z, B]):
         (oc(RS!1(S)) AND oc(RS!1(S2)) AND p(RS!1(S)) = p(RS!1(S2)))
             IMPLIES S = S2)
  |-------
[1]    FU!1 = FU2!1
{2}    st(ss(RS!1(iex!1(FU2!1)))(1)) = BUSY
{3}    st(ss(RS!1(iex!1(FU2!1)))(2)) = BUSY
{4}    a(res!1(FU2!1))
{5}    st(ss(RS!1(iex!1(FU!1)))(1)) = BUSY
{6}    st(ss(RS!1(iex!1(FU!1)))(2)) = BUSY
{7}    a(res!1(FU!1))

All that is needed is to instantiate -10 with iex!1(FU!1) and iex!1(FU2!1)
to complete the proof. 

However, using (inst? :if-match best) PVS uses the instantiation 
S2 gets FU2!1,
S gets FU!1,

to derive 
{-10}    (oc(RS!1(FU!1)) AND oc(RS!1(FU2!1)) AND p(RS!1(FU!1)) = p(RS!1(FU2!1)))
          IMPLIES FU!1 = FU2!1

and 2 unprovable TCCs.

If instead I use (inst -10 "iex!1(FU!1)" "iex!1(FU2!1)") no TCCs are generated
and the proof is easily completed.

My question is why doesn't (inst? :ifmatch best) give me an instantiation which
doesn't generate TCCs since one exists?
How can I force only instantiations which don't generate TCCs to be used?
Could the problem be that the range of iex!1 is [0..Z] and the range of
SLOT_ID[R, U, Z, B] is [1..Z]?

Thanks,
Tamarah
______________________________________

Tamarah Arons
Weizmann Institute of Science
tamarah@wisdom.weizmann.ac.il