Grcov report - main.rs

1

use std::ffi::OsStr;

2

use std::fs::File;

3

use std::path::PathBuf;

4

use std::process::ExitCode;

5

6

use clap::Parser;

7

use clap::Subcommand;

8

9

use itertools::Itertools;

10

use merc_io::LargeFormatter;

11

use merc_lts::AutStream;

12

use merc_lts::LtsBuilderMem;

13

use merc_lts::LtsFormat;

14

use merc_lts::guess_lts_format_from_extension;

15

use merc_lts::write_bcg;

16

use merc_symbolic::ExplorationStrategy;

17

use merc_symbolic::ReachabilityOptions;

18

use merc_symbolic::SymFormat;

19

use merc_symbolic::SymbolicLPS;

20

use merc_symbolic::SymbolicLTS;

21

use merc_symbolic::SymbolicLtsBdd;

22

use merc_symbolic::convert_symbolic_lts;

23

use merc_symbolic::convert_symbolic_lts_bdd;

24

use merc_symbolic::guess_format_from_extension;

25

use merc_symbolic::parse_compacted_dependency_graph;

26

use merc_symbolic::quotient_symbolic;

27

use merc_symbolic::reachability_bdd;

28

use merc_symbolic::reachability_with_options;

29

use merc_symbolic::read_sylvan;

30

use merc_symbolic::read_symbolic_lts;

31

use merc_symbolic::refine_bisimulation;

32

use merc_symbolic::reorder;

33

use merc_symbolic::sigref_symbolic;

34

use merc_tools::VerbosityFlag;

35

use merc_tools::Version;

36

use merc_tools::VersionFlag;

37

use merc_tools::report_error;

38

use merc_unsafety::print_allocator_metrics;

39

use merc_utilities::MercError;

40

use merc_utilities::Timing;

41

use oxidd::BooleanFunction;

42

use oxidd::util::SatCountCache;

43

use rustc_hash::FxBuildHasher;

44

use which::which_in;

45

46

/// Default node capacity for the Oxidd decision diagram manager.

47

const DEFAULT_OXIDD_NODE_CAPACITY: usize = 2048;

48

49

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

50

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

51

#[command(arg_required_else_help = true)]

52

struct Cli {

53

    #[command(flatten)]

54

    version: VersionFlag,

55

56

    #[command(flatten)]

57

    verbosity: VerbosityFlag,

58

59

    #[command(subcommand)]

60

    commands: Option<Commands>,

61

62

    /// Number of workers for the Oxidd decision diagram manager.

63

    #[arg(long, global = true, default_value_t = 1)]

64

    oxidd_workers: u32,

65

66

    /// Node capacity for the Oxidd decision diagram manager.

67

    #[arg(long, global = true, default_value_t = DEFAULT_OXIDD_NODE_CAPACITY)]

68

    oxidd_node_capacity: usize,

69

70

    /// Cache capacity for the Oxidd decision diagram manager, if `None` it is set to the node capacity.

71

    #[arg(long, global = true)]

72

    oxidd_cache_capacity: Option<usize>,

73

74

    #[arg(long, global = true)]

75

    timings: bool,

76

77

78

/// Defines the subcommands for this tool.

79

#[derive(Debug, Subcommand)]

80

enum Commands {

81

    /// Print information related to the given symbolic LTS.

82

    Info(InfoArgs),

83

    /// Explore the given symbolic LTS.

84

    Explore(ExploreArgs),

85

    /// Computes a reordering for a dependency graph given by lpsreach or pbessolvesymbolic.

86

    Reorder(ReorderArgs),

87

    /// Convert a symbolic LTS to a concrete LTS.

88

    Convert(ConvertArgs),

89

    /// Apply reductions to a symbolic LTS.

90

    Reduce(ReduceArgs),

91

92

93

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

94

struct InfoArgs {

95

    filename: PathBuf,

96

97

    /// Sets the input symbolic LTS format.

98

    #[arg(long)]

99

    format: Option<SymFormat>,

100

101

102

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

103

struct ExploreArgs {

104

    filename: PathBuf,

105

106

    /// Sets the input symbolic LTS format.

107

    #[arg(long)]

108

