Date: Tue, 24 Jul 2007 20:13:58 -0000
From: Christian Estler

Hello, I'm trying to prove a Downward Simulation for an abstract
and a conrete Z specifiaction using Alloy RC-10.

The idea is to have a "lamp" that can be switch on or off, depending
on the actual status of the lamp.
In the abstract model, the status value is given as "on" or "off". In
the concrete model it is given as a boolean value.
Initially, the lamp is "off" and "false", respectively.

As Init is handled as an operation in Z, I'm also trying to implement
it as one in Alloy. My actual translation is:

--------------------
-- Abstract Model --
--------------------

abstract sig Status {}

one sig ON, OFF extends Status {}

sig Lamp_abs {
   status: Status
}

pred Init_abs [l: Lamp_abs] {
   l.status in OFF
}

pred Switch_abs [l, l': Lamp_abs] {
   l.status in ON => l'.status in OFF
   l.status in OFF => l'.status in ON
}

For the concrete model I'm using the moduel boolean which comes with Alloy.

-------------------
-- Conrete Model --
-------------------

open util/boolean as B

sig Lamp_con {
  active: B/Bool
}

pred Init_con [l: Lamp_con] {
   l.active = B/False
}

pred Switch_con [l, l': Lamp_con] {
   l'.active = B/Not[l.active]
}

Furthermore, I have to define a "Retrieve Relation" between the
abstract and the concrete model.

-----------------------
-- retrieve relation --
-----------------------

pred R[la: Lamp_abs, lc: Lamp_con] {
   (la.status in ON) <=> B/isTrue[lc.active]
   (la.status in OFF) <=> B/isFalse[lc.active]
}

To prove that C is a downward simulation of A, I have to prove (among
other things) that: "for all CState' such that CInit => there exists
AState'  such that AInit and R'".

Or written in Tex-Notation using the OZ style: "\forall CState' @
CInit \implies \exsits AState' @ AInit \land R'"  where @ denotes the
bullet.

Intuitively I worte an Alloy assertion like this one:

assert init {
  all c: Lamp_con |
     Init_con[c] => (some a: Lamp_abs | Init_abs[a] and R[a, c])
}

Checking the assertion always produces a counterexample which can be
reduced to the situation that Alloy finds an instance such that
Lamp_con.active maps to B/False while Lamp_abs.staus maps to ON.

For my own understandig, I want to know, why Alloy produces such a
counterexample. Am I right that Alloy checks all possible instances of
the model and because there are valid models where (one or more)
Lamp_abs map to ON while Lamp_con maps to B/False the assertion fails?

How do I have to rewirte the assertion to correctly express the Z-formula?
Or maybe my modeling approach is just not adequate?