[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