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

*To*: "'pvs-help@csl.sri.com'" <pvs-help@csl.sri.com>*Subject*: FW: PVS Problems*From*: TENEVA G Ms -NUCLEAR <galina.teneva@opg.com>*Date*: Wed, 2 Jan 2002 13:00:39 -0500*Sender*: pvs-help-owner@csl.sri.com

Hi, Hi, I have two problems using the PVS, version 2.3, patch level 1.2.2.36. 1) After proving the generated TCCs and the theorem (att. B029.pvs), I can not view the TCCs i.e. if I the click on the "Viewing TCCs" and then on "show-tccs", the content is empty and there is a message "parser error". Take into account, please, that during the process of proving the TCCS or the theorem, no error message appears. As we don't have pvs e-mail working, I attached here the pvs files B029.pvs and math_fun.pvs. The math_fun.pvs has to be typechecked (and so math_fun.bin to be created) before running the B029.pvs. The problem can be avoided if in the function: AbstG_AbstA2D_HTPressure( x: ARRAY[subrange(1,4) -> subrange(0,5119)]): t_SnrValAll = LAMBDA(i:subrange(1,48)): COND ((39 <= i) & (i <= 42)) -> AbstA2D(x((i - (39 - 1)))), ELSE -> epsilon(LAMBDA(randomVal:t_SnrValue): FALSE) ENDCOND the ELSE is replaced by NOT((39 <= i) & (i <= 42)). 2) In the att. CIOB051.pvs, among the other input parameters there are mk_SGLLcondIn and mk_SGLLcondOut. The mk_SGLLcondIn is declared as a constant mk_SGLLcondIn: t_SGLLcondRange = 2349, where t_SGLLcondRange is subrange(2349, 3239). The mk_SGLLcondOut is declared as a variable: mk_SGLLcondOut: VAR {x: t_SGLLcondRange | x < mk_SGLLcondIn}. These two inputs are used in the function f_LogNLowForSGLLconditioning: f_LogNLowForSGLLConditioning( mk_SGLLcondIn: t_SGLLcondRange, mk_SGLLcondOut: {x:t_SGLLcondRange | x < mk_SGLLcondIn}, m_LogN: subrange(0,5119), f_LogNLowForSGLLConditioning_s1: bool): bool = COND (m_LogN >= mk_SGLLcondIn) -> FALSE , ((mk_SGLLcondIn > m_LogN) & (m_LogN > mk_SGLLcondOut)) -> f_LogNLowForSGLLConditioning_s1, (mk_SGLLcondOut >= m_LogN) -> TRUE ENDCOND As you can see, if mk_SGLLcondIn = 2349, then mk_SGLLcondOut has to be < 2349 and as the data type of mk_SGLLcondOut is subrange(2349, 3239), there is no x which can satisfied this condition. In the process of proving this theorem, all tccs are proved and the theorem is proved as well. It is not the case, if in the function f_LogNLowForSGLLConditioning, for the input parameter mk_SGLLcondOut, an explicit value for the input constant mk_SGLLcondIn = 2349 is used: ..... f_LogNLowForSGLLConditioning( mk_SGLLcondIn: t_SGLLcondRange, mk_SGLLcondOut: {x:t_SGLLcondRange | x < 2349}, m_LogN: subrange(0,5119), f_LogNLowForSGLLConditioning_s1: bool): bool = ... Then a type check error "Subtype TCC for mk_SGLLcondOut simplifies to FALSE" appears. As these two versions of the theorem look identical to me, why a typecheck error should appear in one of the cases? Actually I would expect that the same typecheck error will appear in both cases, as there is no x of data type t_SGLLcondRange, which is < 2349. Attached to this e-mail is the pvs file CIOB051.pvs. It has to be run from the same directory where math_fun.bin is(math_fun.bin is automatically produced if math_fun.pvs is typechecked). Best wishes: Galina Teneva

- Prev by Date:
**Category Theory** - Next by Date:
**Re: FW: PVS Problems** - Prev by thread:
**Re: Latex printing. a problem.** - Next by thread:
**Re: FW: PVS Problems** - Index(es):