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::LtsBuilderFast;

16

use merc_lts::LtsFormat;

17

use merc_lts::LtsMultiAction;

18

use merc_lts::SimpleAction;

19

use merc_lts::StateIndex;

20

use merc_lts::apply_lts;

21

use merc_lts::apply_lts_pair;

22

use merc_lts::guess_lts_format_from_extension;

23

use merc_lts::read_explicit_lts;

24

use merc_lts::read_lts;

25

use merc_lts::read_mcrl2_aut;

26

use merc_lts::write_aut;

27

use merc_lts::write_bcg;

28

use merc_lts::write_mcrl2_aut;

29

use merc_reduction::Equivalence;

30

use merc_reduction::reduce_lts;

31

use merc_refinement::ExplorationStrategy;

32

use merc_refinement::RefinementType;

33

use merc_refinement::refines;

34

use merc_syntax::generate_formula;

35

use merc_syntax::parse_action_names;

36

use merc_syntax::parse_allow_action_names;

37

use merc_syntax::parse_comm_expr_set;

38

use merc_tools::VerbosityFlag;

39

use merc_tools::Version;

40

use merc_tools::VersionFlag;

41

use merc_tools::format_key_values_json;

42

use merc_unsafety::print_allocator_metrics;

43

use merc_utilities::MercError;

44

use merc_utilities::Timing;

45

46

use crate::combine::combine_lts;

47

48

mod combine;

49

50

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

51

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

52

#[command(arg_required_else_help = true)]

53

struct Cli {

54

    #[command(flatten)]

55

    version: VersionFlag,

56

57

    #[command(flatten)]

58

    verbosity: VerbosityFlag,

59

60

    #[command(subcommand)]

61

    commands: Option<Commands>,

62

63

    #[arg(long, global = true)]

64

    timings: bool,

65

66

67

/// Defines the subcommands for this tool.

68

#[derive(Debug, Subcommand)]

69

enum Commands {

70

    /// Prints information related to the given LTS.

71

    Info(InfoArgs),

72

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

73

    Reduce(ReduceArgs),

74

    /// Compares two LTS modulo an equivalent relation.

75

    Compare(CompareArgs),

76

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

77

    Refines(RefinesArgs),

78

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

79

    Convert(ConvertArgs),

80

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

81

    Combine(CombineArgs),

82

83

84

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

85

struct InfoArgs {

86

    /// Specify the input LTS.

87

    filename: String,

88

89

    /// Explicitly specify the LTS file format.

90

    #[arg(long)]

91

    format: Option<LtsFormat>,

92

93

94

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

95

struct ReduceArgs {

96

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

97

    equivalence: Equivalence,

98

99

    /// Specify the input LTS.

100

    filename: PathBuf,

101

102

    /// Explicitly specify the LTS file format.

103

    #[arg(long)]

104

    format: Option<LtsFormat>,

105

106

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

107

    #[arg(long)]

108

    output: Option<PathBuf>,

109

110

    /// Disables preprocessing of the LTS before reducing.

111

    #[arg(long)]

112

    no_preprocess: bool,

113

114

115

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

116

struct CompareArgs {

117

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

118

    equivalence: Equivalence,

119

120

    /// Specify the input LTS.

121

    left_filename: PathBuf,

122

123

    /// Specify the input LTS.

124

    right_filename: PathBuf,

125

126

    /// Explicitly specify the LTS file format.

127

    #[arg(long)]

128

    format: Option<LtsFormat>,

129

130

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

131

    #[arg(long)]

132

    no_preprocess: bool,

133

134

135

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

136

struct ConvertArgs {

137

    /// Explicitly specify the LTS input file format.

138

    #[arg(long)]

139

    format: Option<LtsFormat>,

140

141

    /// Specify the input LTS.

142

    filename: PathBuf,

143

144

    /// Explicitly specify the LTS output file format.

145

    #[arg(long)]

146

    output_format: Option<LtsFormat>,

147

148

    /// Specify the output LTS.

149

    output: Option<PathBuf>,

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

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

172

