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

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



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