[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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"
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!