Begginner - Open PVSio following the tutorial

[Victor Candeira]

Hi, everyone. I'm new in PVS and started following the tutorial on https://github.com/nasa/vscode-pvs/blob/master/vscode-pvs/docs/TUTORIAL.md. 

My helloworld has the same script of step 3 - Proof Obligations (TCCs).

helloworld: THEORY

BEGIN

posreal: TYPE = { r: real | r >=0 }

abs (x: real): posreal = IF x > 0 THEN x ELSE -x ENDIF

END helloworld

When I typecheck the file, get the message "helloworld.pvs typechecks sucessfully". After discharge all TCCS, get a summary of both tests on the tcc file.

.tcc file

%% TCCs associated with theory helloworld

%% This file was automatically generated by PVS, please **do not modify** by hand.

helloworld_TCCS: THEORY BEGIN

% Subtype TCC generated (at line 4, column 43) for x

% expected type posreal

% proved

abs_TCC1: OBLIGATION

FORALL (x: real): x > 0 IMPLIES x >= 0

% Subtype TCC generated (at line 4, column 50) for -x

% expected type posreal

% proved

abs_TCC2: OBLIGATION

FORALL (x: real): NOT x > 0 IMPLIES -x >= 0

END helloworld_TCCS

.summary file

TCCs summary for theory helloworld

abs_TCC1........................................................✅ proved (0.319 s)

abs_TCC2........................................................✅ proved (0.316 s)

Theory helloworld totals: 2 formulas, 2 attempted, 2 succeeded (0.635 s)

But when I try to open in PVSio (step 4 - Testing), through right click on editor in the pvs file and selecting the option "Evaluate in PVSio", get this message: "Error: could not start Evaluator session. Please check that the file typechecks correctly.".

What am I doing wrong? Sorry for the silly question, but I already revised the steps, tutorial, FAQ, search the message on google and had no sucess so far.

[Paolo Masci]

Hi, thank you for reaching out!

That's a bug of the action item in the vscode-pvs menu, I will soon push a new version with the fix.

To start PVSio while waiting for the new version with the fix, please use the inline code lens action "evaluate-in-pvsio" shown above the theory name (see attached screenshot)

Thanks!

Paolo

[Victor Candeira]

Made a fast test and it worked. Thank you so much, Paolo! I'll get to the tutorial and my studies soon.

[Paolo Masci]

Hi, the bug with the vscode-pvs menu should be resolved in this new pre-release 1.0.64-theta: https://drive.google.com/file/d/1XTnUoPie9Yu5TW-z7b0sonBKWnNPB1xa/view

Thanks,

Paolo