    #[arg(long)]

173

    no_preprocess: bool,

174

175

176

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

177

struct CombineArgs {

178

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

179

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

180

    lts: Vec<PathBuf>,

181

182

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

183

    #[arg(long)]

184

    output: Option<PathBuf>,

185

186

    /// Determines the outermost hide operator.

187

    #[arg(long)]

188

    hide: Option<String>,

189

190

    /// Reads the hide operator from a file.

191

    #[arg(long)]

192

    hide_file: Option<PathBuf>,

193

194

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

195

    #[arg(long)]

196

    allow: Option<String>,

197

198

    /// Reads the allow operator from a file.

199

    #[arg(long)]

200

    allow_file: Option<PathBuf>,

201

202

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

203

    #[arg(long)]

204

    comm: Option<String>,

205

206

    /// Reads the comm operator from a file.

207

    #[arg(long)]

208

    comm_file: Option<PathBuf>,

209

210

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

211

    #[arg(long, default_value_t = 1)]

212

    threads: usize,

213

214

    /// Explicitly specify the LTS file format.

215

    #[arg(long)]

216

    format: Option<LtsFormat>,

217

218

    /// Explicitly specify the output LTS file format.

219

    #[arg(long)]

220

    output_format: Option<LtsFormat>,

221

222

223

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

224

    let cli = Cli::parse();

225

226

    env_logger::Builder::new()

227

        .filter_level(cli.verbosity.log_level_filter())

228

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

229

        .parse_default_env()

230

        .init();

231

232

