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

[brianhicks]

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:

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

and

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

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!)

[alcino]

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).

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:

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

[brianhicks]

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.

[grayswandyr]

@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:

(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.

[brianhicks]

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.)

[grayswandyr]

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)”.

[brianhicks]

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