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

Re: [PVS-Help] Looking for general strategy to solve inequality problem



Hi César,

I was able to get (interval *) to work after adding the IMPORTING statement like you suggested.

However, when I tried to run install-scripts, I got the following results:
▶ ./install-scripts 
./install-scripts: line 4: bin/relocate: No such file or directory

It turns out that my older versions of PVS (6.0) have bin/relocate but my latest bleeding-edge version (7.0) does not. I am using Allegro, and am on Mac OS X 10.11.6.

Best Regards,
Ben Hocking
benjaminhocking@xxxxxxxxx

> On Aug 25, 2016, at 12:50 PM, MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:
> 
> For interval you need
> 
> IMPORTING interval_arith@strategies4Q
> 
> Regarding metit, make sure you have executed install-scripts from nasalib.
> Are you using Allegro? What OS?
> 
> Cesar
> --
> Cesar A. Munoz, NASA <Cesar.A.Munoz@xxxxxxxx>
> Web: http://shemesh.larc.nasa.gov/people/cam
> NASA Langley Research Center, Bldg. 1220, Room 115 MS. 130, Hampton, VA
> 23681-2199, USA
> Office: +1 (757) 864 1446. Fax: +1 (757) 864 4234
> 
> 
> 
> 
> 
> From:  Ben Hocking <benjaminhocking@xxxxxxxxx>
> Date:  Thursday, August 25, 2016 at 11:31 AM
> To:  ODIN <cesar.a.munoz@xxxxxxxx>
> Cc:  "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>
> Subject:  Re: [PVS-Help] Looking for general strategy to solve inequality
> problem
> 
> 
> Hi César,
> 
> I’m using the nasalib from GitHub (latest commit has =
> f242f6d7de385592dc6c943506b87919844573ab), but when I try to run either
> (metit *) or (interval), I get the response:
> Rule? (metit *)
> metit is not a valid prover command
> Rule? (interval)
> interval is not a valid prover command
> 
> ---------------------------------------------------------------------------
> --------------------------------
> 
> 
> Here are some relevant environmental details:
> ---------------------------------------------------------------------------
> --------------------------------
> Toyota2016/Documents/Examples
> ▶
> echo $PVS_LIBRARY_PATH
> /Users/Dependable/Tools/nasalib:/Users/Dependable/Tools/PVS-lib
> 
> 
> Toyota2016/Documents/Examples
> ▶
> cd /Users/Dependable/Tools/nasalib
> 
> 
> ~Tools/nasalib
> ▶
> git log -n1 | cat
> commit f242f6d7de385592dc6c943506b87919844573ab
> Author: Munoz <cesaramh@xxxxxxxxx>
> Date:   Wed Jul 6 18:02:29 2016 -0400
> 
> 
>    Updated exact_real_arith
> 
> ---------------------------------------------------------------------------
> --------------------------------
> 
> Best Regards,
> Ben Hocking
> benjaminhocking@xxxxxxxxx
> 
> 
> 
> 
> 
> On Aug 25, 2016, at 9:45 AM, MUNOZ, CESAR (LARC-D320)
> <cesar.a.munoz@xxxxxxxx> wrote:
> 
> Ben,
> 
> If you are using nasalib from github (https://github.com/nasa/pvslib), you
> can prove this statement using either metit or interval:
> 
> ben: LEMMA
>  dx < -140 AND
>  dv < 50 IMPLIES
>  dx < -150 OR
>  dv < 45 OR
>  (1 + (dv - 50 + dv * ((140 + dx) / 10) - 50 * ((140 + dx) / 10)) / 5
>  + (140 + dx) / 10)
>       / 1
>> =
>       122957620769739151/5000000000000000000 * dx -
> 475345081090927124023/100000000000000000000
> + 10091024637222290039/100000000000000000000 * dv
> 
> %|- ben : PROOF
> %|- (metit *)
> %|- QED
> 
> ben2: LEMMA
>  dx ## [|-150,-140|] AND
>  dv ## [|45, 50|] IMPLIES
>  (1 + (dv - 50 + dv * ((140 + dx) / 10) - 50 * ((140 + dx) / 10)) / 5
>  + (140 + dx) / 10)
>       / 1
>> =
>       122957620769739151/5000000000000000000 * dx -
> 475345081090927124023/100000000000000000000
> + 10091024637222290039/100000000000000000000 * dv
> 
> %|- ben2 : PROOF
> %|- (interval)
> %|- QED
> 
> Note that metit is an oracle, i.e., it uses MetiTarski/Z3. On the other
> hand, interval is a PVS proof-producing strategy.
> 
> Cesar
> 
> ________________________________________
> From: pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx
> [pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx] on behalf of Ben
> Hocking [benjaminhocking@xxxxxxxxx]
> Sent: Wednesday, August 24, 2016 12:28 PM
> To: pvs-help@xxxxxxxxxxx
> Subject: [PVS-Help] Looking for general strategy to solve inequality
> problem
> 
> 
> Hi all,
> 
> I have the following statement, which
> [-1]  dx < -140
> [-2]  dv < 50
>  |-------
> [1]   dx < -150
> [2]   dv < 45
> [3]   (1 + (dv - 50 + dv * ((140 + dx) / 10) - 50 * ((140 + dx) / 10)) / 5
> + (140 + dx) / 10)
>       / 1
>> =
>       122957620769739151/5000000000000000000 * dx -
> 475345081090927124023/100000000000000000000
> + 10091024637222290039/100000000000000000000 * dv
> 
> 
> Leaving the original as-is and doing (field 3) results in:
> {-1}  100000000000000000000 > 0
> {-2}  dx < -140
> {-3}  dv < 50
>  |-------
> {1}   dx < -150
> {2}   dv < 45
> {3}   500000000000000000000 +
>       (20000000000000000000 * (dv * dx) + 2800000000000000000000 * dv) /
> 10
>       - (140000000000000000000000 + 1000000000000000000000 * dx) / 10
>       + 20000000000000000000 * dv
>       + 10000000000000000000 * dx
>> =
>       (10091024637222290039 * dv) - 475345081090927124023 +
> 2459152415394783020 * dx
> 
> 
> I manually figured out that  [3] can also be simplified to:
>   (dx + 150) * (dv - 45) / 50 >=
>       122957620769739151/5000000000000000000 * dx -
> 475345081090927124023/100000000000000000000
> + 10091024637222290039/100000000000000000000 * dv
> 
> 
> 
> Using a case-replace and field I end up with:
> {-1}  100000000000000000000 > 0
> {-2}  (1 + (140 + dx) / 10 +
>        (-50 - 50 * ((140 + dx) / 10) + (140 + dx) / 10 * dv + dv) / 5)
>       / 1
>       = (dx + 150) * (dv - 45) / 50
> {-3}  dx < -140
> {-4}  dv < 50
>  |-------
> {1}   dx < -150
> {2}   dv < 45
> {3}   2000000000000000000 * ((dv - 45) * (dx + 150)) >=
>       (10091024637222290039 * dv) - 475345081090927124023 +
>        2459152415394783020 * dx
> 
> 
> This still wasn’t very helpful, so I used Wolfram-Alpha to simplify the
> inequality and got:
> (2000000000000000000 * dv - 92459152415394783020) * dx >=
> 13024654918909072875977 - 289908975362777709961 * dv
> 
> 
> Using a case-replace and field I end up with:
> {-1}  2000000000000000000 * ((dv - 45) * (dx + 150)) >=
>       (10091024637222290039 * dv) - 475345081090927124023 +
>        2459152415394783020 * dx
>       =
>       (2000000000000000000 * dv - 92459152415394783020) * dx >=
>        13024654918909072875977 - 289908975362777709961 * dv
> {-2}  100000000000000000000 > 0
> {-3}  (1 + (140 + dx) / 10 +
>        (-50 - 50 * ((140 + dx) / 10) + (140 + dx) / 10 * dv + dv) / 5)
>       / 1
>       = (dx + 150) * (dv - 45) / 50
> {-4}  dx < -140
> {-5}  dv < 50
>  |-------
> {1}   dx < -150
> {2}   dv < 45
> {3}   (2000000000000000000 * dv - 92459152415394783020) * dx >=
>       13024654918909072875977 - 289908975362777709961 * dv
> 
> 
> Now, I imagine I could probably solve this eventually (I’ve already
> graphed it to prove to myself that it’s true), but I was wondering if
> there’s a better strategy I could be using in general?
> 
> 
> 
> Best Regards,
> Ben Hocking
> benjaminhocking@xxxxxxxxx