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_explore::combine_lts;

13

use merc_io::LargeFormatter;

14

use merc_lts::GenericLts;

15

use merc_lts::LTS;

16

use merc_lts::LtsBuilderFast;

17

use merc_lts::LtsFormat;

18

use merc_lts::LtsMultiAction;

19

use merc_lts::SimpleAction;

20

use merc_lts::StateIndex;

21

use merc_lts::apply_lts;

22

use merc_lts::apply_lts_pair;

23

use merc_lts::guess_lts_format_from_extension;

24

use merc_lts::read_explicit_lts;

25

use merc_lts::read_lts;

26

use merc_lts::read_mcrl2_aut;

27

use merc_lts::write_aut;

28

use merc_lts::write_bcg;

29

use merc_lts::write_mcrl2_aut;

30

use merc_reduction::Equivalence;

31

use merc_reduction::reduce_lts;

32

use merc_refinement::ExplorationStrategy;

33

use merc_refinement::RefinementType;

34

use merc_refinement::refines;

35

use merc_syntax::generate_formula;

36

use merc_syntax::parse_action_names;

37

use merc_syntax::parse_allow_action_names;

38

use merc_syntax::parse_comm_expr_set;

39

use merc_tools::VerbosityFlag;

40

use merc_tools::Version;

41

use merc_tools::VersionFlag;

42

use merc_tools::format_key_values_json;

43

use merc_tools::report_error;

44

use merc_unsafety::print_allocator_metrics;

45

use merc_utilities::MercError;

46

use merc_utilities::Timing;

47

48

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

49

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

50

#[command(arg_required_else_help = true)]

51

struct Cli {

52

    #[command(flatten)]

53

    version: VersionFlag,

54

55

    #[command(flatten)]

56

    verbosity: VerbosityFlag,

57

58

    #[command(subcommand)]

59

    commands: Option<Commands>,

60

61

    #[arg(long, global = true)]

62

    timings: bool,

63

64

65

/// Defines the subcommands for this tool.

66

#[derive(Debug, Subcommand)]

67

enum Commands {

68

    /// Prints information related to the given LTS.

69

    Info(InfoArgs),

70

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

71

    Reduce(ReduceArgs),

72

    /// Compares two LTS modulo an equivalent relation.

73

    Compare(CompareArgs),

74

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

75

    Refines(RefinesArgs),

76

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

77

    Convert(ConvertArgs),

78

    /// Computes the parallel composition hide(allow(comm(L1 || ... || Ln))).

79

    Combine(CombineArgs),

80

81

82

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

83

struct InfoArgs {

84

    /// Specify the input LTS.

85

    filename: String,

86

87

    /// Explicitly specify the LTS file format.

88

    #[arg(long)]

89

    format: Option<LtsFormat>,

90

91

92

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

93

struct ReduceArgs {

94

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

95

    equivalence: Equivalence,

96

97

    /// Specify the input LTS.

98

    filename: PathBuf,

99

100

    /// Explicitly specify the LTS file format.

101

    #[arg(long)]

102

    format: Option<LtsFormat>,

103

104

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

105

    #[arg(long)]

106

    output: Option<PathBuf>,

107

108

    /// Disables preprocessing of the LTS before reducing.

109

    #[arg(long)]

110

    no_preprocess: bool,

111

112

113

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

114

struct CompareArgs {

115

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

116

    equivalence: Equivalence,

117

118

    /// Specify the input LTS.

119

    left_filename: PathBuf,

120

121

    /// Specify the input LTS.

122

    right_filename: PathBuf,

123

124

    /// Explicitly specify the LTS file format.

125

    #[arg(long)]

126

    format: Option<LtsFormat>,

127

128

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

129

    #[arg(long)]

130

    no_preprocess: bool,

131

132

133

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

134

struct ConvertArgs {

135

    /// Explicitly specify the LTS input file format.

136

    #[arg(long)]

137

    format: Option<LtsFormat>,

138

139

    /// Specify the input LTS.

140

    filename: PathBuf,

141

142

    /// Explicitly specify the LTS output file format.

143

    #[arg(long)]

144

    output_format: Option<LtsFormat>,

145

146

    /// Specify the output LTS.

147

