从合金中检索痕迹

Question

有没有办法将“事件”（谓词）从合金中检索到用于生成测试用例的 xml 中。

以模型为例：

module tryout
open util/ordering[savingAccount]

sig savingAccount{
    amount : Int,
}

pred init(s : savingAccount){
    s.amount = 0
}

pred withdraw(before : savingAccount, after : savingAccount, withdrawal : Int){
    gt[withdrawal,0]
    lt[withdrawal, before.amount]
    after.amount = sub[before.amount,withdrawal]
}

pred deposit(before : savingAccount, after : savingAccount, deposit : Int){
    gt[deposit,0]
    after.amount = add[before.amount,deposit]
}

fact traces{
    init[first]
    all s: savingAccount - last | let s' = next[s] | 
    some change: Int | deposit[s,s',change] or withdraw[s,s',change]
}

pred show{}

run show for 5 Int,10 savingAccount

我想检索由 init/deposit/withdraw 组成的事件/谓词的踪迹。我唯一能找到的是 show_change 变量，但这并不能立即表明哪个事件/谓词为真。

Answer 1

您可以评估实例中的谓词以了解它们是否适用于给定的 SavingAccount。为此，您可以使用 Alloy Analyzer 中集成的评估器，或者编写您自己的小型 Java 程序，该程序将调用 A4Solution 上的方法 eval()。