Skip to content

Yassine/add tlc support #1831

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
beu5a wants to merge 7 commits into from
Closed

Yassine/add tlc support #1831

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
83e56f6
Add draft of TLC verify backend
beu5a Dec 24, 2025
f48eb00
separate CLI output logic from the verification logic
beu5a Dec 24, 2025
ffe9333
rename cliVerify to quintMCWrapper and add section separators
beu5a Dec 24, 2025
aaed814
remove unused quintVerifier.ts
beu5a Dec 24, 2025
a7d2387
extract TLC hardcoded values into constants
beu5a Dec 24, 2025
2a6bf4b
add --tlc-config option for TLC runtime configuration
beu5a Dec 24, 2025
89873f8
ts formatting pass
beu5a Dec 24, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions quint/src/cli.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -380,6 +380,16 @@ const verifyCmd = {
} else {
return errorOrEndpoint.value
}
})
.option('backend', {
desc: 'the backend to use for verification',
type: 'string',
choices: ['apalache', 'tlc'],
default: 'apalache',
})
.option('tlc-config', {
desc: 'path to a TLC configuration file (in JSON)',
type: 'string',
}),
// Timeouts are postponed for:
// https://github.com/informalsystems/quint/issues/633
Expand Down
105 changes: 9 additions & 96 deletions quint/src/cliCommands.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,17 +35,17 @@ import { IdGenerator, newIdGenerator } from './idGenerator'
import { Outcome, SimulatorOptions, showTraceStatistics } from './simulation'
import { verbosity } from './verbosity'
import { fileSourceResolver } from './parsing/sourceResolver'
import { verify } from './quintVerifier'
import { flattenModules } from './flattening/fullFlattener'
import { AnalysisOutput, analyzeInc, analyzeModules } from './quintAnalyzer'
import { newTraceRecorder } from './runtime/trace'
import { flow, isEqual, uniqWith } from 'lodash'
import { Maybe, just, none } from '@sweet-monads/maybe'
import { compileToTlaplus } from './compileToTlaplus'
import { Evaluator } from './runtime/impl/evaluator'
import { NameResolver } from './names/resolver'
import { convertInit } from './ir/initToPredicate'
import { QuintRustWrapper } from './quintRustWrapper'
import { convertInit } from './ir/initToPredicate'
import { compileToTlaplus } from './compileToTlaplus'
import { verifyWithApalacheBackend, verifyWithTlcBackend } from './quintMCWrapper'
import {
cliErr,
findMainModule,
Expand All @@ -56,26 +56,14 @@ import {
outputTestErrors,
outputTestResults,
prepareOnTrace,
printInductiveInvariantProgress,
printViolatedInvariants,
processVerifyResult,
writeOutputToJson,
writeToJson,
} from './cliReporting'
import {
PLACEHOLDERS,
deriveVerbosity,
getInvariants,
guessMainModule,
isMatchingTest,
loadApalacheConfig,
mkErrorMessage,
toExpr,
} from './cliHelpers'
import { deriveVerbosity, getInvariants, guessMainModule, isMatchingTest, mkErrorMessage, toExpr } from './cliHelpers'
import { fail } from 'assert'
import { newRng } from './rng'
import { TestOptions } from './runtime/testing'
import { createConfig } from './apalache'

export type stage =
| 'loading'
Expand All @@ -84,6 +72,7 @@ export type stage =
| 'testing'
| 'running'
| 'compiling'
| 'verifying'
| 'outputting target'
| 'documentation'

Expand Down Expand Up @@ -587,90 +576,14 @@ export async function compile(typechecked: TypecheckedStage): Promise<CLIProcedu
})
}

