Grcov report - labelled_transition

1

use std::collections::HashMap;

2

use std::fmt;

3

4

use merc_collections::ByteCompressedVec;

5

use merc_collections::CompressedEntry;

6

use merc_collections::CompressedVecMetrics;

7

use merc_collections::bytevec;

8

use merc_io::LargeFormatter;

9

use merc_utilities::TagIndex;

10

11

use crate::LTS;

12

use crate::LabelIndex;

13

use crate::LabelTag;

14

use crate::StateIndex;

15

use crate::Transition;

16

use crate::TransitionLabel;

17

18

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

19

/// labelled transitions between them.

20

///

21

/// # Details

22

///

23

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

24

/// transitions efficiently in memory.

25

#[derive(PartialEq, Eq, Clone)]

26

pub struct LabelledTransitionSystem<Label> {

27

    /// Encodes the states and their outgoing transitions.

28

    states: ByteCompressedVec<usize>,

29

    transition_labels: ByteCompressedVec<LabelIndex>,

30

    transition_to: ByteCompressedVec<StateIndex>,

31

32

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

33

    labels: Vec<Label>,

34

35

    /// The index of the initial state.

36

    initial_state: StateIndex,

37

38

39

impl<Label: TransitionLabel> LabelledTransitionSystem<Label> {

40

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

41

    /// labels, and hidden labels.

42

///

43

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

44

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

45

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

46

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

47

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

48

    /// states.

49

9012

    pub fn new<I, F>(

50

9012

        initial_state: StateIndex,

51

9012

        num_of_states: Option<usize>,

52

9012

        mut transition_iter: F,

53

9012

        labels: Vec<Label>,

54

9012

    ) -> LabelledTransitionSystem<Label>

55

9012

    where

56

9012

        F: FnMut() -> I,

57

9012

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

58

59

9012

        let mut states = ByteCompressedVec::new();

60

9012

        if let Some(num_of_states) = num_of_states {

61

9011

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

62

9011

            debug_assert!(

63

9011

                initial_state.value() < num_of_states,

64

                "Initial vertex index {} out of bounds {num_of_states}",

65

                initial_state.value()

66

);

67

1

68

69

        // Count the number of transitions for every state

70

9012

        let mut num_of_transitions = 0;

71

831268

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

72

            // Ensure that the states vector is large enough.

73

831268

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

74

2

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

75

831266

76

77

831268

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

78

831268

            num_of_transitions += 1;

79

80

831268

            if let Some(num_of_states) = num_of_states {

81

831263

                debug_assert!(

82

831263

                    *from < num_of_states && *to < num_of_states,

83

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

84

                    from,

85

to,

86

                    num_of_states

87

);

88

5

89

90

91

9012

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

92

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

93

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

94

9012

95

96

        // Track the number of transitions before every state.

97

161206

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

98

161206

            let result = count + *start;

99

161206

            *start = count;

100

161206

            result

101

161206

});

102

103

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

104

9012

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

105

9012

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

106

831268

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

107

831268

            states.update(*from, |start| {

108

831268

                transition_labels.set(*start, label);

109

831268

                transition_to.set(*start, to);

110

831268

                *start += 1

111

831268

});

112

113

114

        // Reset the offset.

115

161206

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

116

161206

            let result = *start;

117

161206

            *start = previous;

118

161206

            result

119

161206

});

120

121

        // The minus one is because we added one extra state for the sentinel.

122

9012

        debug_assert!(

123

9012

            initial_state.value() < states.len(),

124

            "Initial state {:?} out of bounds (num states: {})",

125

            initial_state,

126

            states.len() - 1

127

);

128

129

        // Add the sentinel state.

130

9012

        states.push(transition_labels.len());

131

132

