Grcov report - main.rs

1

use std::fs::File;

2

use std::io::stdout;

3

use std::io::Write;

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

14

use merc_lts::apply_lts_pair;

15

use merc_lts::guess_lts_format_from_extension;

16

use merc_lts::read_explicit_lts;

17

use merc_lts::write_aut;

18

use merc_lts::write_bcg;

19

use merc_lts::GenericLts;

20

use merc_lts::LtsFormat;

21

use merc_lts::LTS;

22

use merc_reduction::reduce_lts;

23

use merc_reduction::Equivalence;

24

use merc_refinement::generate_formula;

25

use merc_refinement::refines;

26

use merc_refinement::RefinementType;

27

use merc_tools::format_key_values_json;

28

use merc_tools::VerbosityFlag;

29

use merc_tools::Version;

30

use merc_tools::VersionFlag;

31

use merc_unsafety::print_allocator_metrics;

32

use merc_utilities::MercError;

33

use merc_utilities::Timing;

34

35

/// A command line tool for labelled transition systems

36

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

37

#[command(arg_required_else_help = true)]

38

struct Cli {

39

    #[command(flatten)]

40

    version: VersionFlag,

41

42

    #[command(flatten)]

43

    verbosity: VerbosityFlag,

44

45

    #[command(subcommand)]

46

    commands: Option<Commands>,

47

48

    #[arg(long, global = true)]

49

    timings: bool,

50

51

52

/// Defines the subcommands for this tool.

53

#[derive(Debug, Subcommand)]

54

enum Commands {

55

    Info(InfoArgs),

56

    Reduce(ReduceArgs),

57

    Compare(CompareArgs),

58

    Refines(RefinesArgs),

59

    Convert(ConvertArgs),

60

61

62

/// Prints information related to the given LTS"

63

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

64

#[command()]

65

struct InfoArgs {

66

    /// Specify the input LTS.

67

    filename: String,

68

69

    /// Explicitly specify the LTS file format

70

    #[arg(long)]

71

    format: Option<LtsFormat>,

72

73

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

74

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

75

    tau: Option<Vec<String>>,

76

77

78

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

79

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

80

#[command()]

81

struct ReduceArgs {

82

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

83

    equivalence: Equivalence,

84

85

    /// Specify the input LTS.

86

    filename: PathBuf,

87

88

    /// Explicitly specify the LTS file format

89

    #[arg(long)]

90

    filetype: Option<LtsFormat>,

91

92

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

93

    #[arg(long)]

94

    output: Option<PathBuf>,

95

96

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

97

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

98

    tau: Option<Vec<String>>,

99

100

    /// Disables preprocessing of the LTS before reducing.

101

    #[arg(long)]

102

    no_preprocess: bool,

103

104

105

/// Compares two LTS modulo an equivalent relation

106

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

107

#[command()]

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

/// Converts an LTS from one format to another

132

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

133

#[command()]

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

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

150

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

151

    tau: Option<Vec<String>>,

152

153

154

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

155

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

156

#[command()]

157

struct RefinesArgs {

158

    /// Selects the preorder to check for refinement.

159

    refinement: RefinementType,

160

161

    /// Specify the implementation LTS.

162

    implementation_filename: PathBuf,

163

164

    /// Specify the specification LTS.

165

    specification_filename: PathBuf,

166

167

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

168

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

169

    counter_example: Option<PathBuf>,

170

171

    /// Explicitly specify the LTS file format

172

    #[arg(long)]

173

    format: Option<LtsFormat>,

174

175

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

176

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

177

    tau: Option<Vec<String>>,

178

179

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

180

    #[arg(long)]

181

    no_preprocess: bool,

182

183

184

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

185

    let cli = Cli::parse();

186

187

    env_logger::Builder::new()

188

        .filter_level(cli.verbosity.log_level_filter())

189

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

190

        .parse_default_env()

191

        .init();

192

193

