Skip to content

Commit

Permalink
Merge pull request #1407 from informalsystems/1402/compile-init-step-inv
Browse files Browse the repository at this point in the history 
Add q::* operators to compiled targets
  • Loading branch information
@bugarela
bugarela authored Mar 22, 2024
2 parents dfd0f7f + fe3ccb7 commit cb460f3
Show file tree
Hide file tree
Showing 5 changed files with 231 additions and 136 deletions.
53 changes: 34 additions & 19 deletions doc/quint.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -73,15 +73,18 @@ especially useful for debugging complex specifications.
$ quint compile --help
quint compile <input>

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]
--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]
--target the compilation target. Supported values: tlaplus, json
[string] [default: "json"]
--verbosity control how much output is produced (0 to 5)[number] [default: 2]
Expand All @@ -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
Expand All @@ -105,7 +118,7 @@ The following compilation targets are supported
to be expected.*

```sh
$ quint parse --help
$ quint parse --help
quint parse <input>

parse a Quint specification
Expand Down Expand Up @@ -292,30 +305,32 @@ Options:
## Command verify
```sh
$ quint verify <input>
$ quint verify --help
quint verify <input>

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]
```
Expand All @@ -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
Expand Down
69 changes: 64 additions & 5 deletions quint/apalache-tests.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

<!-- !test in can convert ApalacheCompliation.qnt to TLA+ with CLI config -->
```
quint compile --target tlaplus \
--init altInit --step altStep --invariant altInv \
./testFixture/ApalacheCompilation.qnt \
| grep -e q_init -e q_step -e q_inv
```

<!-- !test out can convert ApalacheCompliation.qnt to TLA+ with CLI config -->
```
q_init == altInit
q_step == altStep
q_inv == altInv
```

### Test that we can compile to TLA+ of the expected form, specifying `--main`

<!-- !test in can convert ApalacheCompliation.qnt to TLA+ with alt main -->
```
quint compile --target tlaplus --main ModuleToImport ./testFixture/ApalacheCompilation.qnt
```

<!-- !test out can convert ApalacheCompliation.qnt to TLA+ with alt main -->
```
---------------------------- MODULE ModuleToImport ----------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
step == TRUE
importedValue == 0
init == TRUE
q_init == init
q_step == step
================================================================================
```

Expand All @@ -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.
<!-- !test out can convert clockSync3.qnt to TLA+ -->
```
------------------------------ 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
```
77 changes: 41 additions & 36 deletions quint/src/cli.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ import {
compile,
docs,
load,
outputCompilationTarget,
outputResult,
parse,
runRepl,
Expand All @@ -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
Expand Down Expand Up @@ -77,11 +104,7 @@ const compileCmd = {
command: 'compile <input>',
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',
Expand All @@ -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
Expand Down Expand Up @@ -235,15 +263,7 @@ const verifyCmd = {
command: 'verify <input>',
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',
Expand All @@ -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',
Expand All @@ -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
Expand Down
Loading

0 comments on commit cb460f3

Please sign in to comment.