使用Alloy API生成与模型实例对应的.als文件

Question

假设我有以下模型：

sig counter{
value: Int,
}
{
 value > 0
 value < 3
}
pred show{}

run show for exactly 1 counter

我想生成与此模型的两个实例相对应的als文件：

open counter 
one sig counter_1 extends counter{}{ value=1 }   
fact { counter = {counter_1}}

和

open counter 
one sig counter_2 extends counter{}{ value=2 }   
fact { counter = {counter_2}}

我已经使用Alloy API生成了实例，但是我找不到将它们导出到als文件的方法（除非解析xml或txt文件）。

我可以想象存在这样一种方法，特别适合进行模型转换的人（这是我的情况，因为我想将实例转换回原始的méta模型）

有任何提示吗？谢谢

Answer 1

我认为没有一种方法可以轻松地做到这一点。有一个pkriens/api分支提供了API，它将使导出该API更容易，因为您可以将解决方案作为易于使用的API对象获得。

Answer 2

似乎您已经具有符合您的描述的.als文件；它们在问题的第二和第三代码块中给出。