mc: add --jani-no-constants flag

Author: Philipp15b

src/main.rs

@@ -208,6 +208,10 @@ pub struct JaniOptions {
     #[arg(long)]
     pub jani_skip_quant_pre: bool,
 
+    /// Declare procedure inputs as JANI variables, not constants.
+    #[arg(long)]
+    pub jani_no_constants: bool,
+
     /// By default, Caesar assigns arbitrary initial values to output variables.
     /// This means that the model does not reflect the possible effects of
     /// initial values of output variables on the program. Usually, this is not

src/mc/mod.rs

@@ -185,8 +185,6 @@ pub fn proc_to_model(
     }
 
     // Declare the proc inputs as model parameters
-    // TODO: add an option to instead declare the proc parameters as
-    // (indeterminate) inputs to the automaton
     model.constants.extend(constants);
 
     // Make all of the automaton's variables public so they can be accessed by
@@ -239,15 +237,25 @@ fn translate_var_decls(
 ) -> Result<(Vec<ConstantDeclaration>, Vec<VariableDeclaration>), JaniConversionError> {
     let mut vars = translate_local_decls(expr_translator, proc)?;
 
-    // we declare proc inputs as constants, not variables
+    // by default, proc inputs are translated as constants
     let mut constants = vec![];
     for param in proc.inputs.node.iter() {
-        constants.push(ConstantDeclaration {
-            name: Identifier(param.name.to_string()),
-            typ: translate_type(&param.ty, param.span)?,
-            value: None,
-            comment: None,
-        });
+        if !options.jani_no_constants {
+            constants.push(ConstantDeclaration {
+                name: Identifier(param.name.to_string()),
+                typ: translate_type(&param.ty, param.span)?,
+                value: None,
+                comment: None,
+            });
+        } else {
+            vars.push(VariableDeclaration {
+                name: Identifier(param.name.to_string()),
+                typ: translate_type(&param.ty, param.span)?,
+                transient: false,
+                initial_value: None,
+                comment: None,
+            });
+        }
     }
 
     // proc outputs are normal variables

website/docs/model-checking.md

@@ -176,6 +176,8 @@ The input parameters of the program are translated by Caesar to constants in the
  * For the [Caesar's Storm backend](#caesars-storm-backend) can fix values with the `--storm-constants <name>=<value>,...,<name>=<value>` command-line flag.
   * Storm itself uses the `--constants <name>=<value>,...,<name>=<value>` command-line flag.
 
+Caesar can also be instructed to translate inputs to variables instead of constants with the `--jani-no-constants` flag.
+
 **State Limits to Approximate Infinite-State Models.**
 Storm can be used with a state limit so that the model generation will stop its exploration at some number of states.
 This will yield a correct *under*-approximation of the expected reward.