# How do you say "once this is true, it's always true"?

**URL:** <https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294>\
**Category:** Uncategorized\
**Created:** [October 21, 2022, 10:29pm UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294 "2022-10-21T22:29:02Z")\
**Posts on this page:** 7\
**Page:** 1

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 21, 2022, 10:29pm UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294/1 "2022-10-21T22:29:02Z")

</div>

As in my previous questions this week, I’m trying to model students joining a course. When a student joins a course, if text-to-speech is enabled for the course, it’ll be enabled for the student. The student can disable TTS afterwards, and that’s fine.

I’m trying to get Alloy to give me an instance of a student that disables TTS by saying “once a student has TTS enabled, it’s enabled forever” and asking it to prove me wrong.

Buuuut, I can’t seem to figure out the proper set of keywords to get this to work. I’ve tried:

```nohighlight
check onceYouHaveTTSYouAlwaysHaveTTS {
  some s: Student {
    once s in TTSStudent always s in TTSStudent
  }
}

```

and

```nohighlight
check onceYouHaveTTSYouAlwaysHaveTTS {
  some s: Student {
    eventually s in TTSStudent implies always s in TTSStudent
  }
}

```

but no luck! In the first case, Alloy shows me an example where the student is never in the `TTSStudent` set (which is fine, I suppose, but I don’t care about that until after they’ve been in `TTSStudent` for at least a little bit.)

In the second case, Alloy shows me a student who starts off without TTS, then joins a TTS-enabled course, and that’s it. And… that’s somehow a problem? I guess this is also asserting the student is always in `TTSStudent`; that’s the only way I can think that this would represent a counterexample.

Here’s my full model:

> **Full Model**
>
> ```nohighlight
> sig Student {}
> var sig TTSStudent in Student {}
> 
> sig Course {
> var roster: set Student
> }
> var sig TTSCourse in Course {}
> 
> pred init {
> some Student
> some Course
> no roster
> }
> 
> pred stutter {
> TTSStudent' = TTSStudent
> TTSCourse' = TTSCourse
> roster' = roster
> }
> 
> pred joinCourse [c: Course, s: Student] {
> // guard
> s not in c.roster
> 
> // action
> roster' = roster + c -> s
> c in TTSCourse
> implies TTSStudent' = TTSStudent + s
> else TTSStudent' = TTSStudent
> 
> // frame
> TTSCourse' = TTSCourse
> }
> 
> pred disableOwnTTS [s: Student] {
> // guard
> s in TTSStudent
> 
> // action
> TTSStudent' = TTSStudent - s
> 
> // frame
> roster' = roster
> TTSCourse' = TTSCourse
> }
> 
> pred allStudentsInACourse {
> all s: Student | s in Course.roster
> }
> 
> pred allCoursesHaveStudents {
> all c: Course | some c.roster
> }
> 
> fact traces {
> init
> always {
> stutter
> or (some c: Course, s: Student | joinCourse[c, s])
> or (some s: Student | disableOwnTTS[s])
> }
> }
> 
> fact everythingEventuallyJoinsUp {
> eventually allStudentsInACourse
> eventually allCoursesHaveStudents
> }
> 
> check ttsIsLeftAloneWhenJoiningANonTTSCourse {
> some s: Student, c: Course |
> c not in TTSCourse and joinCourse[c, s]
> implies TTSStudent' = TTSStudent
> }
> 
> run {}
> 
> check onceYouHaveTTSYouAlwaysHaveTTS {
> some s: Student {
> once s in TTSStudent always s in TTSStudent
> }
> }
> 
> ```

(Side note: I’d like to know if there’s any way to get Alloy to prefer to make progress wherever it can before stuttering forever. Right now I have the `everythingEventuallyJoinsUp` fact, but it feels a little bit like a hack!)

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [October 23, 2022, 7:33am UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294/2 "2022-10-23T07:33:46Z")

</div>

Hi,

The first problem with your assertions is that you are using an existential quantifier instead of an universal one. You want the properties to hold for every possible student.

In your first attempt you are not using any logic connective between the `once s in TTSStudent` and the `always s in TTSStudent` so Alloy defaults to `and`. Since unary operators, such as `once` or `always`, have the highest precedence, the `once` part is checking if student `s` has TTS enabled in the initial state (note that the `once` is not preceded by any other temporal operator, so TTS must be enabled in the initial state) and the `always` part checks if TTS is always enabled, including in the initial state (so the `once` part is actually redundant).