    if cli.version.into() {

194

        eprintln!("{}", Version);

195

        return Ok(ExitCode::SUCCESS);

196

197

198

    let mut timing = Timing::new();

199

200

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

201

        match command {

202

            Commands::Info(args) => {

203

                handle_info(args, &mut timing)?;

204

205

            Commands::Reduce(args) => {

206

                handle_reduce(args, &mut timing)?;

207

208

            Commands::Compare(args) => {

209

                handle_compare(args, &mut timing)?;

210

211

            Commands::Refines(args) => {

212

                handle_refinement(args, &mut timing)?;

213

214

            Commands::Convert(args) => {

215

                handle_convert(args, &mut timing)?;

216

217

218

219

220

    if cli.timings {

221

        timing.print();

222

223

224

    print_allocator_metrics();

225

    Ok(ExitCode::SUCCESS)

226

227

228

/// Display information about the given LTS.

229

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

230

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

231

232

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

233

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

234

    println!(

235

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

236

        LargeFormatter(lts.num_of_states()),

237

        LargeFormatter(lts.num_of_transitions())

238

);

239

240

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

241

        println!("Labels:");

242

        for label in lts.labels() {

243

            println!("  {}", label);

244

245

246

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

247

            acc + lts

248

                .outgoing_transitions(s)

249

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

250

                .count()

251

});

252

253

        // Count the number of silent transitions.

254

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

255

256

        // Structured output.

257

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

258

});

259

260

    Ok(())

261

262

263

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

264

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

265

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

266

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

267

268

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

269

    info!(

270

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

271

        LargeFormatter(lts.num_of_states()),

272

        LargeFormatter(lts.num_of_transitions())

273

);

274

275

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

276

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

277

278

        info!(

279

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

280

            LargeFormatter(reduced_lts.num_of_states()),

281

            LargeFormatter(reduced_lts.num_of_transitions())

282

);

283

284

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

285

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

286

            write_aut(&mut writer, &reduced_lts)?;

287

        } else {

288

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

289

290

291

        Ok(())

292

    })?;

293

294

    Ok(())

295

296

297

/// Handles the refinement checking between two LTSs.

298

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

299

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

300

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

301

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

302

303

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

304

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

305

306

    info!(

307

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

308

        LargeFormatter(impl_lts.num_of_states()),

309

        LargeFormatter(impl_lts.num_of_transitions())

310

);

311

    info!(

312

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

313

        LargeFormatter(spec_lts.num_of_states()),

314

        LargeFormatter(spec_lts.num_of_transitions())

315

);

316

317

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

318

                                                 right,

319

                                                 timing|

320

     -> Result<(), MercError> {

321

        let (result, counter_example) = refines(

322

            left,

323

            right,

324

            args.refinement,

325

            !args.no_preprocess,

326

            args.counter_example.is_some(),

327

            timing,

328

);

329

330

        if result {

331

            println!("true");

332

        } else {

333

            if let Some(counter_example) = counter_example {

334

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

335

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

336

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

337

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

338

                } else {

339

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

340

341

342

343

            println!("false");

344

345

346

        Ok(())

347

    })?;

348

349

    Ok(())

350

351

352

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

353

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

354

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

355

356

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

357

    let left_lts = read_explicit_lts(

358

        &args.left_filename,

359

        format,

360

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

361

        timing,

362

)?;

363

    let right_lts = read_explicit_lts(

364

        &args.right_filename,

365

        format,

366

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

367

        timing,

368

)?;

369

370

    info!(

371

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

372

        LargeFormatter(left_lts.num_of_states()),

373

        LargeFormatter(left_lts.num_of_transitions())

374

);

375

    info!(

376

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

377

        LargeFormatter(right_lts.num_of_states()),

378

        LargeFormatter(right_lts.num_of_transitions())

379

);

380

381

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

382

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

383

});

384

385

    if equivalent {

386

        println!("true");

387

    } else {

388

        println!("false");

389

390

391

    Ok(())

392

393

394

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

395

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

396

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

397

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

398

399

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

400

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

401

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

402

        format

403

    } else {

404

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

405

};

406

407

    match input_lts {

408

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

409

            LtsFormat::Bcg => {

410

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

411

                    write_bcg(&lts, path)?;

412

                } else {

413

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

414

415

416

            LtsFormat::Aut => {

417

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

418

419

            _ => {

420

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

421

422

},

423

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

424

            LtsFormat::Aut => {

425

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

426

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

427

                } else {

428

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

429

430

431

            LtsFormat::Bcg => {

432

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

433

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

434

                } else {

435

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

436

437

438

            LtsFormat::Lts => {

439

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

440

441

},

442

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

443

            LtsFormat::Aut => {

444

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

445

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

446

                } else {

447

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

448

449

450

            _ => {

451

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

452

453

},

454

455

456

    Ok(())

457