    output: Option<PathBuf>,

148

149

150

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

151

struct RefinesArgs {

152

    /// Selects the preorder to check for refinement.

153

    refinement: RefinementType,

154

155

    /// Specify the implementation LTS.

156

    implementation_filename: PathBuf,

157

158

    /// Specify the specification LTS.

159

    specification_filename: PathBuf,

160

161

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

162

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

163

    counter_example: Option<PathBuf>,

164

165

    /// Explicitly specify the LTS file format.

166

    #[arg(long)]

167

    format: Option<LtsFormat>,

168

169

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

170

    #[arg(long)]

171

    no_preprocess: bool,

172

173

174

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

175

struct CombineArgs {

176

    /// The input LTSs for which the parallel composition should be computed.

177

    #[arg(required=true, num_args=2..)]

178

    lts: Vec<PathBuf>,

179

180

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

181

    #[arg(long)]

182

    output: Option<PathBuf>,

183

184

    /// Determines the outermost hide operator.

185

    #[arg(long)]

186

    hide: Option<String>,

187

188

    /// Reads the hide operator from a file.

189

    #[arg(long)]

190

    hide_file: Option<PathBuf>,

191

192

    /// Determines the action names for the allow operator.

193

    #[arg(long)]

194

    allow: Option<String>,

195

196

    /// Reads the allow operator from a file.

197

    #[arg(long)]

198

    allow_file: Option<PathBuf>,

199

200

    /// Determines the communication expressions for the comm operator.

201

    #[arg(long)]

202

    comm: Option<String>,

203

204

    /// Reads the comm operator from a file.

205

    #[arg(long)]

206

    comm_file: Option<PathBuf>,

207

208

    /// Determines the number of threads to use for the parallel composition, defaults to one.

209

    #[arg(long, default_value_t = 1)]

210

    threads: usize,

211

212

    /// Explicitly specify the LTS file format.

213

    #[arg(long)]

214

    format: Option<LtsFormat>,

215

216

    /// Explicitly specify the output LTS file format.

217

    #[arg(long)]

218

