# A real-world success story

**URL:** <https://alloytools.discourse.group/t/a-real-world-success-story/443>\
**Category:** models\
**Created:** [February 13, 2024, 7:49am UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443 "2024-02-13T07:49:08Z")\
**Posts on this page:** 13\
**Page:** 1

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [February 13, 2024, 7:49am UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/1 "2024-02-13T07:49:08Z")

</div>

Hello! My company is implementing a permissions-based filesystem, and the reason I joined this forum and learned Alloy was to see if I could use it to stress-test our permissions model. This project turned out to be wildly successful. I found several major but non-obvious holes in our model, and we’re now building it on a much more solid foundation.

The rules of our flawed permissions model:

- For each File or Folder, an administrator can assign an access level (Use, Edit, or Own) to a Group.
- If the admin doesn’t explicitly assign an access level to a File or Folder, then that File or Folder’s access level will be inherited from the nearest ancestor that _does_ have an explicit access level set.
- A User can be a member of multiple Groups, and the User’s permissions for each File will be the _max_ of each Group’s permissions for that File.
- If a User has Own access to a File or Folder, they can move it to a different Folder that they also have Own access to.

This model seemed sound to us, but Alloy shows that there are tricky scenarios where users can move folders to give themselves access to files they couldn’t access before. There are also tricky scenarios where users can _lose_ access to files. _ **This is a system where you can move a file that you own, into a folder that you own… and as a result, somehow, you’ll no longer own the file and can’t move it back!** _

1. To see how users can move folders around to give themselves access they didn’t originally have, run `user_cannot_gain_or_lose_access` and see the failure.
2. Next, uncomment the code below `// User must also own all of the source object's children` in the `move_object` predicate. This represents a patch we made to prevent users from gaining access. But users can still _lose_ access! Run `user_cannot_gain_or_lose_access` again to see how.
3. Finally, run `user_cannot_gain_or_lose_access_if_children_have_greater_explicit_perms_than_parents`. Here, we ask what happens if each child file or folder must always have an access level greater than or equal to that of its parent. This results in a model where users cannot gain or lose access by moving things around.

I’m planning on polishing this story up for public consumption, and hopefully getting more people interested in Alloy. If you have any tips on how to make this spec shine, let me know!

