Error when "verify" this spec in Quint

[mt40]

Hi everyone,

When I verify this spec, I got this error:

> quint verify outbox.qnt --invariant=safety --temporal=liveness --verbosity=5 --max-steps=2

Launching Apalache server
error: internal error: while parsing in Apalache:
'key not found: 440'
Please report an issue: https://github.com/informalsystems/quint/issues/new
Shutting down Apalache

It seems like because of adding the line temporal liveness = eventually(livenessCheck). Anyone know why this is problematic?

For context, this is my attempt at Outbox pattern. There are 3 components:

1. database: entity_table and event_table
2. message relay: read event_table and send events to broker
3. broker: the destination for all events, maybe a message queue in real life

The goal is to create events in database and then move them all to broker.

module outbox {
    //**********************************************************
    // TYPE DEFINITIONS
    //**********************************************************
    type Value = int
    type Time = int

    // State of domain event:
    // created -> sent
    type State = str

    type HistoryEntry = { value: Value, state: State}
    type Entity = { value: Value }
    type Event = { value: Value, state: State }

    //**********************************************************
    // CONSTANTS
    //**********************************************************
    
    //**********************************************************
    // STATE MACHINE
    // State-dependent definitions and actions
    //**********************************************************
    var num: Value
    
    // domain data
    var entity: Value
    
    // domain events
    var events: List[Event]

    // latest message of each value in target queue
    var broker: Value -> Time

    // Global log of system events. Use to specify correctness
    // properties below.
    var history: List[HistoryEntry]

    //**********************************************************
    // FUNCTIONAL LAYER
    // Values and functions that are state-independent
    //**********************************************************


    //**********************************************************
    // HELPERS
    // Functions for convenience
    //**********************************************************

    //**********************************************************
    // ACTIONS
    //**********************************************************

    // Do transaction to write both entity and event atomically
    action applicationProc: bool = all {
        val v = num + 1
        all {
            num' = v,
            entity' = v,
            events' = events.append({value: v, state: "created"}),
            history' = history.append({value: v, state: "created"}),
            broker' = broker,
        }
    }

    // Send events to broker
    action messageRelayProc(v: Value): bool = all {
        events.length() > 0,
        val firstEvent = events.head()
        broker' = broker.put(firstEvent.value, v), // use as time too
        events' = events.tail(),
        history' = history.append({value: v, state: "sent"}),
        entity' = entity,
        num' = num,
    }

    //**********************************************************
    // SETUP
    //**********************************************************

    action init = all {
        num' = 0,
        entity' = 0,
        events' = [],
        broker' = Map(),
        history' = [],
    }

    action step = any {
        applicationProc,
        messageRelayProc(num),
    }

    //**********************************************************
    // CORRECTNESS
    // 1. Safety Properties / Invariants
    //**********************************************************

    // data change and domain event must be written together
    val atomicity: bool = {
        num == 0
        or history.indices().exists(i => {
            val h = history[i]
            h.value == entity and h.state == "created"
        })
    }
    
    def isValidStateCreated(i: int, j: int): bool = {
        history[i].value == history[j].value
        and history[i].state == "created"
        implies history[j].state.in(Set("sent"))
    }

    def isValidStateSent(i: int, j: int): bool = {
        history[i].state == "sent"
        implies history[i].value != history[j].value
    }

    val stateValidity: bool = {
        val idx = history.indices()
        idx.forall(i => {
            idx.forall(j => {
                i >= j
                or { // i < j
                    isValidStateCreated(i, j)
                    or isValidStateSent(i, j)
                }
            })
        })
    }

    // Each event is sent exactly once
    val exactlyOnce: bool = {
        val idx = history.indices()
        idx.forall(i => {
            idx.forall(j => {
                i != j
                and history[i].state == "sent"
                and history[j].state == "sent"
                implies history[i].value != history[j].value
            })
        })
    }

    def brokerContains(v: Value): bool = {
        broker.keys().contains(v)
    }

    def isSentBefore(v1: int, v2: int): bool = or {
        not(brokerContains(v1)) and not(brokerContains(v2)),
        brokerContains(v1) and not(brokerContains(v2)),
        // broker contains both v1 & v2
        broker.get(v1) < broker.get(v2)
    }

    // Events are sent in FIFO order
    val ordering: bool = {
        val idx = history.indices()
        idx.forall(i => {
            idx.forall(j => {
                i < j
                and history[i].state == "created"
                and history[j].state == "created"
                implies isSentBefore(history[i].value, history[j].value)
            })
        })
    }

    val strongConsistency: bool = {
        atomicity
        and stateValidity
        and ordering
    }

    val safety: bool = {
        exactlyOnce
        and strongConsistency
    }

    //**********************************************************
    // CORRECTNESS
    // 2. Liveness Properties / Temporal
    //**********************************************************
    val livenessCheck: bool = {
        val idx = history.indices()
        idx.forall(i => {
            history[i].state == "created"
            implies idx.exists(j => {
                history[j].state == "sent"
                and history[j].value == history[i].value
            })
        })
    }

    // Eventually, any event will be sent to broker
    temporal liveness = eventually(livenessCheck)


    //**********************************************************
    // QUICK TESTS
    //**********************************************************
    // run initAndStepTest = init.then(step)
}

All feedbacks are welcome!

[bugarela]

Hi @mt40! Which version of Quint do you have installed? quint --version should tell you. Also, are you just running quint verify and letting Quint handle Apalache for you, or are you running apalache-mc server by yourself? If the latter, which version of apalache-mc server are you using?

Asking because I couldn't reproduce this problem on my machine using the latest version of Quint (0.22.4) and the Apalache version it installs (0.46.1).

[mt40]

quint version: 0.18.3
apalache: handled by quint verify

I see, could be because of my Quint version. Let me check how I can update Quint

[bugarela]

npm install -g @informalsystems/quint@latest

or

npm install -g @informalsystems/[email protected]

Should work