[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’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,

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,