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

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

18

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

19

///

20

/// # Details

21

///

22

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

23

///

24

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

25

181

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

26

181

    lts: &L,

27

181

    initial_spec: StateIndex,

28

181

    strategy: ExplorationStrategy,

29

181

    counter_example: &mut CE,

30

181

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

31

181

    let mut antichain = Antichain::new();

32

33

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

34

    // pairs that have passed the check so far.

35

181

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

36

181

    let mut positive_antichain = PositiveAntichain::new();

37

38

181

    let result = is_refinement_generic(

39

181

        strategy,

40

181

        lts,

41

181

        lts.initial_state_index(),

42

181

        initial_spec,

43

350

        |impl_state, spec_states| {

44

350

            if !is_stable(lts, impl_state) {

45

                // We can skip unstable states as an optimisation.

46

117

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

47

117

                return (None, true);

48

233

49

50

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

51

            // corresponds to checking for impossible futures.

52

283

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

53

283

                is_weak_trace_refinement(

54

283

                    lts,

55

283

*t,

56

283

                    impl_state,

57

283

                    strategy,

58

283

                    &mut positive_antichain,

59

283

                    &negative_antichain,

60

61

283

            }) {

62

77

                let mut futures = Vec::new();

63

64

114

                for t in spec_states {

65

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

66

114

                    let mut ce_constructor = CounterExampleConstructor::new();

67

68

114

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

69

114

                    debug_assert!(

70

114

                        !result,

71

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

72

);

73

74

114

                    let trace = ce_constructor

75

114

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

76

114

                        .iter()

77

243

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

78

114

                        .collect();

79

80

114

                    futures.push(trace);

81

82

83

77

                return (Some(futures), true);

84

156

85

86

156

            (None, true)

87

350

},

88

        |_, _| (),

89

        true,

90

181

        counter_example,

91

181

        &mut antichain,

92

);

93

94

181

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

95

    // debug!("Positive antichain stats: {:?}", positive_antichain.metrics());

96

181

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

97

181

    result

98

181

99

100

/// This is a combined antichain where we check both the positive and the outer

101

/// antichain at the same time for inclusion. And in the end we integrate the

102

/// positive antichain into the outer antichain when

103

struct PositiveAntichain {

104

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

105

    positive_antichain: Antichain<StateIndex, StateIndex>,

106

107

    /// The antichain used for the current computation.

108

    antichain: Antichain<StateIndex, StateIndex>,

109

110

111

impl PositiveAntichain {

112

539

    fn new() -> Self {

113

539

        Self {

114

539

            positive_antichain: Antichain::new(),

115

539

            antichain: Antichain::new(),

116

539

117

539

118

119

120

impl AC<StateIndex, StateIndex> for PositiveAntichain {

121

2313

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

122

2313

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

123

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

124

46

            return false;

125

2267

126

127

2267

        self.antichain.insert(key, value)

128

2313

129

130

825

    fn clear(&mut self) {

131

825

        self.antichain.clear();

132

825

133

134

135

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

136

/// the impossible futures refinement check.

137

283

fn is_weak_trace_refinement<L: LTS>(

138

283

    lts: &L,

139

283

    impl_state: StateIndex,

140

283

    spec_state: StateIndex,

141

283

    strategy: ExplorationStrategy,

142

283

    positive_antichain: &mut PositiveAntichain,

143

283

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

144

283

) -> bool {

145

283

    let (result, _counter_example, _inner_ce) = is_refinement_generic(

146

283

        strategy,

147

283

        lts,

148

283

        impl_state,

149

283

        spec_state,

150

886

        |impl_state, spec_states| {

151

886

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

152

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

153

24

                return (Some(()), false);

154

862

155

156

862

            (None, true)

157

886

},

158

103

        |impl_state, spec_states| {

159

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

160

103

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

161

103

},

162

        true,

163

283

        &mut (),

164

283

        positive_antichain,

165

);

166

167

283

    if result {

168

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

169

272

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

170

272

            positive_antichain

171

272

                .positive_antichain

172

272

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

173

272

174

127

175

176

283

    positive_antichain.clear();

177

283

    result

178

283

179

180

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

181

114

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

182

114

    lts: &L,

183

114

    impl_state: StateIndex,

184

114

    spec_state: StateIndex,

185

114

    strategy: ExplorationStrategy,

186

114

    counter_example: &mut CE,

187

114

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

188

114

    let mut antichain = Antichain::new();

189

114

    let (result, counter_example, inner_ce) = is_refinement_generic(

190

114

        strategy,

191

114

        lts,

192

114

        impl_state,

193

114

        spec_state,

194

401

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

195

        |_, _| (),

196

        true,

197

114

        counter_example,

198

114

        &mut antichain,

199

);

200

201

114

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

202

114

    (result, counter_example)

203

114

204

205

#[cfg(test)]

206

mod tests {

207

    use merc_lts::read_aut;

208

    use merc_utilities::Timing;

209

    use merc_utilities::test_logger;

210

211

    use crate::ExplorationStrategy;

212

    use crate::RefinementType;

213

    use crate::refines;

214

215

    #[test]

216

1

    fn test_impossible_futures_example() {

217

1

        test_logger();

218

219

1

        let impl_lts = read_aut(

220

1

            b"des (0,8,6)

221

1

            (0,newday,1)

222

1

            (1,i,2)

223

1

            (1,i,3)

224

1

            (2,teach,4)

225

1

            (3,lindyhop,0)

226

1

            (3,i,5)

227

1

            (4,newday,2)

228

1

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

229

230

1

        .unwrap();

231

232

1

        let spec_lts = read_aut(

233

1

            b"des (0,5,4)

234

1

            (0,newday,1)

235

1

            (1,i,2)

236

1

            (1,i,3)

237

1

            (2,teach,0)

238

1

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

239

240

1

        .unwrap();

241

242

1

        let mut timing = Timing::new();

243

244

2

        for preprocess in [false, true] {

245

            // Both directions weak trace included.

246

2

            assert!(

247

2

                refines(

248

2

                    impl_lts.clone(),

249

2

                    spec_lts.clone(),

250

2

                    RefinementType::Weaktrace,

251

2

                    ExplorationStrategy::BFS,

252

2

                    preprocess,

253

2

                    false,

254

2

                    &mut timing

255

2

256

2

.0

257

);

258

2

            assert!(

259

2

                refines(

260

2

                    spec_lts.clone(),

261

2

                    impl_lts.clone(),

262

2

                    RefinementType::Weaktrace,

263

2

                    ExplorationStrategy::BFS,

264

2

                    preprocess,

265

2

                    false,

266

2

                    &mut timing

267

2

268

2

.0

269

);

270

271

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

272

2

            assert!(

273

2

                !refines(

274

2

                    spec_lts.clone(),

275

2

                    impl_lts.clone(),

276

2

                    RefinementType::ImpossibleFutures,

277

2

                    ExplorationStrategy::BFS,

278

2

                    preprocess,

279

2

                    false,

280

2

                    &mut timing

281

2

282

2

.0

283

);

284

285

1

286