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

*To*: Sam Owre <owre@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Help with (both-sides) strategy*From*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Date*: Wed, 25 May 2016 08:27:11 -0400*Authentication-results*: symauth.service.identifier*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <E1b5Szv-0007sB-O8@ubi.csl.sri.com>*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <C92637B4-4BD1-4DE4-B44B-51B82DC80990@dependablecomputing.com> <E1b5Szv-0007sB-O8@ubi.csl.sri.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Sam, Here are my files:

**Attachment:
SelectorAssignment.pvs**

**Attachment:
SelectorAssignment.prf**

It’s with noting that p_Data_Type_Conversion is of type posint8_from_1_to_5, which is defined as: posint8_from_1_to_5?(n: number): bool = posint8?(n) AND (1 <= n) AND (n <= 5); posint8_from_1_to_5: NONEMPTY_TYPE = (posint8_from_1_to_5?) CONTAINING 1; Cesar Muñoz has pointed out that if I replace “number” with “real” in my definition, my problem goes away. I still think the FALSE = TRUE issue seems problematic, but by switching all of my definitions of types from using numbers to using reals, I’ve reduced the generated TCCs by more than 20%, so that’s definitely something. Best Regards, Ben Hocking ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx > On May 25, 2016, at 3:12 AM, Sam Owre <owre@xxxxxxxxxxx> wrote: > > Hi Ben, > > I'm having trouble recreating this. With the spec > > ----- > test: THEORY > BEGIN > p_Data_Type_Conversion: nat > f: formula 1 <= p_Data_Type_Conversion => p_Data_Type_Conversion - 1 >= 0 > END test > ----- > > I get: > > f : > > |------- > {1} 1 <= p_Data_Type_Conversion IMPLIES p_Data_Type_Conversion - 1 >= 0 > > Rule? (flatten) > Applying disjunctive simplification to flatten sequent, > this simplifies to: > f : > > {-1} 1 <= p_Data_Type_Conversion > |------- > {1} p_Data_Type_Conversion - 1 >= 0 > > Rule? (both-sides "+" "1" 1) > Applying + 1 to both sides of an inequality/equality conjunction, > this simplifies to: > f : > > [-1] 1 <= p_Data_Type_Conversion > |------- > {1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1 > > Rule? > > I suspect that the decision procedures have already recorded something in > your case that is affecting the behavior of both-sides (yours shows that > you're in the fourth branch of the proof). Is it possible for you to send > me your specs? > > Thanks, > Sam > > Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: > >> From: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> >> Date: Mon, 23 May 2016 11:54:20 -0400 >> To: pvs-help@xxxxxxxxxxx >> Subject: [PVS-Help] Help with (both-sides) strategy >> Sender: pvs-help-bounces+owre=csl.sri.com@xxxxxxxxxxx >> >> I don’t use the (both-sides) strategy very often, so perhaps I’m using it wrong, but I’m not sure what I’m doing >> wrong in the following: >> Selector_TCC2.4 : >> >> [-1] (1 <= p_Data_Type_Conversion) >> |------- >> [1] p_Data_Type_Conversion - 1 >= 0 >> >> Rule? (both-sides "+" "1" 1) >> Applying + 1 to both sides of an inequality/equality conjunction, >> this yields 3 subgoals: >> Selector_TCC2.4.1 : >> >> [-1] (1 <= p_Data_Type_Conversion) >> |------- >> {1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1 >> >> Rule? (grind) >> Trying repeated skolemization, instantiation, and if-lifting, >> >> This completes the proof of Selector_TCC2.4.1. >> >> Selector_TCC2.4.2 : >> >> [-1] (1 <= p_Data_Type_Conversion) >> |------- >> {1} p_Data_Type_Conversion - 1 >= 0 = >> p_Data_Type_Conversion - 1 + 1 >= 0 + 1 >> [2] p_Data_Type_Conversion - 1 >= 0 >> >> Rule? (assert) >> Simplifying, rewriting, and recording with decision procedures, >> this simplifies to: >> Selector_TCC2.4.2 : >> >> [-1] (1 <= p_Data_Type_Conversion) >> |------- >> {1} FALSE = TRUE >> [2] p_Data_Type_Conversion - 1 >= 0 >> >> At this point, since {1} is clearly false, I’m back to where I started (notwithstanding an additional TCC to prove >> that real_pred(p_Data_Type_Conversion - 1), which can be proved with (lemma "reals.closed_minus" ("x" >> "p_Data_Type_Conversion" "y" "1"))). >> >> Any idea what I’m doing wrong? >> >> And how does: >> {1} p_Data_Type_Conversion - 1 >= 0 = >> p_Data_Type_Conversion - 1 + 1 >= 0 + 1 >> get resolved to: >> {1} FALSE = TRUE >> upon using (assert)? >> >> Best Regards, >> Ben Hocking >> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx >

**References**:**[PVS-Help] Help with (both-sides) strategy***From:*Ben Hocking

**Re: [PVS-Help] Help with (both-sides) strategy***From:*Sam Owre

- Prev by Date:
**Re: [PVS-Help] Help with (both-sides) strategy** - Next by Date:
**[PVS-Help] PVS tool general information** - Previous by thread:
**Re: [PVS-Help] Help with (both-sides) strategy** - Next by thread:
**[PVS-Help] PVS tool general information** - Index(es):