/**
* Verify a spec via Apalache.
*
* @param prev the procedure stage produced by `typecheck`
*/
export async function verifySpec(prev: CompiledStage): Promise<CLIProcedure<TracingStage>> {
const verifying = { ...prev, stage: 'verifying' as stage }
const args = verifying.args
const verifying: TracingStage = { ...prev, stage: 'verifying' as stage }
const verbosityLevel = deriveVerbosity(prev.args)

const itfFile: string | undefined = prev.args.outItf
if (itfFile) {
if (itfFile.includes(PLACEHOLDERS.test) || itfFile.includes(PLACEHOLDERS.seq)) {
console.log(
`${chalk.yellow('[warning]')} the output file contains ${chalk.grey(PLACEHOLDERS.test)} or ${chalk.grey(
PLACEHOLDERS.seq
)}, but this has no effect since at most a single trace will be produced.`
)
}
}

const loadedConfig = loadApalacheConfig(verifying, args.apalacheConfig)

const veryfiyingFlat = { ...prev, modules: [prev.mainModule] }
const parsedSpec = outputJson(veryfiyingFlat)

const [invariantsString, invariantsList] = getInvariants(prev.args)

if (args.inductiveInvariant) {
const hasOrdinaryInvariant = invariantsList.length > 0
const nPhases = hasOrdinaryInvariant ? 3 : 2
const initConfig = createConfig(loadedConfig, parsedSpec, { ...args, maxSteps: 0 }, ['q::inductiveInv'])

// Checking whether the inductive invariant holds in the initial state(s)
printInductiveInvariantProgress(verbosityLevel, args, 1, nPhases)

const startMs = Date.now()
return verify(args.serverEndpoint, args.apalacheVersion, initConfig, verbosityLevel).then(res => {
if (res.isLeft()) {
return processVerifyResult(res, startMs, verbosityLevel, verifying, [args.inductiveInvariant])
}

// Checking whether the inductive invariant is preserved by the step
printInductiveInvariantProgress(verbosityLevel, args, 2, nPhases)

const stepConfig = createConfig(
loadedConfig,
parsedSpec,
{ ...args, maxSteps: 1 },
['q::inductiveInv'],
'q::inductiveInv'
)

return verify(args.serverEndpoint, args.apalacheVersion, stepConfig, verbosityLevel).then(res => {
if (res.isLeft() || !hasOrdinaryInvariant) {
return processVerifyResult(res, startMs, verbosityLevel, verifying, [args.inductiveInvariant])
}

// Checking whether the inductive invariant implies the ordinary invariant
printInductiveInvariantProgress(verbosityLevel, args, 3, nPhases, invariantsString)

const propConfig = createConfig(
loadedConfig,
parsedSpec,
{ ...args, maxSteps: 0 },
['q::inv'],
'q::inductiveInv'
)

return verify(args.serverEndpoint, args.apalacheVersion, propConfig, verbosityLevel).then(res => {
return processVerifyResult(res, startMs, verbosityLevel, verifying, invariantsList)
})
})
})
if (prev.args.backend === 'tlc') {
Copy link

Copilot AI Dec 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Consider validating that Apalache-specific options (such as --apalache-config and --inductive-invariant) are not used when the TLC backend is selected, and provide clear error messages if they are. This will help users understand which options are compatible with each backend.

Suggested change
if (prev.args.backend === 'tlc') {
if (prev.args.backend === 'tlc') {
const incompatibleApalacheOptions: string[] = []
// These options correspond to Apalache-specific CLI flags and are not
// compatible with the TLC backend.
if ((prev.args as any).apalacheConfig !== undefined) {
incompatibleApalacheOptions.push('--apalache-config')
}
if (
(prev.args as any).inductiveInvariant !== undefined &&
(prev.args as any).inductiveInvariant !== null &&
(prev.args as any).inductiveInvariant !== '' &&
(!Array.isArray((prev.args as any).inductiveInvariant) ||
(prev.args as any).inductiveInvariant.length > 0)
) {
incompatibleApalacheOptions.push('--inductive-invariant')
}
if (incompatibleApalacheOptions.length > 0) {
const msg =
`The following options can only be used with the Apalache backend: ` +
`${incompatibleApalacheOptions.join(', ')}. ` +
`Please rerun with --backend apalache or remove these options when using --backend tlc.`
return cliErr(msg, { ...verifying, errors: [] })
}

Copilot uses AI. Check for mistakes.
return verifyWithTlcBackend(prev, verifying, verbosityLevel)
}

// We need to insert the data form CLI args into their appropriate locations
// in the Apalache config
const config = createConfig(loadedConfig, parsedSpec, args, invariantsList.length > 0 ? ['q::inv'] : [])
const startMs = Date.now()

return verify(args.serverEndpoint, args.apalacheVersion, config, verbosityLevel).then(res => {
return processVerifyResult(res, startMs, verbosityLevel, verifying, invariantsList)
})
return verifyWithApalacheBackend(prev, verifying, verbosityLevel)
}

/** output a compiled spec in the format specified in the `compiled.args.target` to stdout
Expand Down
126 changes: 72 additions & 54 deletions quint/src/cliReporting.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ import { Either, left } from '@sweet-monads/either'
import { cwd } from 'process'
import { replacer } from './jsonHelper'
import { ApalacheResult } from './apalache'
import { TlcError } from './tlc'
import { QuintError } from './quintError'
import { TestResult } from './runtime/testing'
import { createFinders, formatError } from './errorReporter'
Expand Down Expand Up @@ -104,60 +105,6 @@ export function printViolatedInvariants(state: QuintEx, invariants: string[], pr
}
}

/**
* Process the result of a verification call.
*
* @param res The result of the verification.
* @param startMs The start time in milliseconds.
* @param verbosityLevel The verbosity level.
* @param verifying The current tracing stage.
* @param invariantsList The list of invariants.
* @param prev The previous stage context.
* @returns The processed result.
*/
export function processVerifyResult(
res: ApalacheResult<void>,
startMs: number,
verbosityLevel: number,
stage: TracingStage,
invariantsList: string[]
): CLIProcedure<TracingStage> {
const elapsedMs = Date.now() - startMs

return res
.map((): TracingStage => {
if (verbosity.hasResults(verbosityLevel)) {
console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`))
if (verbosity.hasHints(verbosityLevel)) {
console.log(chalk.gray('You may increase --max-steps.'))
console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
}
}
return { ...stage, status: 'ok', errors: [] }
})
.mapLeft(err => {
const trace: QuintEx[] | undefined = err.traces ? ofItfNormalized(err.traces[0]) : undefined
const status = trace !== undefined ? 'violation' : 'failure'

if (trace !== undefined) {
maybePrintCounterExample(verbosityLevel, trace, [], stage.args.hide || [])

if (verbosity.hasResults(verbosityLevel)) {
console.log(chalk.red(`[${status}]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
printViolatedInvariants(trace[trace.length - 1], invariantsList, stage)
}

if (stage.args.outItf && err.traces) {
writeToJson(stage.args.outItf, err.traces[0])
}
}
return {
msg: err.explanation,
stage: { ...stage, status, errors: err.errors, trace },
}
})
}

export function outputJson(stage: ProcedureStage): string {
return jsonStringOfOutputStage(pickOutputStage(stage))
}
Expand Down Expand Up @@ -381,3 +328,74 @@ export function printInductiveInvariantProgress(
}
}
}

