Grcov report - main.rs

1

use std::fs::File;

2

use std::io::Write;

3

use std::io::stdout;

4

use std::path::Path;

5

use std::path::PathBuf;

6

use std::process::ExitCode;

7

8

use clap::Parser;

9

use clap::Subcommand;

10

use log::info;

11

12

use merc_io::LargeFormatter;

13

use merc_lts::GenericLts;

14

use merc_lts::LTS;

15

use merc_lts::LtsFormat;

16

use merc_lts::apply_lts;

17

use merc_lts::apply_lts_pair;

18

use merc_lts::guess_lts_format_from_extension;

19

use merc_lts::read_explicit_lts;

20

use merc_lts::write_aut;

21

use merc_lts::write_bcg;

22

use merc_reduction::Equivalence;

23

use merc_reduction::reduce_lts;

24

use merc_refinement::ExplorationStrategy;

25

use merc_refinement::RefinementType;

26

use merc_refinement::generate_formula;

27

use merc_refinement::refines;

28

use merc_tools::VerbosityFlag;

29

use merc_tools::Version;

30

use merc_tools::VersionFlag;

31

use merc_tools::format_key_values_json;

32

use merc_unsafety::print_allocator_metrics;

33

use merc_utilities::MercError;

34

use merc_utilities::Timing;

35

36

/// A command line tool for labelled transition systems.

37

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

38

#[command(arg_required_else_help = true)]

39

struct Cli {

40

    #[command(flatten)]

41

    version: VersionFlag,

42

43

    #[command(flatten)]

44

    verbosity: VerbosityFlag,

45

46

    #[command(subcommand)]

47

    commands: Option<Commands>,

48

49

    #[arg(long, global = true)]

50

    timings: bool,

51

52

53

/// Defines the subcommands for this tool.

54

#[derive(Debug, Subcommand)]

55

enum Commands {

56

    /// Prints information related to the given LTS.

57

    Info(InfoArgs),

58

    /// Reduces the given LTS modulo an equivalent relation.

59

    Reduce(ReduceArgs),

60

    /// Compares two LTS modulo an equivalent relation.

61

    Compare(CompareArgs),

62

    /// Checks whether the given implementation LTS refines the given specification LTS modulo various refinement relations.

63

    Refines(RefinesArgs),

64

    /// Converts an LTS from one format to another format.

65

    Convert(ConvertArgs),

66

67

68

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

69

struct InfoArgs {

70

    /// Specify the input LTS.

71

    filename: String,

72

73

    /// Explicitly specify the LTS file format.

74

    #[arg(long)]

75

    format: Option<LtsFormat>,

76

77

    /// List of actions that should be considered tau actions.

78

    #[arg(short, long, value_delimiter = ',')]

79

    tau: Option<Vec<String>>,

80

81

82

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

83

struct ReduceArgs {

84

    /// Selects the equivalence to reduce the LTS modulo.

85

    equivalence: Equivalence,

86

87

    /// Specify the input LTS.

88

    filename: PathBuf,

89

90

    /// Explicitly specify the LTS file format.

91

    #[arg(long)]

92

    filetype: Option<LtsFormat>,

93

94

    /// Specify the output LTS, if not given, output to stdout.

95

    #[arg(long)]

96

    output: Option<PathBuf>,

97

98

    /// List of actions that should be considered tau actions.

99

    #[arg(long, value_delimiter = ',')]

100

    tau: Option<Vec<String>>,

101

102

    /// Disables preprocessing of the LTS before reducing.

103

    #[arg(long)]

104

    no_preprocess: bool,

105

106

107

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

108

struct CompareArgs {

109

    /// Selects the equivalence to compare the LTSs modulo.

110

    equivalence: Equivalence,

111

112

    /// Specify the input LTS.

113

    left_filename: PathBuf,

114

115

    /// Specify the input LTS.

116

    right_filename: PathBuf,

117

118

    /// Explicitly specify the LTS file format.

119

    #[arg(long)]

120

    format: Option<LtsFormat>,

121

122

    /// List of actions that should be considered tau actions.

123

    #[arg(long, value_delimiter = ',')]

124

    tau: Option<Vec<String>>,

125

126

    /// Disables preprocessing of the LTSs before checking equivalence.

127

    #[arg(long)]

128

    no_preprocess: bool,

129

130

131

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

132

struct ConvertArgs {

133

    /// Explicitly specify the LTS input file format.

134

    #[arg(long)]

135

    format: Option<LtsFormat>,

136

137

    /// Specify the input LTS.

138

    filename: PathBuf,

139

140

    /// Explicitly specify the LTS output file format.

141

    #[arg(long)]

142

    output_format: Option<LtsFormat>,

143

144

    /// Specify the output LTS.

145

    output: Option<PathBuf>,

146

147

    /// List of actions that should be considered tau actions.

148

    #[arg(long, value_delimiter = ',')]

149

    tau: Option<Vec<String>>,

150

151

152

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

153

struct RefinesArgs {

154

    /// Selects the preorder to check for refinement.

155

    refinement: RefinementType,

156

157

    /// Specify the implementation LTS.

158

