Remove init/step for JSON compilation

CHANGELOG.md

@@ -14,6 +14,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Fixed
 
 - Fixed `--step`/`--init` resolving to a state variable instead of an action when the variable is named `step` or `init` (#1969)
+- `quint compile --target=json` no longer requires `init` and `step` to exist in the module (#1971)
 
 ### Security
 

evaluator/benches/tuples.rs

@@ -10,8 +10,6 @@ fn run_in_rust(input: &str) -> Result<(), Box<dyn std::error::Error>> {
     let quint_content = format!(
         "module main {{
           val input = {input}
-          val init = true
-          val step = true
         }}"
     );
 
@@ -46,8 +44,6 @@ fn run_in_quint_repl(input: &str) -> Result<(), Box<dyn std::error::Error>> {
     let quint_content = format!(
         "module main {{
           val input = {input}
-          val init = true
-          val step = true
         }}"
     );
 

evaluator/src/helpers.rs

@@ -18,20 +18,13 @@ use std::process::Command;
 use std::{error::Error, io::Write};
 use tempfile::NamedTempFile;
 
-pub fn parse(
-    quint_content: &str,
-    init: &str,
-    step: &str,
-    inv: Option<&str>,
-) -> Result<QuintOutput, Box<dyn Error>> {
+pub fn parse(quint_content: &str, inv: Option<&str>) -> Result<QuintOutput, Box<dyn Error>> {
     let mut temp_file = NamedTempFile::new()?;
     temp_file.write_all(quint_content.as_bytes())?;
 
     let output = Command::new("quint")
         .arg("compile")
         .arg(temp_file.path())
-        .args(["--init", init])
-        .args(["--step", step])
         .args(["--invariant", inv.unwrap_or("true")])
         .args(["--flatten", "false"])
         .output()?;

evaluator/tests/evaluation_tests.rs

@@ -19,7 +19,7 @@ fn assert_from_string(input: &str, expected: &str) -> Result<(), Box<dyn std::er
         )
     };
 
-    let parsed = helpers::parse(&quint_content(input), "init", "step", None)?;
+    let parsed = helpers::parse(&quint_content(input), None)?;
     let input_def = parsed.find_definition_by_name("expr")?;
     let value = run(&parsed.table, &input_def.expr);
 
@@ -28,7 +28,7 @@ fn assert_from_string(input: &str, expected: &str) -> Result<(), Box<dyn std::er
         return Ok(());
     }
 
-    let parsed_expected = helpers::parse(&quint_content(expected), "init", "step", None)?;
+    let parsed_expected = helpers::parse(&quint_content(expected), None)?;
     let expected_def = parsed_expected.find_definition_by_name("expr")?;
     let expected_value = run(&parsed_expected.table, &expected_def.expr).map(|v| v.normalize());
 
@@ -52,7 +52,7 @@ fn eval_expr(input: &str) -> EvalResult {
         }}"
     );
 
-    let parsed = helpers::parse(&quint_content, "init", "step", None).unwrap();
+    let parsed = helpers::parse(&quint_content, None).unwrap();
     let input_def = parsed.find_definition_by_name("expr").unwrap();
     run(&parsed.table, &input_def.expr)
 }
@@ -68,7 +68,7 @@ fn eval_run(callee: &str, input: &str) -> EvalResult {
         )
     };
 
-    let parsed = helpers::parse(&quint_content, "init", "step", None).unwrap();
+    let parsed = helpers::parse(&quint_content, None).unwrap();
     let run_def = parsed.find_definition_by_name(callee).unwrap();
     let mut interpreter = Interpreter::new(parsed.table.clone());
     let mut env = Env::new(Rc::clone(&interpreter.var_storage), Verbosity::default());
@@ -94,7 +94,7 @@ fn assert_var_after_run(
         )
     };
 
-    let parsed = helpers::parse(&quint_content, "init", "step", None)?;
+    let parsed = helpers::parse(&quint_content, None)?;
     let run_def = parsed.find_definition_by_name(callee)?;
     let mut interpreter = Interpreter::new(parsed.table.clone());
     let mut env = Env::new(Rc::clone(&interpreter.var_storage), Verbosity::default());