    if cli.version.into() {

233

        eprintln!("{}", Version);

234

        return Ok(ExitCode::SUCCESS);

235

236

237

    let mut timing = Timing::new();

238

    if let Err(x) = handle_command(cli.commands, &mut timing) {

239

        println!("Error: {x}");

240

241

242

    if cli.timings {

243

        timing.print();

244

245

246

    print_allocator_metrics();

247

    Ok(ExitCode::SUCCESS)

248

249

250

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

251

    if let Some(command) = &commands {

252

        match command {

253

            Commands::Info(args) => {

254

                handle_info(args, timing)?;

255

256

            Commands::Reduce(args) => {

257

                handle_reduce(args, timing)?;

258

259

            Commands::Compare(args) => {

260

                handle_compare(args, timing)?;

261

262

            Commands::Refines(args) => {

263

                handle_refinement(args, timing)?;

264

265

            Commands::Convert(args) => {

266

                handle_convert(args, timing)?;

267

268

            Commands::Combine(args) => {

269

                handle_combine(args, timing)?;

270

271

272

273

274

    Ok(())

275

276

277

/// Display information about the given LTS.

278

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

279

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

280

281

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

282

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

283

    println!(

284

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

285

        LargeFormatter(lts.num_of_states()),

286

        LargeFormatter(lts.num_of_transitions())

287

);

288

289

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

290

        println!("Labels:");

291

        for label in lts.labels() {

292

            println!("  {}", label);

293

294

295

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

296

            acc + lts

297

                .outgoing_transitions(s)

298

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

299

                .count()

300

});

301

302

        // Count the number of silent transitions.

303

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

304

305

        // Structured output.

306

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

307

});

308

309

    Ok(())

310

311

312

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

313

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

314

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

315

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

316

317

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

318

    info!(

319

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

320

        LargeFormatter(lts.num_of_states()),

321

        LargeFormatter(lts.num_of_transitions())

322

);

323

324

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

325

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

326

327

        info!(

328

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

329

            LargeFormatter(reduced_lts.num_of_states()),

330

            LargeFormatter(reduced_lts.num_of_transitions())

331

);

332

333

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

334

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

335

            write_aut(&mut writer, &reduced_lts)?;

336

        } else {

337

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

338

339

340

        Ok(())

341

    })?;

342

343

    Ok(())

344

345

346

/// Handles the refinement checking between two LTSs.

347

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

348

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

349

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

350

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

351

352

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

353

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

354

355

    info!(

356

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

357

        LargeFormatter(impl_lts.num_of_states()),

358

        LargeFormatter(impl_lts.num_of_transitions())

359

);

360

    info!(

361

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

362

        LargeFormatter(spec_lts.num_of_states()),

363

        LargeFormatter(spec_lts.num_of_transitions())

364

);

365

366

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

367

                                                 right,

368

                                                 timing|

369

     -> Result<(), MercError> {

370

        let (result, counter_example) = refines(

371

            left,

372

            right,

373

            args.refinement,

374

            ExplorationStrategy::BFS,

375

            !args.no_preprocess,

376

            args.counter_example.is_some(),

377

            timing,

378

);

379

380

        if result {

381

            println!("true");

382

        } else {

383

            if let Some(counter_example) = counter_example {

384

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

385

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

386

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

387

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

388

                } else {

389

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

390

391

392

393

            println!("false");

394

395

396

        Ok(())

397

    })?;

398

399

    Ok(())

400

401

402

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

403

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

404

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

405

406

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

407

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

408

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

409

410

    info!(

411

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

412

        LargeFormatter(left_lts.num_of_states()),

413

        LargeFormatter(left_lts.num_of_transitions())

414

);

415

    info!(

416

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

417

        LargeFormatter(right_lts.num_of_states()),

418

        LargeFormatter(right_lts.num_of_transitions())

419

);

420

421

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

422

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

423

});

424

425

    if equivalent {

426

        println!("true");

427

    } else {

428

        println!("false");

429

430

431

    Ok(())

432

433

434

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

435

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

436

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

437

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

438

439

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

440

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

441

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

442

        format

443

    } else {

444

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

445

};

446

447

    match input_lts {

448

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

449

            LtsFormat::Bcg => {

450

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

451

                    write_bcg(&lts, path)?;

452

                } else {

453

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

454

455

456

            LtsFormat::Aut => {

457

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

458

459

            _ => {

460

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

461

462

},

463

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

464

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

465

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

466

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

467

                } else {

468

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

469

470

471

            LtsFormat::Bcg => {

472

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

473

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

474

                } else {

475

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

476

477

478

            LtsFormat::Lts => {

479

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

480

481

},

482

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

483

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

484

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

485

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

486

                } else {

487

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

488

489

490

            LtsFormat::Bcg => {

491

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

492

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

493

                } else {

494

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

495

496

497

            LtsFormat::Lts => {

498

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

499

500

},

501

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

502

            LtsFormat::Aut => {

503

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

504

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

505

                } else {

506

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

507

508

509

            _ => {

510

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

511

512

},

513

514

515

    Ok(())

516

517

518

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

519

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

520

521

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

522

    let mut hide = match &args.hide {

523

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

524

        None => Vec::new(),

525

};

526

527

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

528

        if !hide_file.exists() {

529

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

530

531

        if !hide_file.is_file() {

532

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

533

534

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

535

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

536

537

538

    let mut allow = match &args.allow {

539

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

540

        None => Vec::new(),

541

};

542

543

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

544

        if !allow_file.exists() {

545

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

546

547

        if !allow_file.is_file() {

548

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

549

550

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

551

        allow.extend(

552

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

553

);

554

555

556

    let mut comm = match &args.comm {

557

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

558

        None => Vec::new(),

559

};

560

561

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

562

        if !comm_file.exists() {

563

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

564

565

        if !comm_file.is_file() {

566

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

567

568

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

569

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

570

571

572

    match format {

573

        LtsFormat::AutMcrl2 => {

574

            let lts_list = args

575

                .lts

576

                .iter()

577

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

578

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

579

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

580

})

581

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

582

583

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

584

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

585

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

586

587

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

588

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

589

            } else {

590

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

591

592

593

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

594

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

595

596

        LtsFormat::Lts => {

597

            let lts_list = args

598

                .lts

599

                .iter()

600

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

601

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

602

                    read_lts(&file, false)

603

})

604

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

605

606

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

607

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

608

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

609

610

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

611

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

612

            } else {

613

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

614

615

616

617

618

    Ok(())

619