diff --git a/doc/quint.md b/doc/quint.md
index 18eed574b..af6124f07 100644
--- a/doc/quint.md
+++ b/doc/quint.md
@@ -73,8 +73,7 @@ especially useful for debugging complex specifications.
$ quint compile --help
quint compile
-compile a Quint specification into the target, the output is written to
-stdout
+compile a Quint specification into the target, the output is written to stdout
Options:
--help Show help [boolean]
@@ -82,6 +81,10 @@ Options:
--out output file (suppresses all console output) [string]
--main name of the main module (by default, computed from filename)
[string]
+ --init name of the initializer action [string] [default: "init"]
+ --step name of the step action [string] [default: "step"]
+ --invariant the invariants to check, separated by commas (e.g.) [string]
+ --temporal the temporal properties to check, separated by commas [string]
--target the compilation target. Supported values: tlaplus, json
[string] [default: "json"]
--verbosity control how much output is produced (0 to 5)[number] [default: 2]
@@ -91,6 +94,16 @@ Given a quint specification as input, this command parses, resolves imports,
typechecks, and then "flattens" the specification into on module containing just
the needed definitions.
+The main module is determined as follows: If a module name is specified by
+`--main`, that takes precedence. Otherwise, if there is only one module in the
+input file, that is the main module. Otherwise, the module with the same name as
+the file is taken to be the main module.
+
+The main module must specify a state machine. This means it must either define
+actions named `init` and `step`, specifying the initial state and the
+transition action respectively, or suitable actions defined in the main module
+must be indicated using the `--init` and `--step` options.
+
The following compilation targets are supported
- `json`: The default target, this produces a json representation, in the same
@@ -105,7 +118,7 @@ The following compilation targets are supported
to be expected.*
```sh
-$ quint parse --help
+$ quint parse --help
quint parse
parse a Quint specification
@@ -292,30 +305,32 @@ Options:
## Command verify
```sh
-$ quint verify
+$ quint verify --help
+quint verify
Verify a Quint specification via Apalache
Options:
- --help Show help [boolean]
- --version Show version number [boolean]
- --main name of the main module (by default, computed from
- filename) [string]
- --out output file (suppresses all console output) [string]
- --out-itf output the trace in the Informal Trace Format to file
- (suppresses all console output) [string]
- --max-steps the maximum number of steps in every trace
- [number] [default: 10]
- --init name of the initializer action [string] [default: "init"]
- --step name of the step action [string] [default: "step"]
- --invariant the invariants to check, separated by a comma [string]
- --temporal the temporal properties to check, separated by a comma
+ --help Show help [boolean]
+ --version Show version number [boolean]
+ --out output file (suppresses all console output) [string]
+ --main name of the main module (by default, computed from
+ filename) [string]
+ --init name of the initializer action[string] [default: "init"]
+ --step name of the step action [string] [default: "step"]
+ --invariant the invariants to check, separated by commas (e.g.)
[string]
+ --temporal the temporal properties to check, separated by commas
+ [string]
+ --out-itf output the trace in the Informal Trace Format to file
+ (suppresses all console output) [string]
+ --max-steps the maximum number of steps in every trace
+ [number] [default: 10]
--random-transitions choose transitions at random (= use symbolic simulation)
[boolean] [default: false]
--apalache-config path to an additional Apalache configuration file (in
JSON) [string]
- --verbosity control how much output is produced (0 to 5)
+ --verbosity control how much output is produced (0 to 5)
[number] [default: 2]
```
@@ -332,7 +347,7 @@ steps:
Apalache uses bounded model checking. This technique checks *all runs* up to
`--max-steps` steps via [z3][]. Apalache is highly configurable. See [Apalache
configuration](https://apalache.informal.systems/docs/apalache/config.html?highlight=configuration#apalache-configuration)
-for guidance.
+for guidance.
- If there are no critical errors (e.g., in parsing, typechecking, etc.), this
command sends the Quint specification to the [Apalache][] model checker, which
diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md
index e4ff60b30..56aa13c52 100644
--- a/quint/apalache-tests.md
+++ b/quint/apalache-tests.md
@@ -239,18 +239,24 @@ VARIABLE x
A == Variant("A", "U_OF_UNIT")
-B(__BParam_27) == Variant("B", __BParam_27)
+B(__BParam_31) == Variant("B", __BParam_31)
-foo_bar(id__123_31) == id__123_31
+foo_bar(id__123_35) == id__123_35
importedValue == 0
ApalacheCompilation_ModuleToInstantiate_C == 0
+altInit == x' := 0
+
step == x' := (x + 1)
+altStep == x' := (x + 0)
+
inv == x >= 0
+altInv == x >= 0
+
ApalacheCompilation_ModuleToInstantiate_instantiatedValue ==
ApalacheCompilation_ModuleToInstantiate_C
@@ -259,6 +265,55 @@ init ==
:= (importedValue
+ ApalacheCompilation_ModuleToInstantiate_instantiatedValue)
+q_step == step
+
+q_init == init
+
+================================================================================
+```
+
+### Test that we can compile to TLA+ of the expected form with CLI configs
+
+We check that specifying `--init`, `--step`, and `--invariant` work as expected
+
+
+```
+quint compile --target tlaplus \
+ --init altInit --step altStep --invariant altInv \
+ ./testFixture/ApalacheCompilation.qnt \
+ | grep -e q_init -e q_step -e q_inv
+```
+
+
+```
+q_init == altInit
+q_step == altStep
+q_inv == altInv
+```
+
+### Test that we can compile to TLA+ of the expected form, specifying `--main`
+
+
+```
+quint compile --target tlaplus --main ModuleToImport ./testFixture/ApalacheCompilation.qnt
+```
+
+
+```
+---------------------------- MODULE ModuleToImport ----------------------------
+
+EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
+
+step == TRUE
+
+importedValue == 0
+
+init == TRUE
+
+q_init == init
+
+q_step == step
+
================================================================================
```
@@ -270,14 +325,18 @@ init ==
quint compile --target tlaplus ../examples/classic/distributed/ClockSync/clockSync3.qnt | head
```
+The compiled module is not empty:
-TODO: This is an incorrect result, we are removing all "unused" declarations
-which leaves nothing, thanks to the way clockSync3 is instanced.
```
------------------------------ MODULE clockSync3 ------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
-================================================================================
+VARIABLE clockSync3_clockSync3Spec_time
+
+clockSync3_clockSync3Spec_Proc(clockSync3_clockSync3Spec_id_37) ==
+ [id |-> clockSync3_clockSync3Spec_id_37]
+
+VARIABLE clockSync3_clockSync3Spec_hc
```
diff --git a/quint/src/cli.ts b/quint/src/cli.ts
index da318605e..7bcf81866 100755
--- a/quint/src/cli.ts
+++ b/quint/src/cli.ts
@@ -17,6 +17,7 @@ import {
compile,
docs,
load,
+ outputCompilationTarget,
outputResult,
parse,
runRepl,
@@ -36,6 +37,32 @@ const defaultOpts = (yargs: any) =>
type: 'string',
})
+// Arguments used by routines that pass thru the `compile` stage
+const compileOpts = (yargs: any) =>
+ defaultOpts(yargs)
+ .option('main', {
+ desc: 'name of the main module (by default, computed from filename)',
+ type: 'string',
+ })
+ .option('init', {
+ desc: 'name of the initializer action',
+ type: 'string',
+ default: 'init',
+ })
+ .option('step', {
+ desc: 'name of the step action',
+ type: 'string',
+ default: 'step',
+ })
+ .option('invariant', {
+ desc: 'the invariants to check, separated by commas (e.g.)',
+ type: 'string',
+ })
+ .option('temporal', {
+ desc: 'the temporal properties to check, separated by commas',
+ type: 'string',
+ })
+
// Chain async CLIProcedures
//
// This saves us having to manually thread the result argument like
@@ -77,11 +104,7 @@ const compileCmd = {
command: 'compile ',
desc: 'compile a Quint specification into the target, the output is written to stdout',
builder: (yargs: any) =>
- defaultOpts(yargs)
- .option('main', {
- desc: 'name of the main module (by default, computed from filename)',
- type: 'string',
- })
+ compileOpts(yargs)
.option('target', {
desc: `the compilation target. Supported values: ${supportedTarges.join(', ')}`,
type: 'string',
@@ -99,7 +122,12 @@ const compileCmd = {
default: verbosity.defaultLevel,
}),
handler: (args: any) =>
- load(args).then(chainCmd(parse)).then(chainCmd(typecheck)).then(chainCmd(compile)).then(outputResult),
+ load(args)
+ .then(chainCmd(parse))
+ .then(chainCmd(typecheck))
+ .then(chainCmd(compile))
+ .then(chainCmd(outputCompilationTarget))
+ .then(outputResult),
}
// construct repl commands with yargs
@@ -235,15 +263,7 @@ const verifyCmd = {
command: 'verify ',
desc: `Verify a Quint specification via Apalache`,
builder: (yargs: any) =>
- yargs
- .option('main', {
- desc: 'name of the main module (by default, computed from filename)',
- type: 'string',
- })
- .option('out', {
- desc: 'output file (suppresses all console output)',
- type: 'string',
- })
+ compileOpts(yargs)
.option('out-itf', {
desc: 'output the trace in the Informal Trace Format to file (suppresses all console output)',
type: 'string',
@@ -253,26 +273,6 @@ const verifyCmd = {
type: 'number',
default: 10,
})
- .option('init', {
- desc: 'name of the initializer action',
- type: 'string',
- default: 'init',
- })
- .option('step', {
- desc: 'name of the step action',
- type: 'string',
- default: 'step',
- })
- .option('invariant', {
- desc: 'the invariants to check, separated by a comma',
- type: 'string',
- coerce: (s: string) => s.split(','),
- })
- .option('temporal', {
- desc: 'the temporal properties to check, separated by a comma',
- type: 'string',
- coerce: (s: string) => s.split(','),
- })
.option('random-transitions', {
desc: 'choose transitions at random (= use symbolic simulation)',
type: 'boolean',
@@ -295,7 +295,12 @@ const verifyCmd = {
// type: 'number',
// })
handler: (args: any) =>
- load(args).then(chainCmd(parse)).then(chainCmd(typecheck)).then(chainCmd(verifySpec)).then(outputResult),
+ load(args)
+ .then(chainCmd(parse))
+ .then(chainCmd(typecheck))
+ .then(chainCmd(compile))
+ .then(chainCmd(verifySpec))
+ .then(outputResult),
}
// construct documenting commands with yargs
diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts
index 2fdb81b2c..99c6f968f 100644
--- a/quint/src/cliCommands.ts
+++ b/quint/src/cliCommands.ts
@@ -29,7 +29,7 @@ import { Either, left, right } from '@sweet-monads/either'
import { EffectScheme } from './effects/base'
import { LookupTable, UnusedDefinitions } from './names/base'
import { ReplOptions, quintRepl } from './repl'
-import { OpQualifier, QuintEx, QuintModule, QuintOpDef, qualifier } from './ir/quintIr'
+import { FlatModule, OpQualifier, QuintEx, QuintModule, QuintOpDef, qualifier } from './ir/quintIr'
import { TypeScheme } from './types/base'
import { createFinders, formatError } from './errorReporter'
import { DocumentationEntry, produceDocs, toMarkdown } from './docs'
@@ -44,13 +44,21 @@ import { Rng, newRng } from './rng'
import { fileSourceResolver } from './parsing/sourceResolver'
import { verify } from './quintVerifier'
import { flattenModules } from './flattening/fullFlattener'
-import { analyzeInc, analyzeModules } from './quintAnalyzer'
+import { AnalysisOutput, analyzeInc, analyzeModules } from './quintAnalyzer'
import { ExecutionFrame } from './runtime/trace'
import { flow, isEqual, uniqWith } from 'lodash'
import { Maybe, just, none } from '@sweet-monads/maybe'
import { compileToTlaplus } from './compileToTlaplus'
-export type stage = 'loading' | 'parsing' | 'typechecking' | 'testing' | 'running' | 'compiling' | 'documentation'
+export type stage =
+ | 'loading'
+ | 'parsing'
+ | 'typechecking'
+ | 'testing'
+ | 'running'
+ | 'compiling'
+ | 'outputting target'
+ | 'documentation'
/** The data from a ProcedureStage that may be output to --out */
interface OutputStage {
@@ -138,6 +146,10 @@ interface TypecheckedStage extends ParsedStage {
modes: Map
}
+interface CompiledStage extends TypecheckedStage, AnalysisOutput {
+ mainModule: FlatModule
+}
+
interface TestedStage extends LoadedStage {
// the names of the passed tests
passed: string[]
@@ -606,20 +618,46 @@ export async function runSimulator(prev: TypecheckedStage): Promise> {
- const stage: stage = 'compiling'
+export async function compile(typechecked: TypecheckedStage): Promise> {
const args = typechecked.args
- const verbosityLevel = deriveVerbosity(args)
+ const mainName = guessMainModule(typechecked)
+ const main = typechecked.modules.find(m => m.name === mainName)
+ if (!main) {
+ return cliErr(`module ${mainName} does not exist`, { ...typechecked, errors: [], sourceCode: new Map() })
+ }
+
+ // Wrap init, step, invariant and temporal properties in other definitions,
+ // to make sure they are not considered unused in the main module and,
+ // therefore, ignored by the flattener
+ const extraDefsAsText = [`action q::init = ${args.init}`, `action q::step = ${args.step}`]
+
+ if (args.invariant) {
+ extraDefsAsText.push(`val q::inv = and(${args.invariant})`)
+ }
+ if (args.temporal) {
+ extraDefsAsText.push(`temporal q::temporalProps = and(${args.temporal})`)
+ }
+ const extraDefs = extraDefsAsText.map(d => parseDefOrThrow(d, typechecked.idGen, new Map()))
+ main.declarations.push(...extraDefs)
+
+ // We have to update the lookup table and analysis result with the new definitions. This is not ideal, and the problem
+ // is that is hard to add this definitions in the proper stage, in our current setup. We should try to tackle this
+ // while solving #1052.
+ const resolutionResult = parsePhase3importAndNameResolution({ ...typechecked, errors: [] })
+ if (resolutionResult.errors.length > 0) {
+ const errors = resolutionResult.errors.map(mkErrorMessage(typechecked.sourceMap))
+ return cliErr('name resolution failed', { ...typechecked, errors })
+ }
+
+ typechecked.table = resolutionResult.table
+ analyzeInc(typechecked, typechecked.table, extraDefs)
+
+ // Flatten modules, replacing instances, imports and exports with their definitions
const { flattenedModules, flattenedTable, flattenedAnalysis } = flattenModules(
typechecked.modules,
typechecked.table,
@@ -628,36 +666,43 @@ export async function compile(typechecked: TypecheckedStage): Promise m.name === mainName)!
- if (!main) {
- return cliErr(`module ${mainName} does not exist`, { ...typechecked, errors: [], sourceCode: new Map() })
- }
+ // Pick the main module
+ const flatMain = flattenedModules.find(m => m.name === mainName)!
- const flattenedStage: TypecheckedStage = {
+ return right({
...typechecked,
...flattenedAnalysis,
- modules: [main],
+ mainModule: flatMain,
table: flattenedTable,
- stage,
- }
+ stage: 'compiling',
+ })
+}
- const parsedSpecJson = jsonStringOfOutputStage(pickOutputStage(flattenedStage))
- switch ((typechecked.args.target as string).toLowerCase()) {
+/** output a compiled spec in the format specified in the `compiled.args.target` to stdout
+ *
+ * @param compiled The result of a preceding compile stage
+ */
+export async function outputCompilationTarget(compiled: CompiledStage): Promise> {
+ const stage: stage = 'outputting target'
+ const args = compiled.args
+ const verbosityLevel = deriveVerbosity(args)
+
+ const parsedSpecJson = jsonStringOfOutputStage(pickOutputStage({ ...compiled, modules: [compiled.mainModule] }))
+ switch ((compiled.args.target as string).toLowerCase()) {
case 'json':
process.stdout.write(parsedSpecJson)
- return right(flattenedStage)
+ return right(compiled)
case 'tlaplus': {
const toTlaResult = await compileToTlaplus(parsedSpecJson, verbosityLevel)
return toTlaResult
.mapRight(tla => {
process.stdout.write(tla) // Write out, since all went right
- return flattenedStage
+ return compiled
})
.mapLeft(err => {
return {
msg: err.explanation,
- stage: { ...flattenedStage, stage, status: 'error', errors: err.errors },
+ stage: { ...compiled, stage, status: 'error', errors: err.errors },
}
})
}
@@ -672,7 +717,7 @@ export async function compile(typechecked: TypecheckedStage): Promise> {
+export async function verifySpec(prev: CompiledStage): Promise> {
const verifying = { ...prev, stage: 'verifying' as stage }
const args = verifying.args
const verbosityLevel = deriveVerbosity(args)
@@ -686,51 +731,7 @@ export async function verifySpec(prev: TypecheckedStage): Promise m.name === mainName)
- if (!main) {
- return cliErr(`module ${mainName} does not exist`, { ...verifying, errors: [], sourceCode: new Map() })
- }
-
- // Wrap init, step, invariant and temporal properties in other definitions,
- // to make sure they are not considered unused in the main module and,
- // therefore, ignored by the flattener
- const extraDefsAsText = [`action q::init = ${args.init}`, `action q::step = ${args.step}`]
- if (args.invariant) {
- extraDefsAsText.push(`val q::inv = and(${args.invariant.join(',')})`)
- }
- if (args.temporal) {
- extraDefsAsText.push(`temporal q::temporalProps = and(${args.temporal.join(',')})`)
- }
-
- const extraDefs = extraDefsAsText.map(d => parseDefOrThrow(d, verifying.idGen, new Map()))
- main.declarations.push(...extraDefs)
-
- // We have to update the lookup table and analysis result with the new definitions. This is not ideal, and the problem
- // is that is hard to add this definitions in the proper stage, in our current setup. We should try to tackle this
- // while solving #1052.
- const resolutionResult = parsePhase3importAndNameResolution({ ...prev, errors: [] })
- if (resolutionResult.errors.length > 0) {
- const errors = resolutionResult.errors.map(mkErrorMessage(prev.sourceMap))
- return cliErr('name resolution failed', { ...verifying, errors })
- }
-
- verifying.table = resolutionResult.table
- analyzeInc(verifying, verifying.table, extraDefs)
-
- // Flatten modules, replacing instances, imports and exports with their definitions
- const { flattenedModules, flattenedTable, flattenedAnalysis } = flattenModules(
- verifying.modules,
- verifying.table,
- verifying.idGen,
- verifying.sourceMap,
- verifying
- )
-
- // Pick main module, we only pass this on to Apalache
- const flatMain = flattenedModules.find(m => m.name === mainName)!
-
- const veryfiyingFlat = { ...verifying, ...flattenedAnalysis, modules: [flatMain], table: flattenedTable }
+ const veryfiyingFlat = { ...prev, modules: [prev.mainModule] }
const parsedSpec = jsonStringOfOutputStage(pickOutputStage(veryfiyingFlat))
// We need to insert the data form CLI args into their appropriate locations
diff --git a/quint/testFixture/ApalacheCompilation.qnt b/quint/testFixture/ApalacheCompilation.qnt
index 02a415496..b1ffde284 100644
--- a/quint/testFixture/ApalacheCompilation.qnt
+++ b/quint/testFixture/ApalacheCompilation.qnt
@@ -4,15 +4,19 @@ module ModuleToInstantiate {
val instantiatedValue = C
}
+// Used for import tests and for testing specifying an alternate main module
module ModuleToImport {
val importedValue = 0
+
+ action init = true
+ action step = true
}
module ApalacheCompilation {
// Tests whether we can compile imports
- import ModuleToImport.*
+ import ModuleToImport.importedValue
- // Tests whether we can compile instantiations
+ // Tests whether we can compile instances
import ModuleToInstantiate(C = 0).*
var x: int
@@ -24,12 +28,23 @@ module ApalacheCompilation {
// Tests whether we will sanitize identifiers
def foo::bar(__123) = __123
- // TODO: Tests that we remove primes from assignments in the init functino
+ // TODO: Tests that we remove primes from assignments in the init function
action init = {
x' = importedValue + instantiatedValue
}
+ // Tests that we can specify an alternative init via CLI args
+ action altInit = {
+ x' = 0
+ }
+
action step = x' = x + 1
+ // Tests that we can specify an alternative step via CLI args
+ action altStep = x' = x + 0
+
def inv = x >= 0
+
+ // Tests that we can specify an alternative invariant via CLI args
+ def altInv = x >= 0
}