    format: Option<SymFormat>,

109

110

    /// Use BDD based exploration by converting the symbolic LTS

111

    #[arg(long)]

112

    use_bdd: bool,

113

114

    /// Visualize intermediate BDDs using oxidd-vis.

115

    #[arg(long)]

116

    visualize: bool,

117

118

    /// Exploration strategy to use (LDD path only; ignored with --use-bdd).

119

    #[arg(long, value_enum, default_value = "breadth-first")]

120

    strategy: ExplorationStrategy,

121

122

    /// Detect deadlock states (states without outgoing transitions).

123

    #[arg(long)]

124

    detect_deadlocks: bool,

125

126

127

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

128

struct ReorderArgs {

129

    /// Explicit path to the mCRL2 tools (lpsreach or pbessolvesymbolic)

130

    #[arg(long)]

131

    mcrl2_path: Option<PathBuf>,

132

133

    /// Explicit path to the kahypar tools

134

    #[arg(long)]

135

    kahypar_path: Option<PathBuf>,

136

137

    /// Explicit path to the kahypar.ini file to use.

138

    #[arg(long)]

139

    kahypar_ini_path: Option<PathBuf>,

140

141

    /// The input linear process specification file in the mCRL2 .lps format.

142

    filename: PathBuf,

143

144

145

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

146

struct ConvertArgs {

147

    /// Sets the input symbolic LTS format.

148

    #[arg(long)]

149

    format: Option<SymFormat>,

150

151

    /// The input symbolic LTS file path.

152

    filename: PathBuf,

153

154

    /// Sets the output LTS format.

155

    #[arg(long)]

156

    output_format: Option<LtsFormat>,

157

158

    /// The output LTS file path.

159

    #[arg(long)]

160

    output: Option<PathBuf>,

161

162

163

#[derive(Clone, Copy, clap::ValueEnum, Debug)]

164

enum Equivalence {

165

    StrongBisim,

166

    StrongBisimSigref,

167

168

169

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

170

struct ReduceArgs {

171

    /// The equivalence relation to reduce modulo.

172

    equivalence: Equivalence,

173

174

    /// The input symbolic LTS file path.

175

    filename: PathBuf,

176

177

    /// Sets the input symbolic LTS format.

178

    #[arg(long)]

179

    format: Option<SymFormat>,

180

181

    /// Sets the output LTS format.

182

    #[arg(long)]

183

    output_format: Option<LtsFormat>,

184

185

    /// The output LTS file path.

186

    #[arg(long)]

187

    output: Option<PathBuf>,

188

189

    /// Visualize the reduction steps in oxidd-vis.

190

    #[arg(long)]

191

    visualize: bool,

192

193

    /// Split the signature per transition group.

194

    #[arg(long)]

195

    split_signature: bool,

196

197

    /// Extend each transition relation to the full state and next-state domain.

198

    #[arg(long)]

199

    extend_relation: bool,

200

201

    /// Merge transition relations into a single relation before signature computation.

202

    #[arg(long)]

203

