No livro Software Abstractions , capítulo 5.2.2 Skolemization, ele menciona,
onde sxé uma nova variável livre e F[sx/x]é a restrição F, sxsubstituída por x.
Porém quando apresento a variável livre no Alloy, aparece erro de sintaxe. O Alloy aceita variável livre?
sig A {
relation: A
}
fact {
some A
}
check{
//correct expression
//some a : A | one a.relation
//Skolemization
(a: A) and (one a.relation)
}