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

abstraction in model-checker


When using the model-checker we must first creating a specific state.

Vertex: Type
V: type = [# var1 : int, var2 : boolean #]

state : Type = [# c : finite_set[Vertex],
                  v : V #]

Because of the use of an infinite type in the state type, I have created a
infinite state-space and this I can solve by using an abstraction. And as
a consequence i use the command "abstract-and-mc" with three parameters

first parameter: state    (the record which defines the state)
second parameter: abs_state (an abstracted type of type state)
third parameter: an abstraction expression

However I think I know how to use the first and the last parameter but I
do not know how to create the second parameter. How must I create such an
abstracted type?

Thanks for the help,