Skip to content

Commit

Permalink
Merge pull request #1154 from informalsystems/th/verify-flag-temporal
Browse files Browse the repository at this point in the history 
Add `--temporal` flag for verify
  • Loading branch information
@thpani
thpani authored Sep 7, 2023
2 parents 315e2c1 + bfe6850 commit 5a36609
Show file tree
Hide file tree
Showing 7 changed files with 122 additions and 32 deletions.
4 changes: 4 additions & 0 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
## UNRELEASED

### Added

- Added `--temporal` flag for `verify`, enabling temporal property verification
through Apalache (#1154)

### Changed
### Deprecated
### Removed
Expand Down
4 changes: 2 additions & 2 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,8 +170,8 @@ completely implementing every pass.
| Invariant checking | - | - | - | - | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| [Higher-order definitions][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
| [Runs][] | :white_check_mark: | :white_check_mark: | :green_circle: | :white_check_mark: | :white_check_mark: | *non-goal* | :white_check_mark: |
| [Temporal operators][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :x: | :x: |
| [Fairness][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :x: | :x: |
| [Temporal operators][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :white_check_mark: | :x: |
| [Fairness][] | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | *non-goal* | :white_check_mark: | :x: |
| [Unbounded quantifiers][] | :white_check_mark: | :white_check_mark: | :x: | :x: | *non-goal* | :x: | :x: |
| [String literals][], see #118 | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
| ~~uninterpreted types~~, see #118 | :white_check_mark: | :white_check_mark: | :x: | :x: | :x: | :x: | :x: |
Expand Down
30 changes: 17 additions & 13 deletions doc/quint.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -274,20 +274,25 @@ Options:
[number] [default: 10]
--init name of the initializer action [string] [default: "init"]
--step name of the step action [string] [default: "step"]
--invariant invariant to check: a definition name or an expression
--invariant the invariants to check, separated by a comma [string]
--temporal the temporal properties to check, separated by a comma
[string]
--apalache-config Filename of the additional Apalache configuration (in the
HOCON format, a superset of JSON) [string]
--verbosity control how much output is produced (0 to 5)
[number] [default: 2]
```
<!-- TODO: Update after https://github.com/informalsystems/quint/issues/701 -->
Use of this command has three prerequisites:
By default, this command will automatically obtain and run Apalache. The only
prerequisite is a [compatible installation of OpenJDK](quint/README.md).
You may also manually obtain and run a distribution of Apalache, following these
steps:
1. Install a distribution of [Apalache](https://apalache.informal.systems/docs/apalache/installation/jvm.html).
2. Start the Apalache server `apalache-mc server` and ensure that it is running.
1. You have installed a distribution of
[Apalache](https://apalache.informal.systems/docs/apalache/installation/jvm.html)
2. You have set `APALACHE_DIST` as the path to the distribution.
3. You have started the Apalache server `apalache-mc server` and it is running.
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)
Expand All @@ -296,12 +301,11 @@ 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
will try to find an invariant violation. If it finds one, it prints the trace on
the standard output. If it does not find a violating trace, it prints the
longest sample trace that the simulator has found during the execution. When the
parameter `--out` is supplied, the trace is written as a JSON representation of
Quint IR in the output file. When the parameter `--out-itf` is supplied, the
trace is written in the [Informal Trace Format][]. This output can be
conveniently displayed with the [ITF Trace Viewer][], or just with [jq][].
the standard output. When the parameter `--out` is supplied, the trace is
written as a JSON representation of Quint IR in the output file. When the
parameter `--out-itf` is supplied, the trace is written in the [Informal Trace
Format][]. This output can be conveniently displayed with the [ITF Trace
Viewer][], or just with [jq][].
- If the specification cannot be run (e.g., due to a parsing error), the file
contains an error message in JSON:
Expand Down
62 changes: 61 additions & 1 deletion quint/apalache-tests.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,6 @@ error: found a counterexample

## Deadlocks


<!-- !test in reports deadlock -->
```
output=$(quint verify ./testFixture/apalache/deadlock.qnt)
Expand Down Expand Up @@ -159,3 +158,64 @@ An example execution:
[violation] Found an issue (duration).
```

## Temporal properties

### Can verify with single temporal property

<!-- !test check can specify --temporal -->
```
quint verify --temporal eventuallyOne ./testFixture/apalache/temporalTest.qnt
```

### Can verify with two temporal properties

<!-- !test check can specify multiple temporal props -->
```
quint verify --temporal eventuallyOne,eventuallyFive ./testFixture/apalache/temporalTest.qnt
```

### Temporal violations are reported with traces

<!-- !test in prints a trace on temporal violation -->
```
output=$(quint verify --temporal eventuallyZero ./testFixture/apalache/temporalTest.qnt)
exit_code=$?
echo "$output" | egrep 'State|__InLoop:|n:'
exit $exit_code
```

<!-- !test exit 1 -->
<!-- !test err prints a trace on temporal violation -->
```
error: found a counterexample
```

<!-- !test out prints a trace on temporal violation -->
```
An example execution:
[State 0]
__InLoop: false,
__saved_n: 1,
n: 1
[State 1]
__InLoop: true,
__saved_n: 1,
n: 2
[State 2]
__InLoop: true,
__saved_n: 1,
n: 3
[State 3]
__InLoop: true,
__saved_n: 1,
n: 4
[State 4]
__InLoop: true,
__saved_n: 1,
n: 5
[State 5]
__InLoop: true,
__saved_n: 1,
n: 1
```
33 changes: 19 additions & 14 deletions quint/src/cli.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,13 +84,13 @@ const replCmd = {
desc: 'Disable banners and prompts, to simplify scripting (alias for --verbosity=0)',
alias: 'q',
type: 'boolean',
default: false,
})
.default('quiet', false)
.option('verbosity', {
desc: 'control how much output is produced (0 to 5)',
type: 'number',
})
.default('verbosity', verbosity.defaultLevel),
default: verbosity.defaultLevel,
}),
handler: runRepl,
}

Expand All @@ -112,17 +112,17 @@ const testCmd = {
.option('max-samples', {
desc: 'the maximum number of successful runs to try for every randomized test',
type: 'number',
default: 10000,
})
.default('max-samples', 10000)
.option('seed', {
desc: 'random seed to use for non-deterministic choice',
type: 'string',
})
.option('verbosity', {
desc: 'control how much output is produced (0 to 5)',
type: 'number',
default: verbosity.defaultLevel,
})
.default('verbosity', verbosity.defaultLevel)
// Timeouts are postponed for:
// https://github.com/informalsystems/quint/issues/633
//
Expand Down Expand Up @@ -155,37 +155,37 @@ const runCmd = {
.option('max-samples', {
desc: 'the maximum on the number of traces to try',
type: 'number',
default: 10000,
})
.default('max-samples', 10000)
.option('max-steps', {
desc: 'the maximum on the number of steps in every trace',
type: 'number',
default: 20,
})
.default('max-steps', 20)
.option('init', {
desc: 'name of the initializer action',
type: 'string',
default: 'init',
})
.default('init', 'init')
.option('step', {
desc: 'name of the step action',
type: 'string',
default: 'step',
})
.default('step', 'step')
.option('invariant', {
desc: 'invariant to check: a definition name or an expression',
type: 'string',
default: ['true'],
})
.default('invariant', ['true'])
.option('seed', {
desc: 'random seed to use for non-deterministic choice',
type: 'string',
})
.option('verbosity', {
desc: 'control how much output is produced (0 to 5)',
type: 'number',
})
.default('verbosity', verbosity.defaultLevel),
default: verbosity.defaultLevel,
}),
// Timeouts are postponed for:
// https://github.com/informalsystems/quint/issues/633
//
Expand Down Expand Up @@ -235,15 +235,20 @@ const verifyCmd = {
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('apalache-config', {
desc: 'Filename of the additional Apalache configuration (in the HOCON format, a superset of JSON)',
type: 'string',
})
.option('verbosity', {
desc: 'control how much output is produced (0 to 5)',
type: 'number',
})
.default('verbosity', verbosity.defaultLevel),
default: verbosity.defaultLevel,
}),
// Timeouts are postponed for:
// https://github.com/informalsystems/quint/issues/633
//
Expand Down
9 changes: 7 additions & 2 deletions quint/src/cliCommands.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -550,12 +550,16 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
return cliErr(`module ${mainName} does not exist`, { ...verifying, errors: [], sourceCode: '' })
}

// Wrap init, step and invariant in other definitions, to make sure they are not considered unused in the main module
// and, therefore, ignored by the flattener
// 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)
Expand Down Expand Up @@ -604,6 +608,7 @@ export async function verifySpec(prev: TypecheckedStage): Promise<CLIProcedure<V
init: 'q::init',
next: 'q::step',
inv: args.invariant ? ['q::inv'] : undefined,
'temporal-props': args.temporal ? ['q::temporalProps'] : undefined,
},
}

Expand Down
12 changes: 12 additions & 0 deletions quint/testFixture/apalache/temporalTest.qnt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
// This spec defines a model to test temporal verification
module temporalTest {
var n: int

action init = n' = 1
action step = n' = if (n == 5) 1 else n + 1
def inv = n < 5

temporal eventuallyZero = eventually(n == 0) // does NOT hold
temporal eventuallyOne = eventually(n == 1) // holds
temporal eventuallyFive = eventually(n == 5) // holds
}

0 comments on commit 5a36609

Please sign in to comment.