export function processTlcResult(
res: Either<TlcError, void>,
startMs: number,
verbosityLevel: number,
stage: TracingStage
): CLIProcedure<TracingStage> {
const elapsedMs = Date.now() - startMs

return res
.map((): TracingStage => {
if (verbosity.hasResults(verbosityLevel)) {
console.log('\n' + chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`))
}
return { ...stage, status: 'ok', errors: [] }
})
.mapLeft(err => {
const status = err.isViolation ? 'violation' : 'failure'
const summary = err.isViolation ? 'Found an issue' : 'TLC encountered an error'
if (verbosity.hasResults(verbosityLevel)) {
console.log('\n' + chalk.red(`[${status}]`) + ' ' + summary + ' ' + chalk.gray(`(${elapsedMs}ms).`))
}
return {
msg: err.explanation,
stage: { ...stage, status, errors: err.errors },
}
})
}

export function processApalacheResult(
res: ApalacheResult<void>,
startMs: number,
verbosityLevel: number,
stage: TracingStage,
invariantsList: string[]
): CLIProcedure<TracingStage> {
const elapsedMs = Date.now() - startMs

return res
.map((): TracingStage => {
if (verbosity.hasResults(verbosityLevel)) {
console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`))
if (verbosity.hasHints(verbosityLevel)) {
console.log(chalk.gray('You may increase --max-steps.'))
console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
}
}
return { ...stage, status: 'ok', errors: [] }
})
.mapLeft(err => {
const trace: QuintEx[] | undefined = err.traces ? ofItfNormalized(err.traces[0]) : undefined
const status = trace !== undefined ? 'violation' : 'failure'

if (trace !== undefined) {
maybePrintCounterExample(verbosityLevel, trace, [], stage.args.hide || [])

if (verbosity.hasResults(verbosityLevel)) {
console.log(chalk.red(`[${status}]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
printViolatedInvariants(trace[trace.length - 1], invariantsList, stage)
}

if (stage.args.outItf && err.traces) {
writeToJson(stage.args.outItf, err.traces[0])
}
}
return {
msg: err.explanation,
stage: { ...stage, status, errors: err.errors, trace },
}
})
}
Loading
Loading