```auto
/**
 * Model representing a permissions-based filesystem.
 *
 * It has these facts, which are true today:
 *
 * 1. There are pages and folders arranged in a tree.
 * 2. A User can have many Groups, and a Group can have many Users.
 * 3. There are four levels of access, in decreasing order of strength:
 * Own, Edit, Use, and None.
 * 4. A user's level of access to an object is the max of their group's levels
 * of access.
 * 5. A group's level of access to an object is the permission it was
 * explicitly granted, either to that object or to its nearest ancestor
 * with an explicit grant.
 * 6. A user can move any page that they Own.
 *
 * And we are thinking of adding this fact:
 *
 * 7. A user can also move any folder that they Own.
 *
 * There's a property that I think is pretty important in a permissions system:
 *
 * 1. If a user does not have access to an object, they can never give
 * themselves access to the object just by moving objects around.
 *
 * This spec shows that this property **no longer** holds when we give users
 * the ability to move Folders.
 */

// There is always exactly one RootFolder
one sig RootFolder {
}

// Each Object has a parent Folder
abstract sig Object {
    var parent: one (Folder + RootFolder)
}

// There are two kinds of Object: Page and Folder
sig Page, Folder extends Object {
}

fact all_objects_connected_to_tree {
    always {
        all object: Object {
            RootFolder in object.*parent
        }
    }
}

fact tree_is_acyclic {
    always {
        no folder: Folder {
            folder in folder.^parent
        }
    }
}

abstract sig Perm {
    includes: lone Perm
}

one sig Own, Edit, Use, None extends Perm {
}

/**
 * If you own an object, you can edit it. If you can edit it, you can use it.
 */
fact permission_rankings {
    Own.includes = Edit
    Edit.includes = Use
    Use.includes = None
    None.includes = none
}

// For now, we use only one User. Maybe we can have more, but I'm not sure what
// properties we care about when multiple users are involved.
one sig User {
    // A User can be a member of multiple Groups
    groups: set Group,
    var implicit: Perm -> Object,
} {
    always {
        all perm: Perm, object: Object |
           user_implicit[perm, object] <=> object in implicit[perm]
    }
}

sig Group {
    // The Objects this Group was explicitly granted permissions for
    explicit: Perm -> Object,
} {
    // You can only specify one setting for a Group/Object combination
    disj [explicit[Own], explicit[Edit], explicit[Use], explicit[None]]
}

/**
 * True if `group` implicitly grants `needed_perm` to `object`, based on the
 * directory structure of `object`.
 */
pred group_implicit[needed_perm: Perm, group: Group, object: Object] {
    some group_perm: Perm, ancestor_folder: object.*parent | {
        // True if the group has explicit permission for some ancestor folder
        ancestor_folder in group.explicit[group_perm]
        // and this permission is at least as strong as the permission we need
        needed_perm in group_perm.*includes
        // And also there is no middle folder, in between us and that ancestor,
        // which has a weaker explicit permission
        no
            middle_folder: (object.*parent - ancestor_folder.*parent),
            weaker_perm: Perm
        {
            needed_perm not in weaker_perm.includes
            middle_folder in group.explicit[weaker_perm]
        }
    }
}

pred user_implicit[needed_perm: Perm, object: Object] {
    // A user has implicit permission on an object if any of its groups have
    // that implicit permission
    some group: User.groups | group_implicit[needed_perm, group, object]
}

pred move_object[
    source_object: Object,
    target_folder: Folder + RootFolder
] {
    // User must own the source object
    user_implicit[Own, source_object]
    // User must own the target folder
    user_implicit[Own, target_folder]
    // Object must not be a parent of the folder you're moving it into
    not source_object in target_folder.*parent
    // Object's parent becomes the target folder
    source_object.parent' = target_folder
    // All other parents stay unchanged
    all object: Object - source_object | object.parent' = object.parent
}

fact users_can_move_objects {
    always {
        one
            source_object: Object,
            target_folder: Folder + RootFolder
        | move_object[source_object, target_folder]
    }
}

run {
} for 3 Object, 2 Group, 2 steps

/**
 * True if a user never gains access to an app
 */
check user_cannot_gain_access {
    all missing_perm: Perm, inaccessible_object: Object |
        not user_implicit[missing_perm, inaccessible_object] =>
            always not user_implicit[missing_perm, inaccessible_object]
} for 3 Object, 2 Group, 2 steps

/**
 * True if the user never gains or loses access to an app
 */
pred user_cannot_gain_or_lose_access {
    all missing_perm: Perm, inaccessible_object: Object |
        user_implicit[missing_perm, inaccessible_object] <=>
            always user_implicit[missing_perm, inaccessible_object]
}

check user_cannot_gain_or_lose_access {
    user_cannot_gain_or_lose_access
} for 3 Object, 2 Group, 2 steps

check user_cannot_gain_or_lose_access_if_only_one_group {
    user_cannot_gain_or_lose_access
} for 3 Object, 1 Group, 2 steps

/**
 * True if a folder never has a parent other than the root.
 */
pred subfolders_not_shipped {
    always {
        all object: Folder | object.parent = RootFolder
    }
}

check user_cannot_gain_or_lose_access_without_subfolders {
    subfolders_not_shipped => user_cannot_gain_or_lose_access
} for 3 Object, 2 Group, 2 steps

/**
 * True if a subfolder always has greater explicit permissions than its parents
 */
pred children_have_greater_perms_than_parent {
    all
        group: Group,
        child_perm: Perm,
        child: group.explicit[child_perm],
        ancestor: child.^parent - RootFolder |
            some ancestor_perm: Perm | {
                ancestor in group.explicit[ancestor_perm]
                ancestor_perm in child_perm + child_perm.includes
            }
}

check explicit_greater_implies_implicit_greater {
    children_have_greater_perms_than_parent =>
        all perm: Perm, child: Object, ancestor: child.^parent - RootFolder |
            user_implicit[perm, ancestor] => user_implicit[perm, child]
} for 3 Object, 2 Group, 1 steps

run children_have_greater_perms_than_parent for 3 Object, 2 Group, 2 steps

check user_cannot_gain_or_lose_access_if_children_have_greater_explicit_perms_than_parents {
    children_have_greater_perms_than_parent => user_cannot_gain_or_lose_access
} for 3 Object, 2 Group, 2 steps

```

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [February 13, 2024, 10:02am UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/2 "2024-02-13T10:02:04Z")

