Checking a function

models
1

I have the following simple model:

-- SIGNATURES

sig Device {}

sig Account {
  var devices: set Device,
} 

-- CONSTRAINTS

// Initial conditions
fact init {
  no devices    // No devices, they will get added using addDevice
}

// Always true
fact {
  // If a device is in Account.devices, it got there through addDevice
  always (all a: Account, d: Device | (d in a.devices) implies once addDevice[a, d])
}

-- PREDICATES

pred addDevice[a: Account, d: Device] {
  (a -> d) not in devices       // guard
  devices' = devices + (a -> d) // next state devices adds association
}

fun addDevice : Account -> Device {
  { a: Account, d: Device | addDevice[a, d] }
}

-- CHECK

check {
  no devices      // No devices in the init state
  eventually some a: Account, d: Device | 
    ((a -> d) in devices') implies (once addDevice[a, d])
}

The second fact is intended to enforce that the only way a Device can get added to devices is if addDevice was called on it.

The check statement is intended to check the assertion above: that if we start with an empty devices, and eventually there is an association Account -> Device in devices, it implies that addDevice was once called. However, when I run it, it gives me counterexamples where devices is always empty.

I think what Alloy is trying to tell me is that the only way for this assertion to not be true is if devices is always empty? But doesn’t that violate the eventually some a: Account, d: Device | ((a -> d) in devices') part?

Either the second fact is expressed incorrectly or my check statement is not expressing what I intended.

Please help clarify my misunderstanding, thank you!

2

First you don’t need the no devices in the check as it’s already a fact (also, here an implication would have been necessary to constrain all traces on which you want to evaluate the eventually part).

Now, what your model says is that if there’s something in devices, then addDevice has been called. And then you check whether, in the future, there will be a pair in devices that will either not be in devices or it will have been added to it.

However you never said that devices will effectively become nonempty. So that’s indeed a way to satisfy the spec while violating the check: in traces where devices is always empty, there won’t be any pair a->d such that…

One way out of this is to change the fact to say that devices will become nonempty. Another is to rewrite the fact by saying that, in every state, there is a pair such that addDevice is fired (you will likeley also need a stutter event).

3

@grayswandyr Thank you so much for your reply!

First you don’t need the no devices in the check as it’s already a fact

Agreed! Removing this line.

One way out of this is to change the fact to say that devices will become nonempty.

OK, I’ll add a new fact:

fact "devices will eventually become nonempty" {
  eventually some devices
}

Now when I run the check, no counterexamples are found! Thanks!

Additionally, I noticed that for some reason, my original definition of addDevice only supports adding one Account -> Device pair at a time. That’s not what I wanted.

First, I wrote a scenario

run {
  after #devices > 1
}

that basically says, is there a way for the count of devices to be greater than 1 in the second step?

Surprisingly, no!

I played with the predicate until I arrived at this modification:

pred addDevice[a: Account, d: Device] {
  (a -> d) not in devices // guard
  (a -> d) in devices'    // next state devices contains association(s)
}

Now when I check my scenario above, it indeed finds an instance in which more than one device is added in the first time step.

But why does devices' = devices + (a -> d) not allow multiple pairs to be added to devices in one time step? I thought a and d could be sets?

4

They could indeed. But you only call it with singletons: in all a: Account, d: Device, you consider all combinations of one account and one device.

Writing an operation like this may in general be problematic: when you write (a -> d) in devices', you’re often not constraining the effect enough. You’re not saying anything about the remaining of devices': so for instance, devices lose tuples as long as it contains a->d, or grow arbitrarily as long as it contains a->d (then why specifically consider a->d instead of other tuples?).

There are several ways to address the issue, but they are linked to the chosen specification style so it’s a bit difficult to explain clearly (here you chose to say that some operation has happened if a certain state is observed, which is not “wrong” but not completely conventional).

1 Like
5

Thanks @grayswandyr! With your responses, I reworked my model to this:

-- SIGNATURES

sig Device {}

sig Account {
  var devices: set Device,
} 

-- CONSTRAINTS

// Initial conditions
fact init {
  no devices    // No devices, they will get added using addDevice
}

fact "Devices must be added using addDevice" {
  // If a device is in Account.devices, it got there through addDevice
  always {
    all a: Account, d: Device | {
      (a -> d) in devices implies once addDevice[a, d] else (a -> d) not in devices
    }
  }
}

fact "devices will eventually become nonempty" {
  eventually some devices
}

-- PREDICATES

pred addDevice[a: Account, d: Device] {
  (a -> d) not in devices         // guard
  devices' = devices + (a -> d)   // next state devices adds association
}

fun addDevice : Account -> Device {
  { a: Account, d: Device | addDevice[a, d] }
}

Now I’m trying to prove that the order in which devices are added to an account doesn’t matter, and I’ve been banging my head against the wall on this one …

Here was my thought process as I stumble through this:

To be more specific, I want to prove that for two sets of arguments {(a -> d0), (a -> d1)}, the order in which addDevice is called does not matter. So I’m saying that if we call addDevice[a, d0] and then later we call addDevice[a, d1], we will end up in the same final state as if we did it the other way around.

First I’ll need a predicate that defines the “final state”

pred final_state_reached[ad: Account -> Device, a: Account, d0, d1: Device] {
  (a -> d0) in ad and (a -> d1) in ad
}

Then for convenience I’ll define two traces, one for each order of operations

pred trace_0[a: Account, d0, d1: Device] {
  addDevice[a, d0]
  after addDevice[a, d1]
}

pred trace_1[a: Account, d0, d1: Device] {
  addDevice[a, d1]
  after addDevice[a, d0]
}

Now maybe I can structure the assertion like this

check {
  all a: Account, disj d0, d1: Device | {
    trace_0[a, d0, d1] or trace_1[a, d0, d1]
  } implies {
    eventually final_state_reached[devices, a, d0, d1]
  }
}

No counterexample found. OK!

But I’m not fully convinced.

What I really want to check for is that all the effects of trace0 and trace1 are the same. final_state_reached only tells me if the state of devices is the same, but I want to know if the state of everything is the same.

In Alloy, “everything” is univ (right?), so I want to check that the state of univ after trace0 is equivalent to the state of univ after trace1.

So maybe my assertion could be

{ trace_0[a, d0, d1] and univ' } = { trace_1[a, d0, d1] and univ' }

I’m stuck, please help. :man_facepalming:t2:

6

The semantics of LTL, the temporal logic underlying Alloy, is defined on a given trace. So your check is evaluated on a single trace.

In general, a property of the shape "for all trace t1 such that …, there is a trace t2 such that …` is called a hyper-property. Hyper-properties cannot in general be expressed in LTL, although some tricks are possible for some kinds of hyper-properties.

Second it’s clear that trace_0 and trace_1 are exclusive since d0 and d1 are disjoint (btw, trace_0[a,d0,d1] <=> trace_1[a,d1,d0] so no need to define a trace_1 pred). So you could as well check all ... | trace_0[...] => eventually ..., which is true. As a side note, your formula is only evaluated in the initial state, the way it’s written.

(Also, note the nice operator ; that allows you to mimic sequence. A;B means A and after B, so you could have written pred trace_0[...] { addDevice[a, d0]; addDevice[a, d1] }.)

Now, I don’t think it’s of any use here for the reasons said above, but univ is, in every state, the union of all atoms existing in that state. The definition is per state because a spec may contain toplevel var sigs whose valuation may change in every state. If the only toplevel sigs are static, then univ is constant over a trace.

Finally, I’m pasting a version of your model which is perhaps more common in its modeling style, for reference:

-- SIGNATURES

sig Device {}

sig Account { var devices: set Device } 

fact init { no devices }

// EVENTS

pred add[a: Account, d: Device] {
  (a -> d) not in devices         // guard
  devices' = devices + (a -> d)   // next state devices adds association
}

pred skip { devices' = devices }

fact traces { always some a: Account, d: Device | add[a, d] or skip }

check { always { a: Account, d: Device | before once add[a,d] } = devices }
7

I had more time to complete my previous answer. As I said, you can’t compare traces. But you can say that, in a trace, if devices grows strictly by two tuples, then add must happen twice, in either ordering:

sig Device {}

sig Account { var devices: set Device } 

fact init { no devices }

pred add[a: Account, d: Device] {
  (a -> d) not in devices       
  devices' = devices + (a -> d)  
}

pred skip { devices' = devices }

fact traces { always some a: Account, d: Device | add[a, d] or skip }

check { always { a: Account, d: Device | before once add[a,d] } = devices } expect 0

// WRONG
check { 
	always all a1, a2: Account, d1, d2:Device {
		(a1->d1 != a2->d2 and devices'' - devices = a1->d1 + a2->d2) implies
			((add[a1,d1]; add[a2,d2]) /*or (add[a2,d2]; add[a1,d1])*/) }} expect 1

// OK
check { 
	always all a1, a2: Account, d1, d2:Device {
		(a1->d1 != a2->d2 and devices'' - devices = a1->d1 + a2->d2) implies
			((add[a1,d1]; add[a2,d2]) or (add[a2,d2]; add[a1,d1])) }} expect 0