# Checking a function
**URL:** https://alloytools.discourse.group/t/checking-a-function/357
**Category:** models
**Created:** [June 13, 2023, 12:19pm UTC](https://alloytools.discourse.group/t/checking-a-function/357 "2023-06-13T12:19:46Z")
**Posts on this page:** 7
**Page:** 1
### Author:  [@mputic100](https://alloytools.discourse.group/u/mputic100)
#### Post date: [June 13, 2023, 12:19pm UTC](https://alloytools.discourse.group/t/checking-a-function/357/1 "2023-06-13T12:19:46Z")
I have the following simple model:
```auto
-- 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!
---
### Author:  [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)
#### Post date: [June 14, 2023, 7:21am UTC](https://alloytools.discourse.group/t/checking-a-function/357/2 "2023-06-14T07:21:19Z")
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).
---
### Author:  [@mputic100](https://alloytools.discourse.group/u/mputic100)
#### Post date: [June 14, 2023, 4:26pm UTC](https://alloytools.discourse.group/t/checking-a-function/357/3 "2023-06-14T16:26:17Z")
@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:
```auto
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
```auto
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:
```auto
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?
---
### Author:  [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)
#### Post date: [June 14, 2023, 4:52pm UTC](https://alloytools.discourse.group/t/checking-a-function/357/4 "2023-06-14T16:52:18Z")
> [@mputic100](#):
>
> I thought `a` and `d` could be sets?
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.
> [@mputic100](#):
>
> ```auto
> pred addDevice[a: Account, d: Device] {
> (a -> d) not in devices // guard
> (a -> d) in devices' // next state devices contains association(s)
> }
>
> ```
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).
---
### Author:  [@mputic100](https://alloytools.discourse.group/u/mputic100)
#### Post date: [June 15, 2023, 1:29pm UTC](https://alloytools.discourse.group/t/checking-a-function/357/5 "2023-06-15T13:29:19Z")
Thanks @grayswandyr! With your responses, I reworked my model to this:
```auto
-- 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”
```auto
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
```auto
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
```auto
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
```auto
{ trace_0[a, d0, d1] and univ' } = { trace_1[a, d0, d1] and univ' }
```
I’m stuck, please help. 🤦🏻♂️
---
### Author:  [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)
#### Post date: [June 16, 2023, 5:34pm UTC](https://alloytools.discourse.group/t/checking-a-function/357/6 "2023-06-16T17:34:12Z")
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:
```auto
-- 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 }
```
---
### Author:  [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)
#### Post date: [June 20, 2023, 8:21am UTC](https://alloytools.discourse.group/t/checking-a-function/357/7 "2023-06-20T08:21:46Z")
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:
```auto
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
```