</div>

Hi, looks great. I’m looking forward to reading the said story, this looks quite compelling.  
A few remarks:

- `includes` looks like a total order. In that case, you could just make `Perm` “util/ordered” and use `next` instead of `includes`, thus benefiting for free from the preds and funs defined in `util/ordering`. Actually, you can even make `Perm` an enum. In that case, it will be implicitly “util/ordered” (following the order of declarations in the enum) _and_ I think it should be more efficient in general. If you want to keep the name `includes`, you could even add `fun includes : Perm -> Perm { ordering/next }`.
- a signature-local fact as in `User` implicitly starts with `always all this: User | ...` so the `always` on line 87 can be removed.
- in `Group`, can’t you remove the local fact and rather type `explicit` as `Perm -> (l)one Object`, as it means `always all g: Group, p: Perm | (l)one g.explicit[p]`, which seems to do what you want.
- depending on your needs, you may remove the `RootFolder` declaration and make `parent` `lone`, with an additional fact stating that there’s only one folder which doesn’t have a parent (you could even define it with a fun, then). It may enable you to make less distinctions between this specific folder and others. Indeed, it’s a bit strange that `RootFolder` isn’t a folder itself in your model.
- finally, the two facts `all_objects_connected_to_tree` and `tree_is_acyclic` could perhaps be made assertions rather than facts, because as facts they may rule out bad scenarios implicitly. The price to pay, if you made them assertions, is that you should probably also add new operations to account for the creation of the file system (instead of considering it as a given).

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [February 14, 2024, 7:03am UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/3 "2024-02-14T07:03:58Z")

</div>

