1 
use std::fs::File;
2 
use std::path::Path;
3 
use std::process::ExitCode;
4 

            

        

            

                5
            

            

                
            

            

                
use clap::Parser;

            

        

            

                6
            

            

                
            

            

                
use clap::Subcommand;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
use merc_io::LargeFormatter;

            

        

            

                9
            

            

                
            

            

                
use merc_ldd::Storage;

            

        

            

                10
            

            

                
            

            

                
use merc_symbolic::read_symbolic_lts;

            

        

            

                11
            

            

                
            

            

                
use merc_tools::verbosity::VerbosityFlag;

            

        

            

                12
            

            

                
            

            

                
use merc_tools::Version;

            

        

            

                13
            

            

                
            

            

                
use merc_tools::VersionFlag;

            

        

            

                14
            

            

                
            

            

                
use merc_unsafety::print_allocator_metrics;

            

        

            

                15
            

            

                
            

            

                
use merc_utilities::MercError;

            

        

            

                16
            

            

                
            

            

                
use merc_utilities::Timing;

            

        

            

                17
            

            

                
            

            

                

            

        

            

                18
            

            

                
            

            

                
#[derive(clap::Parser, Debug)]

            

        

            

                19
            

            

                
            

            

                
#[command(

            

        

            

                20
            

            

                
            

            

                
    about = "A command line tool for symbolic labelled transition systems",

            

        

            

                21
            

            

                
            

            

                
    arg_required_else_help = true

            

        

            

                22
            

            

                
            

            

                
)]

            

        

            

                23
            

            

                
            

            

                
struct Cli {

            

        

            

                24
            

            

                
            

            

                
    #[command(flatten)]

            

        

            

                25
            

            

                
            

            

                
    version: VersionFlag,

            

        

            

                26
            

            

                
            

            

                

            

        

            

                27
            

            

                
            

            

                
    #[command(flatten)]

            

        

            

                28
            

            

                
            

            

                
    verbosity: VerbosityFlag,

            

        

            

                29
            

            

                
            

            

                

            

        

            

                30
            

            

                
            

            

                
    #[command(subcommand)]

            

        

            

                31
            

            

                
            

            

                
    commands: Option<Commands>,

            

        

            

                32
            

            

                
            

            

                

            

        

            

                33
            

            

                
            

            

                
    #[arg(long, global = true)]

            

        

            

                34
            

            

                
            

            

                
    timings: bool,

            

        

            

                35
            

            

                
            

            

                
}

            

        

            

                36
            

            

                
            

            

                

            

        

            

                37
            

            

                
            

            

                
/// Defines the subcommands for this tool.

            

        

            

                38
            

            

                
            

            

                
#[derive(Debug, Subcommand)]

            

        

            

                39
            

            

                
            

            

                
enum Commands {

            

        

            

                40
            

            

                
            

            

                
    Info(InfoArgs),

            

        

            

                41
            

            

                
            

            

                
}

            

        

            

                42
            

            

                
            

            

                

            

        

            

                43
            

            

                
            

            

                
#[derive(clap::Args, Debug)]

            

        

            

                44
            

            

                
            

            

                
#[command(about = "Prints information related to the given symbolic LTS")]

            

        

            

                45
            

            

                
            

            

                
struct InfoArgs {

            

        

            

                46
            

            

                
            

            

                
    filename: String,

            

        

            

                47
            

            

                
            

            

                
}

            

        

            

                48
            

            

                
            

            

                

            

        

            

                49
            

            

                
            

            

                
fn main() -> Result<ExitCode, MercError> {

            

        

            

                50
            

            

                
            

            

                
    let cli = Cli::parse();

            

        

            

                51
            

            

                
            

            

                

            

        

            

                52
            

            

                
            

            

                
    env_logger::Builder::new()

            

        

            

                53
            

            

                
            

            

                
        .filter_level(cli.verbosity.log_level_filter())

            

        

            

                54
            

            

                
            

            

                
        .parse_default_env()

            

        

            

                55
            

            

                
            

            

                
        .init();

            

        

            

                56
            

            

                
            

            

                

            

        

            

                57
            

            

                
            

            

                
    if cli.version.into() {

            

        

            

                58
            

            

                
            

            

                
        eprintln!("{}", Version);

            

        

            

                59
            

            

                
            

            

                
        return Ok(ExitCode::SUCCESS);

            

        

            

                60
            

            

                
            

            

                
    }

            

        

            

                61
            

            

                
            

            

                

            

        

            

                62
            

            

                
            

            

                
    let mut timing = Timing::new();

            

        

            

                63
            

            

                
            

            

                

            

        

            

                64
            

            

                
            

            

                
    if let Some(command) = cli.commands {

            

        

            

                65
            

            

                
            

            

                
        match command {

            

        

            

                66
            

            

                
            

            

                
            Commands::Info(args) => handle_info(args, &mut timing)?,

            

        

            

                67
            

            

                
            

            

                
        }

            

        

            

                68
            

            

                
            

            

                
    }

            

        

            

                69
            

            

                
            

            

                

            

        

            

                70
            

            

                
            

            

                
    if cli.timings {

            

        

            

                71
            

            

                
            

            

                
        timing.print();

            

        

            

                72
            

            

                
            

            

                
    }

            

        

            

                73
            

            

                
            

            

                

            

        

            

                74
            

            

                
            

            

                
    print_allocator_metrics();

            

        

            

                75
            

            

                
            

            

                
    Ok(ExitCode::SUCCESS)

            

        

            

                76
            

            

                
            

            

                
}

            

        

            

                77
            

            

                
            

            

                

            

        

            

                78
            

            

                
            

            

                
/// Reads the given symbolic LTS and prints information about it.

            

        

            

                79
            

            

                
            

            

                
fn handle_info(args: InfoArgs, timing: &mut Timing) -> Result<(), MercError> {

            

        

            

                80
            

            

                
            

            

                
    let path = Path::new(&args.filename);

            

        

            

                81
            

            

                
            

            

                
    let mut storage = Storage::new();

            

        

            

                82
            

            

                
            

            

                

            

        

            

                83
            

            

                
            

            

                
    let mut time_read = timing.start("read_symbolic_lts");

            

        

            

                84
            

            

                
            

            

                
    let lts = read_symbolic_lts(File::open(path)?, &mut storage)?;

            

        

            

                85
            

            

                
            

            

                
    time_read.finish();

            

        

            

                86
            

            

                
            

            

                

            

        

            

                87
            

            

                
            

            

                
    println!("Symbolic LTS information:");

            

        

            

                88
            

            

                
            

            

                
    println!("  Number of states: {}", LargeFormatter(merc_ldd::len(&mut storage, lts.states())));

            

        

            

                89
            

            

                
            

            

                
    println!("  Number of summand groups: {}", lts.summand_groups().len());

            

        

            

                90
            

            

                
            

            

                

            

        

            

                91
            

            

                
            

            

                
    Ok(())

            

        

            

                92
            

            

                
            

            

                
}