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

Re: [PVS-Help] Prooflite scripts being ignored?



Hi Cesar,

I tried deleting the greedy proofs altogether, but to no avail. Note that the actual strategy that was used by proveit was (subtype-tcc), which is the default TCC strategy.

Thanks,
Ben Hocking



On Jul 21, 2014, at 9:46 PM, MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:

Ben,
The problem is that you have the proof script:

%|- *_TCC* : PROOF


 %|-   (model-check)


 %|- QED          



after

%|- Sqrt_x_2_y_2_TCC2 : PROOF


 %|-   (grind)    


 %|- QED          



Since *_TCC* matches Sqrt_x_2_y_2_TCC2, it rewrites the proof of
Sqrt_x_2_y_2_TCC2 to (model-check). To solve this problem, put the most
greedy proof script, i.e., *_TCC*, before any other proof script.

Let me know if this solves your problem,

Cesar





On 7/21/14 4:25 PM, "Ben Hocking" <benjaminhocking@xxxxxxxxx> wrote:

I'm running PVS Version 6.0, and have the following (auto-generated)
theory:
distance3:
THEORY
BEGIN
IMPORTING reals@sqrt


% Type of output  


out_type:
TYPE = [#
                 f_result: real
                #]


% Type of system state


sys_type:
TYPE = [#
                 f_output: out_type
                #]


result(p_Sqrt_x_2_y_2: real): real
=
p_Sqrt_x_2_y_2


Sqrt_x_2_y_2(p_x: real, p_y: real): real
=
sqrt((p_x)
^ 2 + (p_y)
^ 2)


% Initialize output


prepare_output(p_result: real): out_type=
(#
  f_result
:= p_result
 #)


% Initialize system state


init: sys_type=
(#
  f_output
:= prepare_output(0)
 #)


% Whole system run, this can only be called after INIT and inputs setting


run(p_sys: sys_type, p_x: real, p_y: real): sys_type=

LET v_Sqrt_x_2_y_2: real = Sqrt_x_2_y_2(p_x, p_y)
IN

LET v_result: real = result(v_Sqrt_x_2_y_2)
IN
(#
  f_output
:= prepare_output(v_result)
 #)


%|- Sqrt_x_2_y_2_TCC1 : PROOF


%|-   (model-check)


%|- QED         




%|- Sqrt_x_2_y_2_TCC2 : PROOF


%|-   (grind)   


%|- QED         




%|- *_TCC* : PROOF


%|-   (model-check)


%|- QED         




%|- *int*_TCC* : PROOF


%|-   (grind)   


%|- QED



END distance3



Running proveit does not execute my Prooflite scripts:
▶ proveit -i -s distance3
Processing ./distance3.pvs. Writing output to file ./distance3.summary
Proving chain of imported theories
Proof summary for theory distance3
  Sqrt_x_2_y_2_TCC2.....................unfinished
[shostak](0.09 s)
  Theory totals: 2 formulas, 2 attempted, 1 succeeded (0.09 s)
Grand Totals: 2 proofs, 2 attempted, 1 succeeded (0.09 s)



I can verify this by entering PVS and choosing to re-run the proof for
Sqrt_x_2_y_2_TCC2:
Sqrt_x_2_y_2_TCC2 :


|-------
{1}   FORALL (p_x, p_y: real): (p_x) ^ 2 + (p_y) ^ 2 >= 0


Rerunning step: (subtype-tcc)



{-1}  real_pred(p_x!1)
{-2}  real_pred(p_y!1)
|-------
{1}   expt(p_x!1, 2) + expt(p_y!1, 2) >= 0


Rule?



If I at this point issue the command
(grind), I get the QED that I would expect.


Am I doing something wrong, or is this a known issue? I could be wrong,
but I think it used to work in PVS Version 5.


Best Regards
Ben Hocking
benjaminhocking@xxxxxxxxx