Since the unary operators have higher precedence, in your second attempt you are checking if student `s` never has TTS enabled or has TTS always enabled, which again is not what you want.

In general, property “once `p` is true, `p` is always true” can be specified as `always (p implies always p)`, so your assertion could be verified as follows (note that the parenthesis are necessary, since `always` has a higher precedence than `implies`).

```auto
check onceYouHaveTTSYouAlwaysHaveTTS {
  all s: Student {
    always (s in TTSStudent implies always s in TTSStudent)
  }
}

```

Concerning your side note:

> [@brianhicks](#):
>
> (Side note: I’d like to know if there’s any way to get Alloy to prefer to make progress wherever it can before stuttering forever. Right now I have the `everythingEventuallyJoinsUp` fact, but it feels a little bit like a hack!)

The standard way to impose progress is to use fairness assumptions in the model. The most common is to impose weak fairness on all actions, which forces all actions to occur if they are continuously enabled. You can read about fairness is most model checking books, but weak fairness can be roughly specified as `(eventually always enabled) implies (always eventually action)`. In your example, we would have:

```auto
fact WeakFairness {
  all c : Course, s : Student {
	(eventually always s not in c.roster) implies (always eventually joinCourse[c,s])
  }
  all s : Student {
    (eventually always s in TTSStudent) implies (always eventually disableOwnTTS[s])
  }
}

```

Note that fairness conditions are usually only necessary when checking liveness properties (properties that force the system to do something). To check safety properties (properties that forbid the system from doing something), such as the `onceYouHaveTTSYouAlwaysHaveTTS` you don’t need them. If you still impose them when checking safety properties, counter-examples can be longer and thus more difficult to understand. So I tend to prefer to put them inside a `pred` instead of a `fact` and only use them as needed.

Best,  
Alcino

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [October 25, 2022, 11:03am UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294/3 "2022-10-25T11:03:44Z")

</div>

Thank you so much for this response! Really helpful!

> [@alcino](#):
>
> In your first attempt you are not using any logic connective between the `once s in TTSStudent` and the `always s in TTSStudent` so Alloy defaults to `and`. Since unary operators, such as `once` or `always`, have the highest precedence, the `once` part is checking if student `s` has TTS enabled in the initial state (note that the `once` is not preceded by any other temporal operator, so TTS must be enabled in the initial state) and the `always` part checks if TTS is always enabled, including in the initial state (so the `once` part is actually redundant).

What is the proper usage of `once`, then? Looking in the spec, I just see “The expression `once F` is true in state _i_ iff `F` is true in some state ≤ _i_.” I thought that meant that _i_ could be any state, not just the initial one.

> [@alcino](#):
>
> In general, property “once `p` is true, `p` is always true” can be specified as `always (p implies always p)`, so your assertion could be verified as follows (note that the parenthesis are necessary, since `always` has a higher precedence than `implies`).

I’m not completely clear how this works, and I think getting my mental model here right will help a lot. How is `always (p implies always p`) different from `p implies always p`? It seems like this is saying "once `p` is true, it is `always true`, so I am not sure what the initial `always` is adding to this.

Also, I assumed `always` applies retroactively, but it just looks like it applies going forward. I guess you have the pair of `always`/`historically` to go forward/backward. Is that the right way to think about this?

> [@alcino](#):
>
> The standard way to impose progress is to use fairness assumptions in the model.

Oh shoot, I knew about fairness and totally forgot about using that to frame this question. Yes, that’s exactly what I’m looking for here! Thanks!

> [@alcino](#):
>
> You can read about fairness is most model checking books

Are there any you’d recommend in particular? I’d like to be able to do this well. I’ve read _Software Abstractions_ but it was a while back, and if I understand correctly has not been updated for Alloy 6?

> [@alcino](#):
>
> but weak fairness can be roughly specified as `(eventually always enabled) implies (always eventually action)`.

I confess that I’m really confused by this bit… how do these operators compose? I can kind of reason out the first one as “at some point, the proposition `enabled` is always true” but I’m not sure what to do with `always eventually`. In addition, wouldn’t `eventually always enabled` in these cases eventually be false? (Or is that where the `implies` comes in?) Part of this may be my confusion around what `always` actually does. 😆

> [@alcino](#):
>
> If you still impose them when checking safety properties, counter-examples can be longer and thus more difficult to understand. So I tend to prefer to put them inside a `pred` instead of a `fact` and only use them as needed.

This is helpful advice and I’ll keep it in mind. Thank you!

And overall, thank you again for such a thorough response. I’m still early on the path to understanding how this works and guidance like this from folks like you is super, super nice to have.

---

<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:** [October 25, 2022, 11:44am UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294/4 "2022-10-25T11:44:35Z")

</div>

> [@brianhicks](#):
>
> What is the proper usage of `once`, then? Looking in the spec, I just see “The expression `once F` is true in state _i_ iff `F` is true in some state ≤ _i_.” I thought that meant that _i_ could be any state, not just the initial one.

All temporal connectives are interpreted _relative to a “current” state_. If you don’t specify anything then the “default” current state is the initial one. But suppose you write `always (p => once q)`: it means that, in any state _s_, if `p` is true, then `q` was true some time in the past (relative to _s_).

> [@brianhicks](#):
>
> I’m not completely clear how this works, and I think getting my mental model here right will help a lot. How is `always (p implies always p`) different from `p implies always p`? It seems like this is saying "once `p` is true, it is `always true`, so I am not sure what the initial `always` is adding to this.

`always` means: in any state starting from the “current” state.  
If you write `p implies always p` (without other temporal connectives above), you mean: if `p` is true in the initial state, then `p` is true in all states (starting from the initial one).  
While if you write `always (p implies always p)`, you mean that `p` is _stable_: whatever the state _s_ (starting from the initial one), if `p` is true in _s_, then it will be true henceforth.

> [@brianhicks](#):
>
> Also, I assumed `always` applies retroactively, but it just looks like it applies going forward. I guess you have the pair of `always`/`historically` to go forward/backward. Is that the right way to think about this?

It is. We have future-time connectives and past-time connectives. Notice the latter refer to a finite past (as there is an initial instant but no final one).

> [@brianhicks](#):
>
> Are there any you’d recommend in particular? I’d like to be able to do this well. I’ve read _Software Abstractions_ but it was a while back, and if I understand correctly has not been updated for Alloy 6?

Indeed. We’re writing a book covering Alloy 6 but we’re a bit late 🙂 I guess a standard reference for fairness properties is Leslie Lamport’s book _Specifying systems_.

> [@brianhicks](#):
>
> I confess that I’m really confused by this bit… how do these operators compose? I can kind of reason out the first one as “at some point, the proposition `enabled` is always true” but I’m not sure what to do with `always eventually`. In addition, wouldn’t `eventually always enabled` in these cases eventually be false? (Or is that where the `implies` comes in?) Part of this may be my confusion around what `always` actually does. 😆

This is admittedly tricky and Lamport’s book is a good reference here, once again.  
You can read `always eventually` as meaning “infinitely often”  
I think a good way to read the property is to rewrite it as follows:

```auto
(eventually always enabled) implies (always eventually action)
= not ((eventually always enabled) and not (always eventually action))
= not ((eventually always enabled) and (eventually always not action))

```

Said otherwise, we reject (first `not`) traces where the action becomes continuously enabled but, eventually, it’s never fired. If we didn’t have this fairness property in a system with a `stutter` event, then the system could do `stutter` infinitely even if `action` becomes continuously enabled, for instance.

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [November 1, 2022, 11:07am UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294/5 "2022-11-01T11:07:40Z")

</div>

Hmm, ok! That makes sense. One last thing, then:

> [@grayswandyr](#):
>
> `always` means: in any state starting from the “current” state.

I thought this was `eventually`? How, then, are they different? (Is it that “always” will eventually be true in every state greater than `i`, while “eventually” will be only true in at least one?)

(sorry about the delay here; I was out of the office last week.)

---

<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:** [November 1, 2022, 2:12pm UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294/6 "2022-11-01T14:12:40Z")

</div>

English isn’t my first language so perhaps I wasn’t clear. Always means “in **every** forthcoming state (including the current one)”. Eventually means “in **at least one** forthcoming state (including the current one)”.

---

<div class="post-metadata">

**Author:** ![brianhicks](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/brianhicks/32/5_2.png) [@brianhicks](https://alloytools.discourse.group/u/brianhicks)\
**Post date:** [November 1, 2022, 2:26pm UTC](https://alloytools.discourse.group/t/how-do-you-say-once-this-is-true-its-always-true/294/7 "2022-11-01T14:26:54Z")

</div>

ah, OK! That clears things up. Thank you very much for your help!