@@ -112,7 +112,7 @@ fn assert_var_after_run(
         .borrow();
     let var_value = var_value.clone().value.unwrap().normalize();
 
-    let parsed_expected = helpers::parse(&quint_content, "init", "step", None)?;
+    let parsed_expected = helpers::parse(&quint_content, None)?;
     let expected_def = parsed_expected.find_definition_by_name("expected")?;
     let expected_value = run(&parsed_expected.table, &expected_def.expr)?.normalize();
 

evaluator/tests/picker_tests.rs

@@ -7,7 +7,7 @@ use quint_evaluator::{
 
 macro_rules! run_test {
     ($content:expr, $expected_value:expr) => {{
-        let parsed = helpers::parse($content, "init", "step", None)?;
+        let parsed = helpers::parse($content, None)?;
         let init_def = parsed.find_definition_by_name("init")?;
 
         let mut interpreter = Interpreter::new(parsed.table.clone());
@@ -98,7 +98,7 @@ fn powerset_large_set_pick_test() -> Result<(), Box<dyn std::error::Error>> {
           action step = subset' = subset
         }";
 
-    let parsed = helpers::parse(quint_content, "init", "step", None)?;
+    let parsed = helpers::parse(quint_content, None)?;
     let init_def = parsed.find_definition_by_name("init")?;
 
     let mut interpreter = Interpreter::new(parsed.table.clone());
@@ -130,7 +130,7 @@ fn powerset_very_large_set_pick_test() -> Result<(), Box<dyn std::error::Error>>
           action step = subset' = subset
         }";
 
-    let parsed = helpers::parse(quint_content, "init", "step", None)?;
+    let parsed = helpers::parse(quint_content, None)?;
     let init_def = parsed.find_definition_by_name("init")?;
 
     let mut interpreter = Interpreter::new(parsed.table.clone());
@@ -157,7 +157,7 @@ fn int_pick_can_be_negative() -> Result<(), Box<dyn std::error::Error>> {
           action step = x' = x
         }";
 
-    let parsed = helpers::parse(quint_content, "init", "step", None)?;
+    let parsed = helpers::parse(quint_content, None)?;
     let init_def = parsed.find_definition_by_name("init")?;
     let mut interpreter = Interpreter::new(parsed.table.clone());
 
@@ -213,7 +213,7 @@ fn nat_pick_is_non_negative() -> Result<(), Box<dyn std::error::Error>> {
           action step = x' = x
         }";
 
-    let parsed = helpers::parse(quint_content, "init", "step", None)?;
+    let parsed = helpers::parse(quint_content, None)?;
     let init_def = parsed.find_definition_by_name("init")?;
     let mut interpreter = Interpreter::new(parsed.table.clone());
 

evaluator/tests/stateful_tests.rs

@@ -7,7 +7,7 @@ use quint_evaluator::{
 
 macro_rules! run_test {
     ($content:expr, $expected_values:expr) => {{
-        let parsed = helpers::parse($content, "init", "step", None)?;
+        let parsed = helpers::parse($content, None)?;
         let init_def = parsed.find_definition_by_name("init")?;
 
         let mut interpreter = Interpreter::new(parsed.table.clone());

evaluator/tests/tester_tests.rs

@@ -6,7 +6,7 @@ use std::path::Path;
 /// Helper to parse a test definition from a Quint file
 fn parse_test_from_path(file_path: &Path, test_name: &str) -> Result<TestCase, Box<dyn Error>> {
     // Use helpers to compile the file
-    let output = helpers::parse(&std::fs::read_to_string(file_path)?, "init", "step", None)?;
+    let output = helpers::parse(&std::fs::read_to_string(file_path)?, None)?;
 
     // Find the test definition
     let test_op_def = output.find_definition_by_name(test_name)?;

quint/integration-tests/lang/io.md

@@ -233,7 +233,7 @@ quint compile --target json --flatten ../examples/language-features/instances.qn
 
 <!-- !test out compile flatten=true -->
 ```
-51
+47
 ```
 
 ### Does not flatten modules on compile with `--flatten=false`
@@ -245,7 +245,7 @@ quint compile --target json --flatten=false ../examples/language-features/instan
 
 <!-- !test out compile flatten=false -->
 ```
-39
+35
 ```
 
 ### Errors are reported in the right file

quint/src/cli.ts

@@ -49,12 +49,10 @@ const compileOpts = (yargs: any) =>
     .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',
@@ -346,6 +344,8 @@ const verifyCmd = {
   desc: `Verify a Quint specification via Apalache`,
   builder: (yargs: any) =>
     compileOpts(yargs)
+      .option('init', { default: 'init' })
+      .option('step', { default: 'step' })
       .option('invariants', {
         desc: 'space separated list of invariants to check (definition names). When specified, all invariants are combined with AND and checked together, with detailed reporting of which ones were violated',
         type: 'array',

quint/src/cliCommands.ts

@@ -551,22 +551,30 @@ export async function compile(typechecked: TypecheckedStage): Promise<CLIProcedu
     return cliErr(`module ${mainName} does not exist`, { ...typechecked, errors: [], sourceCode: new Map() })
   }
 
-  // Validate that --init and --step don't resolve to state variables (same check as runSimulator)
+  const extraDefsAsText: string[] = []
+
+  // init/step are required for TLA+ and verification (default to 'init'/'step'),
+  // but optional for JSON compilation (#1584).
+  if (args.target !== 'json') {
+    args.init = args.init ?? 'init'
+    args.step = args.step ?? 'step'
+  }
+
   for (const [name, flag] of [
     [args.init, 'init'],
     [args.step, 'step'],
   ] as const) {
+    if (name === undefined) continue
     const checkResult = toExpr(typechecked, name, { kind: 'action', flag })
     if (checkResult.isLeft()) {
       return cliErr('Argument error', {
         ...typechecked,
         errors: [checkResult.value].map(mkErrorMessage(new Map())),
       })
     }
+    extraDefsAsText.push(`action q::${flag} = ${name}`)
   }
 
-  const extraDefsAsText = [`action q::init = ${args.init}`, `action q::step = ${args.step}`]
-
   const [invariantString, invariantsList] = getInvariants(typechecked.args)
   if (invariantsList.length > 0) {
     extraDefsAsText.push(`val q::inv = and(${invariantString})`)