有没有办法从合金中检索“事件”（Predicates）的跟踪到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变量，但这并不能立即指出哪个事件/谓词是真的 .
1 回答
您可以评估实例中的谓词，以了解它们是否适用于给定的savingAccount . 为此，您可以使用Alloy Analyzer中集成的求值程序，或编写自己的小型Java程序，该程序将在A4Solution上调用方法eval（） .