expansion in sub-vocabulary

The IDP3 manual has this to say about modelexpand(theory, structure, vocabulary) : "The third argument (vocabulary) is optional and allows you to specify a subvocabulary containing only the symbols in which you’re intersted." This is useful to write test cases on part of the theory.

It does not seem to work though:

vocabulary V {
    p
    q
}
theory T : V {
    p.
    q.
}
vocabulary V2 { // a subvocabulary
    p
}
structure S2 : V {
  p = true
}
procedure main(){
    stdoptions.nbmodels = 0
    printmodels((modelexpand(T,S2,V2)))
}

modelexpand(T,S2,V) is correct, but not modelexpand(T,S2,V2). It finds 2 models for p : true and false. But false is not consistent with S2.

Comments (3)