[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: library importings
It sounds like you found a bug. Is there any chance you
could send me the specs so I can chase it down?
> 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,
> 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
> - 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!
> Marieke Huisman