Quint: those 'Aha' moments that help solidify what I already know

Preface

“What does an experienced software engineer discover when s/he uses an executable specification language to rigorously revisit ideas s/he already knows?”

I've been modeling software systems using Finite State Machine-based approach for many years. 'State transition' is hardly a new territory for me.

My interest in Quint isn't academic. I've been working on an actor-based Digital Twin, where state, events, asynchronous messages and ordering are practical engineering concerns. Quint gives me a way to examine those concerns at a higher level of rigor.

Now, the interesting part hasn't been learning about 'state'-s or 'transition'-s; it has been discovering the assumptions hiding between them - the Aha moments 😃. I am becoming familiar describing 'state'-s and 'transition-s', into executable specifications and subjecting them to systematic exploration.

---

Important ✋ : This is not a Quint tutorial. I have been following their tutorial here, all along. The specifications live in quint-specification-journey.

---

The Aha moments for me

Aha moment #1 — I have known state transitions for many years. Quint makes me pinpoint exactly which transitions are permissible

I have worked with state-machine models for years; so NFAs, DFAs, states, transitions, guard-conditions and exit handlers, were familiar territory. What is different here, is having to express the transition precisely enough for a model checker to explore it.

In a Quint specification, the state is not an abstract notion sitting behind the model. It is the collection of the current values of the state variables. An action examines those values and, through assignments to primed variables (suffixed with '), specifies the values in the next state.

traffic_light' = // The next transition begins with the value assigned, here.
        if (traffic_light == RED) { GREEN }
        else if (traffic_light == GREEN) { YELLOW }
        else { RED }
}

There is no room here for “what I intend the traffic light to do.”. The specification has to say exactly which next state this action permits from the current state.

Quint hasn't taught me what a 'state transition' is (I know that quite well); but it makes me pinpoint exactly what a transition permits.

Code: traffic_light.qnt.

Aha moment #2: I am quite familiar with transitions. Quint reminds me that if I don't expressly forbid it, I permit a transition.

Guard conditions always evaluate to a true/false value. They determine whether a transition is enabled from the current state. If the guard is false, that transition is not part of the possible next transitions from that state.

action openDoor = .. {
          ..
          physical_door.door_access == Closed and physical_door.lock_condition == Unlocked,
	      ..
}

My intuition says that opening a locked door is obviously invalid. Quint doesn't share that intuition. If I don't constrain the transition, it remains a possible behaviour of the model.

The idea of a guard isn't new to me. What Quint exposes more deeply is how completely the guard has to capture the behaviour I want to permit.

Code: door_and_lock.qnt.

Aha moment #3: An invariant pins me down - "think hard; what must always be true"?

I already know invariants as a modelling and verification concept. What Quint exposes more deeply is that formulating the invariant is itself part of understanding the behaviour.

val door_is_stable =
    not (
        physical_door.door_access == Open and
        physical_door.lock_condition == Locked
    )

The invariant is simple, even obvious. But stating it explicitly forces me to articulate what I mean by a valid state — and, more importantly — what must never become true.

When I run quint, I mention the invariant:

quint run door_and_lock.qnt --invariant door_is_stable

Quint explores the states and transitions and informs me if the invariant fails.

Importantly, the model checker can tell me whether my model satisfies the invariant I give it; it cannot tell me whether I captured the property that actually matters. This is a key observation.

Aha moment #4: Quint makes the “unchanged” state explicit.

I know that an action may change some parts of state while leaving others untouched. While programming in my favourite language, that can remain implicit. Quint makes me account for it explicitly.

action deposit = 
       nondet to_account = ACCOUNTS.oneOf()
       nondet d = 1.to(50).oneOf()
       all {
	    balances' = balances.set(to_account, balances.get(to_account) + d) ,
	    total_deposit_amount' = total_deposit_amount + d,
	    total_withdrawal_amount' = total_withdrawal_amount, // <-- No change; yet explicit
	    total_money_supply' = total_money_supply // <-- No change; yet explicit
	   }
}

I have to state explicitly that total_withdrawal_amount and total_money_supply remain unchanged during deposit.

Code: bank_transactions.qnt.

Aha moment #5: Non-determinism lets me leave the environment's choices unspecified.

I already know that asynchronous systems involve choices I don't control. What Quint exposes more deeply is that I canmake that nondeterminism explicit in the specification.

Which transition happens next?

action step = any {
    sendMessage,
    deliverMessage
}

And, when deliverMessage is chosen, which message is delivered?

nondet m = in_transit.oneOf()

Asynchrony gives the environment choices at more than one level. Which transition happens next? And, if delivery happens, which message is involved? any and nondet let me leave those choices unspecified rather than building a convenient execution order into the model.

Aha #2 said: If I don't forbid it, I have permitted it. Here I am deliberately leaving some choices unconstrained because they belong to the environment, not to my system.

Code: send_and_deliver.qnt.

Endnote

Quint is a model checker. A model checker can establish properties of the specification. It cannot determine whether the specification captured the actual requirements.

That responsibility remains mine.

And, the journey continues, anticipating more such Aha moments!