Thank you! Implementing your suggestions now. [You can find the most current version of the code on GitHub](https://github.com/jthemphill/permission-model/blob/main/user-moves-owned-subtrees.als)!

The two exceptions:

> [@grayswandyr](#):
>
> - in `Group`, can’t you remove the local fact and rather type `explicit` as `Perm -> (l)one Object`, as it means `always all g: Group, p: Perm | (l)one g.explicit[p]`, which seems to do what you want.

I think this needs to be `Perm lone -> Object`. A Group can have explicit Permissions for many Objects, but a Group cannot assign multiple explicit Permissions to the same Object. This seems to have the same semantics as the `disj[this.explicit[Own], this.explicit[Edit], ...]` fact did.

> [@grayswandyr](#):
>
> - finally, the two facts `all_objects_connected_to_tree` and `tree_is_acyclic` could perhaps be made assertions rather than facts, because as facts they may rule out bad scenarios implicitly. The price to pay, if you made them assertions, is that you should probably also add new operations to account for the creation of the file system (instead of considering it as a given).

I think that might be out of scope😅 My philosophy is that we write facts to describe the code we explicitly wrote into the system, and we write assertions to describe the properties that we hope will emerge from the system. Our filesystem already has code to guarantee a tree structure, and my goal is to keep the spec under 250 lines even with extensive comments. I’m hoping to impress upon readers just how short a spec you can write in order to stress-test an idea that, to mortals, might look perfectly sound😉

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [February 14, 2024, 8:49am UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/4 "2024-02-14T08:49:00Z")

</div>

> [@jthemphill](#):
>
> Thank you! Implementing your suggestions now. [You can find the most current version of the code on GitHub](https://github.com/jthemphill/permission-model/blob/main/user-moves-owned-subtrees.als)!

Looks like this repo is private, isn’t it?

> [@jthemphill](#):
>
> I think this needs to be `Perm lone -> Object`. A Group can have explicit Permissions for many Objects, but a Group cannot assign multiple explicit Permissions to the same Object. This seems to have the same semantics as the `disj[this.explicit[Own], this.explicit[Edit], ...]` fact did.

Lapsus calami, you’re right.  
In general, I tend to favor multiplicities over additional facts as the former may (supposedly) lead to a better SAT encoding.

> [@jthemphill](#):
>
> I think that might be out of scope😅 My philosophy is that we write facts to describe the code we explicitly wrote into the system, and we write assertions to describe the properties that we hope will emerge from the system.

+1 I was just wondering whether an unwanted behavior might emerge from the combination of permission handling and filesystem operations. If it’s separated, there’s no need to change the model.

Finally, re-reading the original model, I’m stumbling upon fact `users_can_move_objects`: in general, unless it is absolutely required, it’s good practice to avoid `one` as it prunes behaviors where interacting events may happen at the same time and lead to unwanted behaviors. In principle, if your events have “good” frame conditions, then `some` should be enough and allow additional traces (in some cases).

PS: another reason to be wary of `one` is that `one a: A, b: B | p` is in general not equivalent to `one a: A, one b: B | ...` and it’s easy to shoot yourself in the foot.

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [February 14, 2024, 6:55pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/5 "2024-02-14T18:55:13Z")

</div>

> [@grayswandyr](#):
>
> Looks like this repo is private, isn’t it?

Sparkling spanakopita, you’re right! It’s now public: [GitHub - jthemphill/permission-model: Model of a permissions-based filesystem using Alloy](https://github.com/jthemphill/permission-model)

> [@grayswandyr](#):
>
> Finally, re-reading the original model, I’m stumbling upon fact `users_can_move_objects`: in general, unless it is absolutely required, it’s good practice to avoid `one` as it prunes behaviors where interacting events may happen at the same time and lead to unwanted behaviors. In principle, if your events have “good” frame conditions, then `some` should be enough and allow additional traces (in some cases).

I’ll try this when I get some free time!

> [@grayswandyr](#):
>
> PS: another reason to be wary of `one` is that `one a: A, b: B | p` is in general not equivalent to `one a: A, one b: B | ...` and it’s easy to shoot yourself in the foot.

Hm, does the second one apply the predicate only to the `one b: B` clause?

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [February 14, 2024, 11:00pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/6 "2024-02-14T23:00:04Z")

</div>

Not really. See [this](https://stackoverflow.com/questions/46635327/why-are-multiple-alloy-declarations-not-equivalent-to-nested-alloy-declarations/46703498#46703498) for an explanation.

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [February 15, 2024, 8:33pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/7 "2024-02-15T20:33:43Z")

</div>

Ah, that actually seems pretty reasonable after seeing your example!

---

<div class="post-metadata">

**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\
**Post date:** [March 14, 2024, 2:42am UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/8 "2024-03-14T02:42:56Z")

</div>

@[jthemphill](https://alloytools.discourse.group/u/jthemphill): This is wonderful! I strongly encourage you to publish this as it will be very helpful to other people. A few questions/suggestions about the version of the spec [here](https://github.com/jthemphill/permission-model/blob/main/permissions-model.als):

- At first, I thought it was gratuitous to have a permission of `None` (in addition to allowing an object to have no permission) because it seemed to make a distinction that didn’t have any consequence. But now that I’ve played with your spec a bit I can see that there is a very important difference, since the calculation of implicit permissions relies on whether there are explicit permissions, so a permission of `None` in an ancestor overrides an inherited permission. This is very subtle and needs a comment explaining it! I’m not sure I understand the consequence of `group_implicit` always granting `None`: that looks inconsistent with this, but maybe it doesn’t matter.
- I don’t understand why the `Move` sig is variable. Aren’t these `Move` objects just immutable argument pairs for the `move` predicate? I assume you’re doing this to show the move action in the visualization more directly. It’s like going part way towards the style I describe in my book in which events are modeled as signatures. I haven’t worked on this, but I wonder if there is a better way to do this (that is, to exploit Alloy 6 but still get objects for each action).
- A few syntactic nitpicks: rather than `x = none` you can just write `no x`; and instead of `x != none` you can write `some x`.
- You can get shorter commands in the menu by adding a name with a colon. Eg, instead of

```auto
pred user_cannot_gain_or_lose_access {...}
check user_cannot_gain_or_lose_access {user_cannot_gain_or_lose_access} for ...

```

you can write

```auto
user_cannot_gain_or_lose_access: check { ... } for ...

```

- I assume you’ve played with customizing the viz a bit? Here’s a screenshot of a theme that worked well for me.  
 ![CleanShot 2024-03-13 at 11.24.15@2x](https://global.discourse-cdn.com/free1/uploads/alloytools/original/1X/12072f7668f5be522c4769e9db231d72756995f5.jpeg)

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [March 15, 2024, 6:53pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/9 "2024-03-15T18:53:24Z")

</div>

> [@DanielJackson](#):
>
> @[jthemphill](https://alloytools.discourse.group/u/jthemphill): This is wonderful! I strongly encourage you to publish this as it will be very helpful to other people.

Thank you! I’m looking for the right venue to publish it - whether in a personal blog or on behalf of my employer. Also, shipping the project comes before bragging about how we used cool mathy tools to help us nail down the project’s design😉

> [@DanielJackson](#):
>
> At first, I thought it was gratuitous to have a permission of `None` (in addition to allowing an object to have no permission) because it seemed to make a distinction that didn’t have any consequence. But now that I’ve played with your spec a bit I can see that there is a very important difference, since the calculation of implicit permissions relies on whether there are explicit permissions, so a permission of `None` in an ancestor overrides an inherited permission. This is very subtle and needs a comment explaining it!

Correct! In the Alloy model, I might want to rename this level to `CannotSee`, and that would avoid the name/concept collision with Alloy’s `none` keyword.

> [@DanielJackson](#):
>
> I’m not sure I understand the consequence of `group_implicit` always granting `None`: that looks inconsistent with this, but maybe it doesn’t matter.

In the first draft of my model, each permissions level was a subset of stronger permissions. Since `None` is the weakest permission, every other permission includes it. `group_implicit[perm, group, obj]` asks “does `group` have `perm` access, or better, to `obj`?” and the answer is always yes if the needed permission is `None`. But that was before I learned about `Ordering`, `enum`s, and the fact that `enum`s have orderings built in. There is probably a more intuitive way to write this.

> [@DanielJackson](#):
>
> - I don’t understand why the `Move` sig is variable. Aren’t these `Move` objects just immutable argument pairs for the `move` predicate? I assume you’re doing this to show the move action in the visualization more directly. It’s like going part way towards the style I describe in my book in which events are modeled as signatures. I haven’t worked on this, but I wonder if there is a better way to do this (that is, to exploit Alloy 6 but still get objects for each action).

I’m trying to follow [“An idiom to depict events”](https://haslab.github.io/formal-software-design/modelling-tips/index.html#an-idiom-to-depict-events) from [_Formal Software Design with Alloy 6_](https://haslab.github.io/formal-software-design/index.html), which may or may not be the book you’re describing. I actually used a lot of trial-and-error here! I wasn’t even sure what `var sig` meant, at first. It appears that a `var sig` can spontaneously exist or disappear in any given timestep. I believe this is what I want, though - iff an object is moving, I want a `Move` object to exist with relations to the object and its destination folder.

> [@DanielJackson](#):
>
> - I assume you’ve played with customizing the viz a bit? Here’s a screenshot of a theme that worked well for me.

Yes! Naturally, I prefer a completely different theme😉 But I agree the diagram needs a theme in order to make visual sense. Is there a way to encode a theme in the comments?

---

<div class="post-metadata">

**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\
**Post date:** [March 17, 2024, 12:39pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/10 "2024-03-17T12:39:18Z")

</div>

All makes good sense.

Regarding the publication venue, two things you might consider: an industrial track of one of the major conferences (advantage is engaging with people), and an article in CACM (advantage is more readers); and both will give you a permanent record in the ACM digital library.

And regarding the theme: it would be great if you added it to the GH repo with the paper.

Happy to discuss this more with you directly. Best, Daniel

---

<div class="post-metadata">

**Author:** ![DanielJackson](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/danieljackson/32/80_2.png) [@DanielJackson](https://alloytools.discourse.group/u/DanielJackson)\
**Post date:** [March 17, 2024, 4:50pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/11 "2024-03-17T16:50:32Z")

</div>

BTW, by “my book”, I was referring to [the book](http://softwareabstractions.org) I wrote about Alloy. You may find it useful although it doesn’t include the new temporal operators. I’m very excited about the [new book](https://haslab.github.io/formal-software-design/index.html) by Julien Brunel, David Chemouil, Alcino Cunha, Nuno Macedo.

---

<div class="post-metadata">

**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\
**Post date:** [March 17, 2024, 5:13pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/12 "2024-03-17T17:13:01Z")

</div>

> [@jthemphill](#):
>
> I’m trying to follow [“An idiom to depict events”](https://haslab.github.io/formal-software-design/modelling-tips/index.html#an-idiom-to-depict-events) from [_Formal Software Design with Alloy 6_](https://haslab.github.io/formal-software-design/index.html), which may or may not be the book you’re describing. I actually used a lot of trial-and-error here! I wasn’t even sure what `var sig` meant, at first. It appears that a `var sig` can spontaneously exist or disappear in any given timestep. I believe this is what I want, though - iff an object is moving, I want a `Move` object to exist with relations to the object and its destination folder.

Depending on the model, var sigs may be used to depict events but keep in mind that, as any sig, a var sig has a bounded scope. Depending on how traces are specified, the bound could implicitly prune interesting behaviours (e.g. suppose that the possible number of move events in a given step can be larger than the scope on `Move`, then you may miss traces (depending on your exact model)).

The idiom we recommend does _not_ feature var sigs. The idea is rather the following:

- Create an `Event` enum representing the names of all possible events
- For any event (as a predicate), create a fun with the same name, and an arity that accounts for the name and parameters of the event. This fun returns all instances for which the event is true.
- Add and `events` fun which contains the union of all names of events that are known to happen (these are obtained out of the funs defined just above).

This is enough for visualization: all you need now is to play with the theme to tweak the display of all these funs.

This idiom is also described on [this page of the forum](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6/88), you may find it clearer?

---

<div class="post-metadata">

**Author:** ![jthemphill](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/jthemphill/32/220_2.png) [@jthemphill](https://alloytools.discourse.group/u/jthemphill)\
**Post date:** [August 1, 2024, 6:26pm UTC](https://alloytools.discourse.group/t/a-real-world-success-story/443/13 "2024-08-01T18:26:43Z")

</div>

Hello again! I recently gave [this talk](https://www.loom.com/share/4d37266a0a5143b3a2d5bd9e8c45e688) internally at our company. I didn’t go too heavily into the specifics of Alloy, though. I think the level of Alloy detail here was right for a 7-minute talk to people who have never used formal methods, but the talk can be adapted into a tutorial if I’m speaking to specialists who have signed up to hear about Alloy itself.