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

re: a question about a missing TCC

> Date: Sun, 3 Oct 1999 08:21:56 -0400 (EDT)
> From: Mark Aronszajn <aronsz@csee.wvu.edu>
> To: pvs_help list_serve <pvs-help@csl.sri.com>
> Subject: a question about a missing TCC
> I had a parameter on a theory:
>         Sample [
>                 Max_Vertex: ({v: nat| 0 < v})
>         ]: THEORY...
> generating the following TCC:
>         max_vertex_TCC1: OBLIGATION
>   EXISTS (x: ({max_vertex: nat | 0 < max_vertex})): TRUE;
> But subsequently, I added a second parameter; I had:
>         Sample [
>                 Max_Vertex: ({v: nat| 0 < v})
>                 Max_Edges: ({e: nat| 0 < e})
>         ]: THEORY...
> and I don't get a TCC for the new parameter 'Max_Edges'.  That doesn't
> seem right.  I've tried deleting my old Sample.bin and Sample.prf files
> and I still get the same typechecking result.  Why is there no TCC
> generated for 'Max_Edges'?
> Mark Aronszajn

I believe this message was incorrectly forwarded here at SRI from
pvs-help to pvs-bugs.   Our apologies. 

The explanation for the missing TCC is that it is subsumed by the one
already generated.   When PVS typechecks a theory it tells you about
subsumed TCCs in the minibuffer:

Sample typechecked in 0.23s: 2 TCCs, 0 proved, 1 subsumed, 1 unproved; 1 msg

Here we see that there is 1 subsumed TCC; we also see that there is 1
message.   Messages are new in PVS 2.3; they record information about
actions PVS took during typechecking, such as suppressing TCCs, or
applying conversions.   You can display the messages by M-x
show-theory-messages.   Here, you get:

Messages for theory Sample:

Existence TCC for #<FORMAL-CONST-DECL Sample.Max_Edges>:
    EXISTS (x: ({e: nat | 0 < e})): TRUE
  is subsumed by earlier TCC Max_Vertex_TCC1
  so is not generated

Apologies for the delay in answering this.
John Rushby