    merge_transitions: bool,

204

205

206

/// Initializes the Oxidd BDD manager based on CLI arguments.

207

fn init_bdd_manager(cli: &Cli) -> oxidd::bdd::BDDManagerRef {

208

    oxidd::bdd::new_manager(

209

        cli.oxidd_node_capacity,

210

        cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

211

        cli.oxidd_workers,

212

213

214

215

/// Initializes the Oxidd LDD manager based on CLI arguments.

216

fn init_ldd_manager(cli: &Cli) -> oxidd::ldd::LDDManagerRef {

217

    oxidd::ldd::new_manager(

218

        cli.oxidd_node_capacity,

219

        cli.oxidd_cache_capacity.unwrap_or(cli.oxidd_node_capacity),

220

        cli.oxidd_workers,

221

222

223

224

fn main() -> ExitCode {

225

    let cli = Cli::parse();

226

227

    env_logger::Builder::new()

228

        .filter_level(cli.verbosity.log_level_filter())

229

        .parse_default_env()

230

        .init();

231

232

    if cli.version.into() {

233

        eprintln!("{}", Version);

234

        return ExitCode::SUCCESS;

235

236

237

    let timing = Timing::new();

238

    let result = handle_command(&cli, &timing);

239

240

    if cli.timings {

241

        timing.print();

242

243

244

    print_allocator_metrics();

245

    report_error(result)

246

247

248

fn handle_command(cli: &Cli, timing: &Timing) -> Result<(), MercError> {

249

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

250

        match command {

251

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

252

            Commands::Explore(args) => handle_explore(cli, args, timing)?,

253

            Commands::Reorder(args) => handle_reorder(args, timing)?,

254

            Commands::Convert(args) => handle_convert(cli, args, timing)?,

255

            Commands::Reduce(args) => handle_reduce(cli, args, timing)?,

256

257

258

259

    Ok(())

260

261

262

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

263

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

264

    let storage = init_ldd_manager(cli);

265

266

    let format =

267

        guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?;

268

269

    if format != SymFormat::Sym {

270

        return Err("Currently only the .sym format is supported for info".into());

271

272

273

    let lts = timing.measure("read_symbolic_lts", || {

274

        read_symbolic_lts(&storage, File::open(&args.filename)?)

275

    })?;

276

277

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

278

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

279

280

    Ok(())

281

282

283

/// Explores the given symbolic LTS.

284

fn handle_explore(cli: &Cli, args: &ExploreArgs, timing: &Timing) -> Result<(), MercError> {

285

    let storage = init_ldd_manager(cli);

286

287

    let format = guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input format")?;

288

289

    let options = ReachabilityOptions {

290

        strategy: args.strategy,

291

        detect_deadlocks: args.detect_deadlocks,

292

};

293

294

    let mut file = File::open(&args.filename)?;

295

    match format {

296

        SymFormat::Sylvan => {

297

            let mut lts = timing.measure("read_symbolic_lts", || read_sylvan(&storage, &mut file))?;

298

299

            if args.use_bdd {

300

                // Sylvan format carries no action labels or parameter values, so BDD conversion is not supported.

301

                return Err("BDD exploration is not supported for Sylvan format".into());

302

303

304

            println!(

305

                "LTS has {} states",

306

                timing.measure("explore", || -> Result<_, MercError> {

307

                    Ok(reachability_with_options(&storage, &mut lts, &options, timing)?

308

                        .states

309

                        .len())

310

})?

311

);

312

313

        SymFormat::Sym => {

314

            let mut lts = timing.measure("read_symbolic_lts", || read_symbolic_lts(&storage, &mut file))?;

315

            explore_impl(&storage, cli, args, &mut lts, timing)?;

316

317

318

319

    Ok(())

320

321

322

fn explore_impl<L: SymbolicLTS>(

323

    storage: &oxidd::ldd::LDDManagerRef,

324

    cli: &Cli,

325

    args: &ExploreArgs,

326

    lts: &mut L,

327

    timing: &Timing,

328

) -> Result<(), MercError> {

329

    if args.use_bdd {

330

        let manager_ref = init_bdd_manager(cli);

331

332

        let lts_bdd = timing.measure("convert_bdd", || {

333

            SymbolicLtsBdd::from_symbolic_lts(storage, &manager_ref, lts)

334

        })?;

335

336

        println!(

337

            "LTS has {} states",

338

            timing.measure("explore_bdd", || -> Result<_, MercError> {

339

                let reachable_states_bdd = reachability_bdd(&manager_ref, &lts_bdd, args.visualize)?;

340

341

                let num_reachable_states_bdd = reachable_states_bdd.sat_count::<u64, FxBuildHasher>(

342

                    lts_bdd.state_variables().len() as u32,

343

                    &mut SatCountCache::default(),

344

                ) as usize;

345

                Ok(num_reachable_states_bdd)

346

})?

347

);

348

    } else {

349

        let options = ReachabilityOptions {

350

            strategy: args.strategy,

351

            detect_deadlocks: args.detect_deadlocks,

352

};

353

354

        println!(

355

            "LTS has {} states",

356

            timing.measure("explore", || -> Result<_, MercError> {

357

                let result = reachability_with_options(storage, lts, &options, timing)?;

358

359

                Ok(result.states.len())

360

})?

361

);

362

363

    Ok(())

364

365

366

/// Computes a variable reordering for the output of lpsreach.

367

fn handle_reorder(args: &ReorderArgs, _timing: &Timing) -> Result<(), MercError> {

368

    // Find kahypar

369

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

370

        which_in("KaHyPar", Some(path), std::env::current_dir()?).map_err(|_e| "Cannot find KaHyPar")?

371

    } else {

372

        which::which("KaHyPar").map_err(|_e| "Cannot find KaHyPar in PATH")?

373

};

374

375

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

376

        if !path.is_file() {

377

            return Err(format!(

378

                "The specified kahypar.ini path '{}' does not exist or is not a file.",

379

                path.display()

380

381

            .into());

382

383

        path.clone()

384

    } else {

385

        // Get path relative to the current executable, and obtain a path to the `kahypar.ini` configuration file.

386

        let mut default_kahypar_ini_path = std::env::current_exe()?;

387

        default_kahypar_ini_path.pop(); // remove the executable filename

388

        default_kahypar_ini_path.push("kahypar.ini");

389

390

        if !default_kahypar_ini_path.is_file() {

391

            return Err(format!(

392

                "Could not find '{}'. The 'kahypar.ini' file must be present next to the executable, or passed via --kahypar-ini-path.",

393

                default_kahypar_ini_path.display()

394

395

            .into());

396

397

        default_kahypar_ini_path

398

};

399

400

    if args.filename.extension() == Some(OsStr::new("lps")) {

401

        // Find lpsreach

402

        let lpsreach_path = if let Some(path) = &args.mcrl2_path {

403

            which_in("lpsreach", Some(path), std::env::current_dir()?).map_err(|_e| "Cannot find lpsreach")?

404

        } else {

405

            which::which("lpsreach").map_err(|_e| "Cannot find lpsreach in PATH")?

406

};

407

408

        // Run lpsreach with the --info flag to get dependency information

409

        let proc = duct::cmd!(lpsreach_path, "--info", &args.filename)

410

            .stdout_capture()

411

            .run()

412

            .map_err(|e| e.to_string())?;

413

414

        let graph = parse_compacted_dependency_graph(str::from_utf8(&proc.stdout)?);

415

416

        let order = reorder(&kahypar_path, &kahypar_ini_path, &graph)?;

417

        println!("Computed variable order: {}", order.iter().format(" "));

418

    } else if args.filename.extension() == Some(OsStr::new("pbes")) {

419

        // Find pbessolvesymbolic

420

        let pbessolvesymbolic = if let Some(path) = &args.mcrl2_path {

421

            which_in("pbessolvesymbolic", Some(path), std::env::current_dir()?)

422

                .map_err(|_e| "Cannot find pbessolvesymbolic")?

423

        } else {

424

            which::which("pbessolvesymbolic").map_err(|_e| "Cannot find pbessolvesymbolic in PATH")?

425

};

426

427

        // Run pbessolvesymbolic with the --info flag to get dependency information

428

        let proc = duct::cmd!(pbessolvesymbolic, "--info", &args.filename)

429

            .stdout_capture()

430

            .run()

431

            .map_err(|e| e.to_string())?;

432

433

        let graph = parse_compacted_dependency_graph(str::from_utf8(&proc.stdout)?);

434

        let order = reorder(&kahypar_path, &kahypar_ini_path, &graph)?;

435

436

        // Ensure that the first variable is 0 by removing it from order and printing it explicitly

437

        println!(

438

            "Computed variable order: 0 {}",

439

            order.iter().filter(|&x| *x != 0).format(" ")

440

);

441

    } else {

442

        return Err("Input file must be either a .lps or .pbes file".into());

443

444

445

    Ok(())

446

447

448

/// Converts a symbolic LTS to an explicit LTS.

449

fn handle_convert(cli: &Cli, args: &ConvertArgs, _timing: &Timing) -> Result<(), MercError> {

450

    let storage = init_ldd_manager(cli);

451

452

    let format =

453

        guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?;

454

    if format != SymFormat::Sym {

455

        return Err("Currently only the .sym format is supported for conversion".into());

456

457

458

    let mut file = File::open(&args.filename)?;

459

    let lts = read_symbolic_lts(&storage, &mut file)?;

460

461

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

462

        let output_format =

463

            guess_lts_format_from_extension(output, args.output_format).ok_or("Cannot determine output LTS format")?;

464

465

        match output_format {

466

            LtsFormat::Lts => {

467

                unimplemented!("Writing LTS format is not yet implemented");

468

469

            LtsFormat::Aut => {

470

                let mut output = File::create(output)?;

471

                let mut stream = AutStream::new(&mut output)?;

472

                convert_symbolic_lts(&storage, &mut stream, &lts)?;

473

474

            LtsFormat::AutMcrl2 => {

475

                let mut output = File::create(output)?;

476

                let mut stream = AutStream::new_mcrl2(&mut output)?;

477

                convert_symbolic_lts(&storage, &mut stream, &lts)?;

478

479

            LtsFormat::Bcg => {

480

                let explicit_lts =

481

                    convert_symbolic_lts(&storage, &mut LtsBuilderMem::new(Vec::new(), Vec::new()), &lts)?;

482

                write_bcg(&explicit_lts, output)?;

483

484

485

486

487

    Ok(())

488

489

490

/// Applies reductions to a symbolic LTS.

491

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

492

    let format =

493

        guess_format_from_extension(&args.filename, args.format).ok_or("Cannot determine input symbolic LTS format")?;

494

    if format != SymFormat::Sym {

495

        return Err("Currently only the .sym format is supported for reduction".into());

496

497

498

    let storage = init_ldd_manager(cli);

499

    let manager_ref = init_bdd_manager(cli);

500

501

    let mut file = File::open(&args.filename)?;

502

    let lts = read_symbolic_lts(&storage, &mut file)?;

503

504

    let lts_bdd = timing.measure("convert_bdd", || {

505

        SymbolicLtsBdd::from_symbolic_lts(&storage, &manager_ref, &lts)

506

    })?;

507

508

    let quotient_lts = timing.measure("reduction", || -> Result<Option<SymbolicLtsBdd>, MercError> {

509

        match args.equivalence {

510

            Equivalence::StrongBisimSigref => {

511

                let (partition, block_vars, _num_of_blocks) = sigref_symbolic(

512

                    &manager_ref,

513

                    &lts_bdd,

514

                    timing,

515

                    args.split_signature,

516

                    args.extend_relation,

517

                    args.merge_transitions,

518

                    args.visualize,

519

)?;

520

521

                let quotient = timing.measure("quotient", || {

522

                    quotient_symbolic(&manager_ref, &lts_bdd, &partition, &block_vars)

523

                })?;

524

                Ok(Some(quotient))

525

526

            Equivalence::StrongBisim => {

527

                let _ = refine_bisimulation(&manager_ref, &lts_bdd)?;

528

                Ok(None)

529

530

531

    })?;

532

533

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

534

        let quotient_lts =

535

            quotient_lts.ok_or("Writing the quotient is not yet supported for the selected equivalence")?;

536

537

        let output_format =

538

            guess_lts_format_from_extension(output, args.output_format).ok_or("Cannot determine output LTS format")?;

539

540

        match output_format {

541

            LtsFormat::Lts => {

542

                unimplemented!("Writing LTS format is not yet implemented");

543

544

            LtsFormat::Aut => {

545

                let mut output = File::create(output)?;

546

                let mut stream = AutStream::new(&mut output)?;

547

                convert_symbolic_lts_bdd(&manager_ref, &mut stream, &quotient_lts)?;

548

549

            LtsFormat::AutMcrl2 => {

550

                let mut output = File::create(output)?;

551

                let mut stream = AutStream::new_mcrl2(&mut output)?;

552

                convert_symbolic_lts_bdd(&manager_ref, &mut stream, &quotient_lts)?;

553

554

            LtsFormat::Bcg => {

555

                let explicit_lts = convert_symbolic_lts_bdd(

556

                    &manager_ref,

557

                    &mut LtsBuilderMem::new(Vec::new(), Vec::new()),

558

                    &quotient_lts,

559

)?;

560

                write_bcg(&explicit_lts, output)?;

561

562

563

564

565

    Ok(())

566