Grcov report - labelled_transition

1

#![forbid(unsafe_code)]

2

3

use std::collections::HashMap;

4

use std::fmt;

5

6

use merc_collections::ByteCompressedVec;

7

use merc_collections::CompressedEntry;

8

use merc_collections::CompressedVecMetrics;

9

use merc_collections::bytevec;

10

use merc_io::LargeFormatter;

11

use merc_utilities::TagIndex;

12

13

use crate::LTS;

14

use crate::LabelIndex;

15

use crate::LabelTag;

16

use crate::StateIndex;

17

use crate::Transition;

18

use crate::TransitionLabel;

19

20

/// Represents a labelled transition system consisting of states with directed

21

/// labelled transitions between them.

22

///

23

/// # Details

24

///

25

/// Uses byte compressed vectors to store the states and their outgoing

26

/// transitions efficiently in memory.

27

#[derive(PartialEq, Eq, Clone)]

28

pub struct LabelledTransitionSystem<Label> {

29

    /// Encodes the states and their outgoing transitions.

30

    states: ByteCompressedVec<usize>,

31

    transition_labels: ByteCompressedVec<LabelIndex>,

32

    transition_to: ByteCompressedVec<StateIndex>,

33

34

    /// Keeps track of the labels for every index, and which of them are hidden.

35

    labels: Vec<Label>,

36

37

    /// The index of the initial state.

38

    initial_state: StateIndex,

39

40

41

impl<Label: TransitionLabel> LabelledTransitionSystem<Label> {

42

    /// Creates a new labelled transition system with the given transitions,

43

    /// labels, and hidden labels.

44

///

45

    /// The initial state is the state with the given index. `num_of_states` is

46

    /// the number of states in the LTS, if known. If it is not known, pass

47

    /// `None`. However, in that case the number of states will be determined

48

    /// based on the maximum state index in the transitions. And all states that

49

    /// do not have any outgoing transitions will simply be created as deadlock

50

    /// states.

51

18348

    pub fn new<I, F>(

52

18348

        initial_state: StateIndex,

53

18348

        num_of_states: Option<usize>,

54

18348

        mut transition_iter: F,

55

18348

        labels: Vec<Label>,

56

18348

    ) -> LabelledTransitionSystem<Label>

57

18348

    where

58

18348

        F: FnMut() -> I,

59

18348

        I: Iterator<Item = (StateIndex, LabelIndex, StateIndex)>,

60

61

18348

        let mut states = ByteCompressedVec::new();

62

18348

