mc: rename to-jani subcommand to mc

we keep the old name available as an alias

Author: Philipp15b

src/driver.rs

@@ -374,7 +374,7 @@ impl SourceUnit {
     /// Encode the source unit as a JANI file if requested.
     pub fn write_to_jani_if_requested(
         &self,
-        options: &crate::JaniOptions,
+        options: &crate::ModelCheckingOptions,
         tcx: &TyCtx,
     ) -> Result<Option<PathBuf>, VerifyError> {
         if let Some(jani_dir) = &options.jani_dir {

src/main.rs

@@ -92,7 +92,7 @@ impl Cli {
         match &self.command {
             Command::Verify(verify_options) => Some(&verify_options.debug_options),
             Command::Lsp(verify_options) => Some(&verify_options.debug_options),
-            Command::ToJani(to_jani_options) => Some(&to_jani_options.debug_options),
+            Command::Mc(mc_options) => Some(&mc_options.debug_options),
             Command::ShellCompletions(_) => None,
             Command::Other(_vec) => unreachable!(),
         }
@@ -103,8 +103,9 @@ impl Cli {
 pub enum Command {
     /// Verify HeyVL files with Caesar.
     Verify(VerifyCommand),
-    /// Convert HeyVL files to JANI files.
-    ToJani(ToJaniCommand),
+    /// Model checking via JANI, can run Storm directly.
+    #[clap(visible_alias = "to-jani")]
+    Mc(ToJaniCommand),
     /// Run Caesar's LSP server.
     Lsp(VerifyCommand),
     /// Generate shell completions for the Caesar binary.
@@ -124,7 +125,7 @@ pub struct VerifyCommand {
     pub rlimit_options: ResourceLimitOptions,
 
     #[command(flatten)]
-    pub jani_options: JaniOptions,
+    pub model_checking_options: ModelCheckingOptions,
 
     #[command(flatten)]
     pub opt_options: OptimizationOptions,
@@ -148,7 +149,7 @@ pub struct ToJaniCommand {
     pub rlimit_options: ResourceLimitOptions,
 
     #[command(flatten)]
-    pub jani_options: JaniOptions,
+    pub model_checking_options: ModelCheckingOptions,
 
     #[command(flatten)]
     pub debug_options: DebugOptions,
@@ -209,7 +210,7 @@ pub enum RunWhichStorm {
 
 #[derive(Debug, Default, Clone, Args)]
 #[command(next_help_heading = "JANI Output Options")]
-pub struct JaniOptions {
+pub struct ModelCheckingOptions {
     /// Export declarations to JANI files in the provided directory.
     #[arg(long)]
     pub jani_dir: Option<PathBuf>,
@@ -259,7 +260,7 @@ pub struct JaniOptions {
     pub storm_timeout: Option<u64>,
 }
 
-impl JaniOptions {
+impl ModelCheckingOptions {
     pub fn storm_timeout(&self) -> Option<Duration> {
         self.storm_timeout.map(Duration::from_secs)
     }
@@ -449,7 +450,7 @@ async fn main() -> ExitCode {
 
     match options.command {
         Command::Verify(options) => run_cli(options).await,
-        Command::ToJani(options) => run_to_jani_main(options),
+        Command::Mc(options) => run_model_checking_main(options),
         Command::Lsp(options) => run_server(options).await,
         Command::ShellCompletions(options) => run_generate_completions(options),
         Command::Other(_) => unreachable!(),
@@ -779,8 +780,8 @@ fn verify_files_main(
     }
 
     // write to JANI if requested
-    to_jani_main(
-        &options.jani_options,
+    run_model_checking(
+        &options.model_checking_options,
         &mut source_units,
         server,
         &limits_ref,
@@ -949,16 +950,16 @@ fn verify_files_main(
     Ok(num_failures == 0)
 }
 
-fn run_to_jani_main(options: ToJaniCommand) -> ExitCode {
+fn run_model_checking_main(options: ToJaniCommand) -> ExitCode {
     let (user_files, server) = match mk_cli_server(&options.input_options) {
         Ok(value) => value,
         Err(value) => return value,
     };
-    let res = to_jani_loader(&options, user_files, &server).map(|_| true);
+    let res = model_checking_main(&options, user_files, &server).map(|_| true);
     finalize_verify_result(server, &options.rlimit_options, res)
 }
 
-fn to_jani_loader(
+fn model_checking_main(
     options: &ToJaniCommand,
     user_files: Vec<FileId>,
     server: &Mutex<dyn Server>,
@@ -973,8 +974,8 @@ fn to_jani_loader(
     let timeout = Instant::now() + options.rlimit_options.timeout();
     let mem_limit = options.rlimit_options.mem_limit();
     let limits_ref = LimitsRef::new(Some(timeout), Some(mem_limit));
-    to_jani_main(
-        &options.jani_options,
+    run_model_checking(
+        &options.model_checking_options,
         &mut source_units,
         server_lock.deref_mut(),
         &limits_ref,
@@ -983,8 +984,8 @@ fn to_jani_loader(
     )
 }
 
-fn to_jani_main(
-    options: &JaniOptions,
+fn run_model_checking(
+    options: &ModelCheckingOptions,
     source_units: &mut Vec<Item<SourceUnit>>,
     server: &mut dyn Server,
     limits_ref: &LimitsRef,

src/mc/mod.rs

@@ -30,7 +30,7 @@ use crate::{
     procs::proc_verify::verify_proc,
     tyctx::TyCtx,
     version::caesar_version_info,
-    JaniOptions,
+    ModelCheckingOptions,
 };
 
 use self::{
@@ -125,7 +125,7 @@ impl JaniConversionError {
 }
 
 pub fn proc_to_model(
-    options: &JaniOptions,
+    options: &ModelCheckingOptions,
     tcx: &TyCtx,
     proc: &ProcDecl,
 ) -> Result<Model, JaniConversionError> {
@@ -231,7 +231,7 @@ fn check_calculus_annotation(proc: &ProcDecl) -> Result<(), JaniConversionError>
 /// Translate variable declarations, including local variable declarations, as
 /// well as input and output parameters.
 fn translate_var_decls(
-    options: &JaniOptions,
+    options: &ModelCheckingOptions,
     expr_translator: &ExprTranslator<'_>,
     proc: &ProcDecl,
 ) -> Result<(Vec<ConstantDeclaration>, Vec<VariableDeclaration>), JaniConversionError> {

src/mc/run_storm.rs

@@ -18,7 +18,7 @@ use z3rro::util::PrettyRational;
 use crate::{
     ast::{Diagnostic, Label, Span},
     resource_limits::LimitsRef,
-    JaniOptions, RunWhichStorm,
+    ModelCheckingOptions, RunWhichStorm,
 };
 
 pub type StormResult = Result<StormOutput, StormError>;
@@ -40,9 +40,9 @@ pub fn storm_result_to_diagnostic(result: &StormResult, span: Span) -> Diagnosti
                 .with_code(NumberOrString::String("model checking".to_owned())),
         },
         Err(err) => Diagnostic::new(ReportKind::Error, span)
-            .with_message(format!("Error running Storm: {}", err))
+            .with_message(err)
             .with_label(Label::new(span))
-            .with_code(NumberOrString::String("model checking".to_owned())),
+            .with_code(NumberOrString::String("storm".to_owned())),
     }
 }
 
@@ -75,7 +75,7 @@ pub enum StormError {
 ///
 /// Panics if `options.run_storm` is `None`.
 pub fn run_storm(
-    options: &JaniOptions,
+    options: &ModelCheckingOptions,
     mut jani_file: &Path,
     properties: Vec<String>,
     limits_ref: &LimitsRef,
@@ -194,7 +194,7 @@ pub fn run_storm(
 }
 
 fn parse_property_results(
-    options: &JaniOptions,
+    options: &ModelCheckingOptions,
     properties: Vec<String>,
     output: &str,
 ) -> IndexMap<String, StormValue> {
@@ -207,7 +207,11 @@ fn parse_property_results(
         .collect()
 }
 
-fn find_property_result(options: &JaniOptions, output: &str, property: &str) -> StormValue {
+fn find_property_result(
+    options: &ModelCheckingOptions,
+    output: &str,
+    property: &str,
+) -> StormValue {
     const RESULT_TEXT: &str = "Result (for initial states):";
 
     let search_string = format!("Model checking property \"{}\"", property);

website/docs/model-checking.md

@@ -76,10 +76,10 @@ Caesar does not automatically update these images.
 To update the `:ci` image for example, run `docker pull movesrwth/storm:ci`.
 </small>
 
-The above flag can be used with Caesar's `to-jani` command:
+The above flag can be used with Caesar's `mc` command:
 For example:
 ```bash
-caesar to-jani --run-storm path example.heyvl
+caesar mc --run-storm path example.heyvl
 ```
 The result will look like this:
 ```
@@ -93,10 +93,10 @@ Furthermore, you can set the `--no-verify` flag to only run model checking and n
 
 ### Option B: Generating JANI Manually {#generating-jani-manually}
 
-To export JANI files for the model checker, run Caesar with the `to-jani` subcommand and the `--jani-dir DIR` option to instruct it to save all translateable (co)procs to `.jani` files in the directory `DIR`:
+To export JANI files for the model checker, run Caesar with the `mc` subcommand and the `--jani-dir DIR` option to instruct it to save all translateable (co)procs to `.jani` files in the directory `DIR`:
 
 ```bash
-caesar to-jani example.heyvl --jani-dir DIR
+caesar mc example.heyvl --jani-dir DIR
 ```
 
 The output JANI files will have the following structure that you can use:
@@ -163,7 +163,7 @@ proc geo_mc(init_c: UInt) -> (c: UInt, cont: Bool) // added input parameter init
 With Caesar, we could run the following command to approximate the expected reward for the program with `init_c = 5` with 10000 states:
 
 ```bash
-caesar to-jani --run-storm <VALUE> example.heyvl --storm-constants init_c=5 --storm-state-limit 10000
+caesar mc --run-storm <VALUE> example.heyvl --storm-constants init_c=5 --storm-state-limit 10000
 ```
 And we get a result like this:
 ```