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

Re: Strange problems



I have had this kind of problem where two formulas print the same but
are actually different. For example there could be append[U] in the
antecedent, and append[V] in the consequent. PVS does not always choose
the parameter instantiation that u would expect: it may be necessary to
provide it explicitely sometimes. Alternatively, it may be necessary to
prove some lemma, for example relating append[U] and append[V] in my
example.

I dont know of a PVS display feature that would let u see an expanded
version of the sequent with all the actuals, but it would be helpful to
debug this kind of situation.

In your case, I cannot tell which actual is different, but clearly this
is what happens.

Cheers!
     pyg
Kellom{ki Pertti wrote:
> 
> Maybe someone could help me out with this. I am developing a deep
> embedding of the DisCo (http://disco.cs.tut.fi) specification
> language. While trying to verify some properties of the DisCo
> language based on the embedding, I ran into the following sequent
> which PVS does not recognize to be provable:
> 
> action_superposition.3.1.1.1.1 :
> 
> [-1]  sem(variable_assignments(role_of_object(ob!1, ra!1, roles(a!1)),
>                                append(new_fields(ref!1), fields(a!1)),
>                                append(new_assignments(ref!1), body(a!1))),
>           ra!1, b!1)
>   |-------
> [1]   sem(variable_assignments(role_of_object(ob!1, ra!1, roles(a!1)),
>                                append(new_fields(ref!1), fields(a!1)),
>                                append(new_assignments(ref!1), body(a!1))),
>           ra!1, b!1)
> 
> I use subtypes in the specification, and I suspect this has something
> to do with that, but I have not been able to figure out what goes
> wrong here. At least the typepred command does not do anything useful,
> since it only adds antecedents into the sequent.
> 
> The dump file is available at http://www.cs.tut.fi/~pk/tmp/dump and
> the relevant PVS file is superposition.pvs.
> 
> Any help would be greatly appreciated.
> --
> pertti

-- 
Paul Y Gloess
   E.N.S.E.R.B.:   http://www.enserb.u-bordeaux.fr/~gloess
          LaBRI:   http://dept-info.labri.u-bordeaux.fr/~gloess