        if let Some(num_of_states) = num_of_states {

63

18347

            states.resize_with(num_of_states, Default::default);

64

18347

65

66

        // Count the number of transitions for every state

67

18348

        let mut num_of_transitions = 0;

68

3070430

        for (from, _, to) in transition_iter() {

69

            // Ensure that the states vector is large enough.

70

3070430

            if states.len() <= *from.max(to) {

71

2

                states.resize_with(*from.max(to) + 1, || 0);

72

3070428

73

74

3070430

            states.update(*from, |start| *start += 1);

75

3070430

            num_of_transitions += 1;

76

77

3070430

            if let Some(num_of_states) = num_of_states {

78

3070425

                debug_assert!(

79

3070425

                    *from < num_of_states && *to < num_of_states,

80

                    "State index out of bounds: from {:?}, to {:?}, num_of_states {}",

81

                    from,

82

to,

83

                    num_of_states

84

);

85

5

86

87

88

18348

        if initial_state.value() >= states.len() {

89

            // Ensure that the initial state is a valid state (and all states before it exist).

90

            states.resize_with(initial_state.value() + 1, Default::default);

91

18348

92

93

        // Track the number of transitions before every state.

94

2457031

        states.fold(0, |count, start| {

95

2457031

            let result = count + *start;

96

2457031

            *start = count;

97

2457031

            result

98

2457031

});

99

100

        // Place the transitions, and increment the end for every state.

101

18348

        let mut transition_labels = bytevec![LabelIndex::new(labels.len()); num_of_transitions];

102

18348

        let mut transition_to = bytevec![StateIndex::new(states.len()); num_of_transitions];

103

3070430

        for (from, label, to) in transition_iter() {

104

3070430

            states.update(*from, |start| {

105

3070430

                transition_labels.set(*start, label);

106

3070430

                transition_to.set(*start, to);

107

3070430

                *start += 1

108

3070430

});

109

110

111

        // Reset the offset.

112

2457031

        states.fold(0, |previous, start| {

113

2457031

            let result = *start;

114

2457031

            *start = previous;

115

2457031

            result

116

2457031

});

117

118

        // Add the sentinel state.

119

18348

        states.push(transition_labels.len());

120

121

18348

        LabelledTransitionSystem::from_raw_parts(

122

18348

            initial_state,

123

18348

            states,

124

18348

            transition_labels,

125

18348

            transition_to,

126

18348

            labels,

127

128

18348

129

130

    /// Constructs a LTS by a successor function for every state.

131

    pub fn with_successors<F, I>(

132

        initial_state: StateIndex,

133

        num_of_states: usize,

134

        labels: Vec<Label>,

135

        mut successors: F,

136

    ) -> Self

137

    where

138

        F: FnMut(StateIndex) -> I,

139

        I: Iterator<Item = (LabelIndex, StateIndex)>,

140

141

        assert!(

142

            *labels

143

                .first()

144

                .expect("At least one label (the hidden label) must be provided")

145

                == Label::tau_label(),

146

            "The first label must be the hidden label."

147

);

148

149

        let mut states = ByteCompressedVec::new();

150

        states.resize_with(num_of_states, Default::default);

151

152

        let mut transition_labels = ByteCompressedVec::with_capacity(num_of_states, 16usize.bytes_required());

153

        let mut transition_to = ByteCompressedVec::with_capacity(num_of_states, num_of_states.bytes_required());

154

155

        for state_index in 0..num_of_states {

156

            let state_index = StateIndex::new(state_index);

157

            states.update(*state_index, |entry| {

158

                *entry = transition_labels.len();

159

});

160

161

            for (label, to) in successors(state_index) {

162

                transition_labels.push(label);

163

                transition_to.push(to);

164

165

166

167

        // Add the sentinel state.

168

        states.push(transition_labels.len());

169

170

        Self::from_raw_parts(

171

            initial_state,

172

            states,

173

            transition_labels,

174

            transition_to,

175

            labels,

176

177

178

179

    /// Consumes the current LTS and merges it with another one, returning the merged LTS.

180

///

181

    /// # Details

182

///

183

    /// Internally this works by offsetting the state indices of the other LTS by the number of states

184

    /// in the current LTS, and combining the action labels. The offset is returned such that

185

    /// can find the states of the other LTS in the merged LTS as the initial state of the other LTS.

186

2003

    fn merge_disjoint_impl<L: LTS<Label = Label>>(mut self, other: &L) -> (Self, StateIndex) {

187

        // Determine the combination of action labels

188

2003

        let mut all_labels = self.labels().to_vec();

189

15212

        for label in other.labels() {

190

15212

            if !all_labels.contains(label) {

191

3

                all_labels.push(label.clone());

192

15209

193

194

195

2003

        let label_indices: HashMap<Label, TagIndex<usize, LabelTag>> = HashMap::from_iter(

196

2003

            all_labels

197

2003

                .iter()

198

2003

                .enumerate()

199

15212

                .map(|(i, label)| (label.clone(), LabelIndex::new(i))),

200

);

201

202

2003

        let total_number_of_states = self.num_of_states() + other.num_of_states();

203

204

        // Reserve space for the right LTS.

205

2003

        self.states

206

2003

            .reserve(other.num_of_states(), total_number_of_states.bytes_required());

207

2003

        self.transition_labels

208

2003

            .reserve(other.num_of_transitions(), all_labels.len().bytes_required());

209

2003

        self.transition_to

210

2003

            .reserve(other.num_of_transitions(), total_number_of_states.bytes_required());

211

212

2003

        let offset = self.num_of_states();

213

214

        // Remove the sentinel state temporarily. This breaks the state invariant, but we will add it back later.

215

2003

        self.states.pop();

216

217

        // Add vertices for the other LTS that are offset by the number of states in self

218

807245

        for state_index in other.iter_states() {

219

            // Add a new state for every state in the other LTS

220

807245

            self.states.push(self.num_of_transitions());

221

815018

            for transition in other.outgoing_transitions(state_index) {

222

815018

                // Add the transitions of the other LTS, offsetting the state indices

223

815018

                self.transition_to.push(StateIndex::new(transition.to.value() + offset));

224

815018

225

815018

                // Map the label to the new index in all_labels

226

815018

                let label_name = &other.labels()[transition.label.value()];

227

815018

                self.transition_labels

228

815018

                    .push(*label_indices.get(label_name).expect("Label should exist in all_labels"));

229

815018

230

231

232

        // Add back the sentinel state

233

2003

        self.states.push(self.num_of_transitions());

234

2003

        debug_assert_eq!(self.num_of_states(), total_number_of_states);

235

236

2003

237

2003

            Self::from_raw_parts(

238

2003

                self.initial_state,

239

2003

                self.states,

240

2003

                self.transition_labels,

241

2003

                self.transition_to,

242

2003

                all_labels

243

2003

),

244

2003

            StateIndex::new(offset + other.initial_state_index().value()),

245

2003

246

2003

247

248

    /// Creates a labelled transition system from another one, given the permutation of state indices.

249

///

250

    /// The permutation maps old state indices to new state indices, i.e.,

251

    /// `permutation(old) = new`. The transition arrays are rebuilt so that

252

    /// transitions are contiguous per new state index, and all transition

253

    /// targets are updated to reference the new state indices.

254

2700

    pub fn new_from_permutation<P>(lts: Self, permutation: P) -> Self

255

2700

    where

256

2700

        P: Fn(StateIndex) -> StateIndex + Copy,

257

258

        // Build the inverse permutation: inverse[new_index] = old_index

259

2700

        let mut inverse = vec![StateIndex::new(0); lts.num_of_states()];

260

431487

        for state_index in lts.iter_states() {

261

431487

            inverse[*permutation(state_index)] = state_index;

262

431487

263

264

        // Rebuild transition arrays in the order of the new state indices.

265

2700

        let mut states = ByteCompressedVec::new();

266

2700

        let mut transition_labels = ByteCompressedVec::new();

267

2700

        let mut transition_to = ByteCompressedVec::new();

268

269

431487

        for old_index in &inverse {

270

431487

            states.push(transition_labels.len());

271

272

431487

            let start = lts.states.index(**old_index);

273

431487

            let end = lts.states.index(**old_index + 1);

274

275

463275

            for i in start..end {

276

463275

                transition_labels.push(lts.transition_labels.index(i));

277

463275

                transition_to.push(permutation(lts.transition_to.index(i)));

278

463275

279

280

281

        // Add the sentinel state.

282

2700

        states.push(transition_labels.len());

283

284

2700

        Self::from_raw_parts(

285

2700

            permutation(lts.initial_state),

286

2700

            states,

287

2700

            transition_labels,

288

2700

            transition_to,

289

2700

            lts.labels,

290

291

2700

292

293

    /// Consumes the LTS and relabels its transition labels according to the given mapping.

294

2

    pub fn relabel<L, F>(self, labelling: F) -> LabelledTransitionSystem<L>

295

2

    where

296

2

        F: Fn(Label) -> L,

297

2

        L: TransitionLabel,

298

299

2

        let new_labels: Vec<L> = self.labels.into_iter().map(labelling).collect();

300

301

2

        LabelledTransitionSystem::from_raw_parts(

302

2

            self.initial_state,

303

2

            self.states,

304

2

            self.transition_labels,

305

2

            self.transition_to,

306

2

            new_labels

307

308

2

309

310

    /// Constructs a [LabelledTransitionSystem] directly from its raw internal arrays.

311

///

312

    /// The `states` array must contain one entry per state holding the start offset of that

313

    /// state's transitions in the transition arrays, plus a sentinel entry at the end equal

314

    /// to the total number of transitions. `transition_labels` and `transition_to` must have

315

    /// equal length and all indices they contain must be in bounds.

316

///

317

    /// # Panics

318

///

319

    /// Panics (in debug mode) if the invariants of the internal representation are violated.

320

82207

    pub fn from_raw_parts(

321

82207

        initial_state: StateIndex,

322

82207

        states: ByteCompressedVec<usize>,

323

82207

        transition_labels: ByteCompressedVec<LabelIndex>,

324

82207

        transition_to: ByteCompressedVec<StateIndex>,

325

82207

        labels: Vec<Label>,

326

82207

    ) -> Self {

327

82207

        let lts = LabelledTransitionSystem {

328

82207

            initial_state,

329

82207

            states,

330

82207

            transition_labels,

331

82207

            transition_to,

332

82207

            labels,

333

82207

};

334

82207

        lts.assert_valid();

335

82207

lts

336

82207

337

338

    /// Checks that the internal representation satisfies all structural invariants.

339

82207

    pub fn assert_valid(&self) {

340

82207

        let num_states = self.num_of_states();

341

82207

        let num_transitions = self.num_of_transitions();

342

343

82207

        debug_assert!(

344

82207

            !self.states.is_empty(),

345

            "states array must have at least one entry (the sentinel)"

346

);

347

348

82207

        debug_assert!(

349

82207

            self.initial_state.value() < num_states,

350

            "initial_state {:?} is out of bounds (num_states: {})",

351

            self.initial_state,

352

            num_states

353

);

354

355

82207

        debug_assert_eq!(

356

82207

            self.states.index(num_states),

357

            num_transitions,

358

            "sentinel value must equal the number of transitions"

359

);

360

361

82207

        debug_assert_eq!(

362

82207

            self.transition_labels.len(),

363

82207

            self.transition_to.len(),

364

            "transition_labels and transition_to must have equal length"

365

);

366

367

17746101

        for i in 0..num_states {

368

17746101

            debug_assert!(

369

17746101

                self.states.index(i) <= self.states.index(i + 1),

370

                "state {i} has offset {} which is greater than successor offset {}",

371

                self.states.index(i),

372

                self.states.index(i + 1)

373

);

374

375

376

18878847

        for i in 0..num_transitions {

377

18878847

            let label = self.transition_labels.index(i);

378

18878847

            debug_assert!(

379

18878847

                label.value() < self.labels.len(),

380

                "transition {i} references label index {} which is out of bounds (num_labels: {})",

381

                label.value(),

382

                self.labels.len()

383

);

384

385

18878847

            let to = self.transition_to.index(i);

386

18878847

            debug_assert!(

387

18878847

                to.value() < num_states,

388

                "transition {i} references target state {} which is out of bounds (num_states: {})",

389

                to.value(),

390

                num_states

391

);

392

393

82207

394

395

    /// Returns metrics about the LTS.

396

    pub fn metrics(&self) -> LtsMetrics {

397

        LtsMetrics {

398

            num_of_states: self.num_of_states(),

399

            num_of_labels: self.num_of_labels(),

400

            num_of_transitions: self.num_of_transitions(),

401

            state_metrics: self.states.metrics(),

402

            transition_labels_metrics: self.transition_labels.metrics(),

403

            transition_to_metrics: self.transition_to.metrics(),

404

405

406

407

408

impl<L: TransitionLabel> LTS for LabelledTransitionSystem<L> {

409

    type Label = L;

410

411

30754

    fn initial_state_index(&self) -> StateIndex {

412

30754

        self.initial_state

413

30754

414

415

20135244

    fn outgoing_transitions(&self, state_index: StateIndex) -> impl Iterator<Item = Transition> + '_ {

416

20135244

        let start = self.states.index(*state_index);

417

20135244

        let end = self.states.index(*state_index + 1);

418

419

20135244

        (start..end).map(move |i| Transition {

420

43597111

            label: self.transition_labels.index(i),

421

43597111

            to: self.transition_to.index(i),

422

43597111

})

423

20135244

424

425

173387

    fn iter_states(&self) -> impl Iterator<Item = StateIndex> + '_ {

426

173387

        (0..self.num_of_states()).map(StateIndex::new)

427

173387

428

429

3200252

    fn num_of_states(&self) -> usize {

430

        // Remove the sentinel state.

431

3200252

        self.states.len() - 1

432

3200252

433

434

1412664

    fn num_of_labels(&self) -> usize {

435

1412664

        self.labels.len()

436

1412664

437

438

3357427

    fn num_of_transitions(&self) -> usize {

439

3357427

        self.transition_labels.len()

440

3357427

441

442

2777912

    fn labels(&self) -> &[Self::Label] {

443

2777912

        &self.labels[0..]

444

2777912

445

446

34170093

    fn is_hidden_label(&self, label_index: LabelIndex) -> bool {

447

34170093

        label_index.value() == 0

448

34170093

449

450

2003

    fn merge_disjoint<T: LTS<Label = Self::Label>>(self, other: &T) -> (Self, StateIndex) {

451

2003

        self.merge_disjoint_impl(other)

452

2003

453

454

455

/// Metrics for a labelled transition system.

456

#[derive(Debug, Clone)]

457

pub struct LtsMetrics {

458

    /// The number of states in the LTS.

459

    pub num_of_states: usize,

460

    pub state_metrics: CompressedVecMetrics,

461

    /// The number of transitions in the LTS.

462

    pub num_of_transitions: usize,

463

    pub transition_labels_metrics: CompressedVecMetrics,

464

    pub transition_to_metrics: CompressedVecMetrics,

465

    /// The number of action labels in the LTS.

466

    pub num_of_labels: usize,

467

468

469

impl fmt::Display for LtsMetrics {

470

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

471

        // Print some information about the LTS.

472

        writeln!(f, "Number of states: {}", LargeFormatter(self.num_of_states))?;

473

        writeln!(f, "Number of action labels: {}", LargeFormatter(self.num_of_labels))?;

474

        writeln!(

475

f,

476

            "Number of transitions: {}\n",

477

            LargeFormatter(self.num_of_transitions)

478

)?;

479

        writeln!(f, "Memory usage:")?;

480

        writeln!(f, "States {}", self.state_metrics)?;

481

        writeln!(f, "Transition labels {}", self.transition_labels_metrics)?;

482

        write!(f, "Transition to {}", self.transition_to_metrics)

483

484

485

486

/// Checks that two LTSs are equivalent, for testing purposes.

487

#[cfg(test)]

488

300

pub fn check_equivalent<L: LTS>(lts: &L, lts_read: &L) {

489

300

    println!("LTS labels: {:?}", lts.labels());

490

300

    println!("Read LTS labels: {:?}", lts_read.labels());

491

492

    // If labels are not used, the number of labels may be less. So find a remapping of old labels to new labels.

493

300

    let mapping = lts

494

300

        .labels()

495

300

        .iter()

496

300

        .enumerate()

497

1800

        .map(|(_i, label)| lts_read.labels().iter().position(|l| l == label))

498

300

        .collect::<Vec<_>>();

499

500

    // Print the mapping

501

900

    for (i, m) in mapping.iter().enumerate() {

502

900

        println!("Label {} mapped to {:?}", i, m);

503

900

504

505

300

    assert_eq!(lts.num_of_states(), lts_read.num_of_states());

506

300

    assert_eq!(lts.num_of_transitions(), lts_read.num_of_transitions());

507

508

    // Check that all the outgoing transitions are the same.

509

30000

    for state_index in lts.iter_states() {

510

30000

        let transitions: Vec<_> = lts.outgoing_transitions(state_index).collect();

511

30000

        let transitions_read: Vec<_> = lts_read.outgoing_transitions(state_index).collect();

512

513

        // Check that transitions are the same, modulo label remapping.

514

278223

        transitions.iter().for_each(|t| {

515

278223

            let mapped_label = mapping[t.label.value()].expect(&format!("Label {} should be found", t.label));

516

278223

            assert!(

517

278223

                transitions_read

518

278223

                    .iter()

519

1899639

                    .any(|tr| tr.to == t.to && tr.label.value() == mapped_label)

520

);

521

278223

});

522

523

300

524

525

#[cfg(test)]

526

mod tests {

527

    use merc_io::DumpFiles;

528

    use merc_utilities::random_test;

529

530

    use crate::LTS;

531

    use crate::num_reachable_states;

532

    use crate::random_lts;

533

    use crate::write_aut;

534

535

    #[test]

536

    #[cfg_attr(miri, ignore)] // Miri is too slow

537

1

    fn test_random_labelled_transition_system_merge_disjoint() {

538

100

        random_test(100, |rng| {

539

100

            let mut files = DumpFiles::new("test_random_merge_disjoint");

540

541

100

            let left = random_lts(rng, 10, 20, 2);

542

100

            files.dump("left.aut", |w| write_aut(w, &left)).unwrap();

543

544

100

            let right = random_lts(rng, 10, 20, 2);

545

100

            files.dump("right.aut", |w| write_aut(w, &right)).unwrap();

546

547

100

            let (merged, right_initial) = left.clone().merge_disjoint(&right);

548

100

            files.dump("merged.aut", |w| write_aut(w, &merged)).unwrap();

549

550

100

            assert_eq!(

551

100

                num_reachable_states(&left, left.initial_state_index()),

552

100

                num_reachable_states(&merged, merged.initial_state_index()),

553

                "The left LTS should be fully reachable in the merged LTS"

554

);

555

100

            assert_eq!(

556

100

                num_reachable_states(&right, right.initial_state_index()),

557

100

                num_reachable_states(&merged, right_initial),

558

                "The right LTS should be fully reachable in the merged LTS"

559

);

560

100

});

561

1

562