CountreExample代KodKod

Question

我刚刚切换到使用KodKod我仍然试图了解它。我写了一个程序来帮助我理解，我成功地看到了解决方案是否满意或不满意。

我希望能够看到CountreExample就像我们在合金通常做的，我找到了方法证明型解决方案的（）但它总是返回空。

我想知道是否有办法返回CountreExample或不。

预先感谢您。

Answer 1

试着看这个合金API用法的例子：https://github.com/kaptoxic/alloy/tree/master/src/edu/mit/csail/sdg/alloy4whole