# 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:** 1\
**Showing post:** 12

<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?

---

_[View the full topic](https://alloytools.discourse.group/t/a-real-world-success-story/443)._
