Retrieve Traces from alloy

Question

Is there a way to retrieve the trace of 'Events' (Predicates) from alloy into a xml for test case generation.

For example for the model:

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

I would like to retrieve the trace of events/predicates that consists of init/deposit/withdraw. The only thing I can find is the the show_change variable however this does not immediately indicate which event/predicate was true.

Answer 1

You could evaluate the predicates in the instance to know if they hold for a given savingAccount. To do so you might use the evaluator integrated in the Alloy Analyzer, or write your own small java program that would call the method eval() on an A4Solution.