Merge branch 'main' into gabriela/type-quantification-fix

Author: bugarela

doc/quint.md

@@ -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]
@@ -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 <input>
 
 parse a Quint specification
@@ -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]
 ```
 
@@ -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

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
+
+<!-- !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
+
 ================================================================================
 ```
 
@@ -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
 ```

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 <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',
@@ -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 <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',
@@ -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