Search code examples
alloy

Implication vs. Disjunction operators

I must have a misunderstanding somewhere. Here is a specification of everyone's favorite bank account/transfer system:

sig User {
  var balance: one Int
}

var one abstract sig Message {}

var lone sig TransferEvent extends Message {
  var from: User,
  var to: User,
  var amount: Int,
}

pred transfer[from: User, amt: Int, to: User] {
  /* preconditions: */
  { 
    0 <= amt
    amt <= balance[from]
    from != to
  }
  /* postconditions: */
  {
    balance'[from] = minus[balance[from], amt]
    balance'[to] = plus[balance[to], amt]
    all k: User |
      (k != from and k != to) implies balance'[k] = balance[k]
  }

}

pred init {
  all u: User | balance[u] >= 0
}

// A step is either a transfer or a 'stuttering' step
pred step {
  { 
    some TransferEvent
    transfer[Message.from, Message.amount, Message.to]
  } or
  {
    no Message and balance = balance'
  }
}

// The behaviors are those that are reachable from states satisfying
// init via infinitely many "step" steps
pred spec {
  init
  always step
}

run spec for 3 but exactly 3 User, exactly 3 steps, 3 int


fun total: Int {
  sum u: User | balance[u]
}

assert Constant {
  (not spec) or (always (total' = total)) // no counterexample if we execute 'check Constant'
  // (spec) => (always (total' = total)) // finds a counterexample
}

check Constant for 3 int

At the bottom I have a property I expect to hold of the model: basically, the traces specified by spec should be a subset of the traces where the total is constant. If I write this using implication (spec implies always P), then I get a counterexample when executing check Constant. However, if I write (not spec) or (always P) (which I thought should be equivalent), then alloy does not find a counterexample.

I'm thinking there's some obvious misunderstanding or glaring error in my spec, but I just can't seem to figure it out.

I have 'prevent overflows' set to 'yes'.

Solution

  • This is probably a bug in the evaluator. This is the only counterexample I get:

    Counterexample

    In the REPL, though, 3.plus[1] = -4, not -2. Alloy's handling of integer's has always been a little bit wonky, so my instincts are that's cropping up here. If you change "prevent overflows" to "no", the counterexample disappears.

    As for the specific question you asked, P => Q is the same as (not P) or (Q), excepting (as in this case) a bug.