Grcov report - impossible

1

use std::cell::RefCell;

2

3

use log::debug;

4

use merc_collections::VecSet;

5

use merc_lts::LTS;

6

use merc_lts::StateIndex;

7

use merc_reduction::diverges;

8

9

use crate::AC;

10

use crate::Antichain;

11

use crate::CounterExampleConstructor;

12

use crate::CounterExampleTree;

13

use crate::ExplorationStrategy;

14

use crate::is_refinement_generic;

15

use crate::is_stable;

16

17

/// The outcome of an impossible-futures refinement check.

18

pub struct ImpossibleFuturesResult<Index, Label> {

19

    /// Whether the impossible-futures refinement holds.

20

    pub result: bool,

21

22

    /// The node in the counter-example tree that witnesses the failure, if any.

23

    pub counter_example: Option<Index>,

24

25

    /// The impossible futures (traces) witnessing the failure, if any.

26

    pub impossible_futures: Option<Vec<Vec<Label>>>,

27

28

29

/// Checks for the impossible futures refinement between the initial state of

30

/// the `lts` and the `initial_spec` state.

31

///

32

/// # Details

33

///

34

/// Impossible futures are defined in the following article:

35

///

36

/// > Marc Voorhoeve, Sjouke Mauw. Impossible futures and determinism, Inf. Process. Lett. 80, 2001.

37

167

pub fn is_impossible_futures_refinement<L: LTS, CE: CounterExampleTree>(

38

167

    lts: &L,

39

167

    initial_spec: StateIndex,

40

167

    strategy: ExplorationStrategy,

41

167

    counter_example: &mut CE,

42

167

) -> ImpossibleFuturesResult<CE::Index, L::Label> {

43

167

    let mut antichain = Antichain::new();

44

45

    // The inner antichain is reused between computations of the weak trace inclusion. The positive antichain contains all the

46

    // pairs that have passed the check so far.

47

167

    let negative_antichain = RefCell::new(Antichain::new());

48

167

    let mut positive_antichain = PositiveAntichain::new();

49

50

167

    let (holds, ce_index, impossible_futures) = is_refinement_generic(

51

167

        strategy,

52

167

        lts,

53

167

        lts.initial_state_index(),

54

167

        initial_spec,

55

300

        |impl_state, spec_states| {

56

300

            if !is_stable(lts, impl_state) {

57

                // We can skip unstable states as an optimisation.

58

95

                debug_assert!(!diverges(lts, impl_state), "Implementation states should not diverge.");

59

95

                return (None, true);

60

205

61

62

            // Observe that the weak trace inclusion is inverted, this exactly

63

            // corresponds to checking for impossible futures.

64

245

            if !spec_states.iter().any(|t| {

65

245

                is_weak_trace_refinement(

66

245

                    lts,

67

245

*t,

68

245

                    impl_state,

69

245

                    strategy,

70

245

                    &mut positive_antichain,

71

245

                    &negative_antichain,

72

73

245

            }) {

74

66

                let mut futures = Vec::new();

75

76

93

                for t in spec_states {

77

                    // Run the weak trace refinement again with a counter example.

78

93

                    let mut ce_constructor = CounterExampleConstructor::new();

79

80

93

                    let (result, ce) = is_weak_trace_refinement_ce(lts, *t, impl_state, strategy, &mut ce_constructor);

81

93

                    debug_assert!(

82

93

                        !result,

83

                        "The weak trace refinement should fail according to the previous check."

84

);

85

86

93

                    let trace = ce_constructor

87

93

                        .reconstruct_trace(ce.expect("A counter example was requested"))

88

93

                        .iter()

89

198

                        .map(|l| lts.labels()[*l].clone())

90

93

                        .collect();

91

92

93

                    futures.push(trace);

93

94

95

66

                return (Some(futures), true);

96

139

97

98

139

            (None, true)

99

300

},

100

        |_, _| (),

101

        true,

102

167

        counter_example,

103

167

        &mut antichain,

104

);

105

106

167

    debug!("Antichain stats: {:?}", antichain.metrics());

107

167

    debug!("Negative antichain stats: {:?}", negative_antichain.borrow().metrics());

108

167

    ImpossibleFuturesResult {

109

167

        result: holds,

110

167

        counter_example: ce_index,

111

167

        impossible_futures,

112

167

113

167

114

115

/// A combined antichain that checks both the persistent positive antichain and

116

/// the current computation's antichain for inclusion at the same time. When a

117

/// weak trace check passes, the pairs from the current antichain are integrated

118

/// into the positive antichain so later checks can short-circuit on them.

119

struct PositiveAntichain {

120

    /// An antichain that is used for repeated weak trace inclusion checks,

121

    positive_antichain: Antichain<StateIndex, StateIndex>,

122

123

    /// The antichain used for the current computation.

124

    antichain: Antichain<StateIndex, StateIndex>,

125

126

127

impl PositiveAntichain {

128

992

    fn new() -> Self {

129

992

        Self {

130

992

            positive_antichain: Antichain::new(),

131

992

            antichain: Antichain::new(),

132

992

133

992

134

135

136

impl AC<StateIndex, StateIndex> for PositiveAntichain {

137

4176

    fn insert(&mut self, key: StateIndex, value: VecSet<StateIndex>) -> bool {

138

4176

        if self.positive_antichain.contains_subset(&key, &value) {

139

            // If the positive antichain contains a subset of the current pair, then we can immediately conclude that the check passes.

140

58

            return false;

141

4118

142

143

4118

        self.antichain.insert(key, value)

144

4176

145

146

1410

    fn clear(&mut self) {

147

1410

        self.antichain.clear();

148

1410

149

150

151

/// Checks for the various weak trace refinement. This is a helper function for

152

/// the impossible futures refinement check.

153

245

fn is_weak_trace_refinement<L: LTS>(

154

245

    lts: &L,

155

245

    impl_state: StateIndex,

156

245

    spec_state: StateIndex,

157

245

    strategy: ExplorationStrategy,

158

245

    positive_antichain: &mut PositiveAntichain,

159

245

    negative_antichain: &RefCell<Antichain<StateIndex, StateIndex>>,

160

245

) -> bool {

161

245

    let (result, _counter_example, _inner_ce) = is_refinement_generic(

162

245

        strategy,

163

245

        lts,

164

245

        impl_state,

165

245

        spec_state,

166

808

        |impl_state, spec_states| {

167

808

            if negative_antichain.borrow().contains_superset(&impl_state, spec_states) {

168

                // If the negative antichain contains a superset of the current pair, then we can immediately conclude that the check fails.

169

19

                return (Some(()), false);

170

789

171

172

789

            (None, true)

173

808

},

174

87

        |impl_state, spec_states| {

175

            // If the check fails, then we can add the pair to the negative antichain, which is used for the impossible futures check.

176

87

            negative_antichain.borrow_mut().insert(impl_state, spec_states.clone());

177

87

},

178

        true,

179

245

        &mut (),

180

245

        positive_antichain,

181

);

182

183

245

    if result {

184

        // If the check passed, then we can add the pair to the positive antichain, which is used for the impossible futures check.

185

220

        for (impl_state, spec_states) in positive_antichain.antichain.iter() {

186

220

            positive_antichain

187

220

                .positive_antichain

188

220

                .insert(*impl_state, spec_states.clone());

189

220

190

106

191

192

245

    positive_antichain.clear();

193

245

    result

194

245

195

196

/// This is the [is_weak_trace_refinement] but can generate a counter example.

197

93

fn is_weak_trace_refinement_ce<L: LTS, CE: CounterExampleTree>(

198

93

    lts: &L,

199

93

    impl_state: StateIndex,

200

93

    spec_state: StateIndex,

201

93

    strategy: ExplorationStrategy,

202

93

    counter_example: &mut CE,

203

93

) -> (bool, Option<CE::Index>) {

204

93

    let mut antichain = Antichain::new();

205

93

    let (result, counter_example, inner_ce) = is_refinement_generic(

206

93

        strategy,

207

93

        lts,

208

93

        impl_state,

209

93

        spec_state,

210

418

        |_, _| (Option::<()>::None, true),

211

        |_, _| (),

212

        true,

213

93

        counter_example,

214

93

        &mut antichain,

215

);

216

217

93

    debug_assert!(inner_ce.is_none(), "The counter example from check is trivial");

218

93

    (result, counter_example)

219

93

220

221

#[cfg(test)]

222

mod tests {

223

    use merc_lts::read_aut;

224

    use merc_utilities::Timing;

225

    use merc_utilities::test_logger;

226

227

    use crate::ExplorationStrategy;

228

    use crate::RefinementType;

229

    use crate::refines;

230

231

    #[test]

232

1

    fn test_impossible_futures_example() {

233

1

        test_logger();

234

235

1

        let impl_lts = read_aut(

236

1

            b"des (0,8,6)

237

1

            (0,newday,1)

238

1

            (1,i,2)

239

1

            (1,i,3)

240

1

            (2,teach,4)

241

1

            (3,lindyhop,0)

242

1

            (3,i,5)

243

1

            (4,newday,2)

244

1

            (5,teach,0)" as &[u8],

245

246

1

        .unwrap();

247

248

1

        let spec_lts = read_aut(

249

1

            b"des (0,5,4)

250

1

            (0,newday,1)

251

1

            (1,i,2)

252

1

            (1,i,3)

253

1

            (2,teach,0)

254

1

            (3,lindyhop,0)" as &[u8],

255

256

1

        .unwrap();

257

258

1

        let mut timing = Timing::new();

259

260

2

        for preprocess in [false, true] {

261

            // Both directions weak trace included.

262

2

            assert!(

263

2

                refines(

264

2

                    impl_lts.clone(),

265

2

                    spec_lts.clone(),

266

2

                    RefinementType::Weaktrace,

267

2

                    ExplorationStrategy::BFS,

268

2

                    preprocess,

269

2

                    false,

270

2

                    &mut timing

271

2

272

2

.0

273

);

274

2

            assert!(

275

2

                refines(

276

2

                    spec_lts.clone(),

277

2

                    impl_lts.clone(),

278

2

                    RefinementType::Weaktrace,

279

2

                    ExplorationStrategy::BFS,

280

2

                    preprocess,

281

2

                    false,

282

2

                    &mut timing

283

2

284

2

.0

285

);

286

287

            // However, not impossible futures included in one direction.

288

2

            assert!(

289

2

                !refines(

290

2

                    spec_lts.clone(),

291

2

                    impl_lts.clone(),

292

2

                    RefinementType::ImpossibleFutures,

293

2

                    ExplorationStrategy::BFS,

294

2

                    preprocess,

295

2

                    false,

296

2

                    &mut timing

297

2

298

2

.0

299

);

300

301

1

302