    implementation_filename: PathBuf,

159

160

    /// Specify the specification LTS.

161

    specification_filename: PathBuf,

162

163

    /// If set, outputs a counter-example when refinement does not hold.

164

    #[arg(short = 'c', long)]

165

    counter_example: Option<PathBuf>,

166

167

    /// Explicitly specify the LTS file format.

168

    #[arg(long)]

169

    format: Option<LtsFormat>,

170

171

    /// List of actions that should be considered tau actions

172

    #[arg(long, value_delimiter = ',')]

173

    tau: Option<Vec<String>>,

174

175

    /// Disables preprocessing of the LTSs before checking refinement.

176

    #[arg(long)]

177

    no_preprocess: bool,

178

179

180

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

181

    let cli = Cli::parse();

182

183

    env_logger::Builder::new()

184

        .filter_level(cli.verbosity.log_level_filter())

185

        .format_key_values(|formatter, source| format_key_values_json(formatter, source))

186

        .parse_default_env()

187

        .init();

188

189

    if cli.version.into() {

190

        eprintln!("{}", Version);

191

        return Ok(ExitCode::SUCCESS);

192

193

194

    let mut timing = Timing::new();

195

196

    if let Some(command) = &cli.commands {

197

        match command {

198

            Commands::Info(args) => {

199

                handle_info(args, &mut timing)?;

200

201

            Commands::Reduce(args) => {

202

                handle_reduce(args, &mut timing)?;

203

204

            Commands::Compare(args) => {

205

                handle_compare(args, &mut timing)?;

206

207

            Commands::Refines(args) => {

208

                handle_refinement(args, &mut timing)?;

209

210

            Commands::Convert(args) => {

211

                handle_convert(args, &mut timing)?;

212

213

214

215

216

    if cli.timings {

217

        timing.print();

218

219

220

    print_allocator_metrics();

221

    Ok(ExitCode::SUCCESS)

222

223

224

/// Display information about the given LTS.

225

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

226

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

227

228

    let format = guess_lts_format_from_extension(path, args.format).ok_or("Unknown LTS file format.")?;

229

    let lts = read_explicit_lts(path, format, args.tau.clone().unwrap_or_default(), timing)?;

230

    println!(

231

        "LTS has {} states and {} transitions.",

232

        LargeFormatter(lts.num_of_states()),

233

        LargeFormatter(lts.num_of_transitions())

234

);

235

236

    apply_lts!(lts, (), |lts, _| {

237

        println!("Labels:");

238

        for label in lts.labels() {

239

            println!("  {}", label);

240

241

242

        let num_of_silent_transitions = lts.iter_states().fold(0, |acc, s| {

243

            acc + lts

244

                .outgoing_transitions(s)

245

                .filter(|t| lts.is_hidden_label(t.label))

246

                .count()

247

});

248

249

        // Count the number of silent transitions.

250

        println!("Silent transitions: {}", num_of_silent_transitions);

251

252

        // Structured output.

253

        println!("{{\"num_of_silent_transitions\": {}}}", num_of_silent_transitions);

254

});

255

256

    Ok(())

257

258

259

/// Reduce the given LTS into another LTS modulo any of the supported equivalences.

260

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

261

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

262

    let format = guess_lts_format_from_extension(path, args.filetype).ok_or("Unknown LTS file format.")?;

263

264

    let lts = read_explicit_lts(path, format, args.tau.clone().unwrap_or_default(), timing)?;

265

    info!(

266

        "LTS has {} states and {} transitions.",

267

        LargeFormatter(lts.num_of_states()),

268

        LargeFormatter(lts.num_of_transitions())

269

);

270

271

    apply_lts!(lts, timing, |lts, timing| -> Result<(), MercError> {

272

        let reduced_lts = reduce_lts(lts, args.equivalence, !args.no_preprocess, timing);

273

274

        info!(

275

            "Reduced LTS has {} states and {} transitions.",

276

            LargeFormatter(reduced_lts.num_of_states()),

277

            LargeFormatter(reduced_lts.num_of_transitions())

278

);

279

280

        if let Some(file) = &args.output {

281

            let mut writer = File::create(file)?;

282

            write_aut(&mut writer, &reduced_lts)?;

283

        } else {

284

            write_aut(&mut stdout(), &reduced_lts)?;

285

286

287

        Ok(())

288

    })?;

289

290

    Ok(())

291

292

293

/// Handles the refinement checking between two LTSs.

294

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

295

    let impl_path = Path::new(&args.implementation_filename);

296

    let spec_path = Path::new(&args.specification_filename);

297

    let format = guess_lts_format_from_extension(impl_path, args.format).ok_or("Unknown LTS file format.")?;

298

299

    let impl_lts = read_explicit_lts(impl_path, format, args.tau.clone().unwrap_or_default(), timing)?;

300

    let spec_lts = read_explicit_lts(spec_path, format, args.tau.clone().unwrap_or_default(), timing)?;

301

302

    info!(

303

        "Implementation LTS has {} states and {} transitions.",

304

        LargeFormatter(impl_lts.num_of_states()),

305

        LargeFormatter(impl_lts.num_of_transitions())

306

);

307

    info!(

308

        "Specification LTS has {} states and {} transitions.",

309

        LargeFormatter(spec_lts.num_of_states()),

310

        LargeFormatter(spec_lts.num_of_transitions())

311

);

312

313

    apply_lts_pair!(impl_lts, spec_lts, timing, |left,

314

                                                 right,

315

                                                 timing|

316

     -> Result<(), MercError> {

317

        let (result, counter_example) = refines(

318

            left,

319

            right,

320

            args.refinement,

321

            ExplorationStrategy::BFS,

322

            !args.no_preprocess,

323

            args.counter_example.is_some(),

324

            timing,

325

);

326

327

        if result {

328

            println!("true");

329

        } else {

330

            if let Some(counter_example) = counter_example {

331

                if let Some(path) = &args.counter_example {

332

                    // Generate a counterexample formula and output it to the given path.

333

                    let mut writer = File::create(path)?;

334

                    writeln!(&mut writer, "{}", generate_formula(&counter_example))?;

335

                } else {

336

                    panic!("Counter example path not provided.");

337

338

339

340

            println!("false");

341

342

343

        Ok(())

344

    })?;

345

346

    Ok(())

347

348

349

/// Compares two LTSs for equivalence modulo any of the available equivalences.

350

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

351

    let format = guess_lts_format_from_extension(&args.left_filename, args.format).ok_or("Unknown LTS file format.")?;

352

353

    info!("Assuming format {:?} for both LTSs.", format);

354

    let left_lts = read_explicit_lts(

355

        &args.left_filename,

356

        format,

357

        args.tau.clone().unwrap_or_default(),

358

        timing,

359

)?;

360

    let right_lts = read_explicit_lts(

361

        &args.right_filename,

362

        format,

363

        args.tau.clone().unwrap_or_default(),

364

        timing,

365

)?;

366

367

    info!(

368

        "Left LTS has {} states and {} transitions.",

369

        LargeFormatter(left_lts.num_of_states()),

370

        LargeFormatter(left_lts.num_of_transitions())

371

);

372

    info!(

373

        "Right LTS has {} states and {} transitions.",

374

        LargeFormatter(right_lts.num_of_states()),

375

        LargeFormatter(right_lts.num_of_transitions())

376

);

377

378

    let equivalent = apply_lts_pair!(left_lts, right_lts, timing, |left, right, timing| {

379

        merc_reduction::compare_lts(args.equivalence, left, right, !args.no_preprocess, timing)

380

});

381

382

    if equivalent {

383

        println!("true");

384

    } else {

385

        println!("false");

386

387

388

    Ok(())

389

390

391

/// Converts an LTS from one format to another, does not do any reduction, see [handle_reduce] for that.

392

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

393

    let format = guess_lts_format_from_extension(&args.filename, args.format).ok_or("Unknown LTS file format.")?;

394

    let input_lts = read_explicit_lts(&args.filename, format, args.tau.clone().unwrap_or_default(), timing)?;

395

396

    let output_format = if let Some(output) = &args.output {

397

        guess_lts_format_from_extension(output, args.output_format).ok_or("Unknown LTS file format.")?

398

    } else if let Some(format) = args.output_format {

399

        format

400

    } else {

401

        return Err("Either output path or output file format must be specified.".into());

402

};

403

404

    match input_lts {

405

        GenericLts::Aut(lts) => match output_format {

406

            LtsFormat::Bcg => {

407

                if let Some(path) = &args.output {

408

                    write_bcg(&lts, path)?;

409

                } else {

410

                    return Err("Output path must be specified when writing BCG files.".into());

411

412

413

            LtsFormat::Aut => {

414

                return Err("Conversion from AUT to AUT is not useful.".into());

415

416

            _ => {

417

                return Err(format!("Conversion to {output_format:?} format is not yet implemented.").into());

418

419

},

420

        GenericLts::Lts(lts) => match output_format {

421

            LtsFormat::Aut => {

422

                if let Some(path) = &args.output {

423

                    write_aut(&mut File::create(path)?, &lts.relabel(|label| label.to_string()))?;

424

                } else {

425

                    write_aut(&mut stdout(), &lts.relabel(|label| label.to_string()))?;

426

427

428

            LtsFormat::Bcg => {

429

                if let Some(path) = &args.output {

430

                    write_bcg(&lts.relabel(|label| label.to_string()), path)?;

431

                } else {

432

                    return Err("Output path must be specified when writing BCG files.".into());

433

434

435

            LtsFormat::Lts => {

436

                return Err("Conversion from LTS to LTS is not useful.".into());

437

438

},

439

        GenericLts::Bcg(lts) => match output_format {

440

            LtsFormat::Aut => {

441

                if let Some(path) = &args.output {

442

                    write_aut(&mut File::create(path)?, &lts)?;

443

                } else {

444

                    write_aut(&mut stdout(), &lts)?;

445

446

447

            _ => {

448

                return Err(format!("Conversion to {output_format:?}LTS format is not yet implemented.").into());

449

450

},

451

452

453

    Ok(())

454