Grcov report - translate.rs

1

use log::debug;

2

use log::info;

3

use log::trace;

4

5

use merc_collections::IndexedSet;

6

use merc_io::TimeProgress;

7

use merc_lts::LTS;

8

use merc_lts::LabelledTransitionSystem;

9

use merc_lts::StateIndex;

10

use merc_syntax::ActFrm;

11

use merc_syntax::ActFrmBinaryOp;

12

use merc_syntax::FixedPointOperator;

13

use merc_syntax::ModalityOperator;

14

use merc_syntax::MultiAction;

15

use merc_syntax::RegFrm;

16

use merc_syntax::StateFrm;

17

use merc_syntax::StateFrmOp;

18

use merc_utilities::MercError;

19

20

use crate::ModalEquationSystem;

21

use crate::ParityGame;

22

use crate::Player;

23

use crate::Priority;

24

use crate::VertexIndex;

25

use crate::compute_reachable;

26

27

/// Translates a labelled transition system into a variability parity game.

28

357

pub fn translate(lts: &LabelledTransitionSystem<String>, formula: &StateFrm) -> Result<ParityGame, MercError> {

29

    // Parses all labels into MultiAction once

30

357

    let parsed_labels: Result<Vec<MultiAction>, MercError> =

31

3223

        lts.labels().iter().map(|label| MultiAction::parse(label)).collect();

32

357

    let labels = parsed_labels?;

33

34

357

    let equation_system = ModalEquationSystem::new(formula);

35

357

    debug!("{}", equation_system);

36

37

357

    let mut algorithm = Translation::new(lts, &labels, &equation_system);

38

39

357

    algorithm.translate(lts.initial_state_index(), 0)?;

40

41

357

    let result = ParityGame::from_edges(

42

357

        VertexIndex::new(0),

43

357

        algorithm.vertices.iter().map(|(p, _)| p).cloned().collect(),

44

357

        algorithm.vertices.into_iter().map(|(_, pr)| pr).collect(),

45

        true,

46

714

        || algorithm.edges.iter().cloned(),

47

);

48

49

    // Check that all vertices are reachable from the initial vertex. After

50

    // totality it could be that the true or false nodes are not reachable.

51

357

    if cfg!(debug_assertions) {

52

357

        let (_, reachable_vertices) = compute_reachable(&result);

53

357

        debug_assert!(

54

611

            reachable_vertices.iter().all(|v| v.is_some()),

55

            "Not all vertices are reachable from the initial vertex"

56

);

57

58

59

357

    Ok(result)

60

357

61

62

/// Is used to distinguish between StateFrm and Equation vertices in the vertex map.

63

#[derive(Clone, Debug, PartialEq, Eq, Hash)]

64

enum Formula<'a> {

65

    StateFrm(&'a StateFrm),

66

    Equation(usize),

67

68

69

/// Local struct to keep track of the translation state

70

///

71

/// Implements the translation from (s, Ψ) pairs to VPG vertices and edges.

72

/// However, to avoid the complication of merging sub-results we immediately

73

/// store the vertices and edges into mutable vectors. Furthermore, to avoid

74

/// stack overflows we use a breadth-first search approach with a queue. This

75

/// means that during queuing we immediately assign a fresh index to each (s, Ψ)

76

/// pair (if it does not yet exist) and then queue it to assign its actual

77

/// values later on.

78

struct Translation<'a> {

79

    vertex_map: IndexedSet<(StateIndex, Formula<'a>)>,

80

    vertices: Vec<(Player, Priority)>,

81

    edges: Vec<(VertexIndex, VertexIndex)>,

82

83

    // Used for the breadth first search.

84

    queue: Vec<(StateIndex, Formula<'a>, VertexIndex)>,

85

86

    /// The parsed labels of the LTS.

87

    parsed_labels: &'a Vec<MultiAction>,

88

89

    /// The labelled transition system being translated.

90

    lts: &'a LabelledTransitionSystem<String>,

91

92

    /// A reference to the modal equation system being translated.

93

    equation_system: &'a ModalEquationSystem,

94

95

    /// Use to print progress information.

96

    progress: TimeProgress<usize>,

97

98

99

impl<'a> Translation<'a> {

100

    /// Creates a new translation instance.

101

357

    fn new(

102

357

        lts: &'a LabelledTransitionSystem<String>,

103

357

        parsed_labels: &'a Vec<MultiAction>,

104

357

        equation_system: &'a ModalEquationSystem,

105

357

    ) -> Self {

106

357

        let progress: TimeProgress<usize> = TimeProgress::new(

107

            |num_of_vertices: usize| {

108

                info!("Translated {} vertices...", num_of_vertices);

109

},

110

1,

111

);

112

113

357

        Self {

114

357

            vertex_map: IndexedSet::new(),

115

357

            vertices: Vec::new(),

116

357

            edges: Vec::new(),

117

357

            queue: Vec::new(),

118

357

            lts,

119

357

            parsed_labels,

120

357

            equation_system,

121

357

            progress,

122

357

123

357

124

125

    /// Perform the actual translation.

126

357

    fn translate(&mut self, initial_state: StateIndex, initial_equation_index: usize) -> Result<(), MercError> {

127

        // We store (state, formula, N) into the queue, where N is the vertex number assigned to this pair. This means

128

        // that during the traversal we can assume this N to exist.

129

357

        self.queue = vec![(

130

357

            initial_state,

131

357

            Formula::Equation(initial_equation_index),

132

357

            VertexIndex::new(0),

133

357

)];

134

357

        self.vertices.push((Player::Odd, Priority::new(0))); // Placeholder for the initial vertex

135

136

1325

        while let Some((s, formula, vertex_index)) = self.queue.pop() {

137

968

            debug!("Translating vertex {}: (s={}, formula={:?})", vertex_index, s, formula);

138

968

            self.progress.print(self.vertices.len());

139

968

            match formula {

140

610

                Formula::StateFrm(f) => {

141

610

                    self.translate_vertex(s, f, vertex_index);

142

610

143

358

                Formula::Equation(i) => {

144

358

                    self.translate_equation(s, i, vertex_index);

145

358

146

147

148

149

357

        Ok(())

150

357

151

152

    /// Translate a single vertex (s, Ψ) into the variability parity game vertex and its outgoing edges.

153

///

154

    /// The `fts` and `parsed_labels` are used to find the outgoing transitions matching the modalities in the formula.

155

///

156

    /// These are stored in the provided `vertices` and `edges` vectors.

157

    /// The `vertex_map` is used to keep track of already translated vertices.

158

///

159

    /// This function is recursively called for subformulas.

160

610

    pub fn translate_vertex(&mut self, s: StateIndex, formula: &'a StateFrm, vertex_index: VertexIndex) {

161

610

        match formula {

162

206

            StateFrm::True => {

163

206

                // (s, true) → odd, 0

164

206

                self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

165

206

166

            StateFrm::False => {

167

                // (s, false) → even, 0

168

                self.vertices[vertex_index] = (Player::Even, Priority::new(0));

169

170

2

            StateFrm::Binary { op, lhs, rhs } => {

171

2

                match op {

172

2

                    StateFrmOp::Conjunction => {

173

2

                        // (s, Ψ_1 ∧ Ψ_2) →_P odd, (s, Ψ_1) and (s, Ψ_2), 0

174

2

                        self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

175

2

                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

176

2

                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

177

2

178

2

                        self.edges.push((vertex_index, s_psi_1));

179

2

                        self.edges.push((vertex_index, s_psi_2));

180

2

181

                    StateFrmOp::Disjunction => {

182

                        // (s, Ψ_1 ∨ Ψ_2) →_P even, (s, Ψ_1) and (s, Ψ_2), 0

183

                        self.vertices[vertex_index] = (Player::Even, Priority::new(0));

184

                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

185

                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

186

187

                        self.edges.push((vertex_index, s_psi_1));

188

                        self.edges.push((vertex_index, s_psi_2));

189

190

                    _ => {

191

                        unimplemented!("Cannot translate binary operator in {}", formula);

192

193

194

195

1

            StateFrm::Id(identifier, _args) => {

196

1

                let (i, _equation) = self

197

1

                    .equation_system

198

1

                    .find_equation_by_identifier(identifier)

199

1

                    .expect("Variable must correspond to an equation");

200

1

201

1

                self.vertices[vertex_index] = (Player::Odd, Priority::new(0)); // The priority and owner do not matter here

202

1

                let equation_vertex = self.queue_vertex(s, Formula::Equation(i));

203

1

                self.edges.push((vertex_index, equation_vertex));

204

1

205

            StateFrm::Modality {

206

401

                operator,

207

401

                formula,

208

401

                expr,

209

            } => {

210

401

                match operator {

211

                    ModalityOperator::Box => {

212

                        // (s, [a] Ψ) → odd, (s', Ψ) for all s' with s -a-> s', 0

213

3

                        self.vertices[vertex_index] = (Player::Odd, Priority::new(0));

214

215

6

                        for transition in self.lts.outgoing_transitions(s) {

216

6

                            let action = &self.parsed_labels[*transition.label];

217

218

6

                            trace!("Matching action {} against formula {}", action, formula);

219

220

6

                            if match_regular_formula(formula, action) {

221

                                let s_prime_psi = self.queue_vertex(transition.to, Formula::StateFrm(expr));

222

223

                                self.edges.push((vertex_index, s_prime_psi));

224

6

225

226

227

                    ModalityOperator::Diamond => {

228

                        // (s, <a> Ψ) → even, (s', Ψ) for all s' with s -a-> s', 0

229

398

                        self.vertices[vertex_index] = (Player::Even, Priority::new(0));

230

231

1028

                        for transition in self.lts.outgoing_transitions(s) {

232

1028

                            let action = &self.parsed_labels[*transition.label];

233

234

1028

                            if match_regular_formula(formula, action) {

235

252

                                let s_prime_psi = self.queue_vertex(transition.to, Formula::StateFrm(expr));

236

252

237

252

                                self.edges.push((vertex_index, s_prime_psi));

238

776

239

240

241

242

243

            _ => {

244

                unimplemented!("Cannot translate formula {}", formula);

245

246

247

610

248

249

    /// Applies the translation to the given (s, equation) vertex.

250

358

    fn translate_equation(&mut self, s: StateIndex, equation_index: usize, vertex_index: VertexIndex) {

251

358

        let equation = self.equation_system.equation(equation_index);

252

358

        match equation.operator() {

253

357

            FixedPointOperator::Least => {

254

357

                // (s, μ X. Ψ) →_P odd, (s, Ψ[x := μ X. Ψ]), 2 * floor(AD(Ψ)/2) + 1. In Rust division is already floor.

255

357

                self.vertices[vertex_index] = (

256

357

                    Player::Odd,

257

357

                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2) + 1),

258

357

);

259

357

                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

260

357

                self.edges.push((vertex_index, s_psi));

261

357

262

1

            FixedPointOperator::Greatest => {

263

1

                // (s, ν X. Ψ) →_P even, (s, Ψ[x := ν X. Ψ]), 2 * (AD(Ψ)/2). In Rust division is already floor.

264

1

                self.vertices[vertex_index] = (

265

1

                    Player::Even,

266

1

                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2)),

267

1

);

268

1

                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

269

1

                self.edges.push((vertex_index, s_psi));

270

1

271

272

358

273

274

    /// Queues a new pair to be translated, returning its vertex index.

275

615

    fn queue_vertex(&mut self, s: StateIndex, formula: Formula<'a>) -> VertexIndex {

276

615

        let (index, inserted) = self.vertex_map.insert((s, formula.clone()));

277

615

        let vertex_index = VertexIndex::new(*index);

278

279

615

        if inserted {

280

611

            // New vertex, assign placeholder values

281

611

            self.vertices.resize(*vertex_index + 1, (Player::Odd, Priority::new(0)));

282

611

            self.queue.push((s, formula, vertex_index));

283

611

284

285

615

        vertex_index

286

615

287

288

289

/// Returns true iff the given action matches the regular formula.

290

1034

fn match_regular_formula(formula: &RegFrm, action: &MultiAction) -> bool {

291

1034

    match formula {

292

1034

        RegFrm::Action(action_formula) => match_action_formula(action_formula, action),

293

        RegFrm::Choice { lhs, rhs } => match_regular_formula(lhs, action) || match_regular_formula(rhs, action),

294

        _ => {

295

            unimplemented!("Cannot translate regular formula {}", formula);

296

297

298

1034

299

300

/// Returns true iff the given action matches the action formula.

301

1034

fn match_action_formula(formula: &ActFrm, action: &MultiAction) -> bool {

302

1034

    match formula {

303

        ActFrm::True => true,

304

        ActFrm::False => false,

305

1034

        ActFrm::MultAct(expected_action) => expected_action == action,

306

        ActFrm::Binary { op, lhs, rhs } => match op {

307

            ActFrmBinaryOp::Union => match_action_formula(lhs, action) || match_action_formula(rhs, action),

308

            ActFrmBinaryOp::Intersect => match_action_formula(lhs, action) && match_action_formula(rhs, action),

309

            _ => {

310

                unimplemented!("Cannot translate binary operator {}", formula);

311

312

},

313

        ActFrm::Negation(expr) => !match_action_formula(expr, action),

314

        _ => {

315

            unimplemented!("Cannot translate action formula {}", formula);

316

317

318

1034

319

320

#[cfg(test)]

321

mod tests {

322

    use merc_lts::read_aut;

323

    use merc_macros::merc_test;

324

    use merc_syntax::UntypedStateFrmSpec;

325

326

    use super::*;

327

328

    #[merc_test]

329

    #[cfg_attr(miri, ignore)] // Oxidd does not work with miri

330

    fn test_running_example() {

331

        let lts = read_aut(include_bytes!("../../../examples/lts/abp.aut") as &[u8], Vec::new()).unwrap();

332

        let formula = UntypedStateFrmSpec::parse(include_str!("../../../examples/vpg/running_example.mcf")).unwrap();

333

334

        let _pg = translate(&lts, &formula.formula).unwrap();

335

336