# Isn’t frame conditions quite fragile?

**URL:** <https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376>\
**Category:** Questions\
**Created:** [July 18, 2023, 9:17am UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376 "2023-07-18T09:17:57Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![judofyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/judofyr/32/193_2.png) [@judofyr](https://alloytools.discourse.group/u/judofyr)\
**Post date:** [July 18, 2023, 9:17am UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376/1 "2023-07-18T09:17:57Z")

</div>

Hey folks. I’ve been learning a bit Alloy with the intention of using the linear temporal logic checking. I’ve had some experience with rewriting systems (most notably, Maude) and I’m really enjoying Alloy so far.

However, the fact that any (mutable) relation can change (if I don’t write `x’ = x`) in the predicate seems very inconvenient. I’ve already had many unexpected instances caused by forgetting to “lock” one relation. It also leads to a case where when I introduce a new relation, I’ll have to try remember to lock it in all of the time existing predicates - even if they are not related at all. Isn’t this quite fragile?

Am I doing something wrong? Is there another way of modeling such systems?

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [July 18, 2023, 12:16pm UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376/2 "2023-07-18T12:16:43Z")

</div>

I agree … it is criminally error prone.

I once made a PlusCal like interpreter in the Alloy code base. There I analyzed the branches (implies) and made sure to add instructions when one branch set a var that was not set in the other branch. This seemed to work well but I have no idea how theoretically solid it was and nobody got excited … so it has been lingering since. From a user point of view I think it would be really a huge gain.

> [@PlusCal in Alloy](https://alloytools.discourse.group/t/pluscal-in-alloy/59):
>
> I’ve been playing with Alloy (Electrum version) and added a ‘[PlusCal](https://en.wikipedia.org/wiki/PlusCal)’ like feature to Alloy. I finally got the basics to work and I am looking for some expert feedback. I know PlusCal is for us, the deplorable developer class, because it gives the impression of procedural code. However, that might actually convince some other developers to take a look. Many concurrent problems become a lot easier. However, so often in this world I find that my intuition is totally off so some feedback about this…

---

<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:** [July 18, 2023, 12:39pm UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376/3 "2023-07-18T12:39:08Z")

</div>

> [@judofyr](#):
>
> Isn’t this quite fragile?
> 
> Am I doing something wrong? Is there another way of modeling such systems?

It is fragile indeed. It’s the other side of the coin of being so nicely declarative. When specifying an operational device with sort of a state machine, it can be cumbersome and error-prone.

But the freedom given by Alloy is also handy. For instance, you can specify a mutable relation by a _global temporal fact_ rather than by what looks like an event (or an instruction in a PlusCal-like extension), and by no means do you want an _implicit_ frame condition to fix its value because your spec might become inconsistent or implictly restrained.

With the next version of Alloy coming this fall, the combination of macros and meta (which should be fixed and extended to handle mutable stuff) may make it possible to get some shorter ways to handle FCs. Going further and creating an extension is of course possible (and was already prototyped, and is still researched by some of us) but it seems very difficult to come up with something the semantics of which is at the same time general enough and doesn’t put a burden on the user.

---

<div class="post-metadata">

**Author:** ![judofyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/judofyr/32/193_2.png) [@judofyr](https://alloytools.discourse.group/u/judofyr)\
**Post date:** [July 20, 2023, 10:47am UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376/4 "2023-07-20T10:47:53Z")

</div>

It’s not the most elegant solution, but a `mutates` “pragma” on predicate which “locks” every other relationwhich is _not_ in the list (i.e. `r' = r`) would be “good enough” for me to feel more comfortable. And then maybe combined with a warning if you refer to `r'` in the predicate without it being part of the `mutates` list?

```auto
pred foo[] mutates(X, y, z) {
  -- Now every relation _other_ than X, y, z will implicitly get `r' = r` added.
}

```

---

<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:** [July 20, 2023, 11:40am UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376/5 "2023-07-20T11:40:30Z")

</div>

We did this in [Electrum Action](https://hal.science/hal-01774920) some years ago. As I said above, there are issues with this approach too, most notably with variables the value of which may be set outside of events, for instance using a global temporal fact. Also, there is an issue with the granularity of the pragma: you may want something less blunt than “mutated or unchanged”, depending on your time model (e.g. if you want to allow several events simultaneously).

My point is that choosing such an approach is easy but then it forces users to commit to one modeling approach that may not fit their problem domain. This goes against the generality of Alloy. So should we create another language, possibly losing some nice aspects of Alloy? Or is it possible to find an approach that has the wanted properties while keeping the good aspects of the language?

---

<div class="post-metadata">

**Author:** ![judofyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/judofyr/32/193_2.png) [@judofyr](https://alloytools.discourse.group/u/judofyr)\
**Post date:** [July 20, 2023, 12:48pm UTC](https://alloytools.discourse.group/t/isn-t-frame-conditions-quite-fragile/376/6 "2023-07-20T12:48:51Z")

</div>

Aaah, that’s some good points.

I also realize that I might need to change the way I’m thinking. I’m very used to thinking “start with an (specific) initial state” and then “define rules which iteratively change this”. However, Alloy is capable of creating interesting states _without_ any rules being applied. This can also be considered a feature for actions as well: It’s valuable to let Alloy generate other interesting changes that runs “simultaneously” to our actions. And then instead we can add constraints with are more “fundamental” (e.g. `fact { always … }`).

I also realized that the way predicates interact with different parts can also be encode _outside_ of the predicate itself:

```auto
fact {
  -- Model the fact that we need to take out a lock on billing details whenever `upgradeProject` happens.
  always (some p: Project | upgradeProject[p]) implies (billingDetails' = billingDetails)
}

```

This is actually very nice. You can start out _without_ this constraint, and then Alloy can demonstrate a trace where someone is capable of upgrading their project while simultaneously removing their billing details (which leads to an invalid state of “upgraded project has no billing details”). Once we add this constraint we see that this is enough to make our model consistent.

Another modeling approach would be to add constraints the other way. Instead of restricting the different actions which can happen, you can restrict how the relations are allowed to change:

```auto
fact {
  -- New projects can only be created or duplicated:
  always all p: Project' - Project | createdProject[p] or (some other: Project | duplicatedProject[other, p])
  -- Owner can only be changed if a project is transferred: 
  always all p: Project | p.owner' != p.owner implies transferProject[p, p.owner']
  -- Projects can never be deleted:
  always Project in Project'
}

```

And separately we could add other facts to make sure we’re getting an interesting trace (e.g. ensure that we actually do at least one of our actions in every step).

Anyway, I’m just babbling and brainstorming now!