CountreExample代KodKod

Question

我剛剛切換到使用KodKod我仍然試圖瞭解它。我寫了一個程序來幫助我理解，我成功地看到了解決方案是否滿意或不滿意。

我希望能夠看到CountreExample就像我們在合金通常做的，我找到了方法證明型解決方案的（）但它總是返回空。

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

預先感謝您。

Answer 1

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