    output_format: Option<LtsFormat>,

219

220

221

fn main() -> ExitCode {

222

    let cli = Cli::parse();

223

224

    env_logger::Builder::new()

225

        .filter_level(cli.verbosity.log_level_filter())

226

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

227

        .parse_default_env()

228

        .init();

229

230

    if cli.version.into() {

231

        eprintln!("{}", Version);

232

        return ExitCode::SUCCESS;

233

234

235

    let mut timing = Timing::new();

236

    let result = handle_command(cli.commands, &mut timing);

237

238

    if cli.timings {

239

        timing.print();

240

241

242

    print_allocator_metrics();

243

    report_error(result)

244

245

246

fn handle_command(commands: Option<Commands>, timing: &mut Timing) -> Result<(), MercError> {

247

    if let Some(command) = &commands {

248

        match command {

249

            Commands::Info(args) => {

250

                handle_info(args, timing)?;

251

252

            Commands::Reduce(args) => {

253

                handle_reduce(args, timing)?;

254

255

            Commands::Compare(args) => {

256

                handle_compare(args, timing)?;

257

258

            Commands::Refines(args) => {

259

                handle_refinement(args, timing)?;

260

261

            Commands::Convert(args) => {

262

                handle_convert(args, timing)?;

263

264

            Commands::Combine(args) => {

265

                handle_combine(args, timing)?;

266

267

268

269

270

    Ok(())

271

272

273

/// Display information about the given LTS.

274

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

275

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

276

277

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

278

    let lts = read_explicit_lts(path, format, timing)?;

279

    println!(

280

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

281

        LargeFormatter(lts.num_of_states()),

282

        LargeFormatter(lts.num_of_transitions())

283

);

284

285

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

286

        println!("Labels:");

287

        for label in lts.labels() {

288

            println!("  {}", label);

289

290

291

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

292

            acc + lts

293

                .outgoing_transitions(s)

294

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

295

                .count()

296

});

297

298

        // Count the number of silent transitions.

299

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

300

301

        // Structured output.

302

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

303

});

304

305

    Ok(())

306

307

308

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

309

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

310

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

311

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

312

313

    let lts = read_explicit_lts(path, format, timing)?;

314

    info!(

315

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

316

        LargeFormatter(lts.num_of_states()),

317

        LargeFormatter(lts.num_of_transitions())

318

);

319

320

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

321

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

322

323

        info!(

324

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

325

            LargeFormatter(reduced_lts.num_of_states()),

326

            LargeFormatter(reduced_lts.num_of_transitions())

327

);

328

329

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

330

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

331

            write_aut(&mut writer, &reduced_lts)?;

332

        } else {

333

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

334

335

336

        Ok(())

337

    })?;

338

339

    Ok(())

340

341

342

/// Handles the refinement checking between two LTSs.

343

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

344

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

345

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

346

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

347

348

    let impl_lts = read_explicit_lts(impl_path, format, timing)?;

349

    let spec_lts = read_explicit_lts(spec_path, format, timing)?;

350

351

    info!(

352

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

353

        LargeFormatter(impl_lts.num_of_states()),

354

        LargeFormatter(impl_lts.num_of_transitions())

355

);

356

    info!(

357

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

358

        LargeFormatter(spec_lts.num_of_states()),

359

        LargeFormatter(spec_lts.num_of_transitions())

360

);

361

362

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

363

                                                 right,

364

                                                 timing|

365

     -> Result<(), MercError> {

366

        let (result, counter_example) = refines(

367

            left,

368

            right,

369

            args.refinement,

370

            ExplorationStrategy::BFS,

371

            !args.no_preprocess,

372

            args.counter_example.is_some(),

373

            timing,

374

);

375

376

        if result {

377

            println!("true");

378

        } else {

379

            if let Some(counter_example) = counter_example {

380

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

381

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

382

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

383

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

384

                } else {

385

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

386

387

388

389

            println!("false");

390

391

392

        Ok(())

393

    })?;

394

395

    Ok(())

396

397

398

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

399

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

400

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

401

402

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

403

    let left_lts = read_explicit_lts(&args.left_filename, format, timing)?;

404

    let right_lts = read_explicit_lts(&args.right_filename, format, timing)?;

405

406

    info!(

407

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

408

        LargeFormatter(left_lts.num_of_states()),

409

        LargeFormatter(left_lts.num_of_transitions())

410

);

411

    info!(

412

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

413

        LargeFormatter(right_lts.num_of_states()),

414

        LargeFormatter(right_lts.num_of_transitions())

415

);

416

417

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

418

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

419

});

420

421

    if equivalent {

422

        println!("true");

423

    } else {

424

        println!("false");

425

426

427

    Ok(())

428

429

430

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

431

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

432

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

433

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

434

435

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

436

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

437

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

438

        format

439

    } else {

440

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

441

};

442

443

    match input_lts {

444

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

445

            LtsFormat::Bcg => {

446

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

447

                    write_bcg(&lts, path)?;

448

                } else {

449

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

450

451

452

            LtsFormat::Aut => {

453

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

454

455

            _ => {

456

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

457

458

},

459

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

460

            LtsFormat::Aut | LtsFormat::AutMcrl2 => {

461

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

462

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

463

                } else {

464

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

465

466

467

            LtsFormat::Bcg => {

468

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

469

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

470

                } else {

471

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

472

473

474

            LtsFormat::Lts => {

475

                return Err("Conversion from AutMcrl2 to LTS is not yet implemented.".into());

476

477

},

478

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

479

            LtsFormat::Aut | LtsFormat::AutMcrl2 => {

480

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

481

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

482

                } else {

483

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

484

485

486

            LtsFormat::Bcg => {

487

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

488

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

489

                } else {

490

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

491

492

493

            LtsFormat::Lts => {

494

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

495

496

},

497

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

498

            LtsFormat::Aut => {

499

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

500

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

501

                } else {

502

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

503

504

505

            _ => {

506

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

507

508

},

509

510

511

    Ok(())

512

513

514

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

515

    let format = guess_lts_format_from_extension(&args.lts[0], args.format).ok_or("Unknown LTS file format.")?;

516

517

    // Parse the hide, allow and comm arguments, if they are provided.

518

    let mut hide = match &args.hide {

519

        Some(arg) => parse_action_names(arg).map_err(|e| format!("Failed to parse --hide argument:\n{e}"))?,

520

        None => Vec::new(),

521

};

522

523

    if let Some(hide_file) = &args.hide_file {

524

        if !hide_file.exists() {

525

            return Err(format!("--hide-file path does not exist: {}", hide_file.display()).into());

526

527

        if !hide_file.is_file() {

528

            return Err(format!("--hide-file path is not a file: {}", hide_file.display()).into());

529

530

        let contents = std::fs::read_to_string(hide_file)?;

531

        hide.extend(parse_action_names(&contents).map_err(|e| format!("Failed to parse --hide-file argument:\n{e}"))?);

532

533

534

    let mut allow = match &args.allow {

535

        Some(arg) => parse_allow_action_names(arg).map_err(|e| format!("Failed to parse --allow argument:\n{e}"))?,

536

        None => Vec::new(),

537

};

538

539

    if let Some(allow_file) = &args.allow_file {

540

        if !allow_file.exists() {

541

            return Err(format!("--allow-file path does not exist: {}", allow_file.display()).into());

542

543

        if !allow_file.is_file() {

544

            return Err(format!("--allow-file path is not a file: {}", allow_file.display()).into());

545

546

        let contents = std::fs::read_to_string(allow_file)?;

547

        allow.extend(

548

            parse_allow_action_names(&contents).map_err(|e| format!("Failed to parse --allow-file argument:\n{e}"))?,

549

);

550

551

552

    let mut comm = match &args.comm {

553

        Some(arg) => parse_comm_expr_set(arg).map_err(|e| format!("Failed to parse --comm argument:\n{e}"))?,

554

        None => Vec::new(),

555

};

556

557

    if let Some(comm_file) = &args.comm_file {

558

        if !comm_file.exists() {

559

            return Err(format!("--comm-file path does not exist: {}", comm_file.display()).into());

560

561

        if !comm_file.is_file() {

562

            return Err(format!("--comm-file path is not a file: {}", comm_file.display()).into());

563

564

        let contents = std::fs::read_to_string(comm_file)?;

565

        comm.extend(parse_comm_expr_set(&contents).map_err(|e| format!("Failed to parse --comm-file argument:\n{e}"))?);

566

567

568

    match format {

569

        LtsFormat::AutMcrl2 => {

570

            let lts_list = args

571

                .lts

572

                .iter()

573

                .map(|path| -> Result<_, MercError> {

574

                    let file = File::open(path)?;

575

                    read_mcrl2_aut(&file)?.relabel(|label| LtsMultiAction::<SimpleAction>::from_string(&label))

576

})

577

                .collect::<Result<Vec<_>, _>>()?;

578

579

            let mut builder = LtsBuilderFast::new(Vec::new(), Vec::new());

580

            combine_lts(&mut builder, lts_list, &hide, &allow, &comm, timing)?;

581

            let result = builder.finish(StateIndex::new(0), false);

582

583

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

584

                write_mcrl2_aut(&mut File::create(output)?, &result)?;

585

            } else {

586

                write_mcrl2_aut(&mut stdout(), &result)?;

587

588

589

        LtsFormat::Aut | LtsFormat::Bcg => {

590

            return Err(format!("Combining LTSs in {format:?} format is not yet implemented, please convert the LTSs to AutMcrl2 format first.").into());

591

592

        LtsFormat::Lts => {

593

            let lts_list = args

594

                .lts

595

                .iter()

596

                .map(|path| -> Result<_, MercError> {

597

                    let file = File::open(path)?;

598

                    read_lts(&file, false)

599

})

600

                .collect::<Result<Vec<_>, _>>()?;

601

602

            let mut builder = LtsBuilderFast::new(Vec::new(), Vec::new());

603

            combine_lts(&mut builder, lts_list, &hide, &allow, &comm, timing)?;

604

            let result = builder.finish(StateIndex::new(0), false);

605

606

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

607

                write_mcrl2_aut(&mut File::create(output)?, &result)?;

608

            } else {

609

                write_mcrl2_aut(&mut stdout(), &result)?;

610

611

612

613

614

    Ok(())

615