9012

        LabelledTransitionSystem {

133

9012

            initial_state,

134

9012

            labels,

135

9012

            states,

136

9012

            transition_labels,

137

9012

            transition_to,

138

9012

139

9012

140

141

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

142

///

143

    /// # Details

144

///

145

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

146

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

147

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

148

300

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

149

        // Determine the combination of action labels

150

300

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

151

4000

        for label in other.labels() {

152

4000

            if !all_labels.contains(label) {

153

500

                all_labels.push(label.clone());

154

3500

155

156

157

300

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

158

300

            all_labels

159

300

                .iter()

160

300

                .enumerate()

161

4000

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

162

);

163

164

300

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

165

166

        // Reserve space for the right LTS.

167

300

        self.states

168

300

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

169

300

        self.transition_labels

170

300

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

171

300

        self.transition_to

172

300

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

173

174

300

        let offset = self.num_of_states();

175

176

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

177

300

        self.states.pop();

178

179

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

180

24155

        for state_index in other.iter_states() {

181

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

182

24155

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

183

169769

            for transition in other.outgoing_transitions(state_index) {

184

169769

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

185

169769

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

186

169769

187

169769

                // Map the label to the new index in all_labels

188

169769

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

189

169769

                self.transition_labels

190

169769

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

191

169769

192

193

194

        // Add back the sentinel state

195

300

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

196

300

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

197

198

300

199

300

            Self {

200

300

                initial_state: self.initial_state,

201

300

                labels: all_labels,

202

300

                states: self.states,

203

300

                transition_labels: self.transition_labels,

204

300

                transition_to: self.transition_to,

205

300

},

206

300

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

207

300

208

300

209

210

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

211

///

212

700

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

213

700

    where

214

700

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

215

216

700

        let mut states = bytevec![0; lts.num_of_states()];

217

218

5824

        for state_index in lts.iter_states() {

219

            // Keep the transitions the same move the state indices around

220

5824

            let new_state_index = permutation(state_index);

221

5824

            let state = lts.states.index(*state_index);

222

5824

            states.update(*new_state_index, |entry| {

223

5824

                *entry = state;

224

5824

});

225

226

227

        // Add the sentinel state.

228

700

        states.push(lts.num_of_transitions());

229

230

700

        LabelledTransitionSystem {

231

700

            initial_state: permutation(lts.initial_state),

232

700

            labels: lts.labels,

233

700

            states,

234

700

            transition_labels: lts.transition_labels,

235

700

            transition_to: lts.transition_to,

236

700

237

700

238

239

    /// Returns metrics about the LTS.

240

    pub fn metrics(&self) -> LtsMetrics {

241

        LtsMetrics {

242

            num_of_states: self.num_of_states(),

243

            num_of_labels: self.num_of_labels(),

244

            num_of_transitions: self.num_of_transitions(),

245

            state_metrics: self.states.metrics(),

246

            transition_labels_metrics: self.transition_labels.metrics(),

247

            transition_to_metrics: self.transition_to.metrics(),

248

249

250

251

252

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

253

    type Label = L;

254

255

14104

    fn initial_state_index(&self) -> StateIndex {

256

14104

        self.initial_state

257

14104

258

259

775981

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

260

775981

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

261

775981

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

262

263

775981

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

264

4040556

            label: self.transition_labels.index(i),

265

4040556

            to: self.transition_to.index(i),

266

4040556

})

267

775981

268

269

18505

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

270

18505

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

271

18505

272

273

103118

    fn num_of_states(&self) -> usize {

274

        // Remove the sentinel state.

275

103118

        self.states.len() - 1

276

103118

277

278

5750

    fn num_of_labels(&self) -> usize {

279

5750

        self.labels.len()

280

5750

281

282

157720

    fn num_of_transitions(&self) -> usize {

283

157720

        self.transition_labels.len()

284

157720

285

286

1241397

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

287

1241397

        &self.labels[0..]

288

1241397

289

290

242179

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

291

242179

        label_index.value() == 0

292

242179

293

294

200

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

295

200

        self.merge_disjoint_impl(other)

296

200

297

298

299

/// Metrics for a labelled transition system.

300

#[derive(Debug, Clone)]

301

pub struct LtsMetrics {

302

    /// The number of states in the LTS.

303

    pub num_of_states: usize,

304

    pub state_metrics: CompressedVecMetrics,

305

    /// The number of transitions in the LTS.

306

    pub num_of_transitions: usize,

307

    pub transition_labels_metrics: CompressedVecMetrics,

308

    pub transition_to_metrics: CompressedVecMetrics,

309

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

310

    pub num_of_labels: usize,

311

312

313

impl fmt::Display for LtsMetrics {

314

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

315

        // Print some information about the LTS.

316

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

317

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

318

        writeln!(

319

f,

320

            "Number of transitions: {}\n",

321

            LargeFormatter(self.num_of_transitions)

322

)?;

323

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

324

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

325

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

326

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

327

328

329

330

#[cfg(test)]

331

mod tests {

332

    use merc_io::DumpFiles;

333

    use merc_utilities::random_test;

334

335

    use crate::{random_lts, write_aut};

336

337

    #[test]

338

1

    fn test_labelled_transition_system_merge() {

339

100

        random_test(100, |rng| {

340

100

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

341

342

100

            let left = random_lts(rng, 5, 5, 10);

343

100

            let right = random_lts(rng, 5, 10, 10);

344

345

100

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

346

100

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

347

348

100

            let (merged, _offset) = left.clone().merge_disjoint_impl(&right);

349

350

100

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

351

100

})

352

1

353