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

Re: library importings

Hi Marieke,

It sounds like you found a bug.  Is there any chance you
could send me the specs so I can chase it down?


> Hi,
> I have two questions about library importings.
> I have generated two PVS specifications, one of a defensive virtual 
> machine, one of an offensive one. These specifications have many 
> datatype and theory names in common, so to avoid conflicts I've put 
> them in two directories:
> Offensive and Defensive.
> I try to import these as two different libraries:
>   defensive : LIBRARY = "Defensive"
>   offensive : LIBRARY = "Offensive"
>   IMPORTING defensive@nEG_def,
>             offensive@nEG_def
> When I try this with a small example, but here I get two problems:
> - I have constructed .bin files in the Defensive and Offensive 
> directories, but sometimes PVS does not only restore the bin files, 
> but also starts to typecheck, and then it returns with a typecheck 
> problem.
> - In case PVS does not produce a type check problem, it restores all 
> the bin files and finally produces the following error:
> Error: the assertion ITHEORY failed.
> Are there ways I can avoid these problems? Are there better ways to 
> do these importings?
> Any help would be appreciated!
> Thanks,
> Marieke Huisman