Grcov report - main.rs

1

use std::fs::File;

2

use std::io::stdout;

3

use std::path::Path;

4

use std::process::ExitCode;

5

6

use clap::Parser;

7

use clap::Subcommand;

8

use log::info;

9

10

use merc_io::LargeFormatter;

11

use merc_lts::LTS;

12

use merc_lts::LtsFormat;

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_preorder::RefinementType;

19

use merc_preorder::refines;

20

use merc_reduction::Equivalence;

21

use merc_reduction::reduce_lts;

22

use merc_tools::Version;

23

use merc_tools::VersionFlag;

24

use merc_tools::verbosity::VerbosityFlag;

25

use merc_unsafety::print_allocator_metrics;

26

use merc_utilities::MercError;

27

use merc_utilities::Timing;

28

29

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

30

#[command(

31

    about = "A command line tool for labelled transition systems",

32

    arg_required_else_help = true

33

)]

34

struct Cli {

35

    #[command(flatten)]

36

    version: VersionFlag,

37

38

    #[command(flatten)]

39

    verbosity: VerbosityFlag,

40

41

    #[command(subcommand)]

42

    commands: Option<Commands>,

43

44

    #[arg(long, global = true)]

45

    timings: bool,

46

47

48

/// Defines the subcommands for this tool.

49

#[derive(Debug, Subcommand)]

50

enum Commands {

51

    Info(InfoArgs),

52

    Reduce(ReduceArgs),

53

    Compare(CompareArgs),

54

    Refines(RefinesArgs),

55

56

57

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

58

#[command(about = "Prints information related to the given LTS")]

59

struct InfoArgs {

60

    filename: String,

61

    filetype: Option<LtsFormat>,

62

63

64

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

65

#[command(about = "Reduces the given LTS modulo an equivalent relation")]

66

struct ReduceArgs {

67

    equivalence: Equivalence,

68

69

    /// Specify the input LTS.

70

    filename: String,

71

72

    #[arg(long, help = "Explicitly specify the LTS file format")]

73

    filetype: Option<LtsFormat>,

74

75

    output: Option<String>,

76

77

    #[arg(

78

        short,

79

        long,

80

        help = "List of actions that should be considered tau actions",

81

        value_delimiter = ','

82

)]

83

    tau: Option<Vec<String>>,

84

85

86

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

87

#[command(about = "Reduces the given LTS modulo an equivalent relation")]

88

struct CompareArgs {

89

    equivalence: Equivalence,

90

91

    /// Specify the input LTS.

92

    left_filename: String,

93

94

    /// Specify the input LTS.

95

    right_filename: String,

96

97

    #[arg(long, help = "Explicitly specify the LTS file format")]

98

    filetype: Option<LtsFormat>,

99

100

    #[arg(

101

        short,

102

        long,

103

        help = "List of actions that should be considered tau actions",

104

        value_delimiter = ','

105

)]

106

    tau: Option<Vec<String>>,

107

108

109

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

110

#[command(about = "Checks whether the given implementation LTS refines the given specification LTS modulo various preorders.")]

111

struct RefinesArgs {

112

    /// Selects the preorder to check for refinement.

113

    refinement: RefinementType,

114

115

    /// Specify the implementation LTS.

116

    implementation_filename: String,

117

118

    /// Specify the specification LTS.

119

    specification_filename: String,

120

121

122

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

123

    let cli = Cli::parse();

124

125

    env_logger::Builder::new()

126

        .filter_level(cli.verbosity.log_level_filter())

127

        .parse_default_env()

128

        .init();

129

130

    if cli.version.into() {

131

        eprintln!("{}", Version);

132

        return Ok(ExitCode::SUCCESS);

133

134

135

    let mut timing = Timing::new();

136

137

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

138

        match command {

139

            Commands::Info(args) => {

140

                handle_info(args, &mut timing)?;

141

142

            Commands::Reduce(args) => {

143

                handle_reduce(args, &mut timing)?;

144

145

            Commands::Compare(args) => {

146

                handle_compare(args, &mut timing)?;

147

148

            Commands::Refines(args) => {

149

                handle_refinement(args, &mut timing)?;

150

151

152

153

154

    if cli.timings {

155

        timing.print();

156

157

158

    print_allocator_metrics();

159

    Ok(ExitCode::SUCCESS)

160

161

162

/// Display information about the given LTS.

163

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

164

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

165

166

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

167

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

168

    println!(

169

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

170

        LargeFormatter(lts.num_of_states()),

171

        LargeFormatter(lts.num_of_transitions())

172

);

173

174

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

175

        println!("Labels:");

176

        for label in lts.labels() {

177

            println!("\t {}", label);

178

179

});

180

181

    Ok(())

182

183

184

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

185

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

186

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

187

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

188

189

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

190

    info!(

191

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

192

        LargeFormatter(lts.num_of_states()),

193

        LargeFormatter(lts.num_of_transitions())

194

);

195

196

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

197

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

198

199

        info!(

200

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

201

            LargeFormatter(reduced_lts.num_of_states()),

202

            LargeFormatter(reduced_lts.num_of_transitions())

203

);

204

205

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

206

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

207

            write_aut(&mut writer, &reduced_lts)?;

208

        } else {

209

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

210

211

212

        Ok(())

213

    })?;

214

215

    Ok(())

216

217

218

/// Handles the refinement checking between two LTSs.

219

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

220

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

221

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

222

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

223

224

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

225

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

226

227

    info!(

228

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

229

        LargeFormatter(impl_lts.num_of_states()),

230

        LargeFormatter(impl_lts.num_of_transitions())

231

);

232

    info!(

233

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

234

        LargeFormatter(spec_lts.num_of_states()),

235

        LargeFormatter(spec_lts.num_of_transitions())

236

);

237

238

    let refines = apply_lts_pair!(impl_lts, spec_lts, timing, |left, right, timing| {

239

        refines(left, right, args.refinement, timing)

240

});

241

242

    if refines {

243

        println!("true");

244

    } else {

245

        println!("false");

246

247

248

    Ok(())

249

250

251

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

252

    let left_path = Path::new(&args.left_filename);

253

    let right_path = Path::new(&args.right_filename);

254

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

255

256

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

257

    let left_lts = read_explicit_lts(left_path, format, args.tau.clone().unwrap_or_default(), timing)?;

258

    let right_lts = read_explicit_lts(right_path, format, args.tau.clone().unwrap_or_default(), timing)?;

259

260

    info!(

261

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

262

        LargeFormatter(left_lts.num_of_states()),

263

        LargeFormatter(left_lts.num_of_transitions())

264

);

265

    info!(

266

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

267

        LargeFormatter(right_lts.num_of_states()),

268

        LargeFormatter(right_lts.num_of_transitions())

269

);

270

271

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

272

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

273

});

274

275

    if equivalent {

276

        println!("true");

277

    } else {

278

        println!("false");

279

280

281

    Ok(())

282