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

*To*: pvs-help@csl.sri.com*Subject*: Auto-rewrites and instantiations*From*: Arons Tamarah <tamarah@wisdom.weizmann.ac.il>*Date*: Wed, 4 Nov 1998 17:06:26 +0200

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

- Prev by Date:
**Re: How to recover from a runaway proof attempt?** - Next by Date:
**TCCs on inst?** - Prev by thread:
**Re: TCCs on inst?** - Next by thread:
**Re: Auto-rewrites and instantiations** - Index(es):